2026-07-21T14:19:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20542 2024-08-19T06:03:43Z ddc:004 open_access

The Strength of the Dominance Rule Kołodziejczyk, Leszek Aleksander Thapen, Neil proof complexity DRAT symmetry breaking dominance It has become standard that, when a SAT solver decides that a CNF Γ is unsatisfiable, it produces a certificate of unsatisfiability in the form of a refutation of Γ in some proof system. The system typically used is DRAT, which is equivalent to extended resolution (ER) - for example, until this year DRAT refutations were required in the annual SAT competition. Recently [Bogaerts et al. 2023] introduced a new proof system, associated with the tool VeriPB, which is at least as strong as DRAT and is further able to handle certain symmetry-breaking techniques. We show that this system simulates the proof system G₁, which allows limited reasoning with QBFs and forms the first level above ER in a natural hierarchy of proof systems. This hierarchy is not known to be strict, but nevertheless this is evidence that the system of [Bogaerts et al. 2023] is plausibly strictly stronger than ER and DRAT. In the other direction, we show that symmetry-breaking for a single symmetry can be handled inside ER. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Leszek Aleksander Kołodziejczyk and Neil Thapen 2024 Is Part Of LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2024.20 urn:nbn:de:0030-drops-205421 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.20 eng https://creativecommons.org/licenses/by/4.0/legalcode