Document Open Access Logo

Redundancy Rules for MaxSAT

Authors Ilario Bonacina , Maria Luisa Bonet , Sam Buss , Massimo Lauria

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.SAT.2025.7.pdf
  • Filesize: 0.81 MB
  • 17 pages
HTML5 Logo HTML (experimental)
LIPIcs.SAT.2025.7.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • MaxSAT
  • Redundancy Rules
  • Pigeonhole Principle

Metrics

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

Abstract

The concept of redundancy in SAT leads to more expressive and powerful proof search techniques, e.g., able to express various inprocessing techniques, and originates interesting hierarchies of proof systems [Heule et.al'20, Buss-Thapen'19]. Redundancy has also been integrated in MaxSAT [Ihalainen et.al'22, Berg et.al'23, Bonacina et.al'24].
In this paper, we define a structured hierarchy of redundancy proof systems for MaxSAT, with the goal of studying its proof complexity. We obtain MaxSAT variants of proof systems such as SPR, PR, SR, and others, previously defined for SAT.
All our rules are polynomially checkable, unlike [Ihalainen et.al'22]. Moreover, they are simpler and weaker than [Berg et.al'23], and possibly amenable to lower bounds. This work also complements the approach of [Bonacina et.al'24]. Their proof systems use different rule sets for soft and hard clauses, while here we propose a system using only hard clauses and blocking variables. This is easier to integrate with current solvers and proof checkers.
We discuss the strength of the systems introduced, we show some limitations of them, and we give a short cost-SR proof that any assignment for the weak pigeonhole principle PHP^m_n falsifies at least m-n clauses.

Cite As Get BibTex

Ilario Bonacina, Maria Luisa Bonet, Sam Buss, and Massimo Lauria. Redundancy Rules for MaxSAT. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.SAT.2025.7

Author Details

Ilario Bonacina
  • UPC Universitat Politècnica de Catalunya, Barcelona, Spain
Maria Luisa Bonet
  • UPC Universitat Politècnica de Catalunya, Barcelona, Spain
Sam Buss
  • University of California, San Diego, CA, USA
Massimo Lauria
  • Sapienza Università di Roma, Rome, 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-C21 (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).

Acknowledgements

The authors would like to thank the Simons Institute for the Theory of Computing: part of this work has been done during the "Extended Reunion: Satisfiability" program (Spring 2023). Another part of this work has been done during the Oberwolfach workshop 2413 "Proof Complexity and Beyond" and during the 2023 Workshop on Proof Theory and its Applications organized by the Proof Society.

References

  1. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. SAT-based MaxSAT algorithms. Artif. Intell., 196:77-105, 2013. URL: https://doi.org/10.1016/J.ARTINT.2013.01.002.
  2. 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.
  3. 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), volume 14132, pages 1-22, 2023. URL: https://doi.org/10.1007/978-3-031-38499-8_1.
  4. Jeremias Berg and Matti Järvisalo. Unifying reasoning and core-guided search for maximum satisfiability. In Proceedings of the 16th European Conference on Logics in Artificial Intelligence (JELIA), volume 11468, pages 287-303, 2019. URL: https://doi.org/10.1007/978-3-030-19570-0_19.
  5. Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob 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.
  6. Ilario Bonacina, Maria Luisa Bonet, and Massimo Lauria. MaxSAT Resolution with Inclusion Redundancy. In Proceedings of the 27th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 305, pages 7:1-7:15, 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.7.
  7. Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, João Marques-Silva, and António Morgado. MaxSAT resolution with the dual rail encoding. In Proceedings of the 32nd AAAI Conference on Artificial Intelligence, (AAAI), the 30th innovative Applications of Artificial Intelligence (IAAI), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI), pages 6565-6572, 2018. URL: https://doi.org/10.1609/AAAI.V32I1.12204.
  8. Maria Luisa Bonet, Jordi Levy, and Felip Manyà. Resolution for Max-SAT. Artificial Intelligence, 171(8-9):606-618, 2007. URL: https://doi.org/10.1016/J.ARTINT.2007.03.001.
  9. Sam Buss and Neil Thapen. DRAT and propagation redundancy proofs without new variables. Logical Methods in Computer Science, 17(2), 2021. URL: https://lmcs.episciences.org/7400.
  10. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
  11. Jessica Davies and Fahiem Bacchus. Solving MAXSAT by solving a sequence of simpler SAT instances. In Proceedings of the 17th International Conference on Principles and Practice of Constraint Programming (CP), pages 225-239, 2011. URL: https://doi.org/10.1007/978-3-642-23786-7_19.
  12. Zhaohui Fu and Sharad Malik. On solving the partial MAX-SAT problem. In Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 252-265, 2006. URL: https://doi.org/10.1007/11814948_25.
  13. Michel X. Goemans and David P. Williamson. New 3/4-approximation algorithms for the maximum satisfiability problem. SIAM Journal on Discrete Mathematics, 7(4):656-666, 1994. URL: https://doi.org/10.1137/S0895480192243516.
  14. Marijn Heule, Warren A. Hunt Jr., and Nathan Wetzler. Trimming while checking clausal proofs. In Proceedings of the conference on Formal Methods in Computer-Aided Design (FMCAD), pages 181-188, 2013. URL: https://ieeexplore.ieee.org/document/6679408/.
  15. Marijn Heule, Warren A. Hunt Jr., and Nathan Wetzler. Verifying refutations with extended resolution. In Proceedings of the 24th International Conference on Automated Deduction (CADE), volume 7898, pages 345-359, 2013. URL: https://doi.org/10.1007/978-3-642-38574-2_24.
  16. Marijn Heule, Warren A. Hunt Jr., and Nathan Wetzler. Expressing symmetry breaking in DRAT proofs. In Proceedings of the 25th International Conference on Automated Deduction (CADE), volume 9195, pages 591-606, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_40.
  17. Marijn J. H. Heule and Armin Biere. What a difference a variable makes. In Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS), volume 10806, pages 75-92, 2018. URL: https://doi.org/10.1007/978-3-319-89963-3_5.
  18. Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Short proofs without new variables. In Proceedings of the 26th International Conference on Automated Deduction (CADE), volume 10395, pages 130-147, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_9.
  19. Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Strong extension-free proof systems. Journal of Automated Reasoning, 64(3):533-554, 2019. Extended version of [Marijn J. H. Heule et al., 2017]. URL: https://doi.org/10.1007/s10817-019-09516-0.
  20. Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, and Armin Biere. Pruning through satisfaction. In Proceedings of the Hardware and Software: Verification and Testing - 13th International Haifa Verification Conference (HVC), volume 10629, pages 179-194, 2017. URL: https://doi.org/10.1007/978-3-319-70389-3_12.
  21. Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo. Clause redundancy and preprocessing in maximum satisfiability. In Proceedings of the 11th International Joint Conference on Automated Reasoning (IJCAR), volume 13385, pages 75-94, 2022. URL: https://doi.org/10.1007/978-3-031-10769-6_6.
  22. Matti Järvisalo, Marijn Heule, and Armin Biere. Inprocessing rules. In Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR), volume 7364, pages 355-370, 2012. URL: https://doi.org/10.1007/978-3-642-31365-3_28.
  23. Benjamin Kiesl, Adrián Rebola-Pardo, and Marijn J. H. Heule. Extended resolution simulates DRAT. In Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR), Held as Part of the Federated Logic Conference, FloC 2018, volume 10900, pages 516-531, 2018. URL: https://doi.org/10.1007/978-3-319-94205-6_34.
  24. Leszek Aleksander Kołodziejczyk and Neil Thapen. The Strength of the Dominance Rule. In Proceedings of the 27th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 305, pages 20:1-20:22, 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.20.
  25. 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.
  26. Javier Larrosa and Federico Heras. Resolution in max-sat and its relation to local consistency in weighted csps. In Proceedings of the 19h International Joint Conference on Artificial Intelligence (IJCAI), pages 193-198, 2005. URL: http://ijcai.org/Proceedings/05/Papers/0360.pdf.
  27. António Morgado, Carmine Dodaro, and João Marques-Silva. Core-guided MaxSAT with soft cardinality constraints. In Proceedings of the 20th International Conference on Principles and Practice of Constraint Programming (CP), pages 564-573, 2014. URL: https://doi.org/10.1007/978-3-319-10428-7_41.
  28. António Morgado, Federico Heras, Mark H. Liffiton, Jordi Planes, and João Marques-Silva. Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints An Int. J., 18(4):478-534, 2013. URL: https://doi.org/10.1007/S10601-013-9146-2.
  29. Nina Narodytska and Fahiem Bacchus. Maximum satisfiability using core-guided MaxSAT resolution. In Proceedings of the 28th Conference on Artificial Intelligence (AAAI), pages 2717-2723, 2014. URL: https://doi.org/10.1609/AAAI.V28I1.9124.
  30. Adrián Rebola-Pardo and Martin Suda. A theory of satisfiability-preserving proofs in SAT solving. In Proceedings of the 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), volume 57, pages 583-603, 2018. URL: https://doi.org/10.29007/TC7Q.
  31. Paul Saikko, Jeremias Berg, and Matti Järvisalo. LMHS: a SAT-IP hybrid MaxSAT solver. In Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 539-546, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_34.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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