TY - GEN
T1 - Even Shorter Proofs Without New Variables
AU - Rebola Pardo, Adrian
PY - 2023/8
Y1 - 2023/8
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85170560913&partnerID=8YFLogxK
M3 - Conference proceedings
SN - 978-3-95977-286-0
VL - 271
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 22:1 - 22:20
BT - 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
A2 - Mahajan, Meena
A2 - Slivovsky, Friedrich
ER -