Publications

How to cite VeriPB

Please cite up to three of the following references in this order of priority. You can click on the references to get their BibTeX entry:

Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified Dominance and Symmetry Breaking for Combinatorial Optimisation. Journal of Artificial Intelligence Research, 2023.


        @article{BGMN23Dominance,
        author    = {Bart Bogaerts and Stephan Gocht and Ciaran McCreesh
                    and Jakob Nordström},
        title     = {Certified Dominance and Symmetry Breaking for
                    Combinatorial Optimisation},
        year      = {2023},
        month     = aug,
        journal   = {Journal of Artificial Intelligence Research},
        volume    = {77},
        pages     = {1539\nobreakdash--1589},
        note      = {Preliminary version in \emph{AAAI~'22}},
        }

Stephan Gocht, and Jakob Nordström. Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs. Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI '21), 2021.


        @inproceedings{GN21CertifyingParity,
        author    = {Stephan Gocht and Jakob Nordström},
        title     = {Certifying Parity Reasoning Efficiently Using
                    Pseudo-{B}oolean Proofs},
        year      = {2021},
        month     = feb,
        booktitle = {Proceedings of the 35th {AAAI} Conference on
                    Artificial Intelligence ({AAAI}~'21)},
        pages     = {3768\nobreakdash--3777}
        }

Stephan Gocht. Certifying Correctness for Combinatorial Algorithms by Using Pseudo-Boolean Reasoning. Lund University, Lund, Sweden, 2022.


        @phdthesis{Gocht22Thesis,
        author  = {Stephan Gocht},
        title   = {Certifying Correctness for Combinatorial Algorithms
                    by Using Pseudo-{B}oolean Reasoning},
        school  = {Lund University},
        address = {Lund, Sweden},
        year    = {2022},
        month   = jun,
        note    = {Available at
                    \url{https://portal.research.lu.se/en/publications/certifying-correctness-for-combinatorial-algorithms-by-using-pseu}},
        }

VeriPB in the Literature

The following is a list of scientific publications that make use of (some version of) VeriPB.

Berhan Oumer Adame, Bart Bogaerts, Benjamin Bogø, Simon Dold, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Matthew McIlree, Jakob Nordström, Andy Oertel, Adrián Rebola-Pardo, Mark Turnbull, "Trimming Pseudo-Boolean Proofs", Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design (FMCAD '26), pp. 743–756, September, 2026. doi:10.34727/2026/isbn.978-3-85448-093-8_74

Simon Dold, George Katsirelos, Wietze Koops, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, "End-to-End Certified Graph Colouring", Proceedings of the 32nd International Conference on Principles and Practice of Constraint Programming (CP '26), pp. 21:1–21:27, July, 2026. doi:10.4230/LIPIcs.CP.2026.21

Ciaran McCreesh, Jakob Nordström, Andy Oertel, Yong Kiam Tan, "Proof Logging for Projected Enumeration (and Counting?) Problems in VeriPB", Proceedings of the 32nd International Conference on Principles and Practice of Constraint Programming (CP '26), pp. 43:1–43:21, July, 2026. doi:10.4230/LIPIcs.CP.2026.43

Matthew McIlree, "Pseudo-Boolean Proof Logging for Constraint Propagation Algorithms", PhD thesis, University of Glasgow, June, 2026. URL: https://theses.gla.ac.uk/86049/

Andy Oertel, "Certifying Combinatorial Optimization: A Unified Approach Using Pseudo-Boolean Reasoning", PhD thesis, Lund University, May, 2026. URL: https://portal.research.lu.se/sv/publications/certifying-combinatorial-optimization-a-unified-approach-using-ps/

Stefan Szeider, "PBLean: Pseudo-Boolean Proof Certificates for Lean 4", 2602.08692, no. arXiv:2602.08692, February, 2026. doi:10.48550/arXiv.2602.08692

Dieter Vandesande, Jordi Coll, Bart Bogaerts, "Certified Branch-and-Bound MaxSAT Solving", Proceedings of the 40th AAAI Conference on Artificial Intelligence (AAAI '26), pp. 14342–14351, January, 2026. doi:10.1609/aaai.v40i17.38449

Hannes Ihalainen, Dieter Vandesande, André Schidler, Jeremias Berg, Bart Bogaerts, Matti Järvisalo, "Efficient and Reliable Hitting-Set Computations for the Implicit Hitting Set Approach", Proceedings of the 40th AAAI Conference on Artificial Intelligence (AAAI '26), pp. 14251–14260, January, 2026. doi:10.1609/aaai.v40i17.38439

Markus Anders, Bart Bogaerts, Benjamin Bogø, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Adrián Rebola-Pardo, Yong Kiam Tan, "Faster Certified Symmetry Breaking using Orders with Auxiliary Variables", Proceedings of the 40th AAAI Conference on Artificial Intelligence (AAAI '26), pp. 14140–14148, January, 2026. doi:10.1609/aaai.v40i17.38426

Simon Dold, Malte Helmert, Jakob Nordström, Gabriele Röger, Tanja Schindler, "Pseudo-Boolean Proof Logging for Optimal Classical Planning", Proceedings of the 35th International Conference on Automated Planning and Scheduling (ICAPS '25), pp. 54–63, November, 2025. doi:10.1609/icaps.v35i1.36101

Christoph Jabs, Jeremias Berg, Matti Järvisalo, "Engineering and Evaluating Multi-objective Pseudo-Boolean Optimizers", Proceedings of the 19th European Conference on Logics in Artificial Intelligence (JELIA '25), pp. 115–134, September, 2025. doi:10.1007/978-3-032-04587-4_8

Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, Marc Vinyals, "Practically Feasible Proof Logging for Pseudo-Boolean Optimization", Proceedings of the 31st International Conference on Principles and Practice of Constraint Programming (CP '25), vol. 340, pp. 21:1–21:27, August, 2025. doi:10.4230/LIPIcs.CP.2025.21

Carlos Ansótegui, Vaidyanathan Peruvemba Ramaswamy, Stefan Szeider, Hai Xia, "Uncovering and Verifying Optimal Community Structure in Complex Networks: A MaxSAT Approach", Proceedings of the 25th International Conference on Computational Science (ICCS '25), vol. 15904, pp. 35–49, July, 2025. doi:10.1007/978-3-031-97629-2_3

Christoph Jabs, Jeremias Berg, Bart Bogaerts, Matti Järvisalo, "Certifying Pareto-Optimality in Multi Objective Maximum Satisfiability", Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '25), vol. 15697, pp. 108–129, May, 2025. doi:10.1007/978-3-031-90653-4_6

Matthew McIlree, Ciaran McCreesh, "Certifying Bounds Propagation for Integer Multiplication Constraints", Proceedings of the 39th AAAI Conference on Artificial Intelligence (AAAI '25), pp. 11309–11317, February-March, 2025. doi:10.1609/aaai.v39i11.33230

Karthik V. Nukala, Soumyaditya Choudhuri, Randal E. Bryant, Marijn J. H. Heule, "Translating Pseudo-Boolean Proofs into Boolean Clausal Proofs", Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design (FMCAD '24), pp. 175–185, October, 2024. doi:10.34727/2024/isbn.978-3-85448-065-5_23

Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Tobias Paxian, Dieter Vandesande, "Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability", Proceedings of the 30th International Conference on Principles and Practice of Constraint Programming (CP '24), vol. 307, pp. 4:1–4:28, September, 2024. doi:10.4230/LIPIcs.CP.2024.4

Emir Demirović, Ciaran McCreesh, Matthew McIlree, Jakob Nordström, Andy Oertel, Konstantin Sidorov, "Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms", Proceedings of the 30th International Conference on Principles and Practice of Constraint Programming (CP '24), vol. 307, pp. 9:1–9:21, September, 2024. doi:10.4230/LIPIcs.CP.2024.9

Maarten Flippo, Konstantin Sidorov, Imko Marijnissen, Jeff Smits, Emir Demirović, "A Multi-Stage Proof Logging Framework to Certify the Correctness of CP Solvers", Proceedings of the 30th International Conference on Principles and Practice of Constraint Programming (CP '24), vol. 307, pp. 11:1–11:20, September, 2024. doi:10.4230/LIPIcs.CP.2024.11

Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, Florian Pollitt, "CaDiCaL 2.0", Proceedings of the 36th International Conference on Computer Aided Verification (CAV '24), vol. 14681, pp. 133–152, July, 2024. doi:10.1007/978-3-031-65627-9_7

Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen, Jakob Nordström, "Certified MaxSAT Preprocessing", Proceedings of the 12th International Joint Conference on Automated Reasoning (IJCAR '24), vol. 14739, pp. 396–418, July, 2024. doi:10.1007/978-3-031-63498-7_24

Alexander Hoen, Andy Oertel, Ambros Gleixner, Jakob Nordström, "Certifying MIP-based Presolve Reductions for 0-1 Integer Linear Programs", Proceedings of the 21st International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR '24), vol. 14742, pp. 310–328, May, 2024. doi:10.1007/978-3-031-60597-0_20

Matthew McIlree, Ciaran McCreesh, Jakob Nordström, "Proof Logging for the Circuit Constraint", Proceedings of the 21st International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR '24), vol. 14743, pp. 38–55, May, 2024. doi:10.1007/978-3-031-60599-4_3

Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, "End-to-End Verification for Subgraph Solving", Proceedings of the 38th AAAI Conference on Artificial Intelligence (AAAI '24), pp. 8038–8047, February, 2024. doi:10.1609/AAAI.V38I8.28642

Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, Jakob Nordström, "Certified Dominance and Symmetry Breaking for Combinatorial Optimisation", Journal of Artificial Intelligence Research, vol. 77, pp. 1539–1589, August, 2023. doi:10.1613/jair.1.14296

Matthew McIlree, Ciaran McCreesh, "Proof Logging for Smart Extensional Constraints", Proceedings of the 29th International Conference on Principles and Practice of Constraint Programming (CP '23), vol. 280, pp. 26:1–26:17, August, 2023. doi:10.4230/LIPIcs.CP.2023.26

Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Dieter Vandesande, "Certified Core-Guided MaxSAT Solving", Proceedings of the 29th International Conference on Automated Deduction (CADE-29), vol. 14132, pp. 1–22, July, 2023. doi:10.1007/978-3-031-38499-8_1

Dieter Vandesande, Wolf De Wulf, Bart Bogaerts, "QMaxSATpb: A Certified MaxSAT Solver", Proceedings of the 16th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR '22), vol. 13416, pp. 429–442, September, 2022. doi:10.1007/978-3-031-15707-3_33

Stephan Gocht, Ciaran McCreesh, Jakob Nordström, "An Auditable Constraint Programming Solver", Proceedings of the 28th International Conference on Principles and Practice of Constraint Programming (CP '22), vol. 235, pp. 25:1–25:18, August, 2022. doi:10.4230/LIPIcs.CP.2022.25

Stephan Gocht, Ruben Martins, Jakob Nordström, Andy Oertel, "Certified CNF Translations for Pseudo-Boolean Solving", Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing (SAT '22), vol. 236, pp. 16:1–16:25, August, 2022. doi:10.4230/LIPIcs.SAT.2022.16

Stephan Gocht, "Certifying Correctness for Combinatorial Algorithms by Using Pseudo-Boolean Reasoning", PhD thesis, Lund University, June, 2022. URL: https://portal.research.lu.se/en/publications/certifying-correctness-for-combinatorial-algorithms-by-using-pseu

Stephan Gocht, Jakob Nordström, "Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs", Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI '21), pp. 3768–3777, February, 2021. doi:10.1609/aaai.v35i5.16494

Stephan Gocht, Ross McBride, Ciaran McCreesh, Jakob Nordström, Patrick Prosser, James Trimble, "Certifying Solvers for Clique and Maximum Common (Connected) Subgraph Problems", Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP '20), vol. 12333, pp. 338–357, September, 2020. doi:10.1007/978-3-030-58475-7_20

Stephan Gocht, Ciaran McCreesh, Jakob Nordström, "VeriPB: The Easy Way to Make Your Combinatorial Search Algorithm Trustworthy", September, 2020. URL: https://jakobnordstrom.se/docs/publications/VeriPB_CPTAI2020.pdf

Stephan Gocht, Ciaran McCreesh, Jakob Nordström, "Subgraph Isomorphism Meets Cutting Planes: Solving With Certified Solutions", Proceedings of the 29th International Joint Conference on Artificial Intelligence (IJCAI '20), pp. 1134–1140, July, 2020. doi:10.24963/ijcai.2020/158

Jan Elffers, Stephan Gocht, Ciaran McCreesh, Jakob Nordström, "Justifying All Differences Using Pseudo-Boolean Reasoning", Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI '20), February, 2020. doi:10.1609/aaai.v34i02.5507