2026-08-16T04:29:03Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18484 2024-03-06T11:02:01Z ddc:004 open_access

Even Shorter Proofs Without New Variables Rebola-Pardo, Adrián Interference SAT solving Unsatisfiability proofs Unsatisfiable cores 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Adrián Rebola-Pardo 2023 Is Part Of LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2023.22 urn:nbn:de:0030-drops-184844 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.22 eng https://creativecommons.org/licenses/by/4.0/legalcode