Document Open Access Logo

MaxSAT Resolution with Inclusion Redundancy

Authors Ilario Bonacina , Maria Luisa Bonet , Massimo Lauria

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2024.7.pdf
  • Filesize: 0.71 MB
  • 15 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Complexity theory and logic
Keywords
  • MaxSAT
  • Redundancy
  • MaxSAT resolution
  • Branch-and-bound
  • Pigeonhole principle
  • Parity Principle

Metrics

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

Abstract

Popular redundancy rules for SAT are not necessarily sound for MaxSAT. The works of [Bonacina-Bonet-Buss-Lauria'24] and [Ihalainen-Berg-Järvisalo'22] proposed ways to adapt them, but required specific encodings and more sophisticated checks during proof verification. Here, we propose a different way to adapt redundancy rules from SAT to MaxSAT. Our rules do not require specific encodings, their correctness is simpler to check, but they are slightly less expressive. However, the proposed redundancy rules, when added to MaxSAT-Resolution, are already strong enough to capture Branch-and-bound algorithms, enable short proofs of the optimal cost of notable principles (e.g., the Pigeonhole Principle and the Parity Principle), and allow to break simple symmetries (e.g., XOR-ification does not make formulas harder).

Cite As Get BibTex

Ilario Bonacina, Maria Luisa Bonet, and Massimo Lauria. MaxSAT Resolution with Inclusion Redundancy. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.SAT.2024.7

Author Details

Ilario Bonacina
  • Universitat Politècnica de Catalunya, Barcelona, Spain
Maria Luisa Bonet
  • Universitat Politècnica de Catalunya, Barcelona, Spain
Massimo Lauria
  • Sapienza Università di Roma, Italy

Funding

  • Bonacina, Ilario: The author was supported by grant PID2022-138506NB-C22 (PROOFS BEYOND) funded by AEI.
  • Bonet, Maria Luisa: The author was supported by grant PID2022-138506NB-C22 (PROOFS BEYOND) funded by AEI.
  • Lauria, Massimo: The author has been supported by the project PRIN 2022 "Logical Methods in Combinatorics" N. 2022BXH4R5 of the Italian Ministry of University and Research (MIUR).

References

  1. Albert Atserias and Tuomas Hakoniemi. Size-degree trade-offs for Sums-of-Squares and Positivstellensatz proofs. In 34th Computational Complexity Conference (CCC), volume 137, pages 24:1-24:20, 2019. URL: https://doi.org/10.4230/LIPIcs.CCC.2019.24.
  2. Albert Atserias and Massimo Lauria. Circular (yet sound) proofs in propositional logic. ACM Trans. Comput. Log., 24(3):20:1-20:26, 2023. Conference version appeared in SAT'19. URL: https://doi.org/10.1145/3579997.
  3. Per Austrin and Kilian Risse. Perfect matching in random graphs is as hard as Tseitin. TheoretiCS, 1, 2022. URL: https://doi.org/10.46298/THEORETICS.22.2.
  4. Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. Maximum satisfiabiliy. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 929-991. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201008.
  5. Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, , and Dieter Vandesande. Certified core-guided maxsat solving. In Proceedings of the 29th International Conference on Automated Deduction (CADE-29), July 2023, 2023. Google Scholar
  6. Jeremias Berg and Matti Järvisalo. Unifying reasoning and care-guided search for maximum satisfiability. In 16th European Conf. on Logics in Artificial Intelligence (JELIA), pages 287-303, 2019. Google Scholar
  7. Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified dominance and symmetry breaking for combinatorial optimisation. J. Artif. Intell. Res., 77:1539-1589, 2023. URL: https://doi.org/10.1613/JAIR.1.14296.
  8. Ilario Bonacina, Maria Luisa Bonet, Sam Buss, and Massimo Lauria. Redundancy rules for MaxSAT. Electron. Colloquium Comput. Complex., TR24-045, 2024. URL: https://eccc.weizmann.ac.il/report/2024/045.
  9. Ilario Bonacina, Maria Luisa Bonet, and Jordi Levy. Weighted, circular and semi-algebraic proofs. Journal of Artificial Intelligence Research (JAIR), 79:447-482, February 2024. URL: https://doi.org/10.1613/jair.1.15075.
  10. Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, João Marques-Silva, and Antonio Morgado. MaxSAT resolution with the dual rail encoding. In 32nd Intl. AAAI Conference on Artificial Intelligence (AAAI), 2018. Google Scholar
  11. Maria Luisa Bonet and Jordi Levy. Equivalence between systems stronger than resolution. In 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 166-181, Cham, 2020. Google Scholar
  12. Maria Luisa Bonet, Jordi Levy, and Felip Manyà. Resolution for max-SAT. Artif. Intell., 171(8-9):606-618, 2007. Google Scholar
  13. Sam Buss and Neil Thapen. DRAT and propagation redundancy proofs without new variables. Logical Methods in Computer Science, Volume 17, Issue 2, April 2021. Conference version appeared in SAT'19. Google Scholar
  14. Armin Haken. The intractability of resolution. Theoretical Computer Science, 39:297-308, 1985. Google Scholar
  15. Federico Heras and Javier Larrosa. New inference rules for efficient Max-SAT solving. In 21st National Conference on Artificial Intelligence and 18th Innovative Applications of Artificial Intelligence Conference, pages 68-73, 2006. Google Scholar
  16. Marijn J. H. Heule and Armin Biere. What a difference a variable makes. In 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 75-92, 2018. Google Scholar
  17. Marijn J. H. Heule, Warren A. Hunt Jr., and Nathan Wetzler. Trimming while checking clausal proofs. In Formal Methods in Computer-Aided Design (FMCAD), pages 181-188, 2013. Google Scholar
  18. Marijn J. H. Heule, Warren A. Hunt Jr., and Nathan Wetzler. Verifying refutations with extended resolution. In 24th International Conference on Automated Deduction (CADE), pages 345-359, 2013. Google Scholar
  19. Marijn J. H. Heule, Warren A. Hunt Jr., and Nathan Wetzler. Expressing symmetry breaking in DRAT proofs. In 25th International Conference on Automated Deduction (CADE), pages 591-606, 2015. Google Scholar
  20. Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Strong extension-free proof systems. Journal of Automated Reasoning, 64(3):533-554, 2019. Conference version appeared in CADE'17. URL: https://doi.org/10.1007/s10817-019-09516-0.
  21. Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, and Armin Biere. PRuning through satisfaction. In Hardware and Software: Verification and Testing - 13th International Haifa Verification Conference (HVC), pages 179-194, 2017. Google Scholar
  22. Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo. Clause redundancy and preprocessing in maximum satisfiability. In Automated Reasoning, pages 75-94. Springer International Publishing, 2022. Google Scholar
  23. Matti Järvisalo, Marijn J. H. Heule, and Armin Biere. Inprocessing rules. In 6th International Joint Conference on Automated Reasoning (IJCAR), pages 355-270, 2012. Google Scholar
  24. Benjamin Kiesl, Adrián Rebola-Pardo, and Marijn J. H. Heule. Extended resolution simulates DRAT. In 6th International Joint Conference on Automated Reasoning (IJCAR), pages 516-531, 2018. Google Scholar
  25. Benjamin Kiesl, Martina Seidl, Hans Tompits, and Armin Biere. Super-blocked clauses. In 8th International Joint Conference on Automated Reasoning (IJCAR), volume 9706 of Lecture Notes in Computer Science, pages 45-61. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40229-1_5.
  26. Oliver Kullmann. On a generalization of extended resolution. Discrete Applied Mathematics, 96-97:149-176, 1999. URL: https://doi.org/10.1016/S0166-218X(99)00037-2.
  27. Chu Min Li and Felip Manyà. MaxSAT, hard and soft constraints. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 903-927. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201007.
  28. Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He. Combining clause learning and branch and bound for MaxSAT. In Constraint Programming (CP), volume 210, pages 38:1-38:18, 2021. Google Scholar
  29. Adrián Rebola-Pardo and Martin Suda. A theory of satisfiability-preserving proofs in SAT solving. In 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), pages 583-603, 2018. Google Scholar
  30. Emre Yolcu and Marijn J. H. Heule. Exponential separations using guarded extension variables. In Yael Tauman Kalai, editor, 14th Innovations in Theoretical Computer Science Conference (ITCS), volume 251 of LIPIcs, pages 101:1-101:22, 2023. URL: https://doi.org/10.4230/LIPICS.ITCS.2023.101.
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