Document Open Access Logo

Certified CNF Translations for Pseudo-Boolean Solving

Authors Stephan Gocht , Ruben Martins , Jakob Nordström , Andy Oertel

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.16.pdf
  • Filesize: 1.55 MB
  • 25 pages

Document Identifiers

Author Details

Stephan Gocht
  • Lund University, Sweden
  • University of Copenhagen, Denmark
Ruben Martins
  • Carnegie Mellon University, Pittsburgh, PA, USA
Jakob Nordström
  • University of Copenhagen, Denmark
  • Lund University, Sweden
Andy Oertel
  • Lund University, Sweden
  • University of Copenhagen, Denmark

Funding

  • Gocht, Stephan: Swedish Research Council grant 2016-00782.
  • Martins, Ruben: National Science Foundation award CCF-1762363 and Amazon Research Award.
  • 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.

Acknowledgements

The authors wish to acknowledge helpful and stimulating discussions with Bart Bogaerts and Ciaran McCreesh. We are particularly grateful to Bart for sharing the manuscript [Dieter Vandesande et al., 2022] using a very elegant reification technique that we wish we would have thought of, and we believe it would be worth exploring whether similar ideas could be used in our framework to improve the efficiency of verification. We are also thankful for discussions and feedback at the workshops Pragmatics of SAT and Proof eXchange for Theorem Proving in 2021, where a preliminary version of this work was presented, and we would like to extend a special thanks to the SAT '22 anonymous reviewers for a wealth of comments and questions that helped to improve this manuscript considerably.

Cite AsGet BibTex

Stephan Gocht, Ruben Martins, Jakob Nordström, and Andy Oertel. Certified CNF Translations for Pseudo-Boolean Solving. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 16:1-16:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.16

Abstract

The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage state-of-the-art conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in increasing the confidence that the results these solvers produce are correct. However, the fact that SAT proof logging is performed in conjunctive normal form (CNF) clausal format means that it has not been possible to extend guarantees of correctness to the use of SAT solvers for more expressive combinatorial paradigms, where the first step is an unverified translation of the input to CNF. In this work, we show how cutting-planes-based reasoning can provide proof logging for solvers that translate pseudo-Boolean (a.k.a. 0-1 integer linear) decision problems to CNF and then run CDCL. To support a wide range of encodings, we provide a uniform and easily extensible framework for proof logging of CNF translations. We are hopeful that this is just a first step towards providing a unified proof logging approach that will also extend to maximum satisfiability (MaxSAT) solving and pseudo-Boolean optimization in general.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Hardware → Theorem proving and SAT solving
  • Theory of computation → Logic and verification
Keywords
  • pseudo-Boolean solving
  • 0-1 integer linear program
  • proof logging
  • certifying algorithms
  • certified translation
  • CNF encoding
  • cutting planes

Metrics

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

Supplementary Materials

References

  1. Özgür Akgün, Ian P. Gent, Christopher Jefferson, Ian Miguel, and Peter Nightingale. Metamorphic testing of constraint solvers. In Proceedings of the 24th International Conference on Principles and Practice of Constraint Programming (CP '18), volume 11008 of Lecture Notes in Computer Science, pages 727-736. Springer, August 2018. Google Scholar
  2. 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
  3. 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
  4. Lee A. Barnett and Armin Biere. Non-clausal redundancy properties. In Proceedings of the 28th International Conference on Automated Deduction (CADE-28), volume 12699 of Lecture Notes in Computer Science, pages 252-272. Springer, July 2021. Google Scholar
  5. Peter Barth. A Davis-Putnam based enumeration algorithm for linear pseudo-Boolean optimization. Technical Report MPI-I-95-2-003, Max-Planck-Institut für Informatik, January 1995. Google Scholar
  6. Kenneth E. Batcher. Sorting networks and their applications. In Proceedings of the Spring Joint Computer Conference of the American Federation of Information Processing Societies (AFIPS '68), volume 32, pages 307-314, April 1968. Google Scholar
  7. Jeremias Berg, Fahiem Bacchus, and Alex Poole. Abstract cores in implicit hitting set MaxSat solving. In Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT '20), volume 12178 of Lecture Notes in Computer Science, pages 277-294. Springer, July 2020. Google Scholar
  8. Armin Biere. Tracecheck. http://fmv.jku.at/tracecheck/, 2006.
  9. 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
  10. Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified symmetry and dominance breaking for combinatorial optimisation. In Proceedings of the 36th AAAI Conference on Artificial Intelligence (AAAI '22), February 2022. To appear. Google Scholar
  11. 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
  12. Randal E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-691, August 1986. Google Scholar
  13. Randal E. Bryant, Armin Biere, and Marijn J. H. Heule. Clausal proofs for pseudo-Boolean reasoning. In Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '22), volume 13243 of Lecture Notes in Computer Science, pages 443-461. Springer, April 2022. Google Scholar
  14. 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
  15. Kevin K. H. Cheung, Ambros M. Gleixner, and Daniel E. Steffy. Verifying integer programming results. In Proceedings of the 19th International Conference on Integer Programming and Combinatorial Optimization (IPCO '17), volume 10328 of Lecture Notes in Computer Science, pages 148-160. Springer, June 2017. Google Scholar
  16. 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
  17. 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
  18. Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt, Matt Kaufmann, and Peter Schneider-Kamp. Efficient certified RAT verification. In Proceedings of the 26th International Conference on Automated Deduction (CADE-26), volume 10395 of LNCS, pages 220-236. Springer, 2017. Google Scholar
  19. Luís Cruz-Filipe, Joao Marques-Silva, and Peter Schneider-Kamp. Efficient certified resolution proof checking. In Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '17), volume 10205 of LNCS, pages 118-135. Springer, 2017. Google Scholar
  20. 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 '11), volume 6876 of Lecture Notes in Computer Science, pages 225-239. Springer, September 2011. Google Scholar
  21. Jo Devriendt, Ambros Gleixner, and Jakob Nordström. Learn to relax: Integrating 0-1 integer linear programming with pseudo-Boolean conflict-driven search. Constraints, 26(1-4):26-55, October 2021. Preliminary version in CPAIOR '20. Google Scholar
  22. Jo Devriendt, Stephan Gocht, Emir Demirović, Jakob Nordström, and Peter Stuckey. Cutting to the core of pseudo-Boolean optimization: Combining core-guided search with cutting planes reasoning. In Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI '21), pages 3750-3758, February 2021. 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. In Proceedings of the 22nd International Conference on Integer Programming and Combinatorial Optimization (IPCO '21), volume 12707 of Lecture Notes in Computer Science, pages 163-177. Springer, May 2021. Google Scholar
  25. Jan Elffers, Jesús Giráldez-Cru, Jakob Nordström, and Marc Vinyals. Using combinatorial benchmarks to probe the reasoning power of pseudo-Boolean solvers. 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 75-93. Springer, July 2018. Google Scholar
  26. Jan Elffers, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Justifying all differences using pseudo-Boolean reasoning. In Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI '20), pages 1486-1494, February 2020. Google Scholar
  27. Jan Elffers and Jakob Nordström. Divide and conquer: Towards faster pseudo-Boolean solving. In Proceedings of the 27th International Joint Conference on Artificial Intelligence (IJCAI '18), pages 1291-1299, July 2018. Google Scholar
  28. 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
  29. 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
  30. Stephan Gocht, Ruben Martins, Jakob Nordström, and Andy Oertel. Experimental repository for "Certified CNF translations for pseudo-Boolean solving". Available at https://doi.org/10.5281/zenodo.6610581, June 2022.
  31. 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
  32. Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Subgraph isomorphism meets cutting planes: Solving with certified solutions. In Proceedings of the 29th International Joint Conference on Artificial Intelligence (IJCAI '20), pages 1134-1140, July 2020. Google Scholar
  33. 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
  34. 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
  35. Marijn J. H. Heule, Warren A. Hunt Jr., and Nathan Wetzler. Trimming while checking clausal proofs. In Proceedings of the 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD '13), pages 181-188, October 2013. Google Scholar
  36. Marijn J. H. Heule, Warren A. Hunt Jr., and Nathan Wetzler. Verifying refutations with extended resolution. In Proceedings of the 24th International Conference on Automated Deduction (CADE-24), volume 7898 of Lecture Notes in Computer Science, pages 345-359. Springer, June 2013. Google Scholar
  37. Steffen Hölldobler, Norbert Manthey, and Peter Steinke. A compact encoding of pseudo-Boolean constraints into SAT. In Proceedings of KI 2012: Advances in Artificial Intelligence, the 35th Annual German Conference on AI, volume 7526 of Lecture Notes in Computer Science, pages 107-118. Springer, 2012. 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. Daniela Kaufmann, Paul Beame, Armin Biere, and Jakob Nordström. Adding dual variables to algebraic reasoning for circuit verification. In Proceedings of the 25th Design, Automation and Test in Europe Conference (DATE '22), pages 1435-1440, March 2022. Google Scholar
  40. Daniela Kaufmann and Armin Biere. AMulet 2.0 for verifying multiplier circuits. In Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '21), volume 12652 of Lecture Notes in Computer Science, pages 357-364. Springer, March-April 2021. Google Scholar
  41. Daniela Kaufmann, Mathias Fleury, and Armin Biere. The proof checkers Pacheck and Pastèque for the practical algebraic calculus. In Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design (FMCAD '20), pages 264-269, September 2020. Google Scholar
  42. Kissat SAT solver. URL: http://fmv.jku.at/kissat/.
  43. Daniel Le Berre and Anne Parrain. The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation, 7:59-64, July 2010. Google Scholar
  44. João P. Marques-Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506-521, May 1999. Preliminary version in ICCAD '96. Google Scholar
  45. Ruben Martins, Vasco M. Manquinho, and Inês Lynce. Open-WBO: A modular MaxSAT solver. 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 438-445. Springer, July 2014. Google Scholar
  46. Ross M. McConnell, Kurt Mehlhorn, Stefan Näher, and Pascal Schweitzer. Certifying algorithms. Computer Science Review, 5(2):119-161, May 2011. Google Scholar
  47. António Morgado, Federico Heras, Mark H. Liffiton, Jordi Planes, and João P. Marques-Silva. Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints, 18(4):478-534, October 2013. Google Scholar
  48. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference (DAC '01), pages 530-535, June 2001. Google Scholar
  49. NaPS (Nagoya pseudo-Boolean solver). URL: https://www.trs.cm.is.nagoya-u.ac.jp/projects/NaPS/.
  50. Open-WBO: An open source version of the MaxSAT solver WBO. URL: http://sat.inesc-id.pt/open-wbo/.
  51. Tobias Philipp and Peter Steinke. PBLib - a library for encoding pseudo-Boolean constraints into CNF. In Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT '15), volume 9340 of Lecture Notes in Computer Science, pages 9-16. Springer, September 2015. Google Scholar
  52. Pseudo-Boolean competition 2016. http://www.cril.univ-artois.fr/PB16/, July 2016.
  53. Daniela Ritirc, Armin Biere, Manuel Kauers, A Bigatti, and M Brain. A practical polynomial calculus for arithmetic circuit verification. In 3rd International Workshop on Satisfiability Checking and Symbolic Computation (SC2 ’18), pages 61-76, 2018. Google Scholar
  54. Olivier Roussel and Vasco M. Manquinho. Input/output format and solver requirements for the competitions of pseudo-Boolean solvers. Revision 2324. Available at http://www.cril.univ-artois.fr/PB16/format.pdf, January 2016.
  55. Masahiko Sakai and Hidetomo Nabeshima. Construction of an ROBDD for a PB-constraint in band form and related techniques for PB-solvers. IEICE Transactions on Information and Systems, 98-D(6):1121-1127, June 2015. Google Scholar
  56. The international SAT Competitions web page. URL: http://www.satcompetition.org.
  57. 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
  58. Allen Van Gelder. Verifying RUP proofs of propositional unsatisfiability. In 10th International Symposium on Artificial Intelligence and Mathematics (ISAIM '08), 2008. Available at URL: http://isaim2008.unl.edu/index.php?page=proceedings.
  59. Dieter Vandesande, Wolf De Wulf, and Bart Bogaerts. QMaxSATpb: A certified MaxSAT solver. Manuscript, 2022. Google Scholar
  60. VeriPB: Verifier for pseudo-Boolean proofs. URL: https://gitlab.com/MIAOresearch/VeriPB.
  61. Joost P. Warners. A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters, 68(2):63-69, 1998. Google Scholar
  62. 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