Thesis Papers - Andy Oertel

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)

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)

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