Publications

• Trimming Pseudo-Boolean Proofs

  Berhan Oumer Adame, Bart Bogaerts, Benjamin Bogø, Simon Dold, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Matthew McIlree, Jakob Nordström, Andy Oertel, Adrian Rebola-Pardo, and Mark Turnbull

  Formal Methods in Computer-Aided Design 2026 (FMCAD 2026), 2026

  To appear

  PDF Artefact

• End-to-End Certified Graph Colouring

  Simon Dold, George Katsirelos, Wietze Koops, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan

  32nd International Conference on Principles and Practice of Constraint Programming (CP 2026), 2026

  PDF Experimental Data Code (CertifyingZykovColor) Code (VeriPB) Code (CakePB)

• Proof Logging for Projected Enumeration (and Counting?) Problems in VeriPB

  Ciaran McCreesh, Jakob Nordström, Andy Oertel, Yong Kiam Tan

  32nd International Conference on Principles and Practice of Constraint Programming (CP 2026), 2026

  PDF Slides Code (Glasgow Constraint Solver) Code (VeriPB) Code (CakePB)

• Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables

  Markus Anders, Bart Bogaerts, Benjamin Bogø, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Adrian Rebola-Pardo, Yong Kiam Tan

  40th Annual AAAI Conference on Artificial Intelligence (AAAI-26), 2026

  PDF (extended version) Code (satsuma) Code (VeriPB) Code (CakePB)

• Practically Feasible Proof Logging for Pseudo-Boolean Optimization

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

  31st International Conference on Principles and Practice of Constraint Programming (CP 2025), 2025

  PDF Experimental Data

• Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms

  Emir Demirović, Ciaran McCreesh, Matthew J. McIlree, Jakob Nordström, Andy Oertel, Konstantin Sidorov

  30th International Conference on Principles and Practice of Constraint Programming (CP 2024), 2024

  PDF Software

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

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

  30th International Conference on Principles and Practice of Constraint Programming (CP 2024), 2024

  PDF Experimental data

• Certified MaxSAT Preprocessing

  Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen, Jakob Nordström

  International Joint Conference on Automated Reasoning (IJCAR 2024), 2024

  PDF (extended version) Code Experimental data

• Certifying MIP-based Presolve Reductions for 0-1 Integer Linear Programs

  Alexander Hoen, Andy Oertel, Ambros Gleixner, Jakob Nordström

  21st International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR 2024), 2024

  PDF Code Slides WHOOPS'24

• End-to-End Verification for Subgraph Solving

  Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan

  38th Annual AAAI Conference on Artificial Intelligence (AAAI-24), 2024

  Best Poster Award at WASP Winter Conference 2025

  PDF Poster CakePB (verified checker)

• Graphs with many edge-colorings such that complete graphs are rainbow

  Josefran de Oliveira Bastos, Hanno Lefmann, Andy Oertel, Carlos Hoppen, Dionatan Ricardo Schmidt

  Discrete Applied Mathematics, 2023

  Journal version of "Maximum number of \( r \)-edge-colorings such that all copies of \( K_k \) are rainbow"

  Paper

• Certified Core-Guided MaxSAT Solving

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

  29th International Conference on Automated Deduction (CADE-29), 2023

  PDF Code Slides SAT: Extended Reunion Slides NordConsNet 2023 Slides CADE-29

• Certified CNF Translations for Pseudo-Boolean Solving

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

  25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022), 2022

  Best Paper Award at SAT 2022

  PDF PDF IJCAI Code Data Slides SAT+SMT 2022 slides SAT+SMT 2022 video

• Fast ultrametric matrix-vector multiplication

  Tobias Hofmann, Andy Oertel

  Preprint

  PDF Code

• Maximum number of \( r \)-edge-colorings such that all copies of \( K_k \) are rainbow

  Josefran de Oliveira Bastos, Hanno Lefmann, Andy Oertel, Carlos Hoppen, Dionatan Ricardo Schmidt

  LAGOS (Procedia Computer Science), 2021

  PDF