<div class="csl-bib-body">
<div class="csl-entry">Rebola Pardo, A. (2023). Even Shorter Proofs Without New Variables. In M. Mahajan & F. Slivovsky (Eds.), <i>26th International Conference on Theory and Applications of Satisfiability Testing</i> (pp. 22:1-22:20). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.SAT.2023.22</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/192587
-
dc.description.abstract
Proof formats for SAT solvers have diversified over the last decade, enabling new features such as extended resolution-like capabilities, very general extension-free rules, inclusion of proof hints, and pseudo-boolean reasoning. Interference-based methods have been proven effective, and some theoretical work has been undertaken to better explain their limits and semantics. In this work, we combine the subsumption redundancy notion from [Sam Buss and Neil Thapen, 2019] and the overwrite logic framework from [Adrián Rebola{-}Pardo and Martin Suda, 2018]. Natural generalizations then become apparent, enabling even shorter proofs of the pigeonhole principle (compared to those from [Marijn J. H. Heule et al., 2017]) and smaller unsatisfiable core generation.
en
dc.description.sponsorship
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
-
dc.language.iso
en
-
dc.subject
satisfiability testing
en
dc.subject
interference
en
dc.subject
unsatisfiability proofs
en
dc.title
Even Shorter Proofs Without New Variables
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.relation.publication
26th International Conference on Theory and Applications of Satisfiability Testing
-
dc.contributor.editoraffiliation
Institute of Mathematical Sciences, HBNI,India
-
dc.relation.isbn
978-3-95977-286-0
-
dc.relation.doi
10.4230/LIPIcs.SAT.2023.0
-
dc.description.startpage
22:1
-
dc.description.endpage
22:20
-
dc.relation.grantno
VRG11-005
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
26th International Conference on Theory and Applications of Satisfiability Testing
-
tuw.container.volume
271
-
tuw.peerreviewed
true
-
tuw.book.ispartofseries
LIPIcs
-
tuw.relation.publisher
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
-
tuw.project.title
LogiCs-Stipendien
-
tuw.project.title
Heisenbugs: Auffindung und Erklärung
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.publisher.doi
10.4230/LIPICS.SAT.2023.22
-
dc.description.numberOfPages
20
-
tuw.author.orcid
0000-0001-9234-4377
-
tuw.event.name
26th International Conference on Theory and Applications of Satisfiability Testing (SAT)
en
tuw.event.startdate
04-07-2023
-
tuw.event.enddate
08-07-2023
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Alghero
-
tuw.event.country
IT
-
tuw.event.presenter
Rebola Pardo, Adrian
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
item.languageiso639-1
en
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openairetype
conference paper
-
item.cerifentitytype
Publications
-
item.fulltext
no Fulltext
-
item.grantfulltext
none
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.orcid
0000-0001-9234-4377
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.project.funder
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds