Document Open Access Logo

Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability

Authors Jeremias Berg , Bart Bogaerts , Jakob Nordström , Andy Oertel , Tobias Paxian , Dieter Vandesande

PDF
Thumbnail PDF

File

LIPIcs.CP.2024.4.pdf
  • Filesize: 1.74 MB
  • 28 pages

Document Identifiers

Author Details

Jeremias Berg
  • Department of Computer Science, HIIT, Helsinki, Finland
  • University of Helsinki, Finland
Bart Bogaerts
  • Vrije Universiteit Brussel, Belgium
Jakob Nordström
  • University of Copenhagen, Denmark
  • Lund University, Sweden
Andy Oertel
  • Lund University, Sweden
  • University of Copenhagen, Denmark
Tobias Paxian
  • University of Freiburg, Germany
Dieter Vandesande
  • Vrije Universiteit Brussel, Belgium

Funding

  • Berg, Jeremias: Research Council of Finland under grants 342145.
  • Nordström, Jakob: Swedish Research Council grant 2016-00782 and Independent Research Fund Denmark grant 9040-00389B.
  • Oertel, Andy: Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.
  • Vandesande, Dieter: Fonds Wetenschappelijk Onderzoek - Vlaanderen (project G070521N).

Acknowledgements

We want to thank Florian Pollitt and Mathias Fleury for their assistance with the CADICAL proof tracer and for fuzzing VeriPB within CADICAL. Their contributions were very helpful to further improve the robustness of the VeriPB toolchain. We also wish to acknowledge useful discussions with participants of the Dagstuhl workshop 23261 SAT Encodings and Beyond. The computational experiments were enabled by resources provided by LUNARC at Lund University.

Cite AsGet BibTex

Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Tobias Paxian, and Dieter Vandesande. Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 4:1-4:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CP.2024.4

Abstract

Proof logging has long been the established method to certify correctness of Boolean satisfiability (SAT) solvers, but has only recently been introduced for SAT-based optimization (MaxSAT). The focus of this paper is solution-improving search (SIS), in which a SAT solver is iteratively queried for increasingly better solutions until an optimal one is found. A challenging aspect of modern SIS solvers is that they make use of complex "without loss of generality" arguments that are quite involved to understand even at a human meta-level, let alone to express in a simple, machine-verifiable proof. In this work, we develop pseudo-Boolean proof logging methods for solution-improving MaxSAT solving, and use them to produce a certifying version of the state-of-the-art solver Pacose with VeriPB proofs. Our experimental evaluation demonstrates that this approach works in practice. We hope that this is yet another step towards general adoption of proof logging in MaxSAT solving.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Constraint and logic programming
  • Mathematics of computing → Combinatorial optimization
Keywords
  • proof logging
  • certifying algorithms
  • MaxSAT
  • solution-improving search
  • SAT-UNSAT
  • maximum satisfiability
  • combinatorial optimization
  • certification
  • pseudo-Boolean

Metrics

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

Supplementary Materials

References

  1. Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn, Christine Rizkallah, and Pascal Schweitzer. An introduction to certifying algorithms. it - Information Technology Methoden und innovative Anwendungen der Informatik und Informationstechnik, 53(6):287-293, December 2011. Google Scholar
  2. Josep Argelich, Inês Lynce, and João P. Marques-Silva. On solving Boolean multilevel optimization problems. In Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI '09), pages 393-398, July 2009. Google Scholar
  3. Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. Maximum satisfiabiliy. In Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications, chapter 24, pages 929-991. IOS Press, 2nd edition, February 2021. Google Scholar
  4. Seulkee Baek, Mario Carneiro, and Marijn J. H. Heule. A flexible proof format for SAT solver-elaborator communication. In Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '21), volume 12651 of Lecture Notes in Computer Science, pages 59-75. Springer, March-April 2021. Google Scholar
  5. Olivier Bailleux and Yacine Boufkhad. Efficient CNF encoding of Boolean cardinality constraints. In Proceedings of the 9th International Conference on Principles and Practice of Constraint Programming (CP '03), volume 2833 of Lecture Notes in Computer Science, pages 108-122. Springer, September 2003. Google Scholar
  6. Olivier Bailleux, Yacine Boufkhad, and Olivier Roussel. New encodings of pseudo-Boolean constraints into CNF. In Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT '09), volume 5584 of Lecture Notes in Computer Science, pages 181-194. Springer, June 2009. Google Scholar
  7. Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, and Clark Barrett. Flexible proof production in an industrial-strength SMT solver. In Proceedings of the 11th International Joint Conference on Automated Reasoning (IJCAR '22), volume 13385 of Lecture Notes in Computer Science, pages 15-35. Springer, August 2022. Google Scholar
  8. Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Tobias Paxian, and Dieter Vandesande. Experimental Repository for "Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability", June 2024. URL: https://doi.org/10.5281/zenodo.10826301.
  9. 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), volume 14132 of Lecture Notes in Computer Science, pages 1-22. Springer, July 2023. Google Scholar
  10. Armin Biere. Tracecheck. http://fmv.jku.at/tracecheck/, 2006.
  11. Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2nd edition, February 2021. Google Scholar
  12. 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, August 2023. Preliminary version in AAAI '22. Google Scholar
  13. Bart Bogaerts, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, and Yong Kiam Tan. Documentation of VeriPB and CakePB for the SAT competition 2023. Available at https://satcompetition.github.io/2023/checkers.html, March 2023.
  14. Maria Luisa Bonet, Jordi Levy, and Felip Manyà. Resolution for Max-SAT. Artificial Intelligence, 171(8-9):606-618, June 2007. Extended version of paper in SAT '06. Google Scholar
  15. Robert Brummayer and Armin Biere. Fuzzing and delta-debugging SMT solvers. In Proceedings of the 7th International Workshop on Satisfiability Modulo Theories (SMT '09), pages 1-5, August 2009. Google Scholar
  16. Robert Brummayer, Florian Lonsing, and Armin Biere. Automated testing and debugging of SAT and QBF solvers. In Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT '10), volume 6175 of Lecture Notes in Computer Science, pages 44-57. Springer, July 2010. Google Scholar
  17. Samuel R. Buss and Jakob Nordström. Proof complexity and SAT solving. In Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications, chapter 7, pages 233-350. IOS Press, 2nd edition, February 2021. Google Scholar
  18. William Cook, Collette Rene Coullard, and György Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, November 1987. Google Scholar
  19. William Cook, Thorsten Koch, Daniel E. Steffy, and Kati Wolter. A hybrid branch-and-bound approach for exact rational mixed-integer programming. Mathematical Programming Computation, 5(3):305-344, September 2013. Google Scholar
  20. Jessica Davies and Fahiem Bacchus. Exploiting the power of MIP solvers in MAXSAT. In Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT '13), volume 7962 of Lecture Notes in Computer Science, pages 166-181. Springer, July 2013. Google Scholar
  21. Jasper van Doornmalen, Leon Eifler, Ambros Gleixner, and Christopher Hojny. A proof system for certifying symmetry and optimality reasoning in integer programming. Technical Report 2311.03877, arXiv.org, November 2023. Google Scholar
  22. Niklas Eén and Niklas Sörensson. Temporal induction by incremental SAT solving. In Proceedings of the 1st International Workshop on Bounded Model Checking (BMC '03), volume 89 of Electronic Notes in Theoretical Computer Science, pages 543-560, July 2003. Google Scholar
  23. Niklas Eén and Niklas Sörensson. Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4):1-26, March 2006. Google Scholar
  24. Leon Eifler and Ambros Gleixner. A computational status update for exact rational mixed integer programming. Mathematical Programming, 197(2):793-812, February 2023. Google Scholar
  25. Salomé Eriksson and Malte Helmert. Certified unsolvability for SAT planning with property directed reachability. In Proceedings of the 30th International Conference on Automated Planning and Scheduling, pages 90-100, October 2020. Google Scholar
  26. Salomé Eriksson, Gabriele Röger, and Malte Helmert. Unsolvability certificates for classical planning. In Proceedings of the 27th International Conference on Automated Planning and Scheduling (ICAPS '17), pages 88-97, June 2017. Google Scholar
  27. Salomé Eriksson, Gabriele Röger, and Malte Helmert. A proof system for unsolvable planning tasks. In Proceedings of the 28th International Conference on Automated Planning and Scheduling (ICAPS '18), pages 65-73, June 2018. Google Scholar
  28. Mathias Fleury. Formalization of Logical Calculi in Isabelle/HOL. PhD thesis, Universität des Saarlandes, 2020. Available at URL: https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/28722.
  29. 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 '06), volume 4121 of Lecture Notes in Computer Science, pages 252-265. Springer, August 2006. Google Scholar
  30. Xavier Gillard, Pierre Schaus, and Yves Deville. SolverCheck: Declarative testing of constraints. In Proceedings of the 25th International Conference on Principles and Practice of Constraint Programming (CP '19), volume 11802 of Lecture Notes in Computer Science, pages 565-582. Springer, October 2019. Google Scholar
  31. Stephan Gocht, Ruben Martins, Jakob Nordström, and Andy Oertel. Certified CNF translations for pseudo-Boolean solving. In Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing (SAT '22), volume 236 of Leibniz International Proceedings in Informatics (LIPIcs), pages 16:1-16:25, August 2022. Google Scholar
  32. Stephan Gocht, Ross McBride, Ciaran McCreesh, Jakob Nordström, Patrick Prosser, and James Trimble. Certifying solvers for clique and maximum common (connected) subgraph problems. In Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP '20), volume 12333 of Lecture Notes in Computer Science, pages 338-357. Springer, September 2020. Google Scholar
  33. Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, and Yong Kiam Tan. End-to-end verification for subgraph solving. In Proceedings of the 368h AAAI Conference on Artificial Intelligence (AAAI '24), pages 8038-8047, February 2024. Google Scholar
  34. Stephan Gocht and Jakob Nordström. Certifying parity reasoning efficiently using pseudo-Boolean proofs. In Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI '21), pages 3768-3777, February 2021. Google Scholar
  35. Evgueni Goldberg and Yakov Novikov. Verification of proofs of unsatisfiability for CNF formulas. In Proceedings of the Conference on Design, Automation and Test in Europe (DATE '03), pages 886-891, March 2003. Google Scholar
  36. Alexander Hoen, Andy Oertel, Ambros Gleixner, and Jakob Nordström. Certifying MIP-based presolve reductions for 0-1 integer linear programs. In Proceedings of the 21st International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR '24), volume 14742 of Lecture Notes in Computer Science, pages 310-328. Springer, May 2024. Google Scholar
  37. Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen, and Jakob Nordström. Certified MaxSAT preprocessing. In Proceedings of the 12th International Joint Conference on Automated Reasoning (IJCAR '24), volume 14739 of Lecture Notes in Computer Science, pages 396-418. Springer, July 2024. Google Scholar
  38. Saurabh Joshi, Ruben Martins, and Vasco M. Manquinho. Generalized totalizer encoding for pseudo-Boolean constraints. In Proceedings of the 21st International Conference on Principles and Practice of Constraint Programming (CP '15), volume 9255 of Lecture Notes in Computer Science, pages 200-209. Springer, august-september 2015. Google Scholar
  39. Matti Järvisalo, Marijn J. H. Heule, and Armin Biere. Inprocessing rules. In Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR '12), volume 7364 of Lecture Notes in Computer Science, pages 355-370. Springer, June 2012. Google Scholar
  40. Michal Karpinski and Marek Piotrów. Encoding cardinality constraints using multiway merge selection networks. Constraints, 24(3-4):234-251, October 2019. Google Scholar
  41. Sonja Kraiczy and Ciaran McCreesh. Solving graph homomorphism and subgraph isomorphism problems faster through clique neighbourhood constraints. In Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI '21), pages 1396-1402, August 2021. Google Scholar
  42. Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. A framework for certified Boolean branch-and-bound optimization. Journal of Automated Reasoning, 46(1):81-102, January 2011. Google Scholar
  43. Marcus Leivo, Jeremias Berg, and Matti Järvisalo. Preprocessing in incomplete MaxSAT solving. In Proceedings of the 24th European Conference on Artificial Intelligence (ECAI '20), volume 325 of Frontiers in Artificial Intelligence and Applications, pages 347-354, August-September 2020. Google Scholar
  44. Chu Min Li and Felip Manyà. MaxSAT, hard and soft constraints. In Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications, chapter 23, pages 903-927. IOS Press, 2nd edition, February 2021. Google Scholar
  45. Norbert Manthey, Tobias Philipp, and Peter Steinke. A more compact translation of pseudo-Boolean constraints into CNF such that generalized arc consistency is maintained. In Proceedings of the 37th Annual German Conference on Artificial Intelligence (KI '14), volume 8736 of Lecture Notes in Computer Science, pages 123-134. Springer, September 2014. Google Scholar
  46. MaxSAT evaluations: Evaluating the state of the art in maximum satisfiability solver technology. URL: https://maxsat-evaluations.github.io/.
  47. MaxSAT evaluation 2023. https://maxsat-evaluations.github.io/2023, July 2023.
  48. Ross M. McConnell, Kurt Mehlhorn, Stefan Näher, and Pascal Schweitzer. Certifying algorithms. Computer Science Review, 5(2):119-161, May 2011. Google Scholar
  49. António Morgado and João P. Marques-Silva. On validating Boolean optimizers. In Proceedings of the 23rd IEEE International Conference on Tools with Artificial Intelligence (ICTAI '12), pages 924-926, November 2011. Google Scholar
  50. Tobias Paxian and Armin Biere. Uncovering and classifying bugs in MaxSAT solvers through fuzzing and delta debugging. In Proceedings of the 14th International Workshop on Pragmatics of SAT, volume 3545 of CEUR Workshop Proceedings, pages 59-71. CEUR-WS.org, July 2023. Google Scholar
  51. Tobias Paxian, Pascal Raiola, and Bernd Becker. On preprocessing for weighted MaxSAT. In Proceedings of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '21), volume 12597 of Lecture Notes in Computer Science, pages 556-577. Springer, January 2021. Google Scholar
  52. Tobias Paxian, Sven Reimer, and Bernd Becker. Dynamic polynomial watchdog encoding for solving weighted MaxSAT. In Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing (SAT '18), volume 10929 of Lecture Notes in Computer Science, pages 37-53. Springer, July 2018. Google Scholar
  53. Matthieu Py, Mohamed Sami Cherif, and Djamal Habet. Towards bridging the gap between SAT and Max-SAT refutations. In Proceedings of the 32nd IEEE International Conference on Tools with Artificial Intelligence (ICTAI '20), pages 137-144, November 2020. Google Scholar
  54. Matthieu Py, Mohamed Sami Cherif, and Djamal Habet. A proof builder for Max-SAT. In Proceedings of the 24th International Conference on Theory and Applications of Satisfiability Testing (SAT '21), volume 12831 of Lecture Notes in Computer Science, pages 488-498. Springer, July 2021. Google Scholar
  55. Matthieu Py, Mohamed Sami Cherif, and Djamal Habet. Proofs and certificates for Max-SAT. Journal of Artificial Intelligence Research, 75:1373-1400, December 2022. Google Scholar
  56. Gabriele Röger. Towards certified unsolvability in classical planning. In Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI '17), pages 5141-5145, August 2017. Google Scholar
  57. Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, and Pascal Fontaine. Alethe: Towards a generic SMT proof format (extended abstract). In Proceedings of the 7th Workshop on Proof eXchange for Theorem Proving (PxTP '21, volume 336 of Electronic Proceedings in Theoretical Computer Science, pages 49-54, July 2021. Google Scholar
  58. Carsten Sinz. Towards an optimal CNF encoding of Boolean cardinality constraints. In Proceedings of the 11th International Conference on Principles and Practice of Constraint Programming (CP '05), volume 3709 of Lecture Notes in Computer Science, pages 827-831. Springer, October 2005. Google Scholar
  59. Dieter Vandesande. Towards certified MaxSAT solving: Certified MaxSAT solving with SAT oracles and encodings of pseudo-Boolean constraints. Master’s thesis, Vrije Universiteit Brussel (VUB), 2023. URL: https://researchportal.vub.be/nl/studentTheses/towards-certified-maxsat-solving.
  60. Dieter Vandesande, Wolf De Wulf, and Bart Bogaerts. QMaxSATpb: A certified MaxSAT solver. In Proceedings of the 16th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR '22), volume 13416 of Lecture Notes in Computer Science, pages 429-442. Springer, September 2022. Google Scholar
  61. VeriPB: Verifier for pseudo-Boolean proofs. URL: https://gitlab.com/MIAOresearch/software/VeriPB.
  62. Joost P. Warners. A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters, 68(2):63-69, October 1998. Google Scholar
  63. Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt Jr. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT '14), volume 8561 of Lecture Notes in Computer Science, pages 422-429. Springer, July 2014. Google Scholar
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact