Document Open Access Logo

Practically Feasible Proof Logging for Pseudo-Boolean Optimization

Authors Wietze Koops , Daniel Le Berre , Magnus O. Myreen , Jakob Nordström , Andy Oertel , Yong Kiam Tan , Marc Vinyals

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CP.2025.21.pdf
  • Filesize: 1.28 MB
  • 27 pages
HTML5 Logo HTML (experimental)
LIPIcs.CP.2025.21.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Mathematics of computing → Combinatorial optimization
Keywords
  • proof logging
  • certifying algorithms
  • combinatorial optimization
  • certification
  • pseudo-Boolean solving
  • 0-1 integer linear programming

Metrics

Abstract

Certifying solvers have long been standard for decision problems in Boolean satisfiability (SAT), allowing for proof logging and checking with very limited overhead, but developing similar tools for combinatorial optimization has remained a challenge. A recent promising approach covering a wide range of solving paradigms is pseudo-Boolean proof logging, but this has mostly consisted of proof-of-concept works far from delivering the performance required for real-world deployment.
In this work, we present an efficient toolchain based on VeriPB and CakePB for formally verified pseudo-Boolean optimization. We implement proof logging for the full range of techniques in the state-of-the-art solvers RoundingSat and Sat4j, including core-guided search and linear programming integration with Farkas certificates and cut generation. Our experimental evaluation shows that proof logging and checking performance in this much more expressive paradigm is now quite close to the level of SAT solving, and hence is clearly practically feasible.

Cite As Get BibTex

Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, and Marc Vinyals. Practically Feasible Proof Logging for Pseudo-Boolean Optimization. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 21:1-21:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CP.2025.21

Author Details

Wietze Koops
  • Lund University, Sweden
  • University of Copenhagen, Denmark
Daniel Le Berre
  • Univ. Artois, CNRS, UMR 8188 CRIL, Lens, France
Magnus O. Myreen
  • Chalmers University of Technology, Gothenburg, Sweden
  • University of Gothenburg, Sweden
Jakob Nordström
  • University of Copenhagen, Denmark
  • Lund University, Sweden
Andy Oertel
  • Lund University, Sweden
  • University of Copenhagen, Denmark
Yong Kiam Tan
  • Institute for Infocomm Research (I²R), A*STAR, Singapore
  • Nanyang Technological University, Singapore
Marc Vinyals
  • University of Auckland, New Zealand

Funding

  • Koops, Wietze: Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.
  • Le Berre, Daniel: BLaSST ANR-21-CE25-0010.
  • Myreen, Magnus O.: Swedish Research Council grant 2021-05165.
  • Nordström, Jakob: Swedish Research Council grants 2016-00782 and 2024-05801 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.
  • Tan, Yong Kiam: Singapore NRF Fellowship Programme NRF-NRFF16-2024-0002
  • Vinyals, Marc: UoA FoS RDF 3729031

Acknowledgements

We would like to acknowledge earlier work on RoundingSat and by Jan Elffers, Jo Devriendt, and Stephan Gocht, and on Sat4j by Anthony Blomme and Romain Wallon, including preliminary contributions to proof logging. We are most grateful to Benjamin Bogø for useful feedback and for helping us to fix a bug in the proof logging code developed for this paper. Different subsets of the authors wish to thank the participants of the Dagstuhl workshops 22411 Theory and Practice of SAT and Combinatorial Solving and 23261 SAT Encodings and Beyond for several stimulating discussions. The first, fourth, and fifth authors also gratefully acknowledge that they have benefitted greatly from being part of the Basic Algorithms Research Copenhagen (BARC) environment financed by the Villum Investigator grant 54451. The computational experiments were enabled by resources provided by LUNARC at Lund University.

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. URL: https://doi.org/10.1007/978-3-319-98334-9_46.
  2. Katherine I. Albanese, Sophie Barbe, Shunsuke Tagami, Derek N. Woolfson, and Thomas Schiex. Computational protein design. Nature Reviews Methods Primers, 5(13), February 2025. Google Scholar
  3. Bruno Andreotti, Hanna Lachnitt, and Haniel Barbosa. Carcara: An efficient proof checker and elaborator for SMT proofs in the alethe format. In Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '23), volume 13993 of Lecture Notes in Computer Science, pages 367-386. Springer, April 2023. URL: https://doi.org/10.1007/978-3-031-30823-9_19.
  4. 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. URL: https://doi.org/10.1007/978-3-031-10769-6_3.
  5. 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 Proceedings of the 30th International Conference on Principles and Practice of Constraint Programming (CP '24), volume 307 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1-4:28, September 2024. URL: https://doi.org/10.4230/LIPICS.CP.2024.4.
  6. 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. URL: https://doi.org/10.1007/978-3-031-38499-8_1.
  7. Daniel Le Berre and Stéphanie Roussel. Sat4j 2.3.2: on the fly solver configuration: System description. Journal on Satisfiability, Boolean Modelling and Computation, 8(3/4):197-202, August 2012. Google Scholar
  8. Frédéric Besson, Pascal Fontaine, and Laurent Théry. A flexible proof format for SMT: a proposal. In Proceedings of the 1st Workshop on Proof eXchange for Theorem Proving (PxTP '11), pages 15-26, August 2011. URL: https://pxtp2011.loria.fr/PxTP2011.pdf#page=19.
  9. Armin Biere. Tracecheck. http://fmv.jku.at/tracecheck/, 2006.
  10. Armin Biere and Daniel Kröning. SAT-based model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, chapter 10, pages 277-303. Springer, December 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_10.
  11. Péter Biró, Joris van de Klundert, David F. Manlove, William Pettersson, Tommy Andersson, Lisa Burnapp, Pavel Chromy, Pablo Delgado, Piotr Dworczak, Bernadette Haase, Aline Hemke, Rachel Johnson, Xenia Klimentova, Dirk Kuypers, Alessandro Nanni Costa, Bart Smeulders, Frits C. R. Spieksma, María O. Valentín, and Ana Viana. Modelling and optimisation in European kidney exchange programmes. European Journal of Operational Research, 291(2):447-456, June 2021. URL: https://doi.org/10.1016/J.EJOR.2019.09.006.
  12. Péter Biró, Bernadette Haase-Kromwijk, Tommy Andersson, Eyjólfur Ingi Ásgeirsson, Tatiana Baltesová, Ioannis Boletis, Catarina Bolotinha, Gregor Bond, Georg Böhmig, Lisa Burnapp, Katarína Cechlárová, Paola Di Ciaccio, Jiri Fronek, Karine Hadaya, Aline Hemke, Christian Jacquelinet, Rachel Johnson, Rafal Kieszek, Dirk R. Kuypers, Ruthanne Leishman, Marie-Alice Macher, David Manlove, Georgia Menoudakou, Mikko Salonen, Bart Smeulders, Vito Sparacino, Frits C. R. Spieksma, María Oliva Valentín, Nic Wilson, and Joris van der Klundert. Building kidney exchange programmes in Europe - An overview of exchange practice and activities. Transplantation, 103(7):1514-1522, June 2019. Google Scholar
  13. 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. URL: https://doi.org/10.1613/JAIR.1.14296.
  14. 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
  15. Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, and Marijn J. H. Heule. Certified knowledge compilation with application to verified model counting. In Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing (SAT '23), volume 271 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1-6:20, 2023. URL: https://doi.org/10.4230/LIPICS.SAT.2023.6.
  16. 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. URL: https://doi.org/10.3233/FAIA200990.
  17. Florent Capelli. Knowledge compilation languages as proof systems. In Mikolás Janota and Inês Lynce, editors, Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT '19), volume 11628 of Lecture Notes in Computer Science, pages 90-99. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_6.
  18. 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. URL: https://doi.org/10.1007/978-3-319-59250-3_13.
  19. 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. URL: https://doi.org/10.1016/0166-218X(87)90039-4.
  20. 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. URL: https://doi.org/10.1007/S12532-013-0055-6.
  21. Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., 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 Lecture Notes in Computer Science, pages 220-236. Springer, August 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_14.
  22. Luís Cruz-Filipe, João P. 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 Lecture Notes in Computer Science, pages 118-135. Springer, April 2017. URL: https://doi.org/10.1007/978-3-662-54577-5_7.
  23. Emir Demirović, Ciaran McCreesh, Matthew McIlree, Jakob Nordström, Andy Oertel, and Konstantin Sidorov. Pseudo-Boolean reasoning about states and transitions to certify dynamic programming and decision diagram algorithms. In Proceedings of the 30th International Conference on Principles and Practice of Constraint Programming (CP '24), volume 307 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:21, September 2024. URL: https://doi.org/10.4230/LIPICS.CP.2024.9.
  24. Jo Devriendt. Watched propagation of 0-1 integer linear constraints. 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 160-176. Springer, September 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_10.
  25. 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. URL: https://doi.org/10.1007/S10601-020-09318-X.
  26. 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. URL: https://doi.org/10.1609/AAAI.V35I5.16492.
  27. Simon Dold, Malte Helmert, Jakob Nordström, Gabriele Röger, and Tanja Schindler. Pseudo-Boolean proof logging for optimal classical planning. In Proceedings of the 35th International Conference on Automated Planning and Scheduling (ICAPS '25), November 2025. To appear. Google Scholar
  28. Nicholas Downing, Thibaut Feydy, and Peter J. Stuckey. Explaining alldifferent. In Proceedings of the 35th Australasian Computer Science Conference (ACSC '12), pages 115-124, January 2012. URL: http://crpit.scem.westernsydney.edu.au/abstracts/CRPITV122Downing.html.
  29. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In 6th International Conference on Theory and Applications of Satisfiability Testing (SAT '03), Selected Revised Papers, volume 2919 of Lecture Notes in Computer Science, pages 502-518. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24605-3_37.
  30. Leon Eifler and Ambros Gleixner. A computational status update for exact rational mixed integer programming. Mathematical Programming, 197(2):793-812, February 2023. URL: https://doi.org/10.1007/S10107-021-01749-5.
  31. 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. URL: https://doi.org/10.1609/AAAI.V34I02.5507.
  32. 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. URL: https://doi.org/10.24963/IJCAI.2018/180.
  33. 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. URL: https://aaai.org/ocs/index.php/ICAPS/ICAPS17/paper/view/15734.
  34. 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. URL: https://aaai.org/ocs/index.php/ICAPS/ICAPS18/paper/view/17760.
  35. Katalin Fazekas, Florian Pollitt, Mathias Fleury, and Armin Biere. Certifying incremental SAT solving. In Proceedings of the 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2024), volume 100 of EPiC Series in Computing, pages 321-340, May 2024. URL: https://doi.org/10.29007/PDCC.
  36. Johannes Klaus Fichte, Markus Hecher, and Valentin Roland. Proofs for propositional model counting. 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 30:1-30:24, August 2022. URL: https://doi.org/10.4230/LIPICS.SAT.2022.30.
  37. 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. URL: https://doi.org/10.1007/978-3-030-30048-7_33.
  38. 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. URL: https://doi.org/10.1007/978-3-030-58475-7_20.
  39. 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 38th AAAI Conference on Artificial Intelligence (AAAI '24), pages 8038-8047, February 2024. URL: https://doi.org/10.1609/AAAI.V38I8.28642.
  40. 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. URL: https://doi.org/10.24963/IJCAI.2020/158.
  41. Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. An auditable constraint programming solver. In Proceedings of the 28th International Conference on Principles and Practice of Constraint Programming (CP '22), volume 235 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1-25:18, August 2022. URL: https://doi.org/10.4230/LIPICS.CP.2022.25.
  42. 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. URL: https://doi.org/10.1609/AAAI.V35I5.16494.
  43. 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
  44. Mark A. Hallen and Bruce Randall Donald. Protein design by provable algorithms. Communications of the ACM, 62(10):76-84, October 2019. URL: https://doi.org/10.1145/3338124.
  45. Peter L. Hammer and Sergiu Rudeanu. Boolean Methods in Operations Research and Related Areas. Springer Verlag, New York, 1968. Google Scholar
  46. 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. URL: https://ieeexplore.ieee.org/document/6679408/.
  47. 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. URL: https://doi.org/10.1007/978-3-642-38574-2_24.
  48. Jochen Hoenicke and Tanja Schindler. A simple proof format for SMT. In Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories (SMT '22), volume 3185 of CEUR Workshop Proceedings, pages 54-70, August 2022. URL: https://ceur-ws.org/Vol-3185/paper9527.pdf.
  49. 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. URL: https://doi.org/10.1007/978-3-031-63498-7_24.
  50. 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. URL: https://doi.org/10.24963/IJCAI.2021/193.
  51. Peter Lammich. Efficient verified (UN)SAT certificate checking. Journal of Automated Reasoning, 64(3):513-532, March 2020. Extended version of paper in CADE 2017. URL: https://doi.org/10.1007/S10817-019-09525-Z.
  52. 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
  53. Hugues Marchand and Laurence A. Wolsey. Aggregation and mixed integer rounding to solve MIPs. Operations Research, 49(3):325-468, June 2001. Google Scholar
  54. Fabio Massacci and Laura Marraro. Logical cryptanalysis as a SAT problem. Journal of Automated Reasoning, 24:165-203, February 2000. URL: https://doi.org/10.1023/A:1006326723002.
  55. Matthew McIlree and Ciaran McCreesh. Proof logging for smart extensional constraints. In Proceedings of the 29th International Conference on Principles and Practice of Constraint Programming (CP '23), volume 280 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1-26:17, August 2023. URL: https://doi.org/10.4230/LIPICS.CP.2023.26.
  56. Matthew McIlree and Ciaran McCreesh. Certifying bounds propagation for integer multiplication constraints. In Proceedings of the 39th AAAI Conference on Artificial Intelligence (AAAI '25), pages 11309-11317, February-March 2025. URL: https://doi.org/10.1609/AAAI.V39I11.33230.
  57. Matthew McIlree, Ciaran McCreesh, and Jakob Nordström. Proof logging for the circuit constraint. In Proceedings of the 21st International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR '24), volume 14743 of Lecture Notes in Computer Science, pages 38-55. Springer, May 2024. URL: https://doi.org/10.1007/978-3-031-60599-4_3.
  58. Esther Mugdan, Remo Christen, and Salomé Eriksson. Optimality certificates for classical planning. In Proceedings of the 33rd International Conference on Automated Planning and Scheduling (ICAPS '23), pages 286-294, July 2023. URL: https://doi.org/10.1609/ICAPS.V33I1.27206.
  59. Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Rui Zhao. Speeding up pseudo-Boolean propagation. In Proceedings of the 27th International Conference on Theory and Applications of Satisfiability Testing (SAT '24), volume 305 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:18, August 2024. URL: https://doi.org/10.4230/LIPICS.SAT.2024.22.
  60. Olga Ohrimenko, Peter J. Stuckey, and Michael Codish. Propagation via lazy clause generation. Constraints, 14(3):357-391, January 2009. URL: https://doi.org/10.1007/S10601-008-9064-X.
  61. Florian Pollitt, Mathias Fleury, and Armin Biere. Faster LRAT checking than solving with CaDiCaL. In Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing (SAT '23), volume 271 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:12, July 2023. URL: https://doi.org/10.4230/LIPICS.SAT.2023.21.
  62. Pseudo-Boolean competition 2024. https://www.cril.univ-artois.fr/PB24/, August 2024.
  63. The International SAT Competitions web page. URL: https://satcompetition.github.io.
  64. Dominik Schreiber. Lilotane: A lifted SAT-based approach to hierarchical planning. Journal of Artificial Intelligence Research, 70:1117-1181, March 2021. URL: https://doi.org/10.1613/JAIR.1.12520.
  65. 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. URL: https://doi.org/10.4204/EPTCS.336.6.
  66. Yong Kiam Tan, Marijn J. H. Heule, and Magnus O. Myreen. cake_lpr: Verified propagation redundancy checking in CakeML. 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 223-241. Springer, March-April 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_12.
  67. Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, and Michael Norrish. The verified CakeML compiler backend. Journal of Functional Programming, 29:e2:1-e2:57, February 2019. Google Scholar
  68. 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.
  69. Michael Veksler and Ofer Strichman. A proof-producing CSP solver. In Proceedings of the 24th AAAI Conference on Artificial Intelligence (AAAI '10), pages 204-209, July 2010. URL: https://doi.org/10.1609/AAAI.V24I1.7543.
  70. VeriPB: Verifier for pseudo-Boolean proofs. URL: https://gitlab.com/MIAOresearch/software/VeriPB.
  71. 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. URL: https://doi.org/10.1007/978-3-319-09284-3_31.
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