Adrian Rebola Pardo,
"Even Shorter Proofs Without New Variables"
: 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), Serie Leibniz International Proceedings in Informatics (LIPIcs), Vol. 271, Seite(n) 22:1 - 22:20, 8-2023, ISBN: 978-3-95977-286-0
Original Titel:
Even Shorter Proofs Without New Variables
Sprache des Titels:
Englisch
Original Buchtitel:
26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
Original Kurzfassung:
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.
Sprache der Kurzfassung:
Englisch
Serie:
Leibniz International Proceedings in Informatics (LIPIcs)
Forschungs-