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:

        @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}},
        }
        

        @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}
        }
        

        @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.

• Jan Elffers, Stephan Gocht, Ciaran McCreesh, Jakob Nordström, "Justifying All Differences Using Pseudo-Boolean Reasoning", Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34, pp. 1486–1494, April, 2020.


• Stephan Gocht, Ross McBride, Ciaran McCreesh, Jakob Nordström, Patrick Prosser, James Trimble, "Certifying Solvers for Clique and Maximum Common (Connected) Subgraph Problems", Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7-11, 2020, Proceedings, vol. 12333, pp. 338–357, September, 2020.


• Stephan Gocht, Ciaran McCreesh, Jakob Nordström, "Subgraph Isomorphism Meets Cutting Planes: Solving With Certified Solutions", Electronic Proceedings of IJCAI 2020, vol. 2, pp. 1134–1140, July, 2020.


• Stephan Gocht, Ciaran McCreesh, Jakob Nordström, "VeriPB: The Easy Way to Make Your Combinatorial Search Algorithm Trustworthy", From Constraint Programming to Trustworthy AI, vol. 2, pp. 4, 2020.


• Stephan Gocht, Jakob Nordström, "Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs", Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021, pp. 3768–3777, 2021.


• Stephan Gocht, "Certifying Correctness for Combinatorial Algorithms: By Using Pseudo-Boolean Reasoning", PhD thesis, Lund University, Sweden, 2022.


• Stephan Gocht, Ciaran McCreesh, Jakob Nordström, "An Auditable Constraint Programming Solver", Proceeding of the 28th International Conference on Principles and Practice of Constraint Programming, vol. 235, pp. 25:1–25:18, 2022.


• Stephan Gocht, Ruben Martins, Jakob Nordström, Andy Oertel, "Certified CNF Translations for Pseudo-Boolean Solving", 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022), vol. 236, pp. 16:1–16:25, 2022.


• Dieter Vandesande, De Wulf, Wolf, Bart Bogaerts, "QMaxSATpb: A Certified MaxSAT Solver", Logic Programming and Nonmonotonic Reasoning, pp. 429–442, 2022.


• 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.


• Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Dieter Vandesande, "Certified Core-Guided MaxSAT Solving", Automated Deduction -- CADE 29, pp. 1–22, 2023.


• Matthew J. McIlree, Ciaran McCreesh, "Proof Logging for Smart Extensional Constraints", 29th International Conference on Principles and Practice of Constraint Programming (CP 2023), vol. 280, pp. 26:1–26:17, 2023.


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


• Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, Florian Pollitt, "CaDiCaL 2.0", Computer Aided Verification, pp. 133–152, 2024.


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


• Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, "End-to-End Verification for Subgraph Solving", Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI 2024, Fourteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2014, February 20-27, 2024, Vancouver, Canada, pp. 8038–8047, 2024.


• Alexander Hoen, Andy Oertel, Ambros Gleixner, Jakob Nordström, "Certifying MIP-Based Presolve Reductions for 0 -- 1 Integer Linear Programs", Integration of Constraint Programming, Artificial Intelligence, and Operations Research, pp. 310–328, 2024.


• Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen, Jakob Nordström, "Certified MaxSAT Preprocessing", Automated Reasoning, pp. 396–418, 2024.


• Matthew J. McIlree, Ciaran McCreesh, Jakob Nordström, "Proof Logging for the Circuit Constraint", Integration of Constraint Programming, Artificial Intelligence, and Operations Research, pp. 38–55, 2024.


• Karthik V. Nukala, Soumyaditya Choudhuri, Randal E. Bryant, Marijn J.H. Heule, "Translating Pseudo-Boolean Proofs into Boolean Clausal Proofs", 2024 Formal Methods in Computer-Aided Design (FMCAD), pp. 175–185, October, 2024.


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


• Carlos Ansótegui, Vaidyanathan Peruvemba Ramaswamy, Stefan Szeider, Hai Xia, "Uncovering and Verifying Optimal Community Structure in Complex Networks: A MaxSAT Approach", Computational Science -- ICCS 2025, pp. 35–49, 2025.


• Simon Dold, Malte Helmert, Jakob Nordström, Gabriele Röger, Tanja Schindler, "Pseudo-Boolean Proof Logging for Optimal Classical Planning", International Conference on Automated Planning and Scheduling, vol. 35, pp. 54–63, 2025.


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


• Matthew J. McIlree, Ciaran McCreesh, "Certifying Bounds Propagation for Integer Multiplication Constraints", Proceedings of the AAAI Conference on Artificial Intelligence, vol. 39, pp. 11309–11317, 2025.


• Christoph Jabs, Jeremias Berg, Matti Järvisalo, "Engineering and Evaluating Multi-objective Pseudo-Boolean Optimizers", Logics in Artificial Intelligence, pp. 115–134, 2026.


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