License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2023.22
URN: urn:nbn:de:0030-drops-184844
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18484/
Rebola-Pardo, Adrián
Even Shorter Proofs Without New Variables
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.
BibTeX - Entry
@InProceedings{rebolapardo:LIPIcs.SAT.2023.22,
author = {Rebola-Pardo, Adri\'{a}n},
title = {{Even Shorter Proofs Without New Variables}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {22:1--22:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18484},
URN = {urn:nbn:de:0030-drops-184844},
doi = {10.4230/LIPIcs.SAT.2023.22},
annote = {Keywords: Interference, SAT solving, Unsatisfiability proofs, Unsatisfiable cores}
}
Keywords: |
|
Interference, SAT solving, Unsatisfiability proofs, Unsatisfiable cores |
Collection: |
|
26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) |
Issue Date: |
|
2023 |
Date of publication: |
|
09.08.2023 |