Document Open Access Logo

The Strength of the Dominance Rule

Authors Leszek Aleksander Kołodziejczyk , Neil Thapen

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2024.20.pdf
  • Filesize: 0.78 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • proof complexity
  • DRAT
  • symmetry breaking
  • dominance

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get BibTex

Leszek Aleksander Kołodziejczyk and Neil Thapen. The Strength of the Dominance Rule. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 20:1-20:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.SAT.2024.20

Author Details

Leszek Aleksander Kołodziejczyk
  • Institute of Mathematics, University of Warsaw, Poland
Neil Thapen
  • Institute of Mathematics, Czech Academy of Sciences, Prague, Czech Republic

Funding

  • Thapen, Neil: Supported by the Institute of Mathematics, Czech Academy of Sciences (RVO 67985840) and GAČR grant 23-04825S.

Acknowledgements

We are grateful to Jakob Nordström for introducing us to this topic and answering our questions about it, and to Sam Buss and Vijay Ganesh for other helpful discussions.

References

  1. P. Beame, H. Kautz, and A. Sabharwal. Towards understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research, 22:319-351, 2004. URL: https://doi.org/10.1613/jair.1410.
  2. A. Beckmann and S. R. Buss. Polynomial local search in the polynomial hierarchy and witnessing in fragments of bounded arithmetic. Journal of Mathematical Logic, 9(1):103-138, 2009. URL: https://doi.org/10.1142/S0219061309000847.
  3. O. Beyersdorff and J. Pich. Understanding Gentzen and Frege systems for QBF. In Proceedings of the Annual Symposium on Logic in Computer Science (LICS '16), pages 146-155, 2016. URL: https://doi.org/10.1145/2933575.2933597.
  4. B. Bogaerts, S. Gocht, C. McCreesh, and J. Nordström. Certified dominance and symmetry breaking for combinatorial optimisation. Journal of Artificial Intelligence Research, 77:1539-1589, 2023. URL: https://doi.org/10.1613/jair.1.14296.
  5. S. Buss and N. Thapen. DRAT and propagation redundancy proofs without new variables. Logical Methods in Computer Science, 17, 2021. URL: https://lmcs.episciences.org/7400.
  6. S. R. Buss. Bounded Arithmetic. Bibliopolis, 1986. Google Scholar
  7. S. R. Buss. Axiomatizations and conservation results for fragments of bounded arithmetic. In Logic and Computation, volume 106 of Contemporary Mathematics, pages 57-84. ACM, 1990. Google Scholar
  8. S. R. Buss and J. Krajíček. An application of Boolean complexity to separation problems in bounded arithmetic. Proceedings of the London Mathematical Society, 69:1-21, 1994. URL: https://doi.org/10.1112/plms/s3-69.1.1.
  9. L. Chew and M. J. H. Heule. Relating existing powerful proof systems for QBF. In International Conference on Theory and Applications of Satisfiability Testing (SAT '22), pages 10:1-10:22, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.10.
  10. S. A. Cook. Feasibly constructive proofs and the propositional calculus (preliminary version). In Annual ACM Symposium on Theory of Computing (STOC '75), pages 83-97. ACM, 1975. URL: https://doi.org/10.1145/800116.803756.
  11. W. Cook, C. R. Coullard, and G. Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, 1987. URL: https://doi.org/10.1016/0166-218X(87)90039-4.
  12. J. Crawford, M. Ginsberg, E. Luks, and A. Roy. Symmetry-breaking predicates for search problems. In Principles of Knowledge Representation and Reasoning (KR '96), pages 148-159, 1996. Google Scholar
  13. M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Communications of the ACM, 5:394-397, 1962. URL: https://doi.org/10.1145/368273.368557.
  14. J. Elffers, S. Gocht, C. McCreesh, and J. Nordström. Justifying all differences using pseudo-Boolean reasoning. In AAAI Conference on Artificial Intelligence, volume 34(02), pages 1486-1494, 2020. URL: https://doi.org/10.1609/aaai.v34i02.5507.
  15. P. Hájek and P. Pudlák. Metamathematics of First-Order Arithmetic. Springer-Verlag, 1993. URL: https://doi.org/10.1007/978-3-662-22156-3.
  16. M. J. H. Heule, W. A. Hunt, Jr., and N. Wetzler. Expressing symmetry breaking in DRAT proofs. In International Conference on Automated Deduction, pages 591-606. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_40.
  17. M. J. H. Heule, B. Kiesl, and A. Biere. Strong extension-free proof systems. Journal of Automated Reasoning, 64(3):533-554, 2020. URL: https://doi.org/10.1007/s10817-019-09516-0.
  18. E. Jeřábek. Dual weak pigeonhole principle, Boolean complexity, and derandomization. Annals of Pure and Applied Logic, 129:1-37, 2004. URL: https://doi.org/10.1016/j.apal.2003.12.003.
  19. E. Jeřábek. The strength of sharply bounded induction. Mathematical Logic Quarterly, 52:613-624, 2006. URL: https://doi.org/10.1002/malq.200610019.
  20. D. S. Johnson, C. H. Papadimitriou, and M. Yannakakis. How easy is local search? Journal of Computer and System Sciences, 37:79-100, 1988. URL: https://doi.org/10.1016/0022-0000(88)90046-3.
  21. B. Kiesl, A. Rebola-Pardo, and M. J. H. Heule. Extended resolution simulates DRAT. In International Joint Conference on Automated Reasoning (IJCAR '18), pages 516-531, 2018. URL: https://doi.org/10.1007/978-3-319-94205-6_34.
  22. Leszek Aleksander Kołodziejczyk and Neil Thapen. The strength of the dominance rule, 2024. URL: https://arxiv.org/abs/2406.13657.
  23. J. Krajíček. Proof complexity, volume 170 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, 2019. Google Scholar
  24. J. Krajíček and P. Pudlák. Quantified propositional calculi and fragments of bounded arithmetic. Z. Math. Logik Grundlag. Math., 36(1):29-46, 1990. URL: https://doi.org/10.1002/malq.19900360106.
  25. O. Kullmann. On a generalization of extended resolution. Discrete Applied Mathematics, 96:149-176, 1999. URL: https://doi.org/10.1016/S0166-218X(99)00037-2.
  26. J. P. Marques-Silva and K. A. Sakallah. GRASP-a search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48:506-521, 1999. URL: https://doi.org/10.1109/12.769433.
  27. J. B. Paris and A. J. Wilkie. Counting problems in bounded arithmetic. In Methods in Mathematical Logic, volume 1130 of Lecture Notes in Mathematics, pages 317-340. Springer-Verlag, 1985. URL: https://doi.org/10.1007/BFb0075316.
  28. A. A. Razborov. Propositional proof complexity. In European Congress of Mathematics 2021, pages 439-464. EMS Press, 2023. Google Scholar
  29. S. Riis. Finitisation in bounded arithmetic. BRICS Report Series, 23, 1994. Google Scholar
  30. N. Wetzler, M. J. H. Heule, and W. A. Hunt, Jr. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In International Conference on Theory and Applications of Satisfiability Testing (SAT '14), pages 422-429, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_31.
  31. A. J. Wilkie and J. B. Paris. On the scheme of induction for bounded arithmetic formulas. Annals of Pure and Applied Logic, 35:261-302, 1987. URL: https://doi.org/10.1016/0168-0072(87)90066-2.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact