Document Open Access Logo

End-to-End Certified Graph Colouring

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.CP.2026.21.pdf
  • Filesize: 1.32 MB
  • 27 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Graph coloring
  • Theory of computation → Logic and verification
Keywords
  • graph colouring
  • proof logging
  • certifying algorithms

Metrics

Abstract

Applied combinatorial optimization has witnessed a revolution in performance since the turn of the millennium, but the complexity of modern solvers is making bugs an ever more serious concern. The most promising remedy is to make solvers certifying, so that they use proof logging to generate machine-verifiable proofs of correctness. We present the first example of state-of-the-art certified graph colouring by equipping the solver ZykovColor with VeriPB proof logging. Combined with the formally verified CakePB checker, this provides end-to-end formally certified results. An experimental evaluation shows excellent results with only moderate overhead for proof logging and checking.

Cite As Get BibTex

Simon Dold, George Katsirelos, Wietze Koops, Magnus O. Myreen, Jakob Nordström, Andy Oertel, and Yong Kiam Tan. End-to-End Certified Graph Colouring. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 21:1-21:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CP.2026.21

Author Details

Simon Dold
  • University of Basel, Switzerland
George Katsirelos
  • MIA Paris, INRAE, Université Paris-Saclay, France
  • Université de Toulouse, ANITI, France
Wietze Koops
  • Lund University, Sweden
  • University of Copenhagen, Denmark
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
  • Nanyang Technological University, Singapore
  • Institute for Infocomm Research (I²R), A*STAR, Singapore

Funding

  • Dold, Simon: Swiss National Science Foundation (SNSF), project "Unifying the Theory and Algorithms of Factored State-Space Search" (UTA).
  • Katsirelos, George: Funded by the AI Interdisciplinary Institute ANITI. ANITI is funded by the French "Investing for the Future – PIA3" program under the Grant agreement n°ANR-23-IACL-0002.
  • Koops, Wietze: Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.
  • Myreen, Magnus O.: Swedish Research Council grant 2021-05165.
  • Nordström, Jakob: Swedish Research Council grant 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.

Acknowledgements

We would like to thank the anonymous reviewers of CP for their useful comments. We are grateful to Benjamin Bogø, Ciaran McCreesh, and Shuo Pang for helpful discussions. Also, we are thankful for stimulating conversations with and useful feedback from participants of the Dagstuhl Seminar 25231 Certifying Algorithms for Automated Reasoning and the 2nd International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS '25) at Institut Pascal in Paris. The third, fifth, and sixth authors wish to acknowledge that they have benefited greatly from being part of the Basic Algorithms Research Copenhagen (BARC) environment financed by the Villum Investigator grant 54451. Our computational experiments used 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. Markus Anders, Bart Bogaerts, Benjamin Bogø, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Adrián Rebola-Pardo, and Yong Kiam Tan. Faster certified symmetry breaking using orders with auxiliary variables. In Proceedings of the 40th AAAI Conference on Artificial Intelligence (AAAI '26), pages 14140-14148, January 2026. URL: https://doi.org/10.1609/AAAI.V40I17.38426.
  3. Paul Beame, Joseph C. Culberson, David G. Mitchell, and Cristopher Moore. The resolution complexity of random graph k-colorability. Discrete Applied Mathematics, 153(1-3):25-47, December 2005. URL: https://doi.org/10.1016/J.DAM.2005.05.004.
  4. Richard Beigel and David Eppstein. 3-coloring in time O(1.3289ⁿ). Journal of Algorithms, 54(2):168-204, February 2005. Google Scholar
  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. Armin Biere. Tracecheck. http://fmv.jku.at/tracecheck/, 2006.
  8. 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.
  9. Maria Luisa Bonet, Jordi Levy, and Felip Manyà. Resolution for Max-SAT. Artificial Intelligence, 171(8-9):606-618, June 2007. Extended version of paper in SAT '06. URL: https://doi.org/10.1016/J.ARTINT.2007.03.001.
  10. Timo Brand, Daniel Faber, Stephan Held, and Petra Mutzel. A customized SAT-based solver for graph coloring, October 2025. Repository with experimental data. URL: https://doi.org/10.5281/zenodo.17328845.
  11. Timo Brand, Daniel Faber, Stephan Held, and Petra Mutzel. A customized SAT-based solver for graph coloring. In 2026 Proceedings of the SIAM Symposium on Algorithm Engineering and Experiments (ALENEX), pages 142-155. SIAM, 2026. URL: https://doi.org/10.1137/1.9781611978957.11.
  12. Daniel Brélaz. New methods to color the vertices of a graph. Communications of the ACM, 22(4):251-256, April 1979. URL: https://doi.org/10.1145/359094.359101.
  13. 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
  14. Robert Brummayer, Florian Lonsing, and Armin Biere. Automated testing and debugging of SAT and QBF solvers. In Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT '10), volume 6175 of Lecture Notes in Computer Science, pages 44-57. Springer, July 2010. URL: https://doi.org/10.1007/978-3-642-14186-7_6.
  15. 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.
  16. Gregory J. Chaitin. Register allocation & spilling via graph coloring. SIGPLAN Not., 17(6):98-101, June 1982. Google Scholar
  17. 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.
  18. Jonas Conneryd, Susanna F. de Rezende, Jakob Nordström, Shuo Pang, and Kilian Risse. Graph colouring is hard on average for polynomial calculus and Nullstellensatz. In Proceedings of the 64th Annual IEEE Symposium on Foundations of Computer Science (FOCS '23), pages 1-11, November 2023. URL: https://doi.org/10.1109/FOCS57990.2023.00007.
  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. 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.
  21. 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.
  22. 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.
  23. 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), pages 54-63, November 2025. Google Scholar
  24. 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.
  25. 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.
  26. 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.
  27. 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.
  28. 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.
  29. Daniel Faber, Adalat Jabrayilov, and Petra Mutzel. SAT Encoding of Partial Ordering Models for Graph Coloring Problems. 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 12:1-12:20, August 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.12.
  30. Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. IPASIR-UP: User Propagators for CDCL. 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 8:1-8:13, July 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.8.
  31. Mathias Fleury. Formalization of Logical Calculi in Isabelle/HOL. PhD thesis, Universität des Saarlandes, 2020. Available at URL: https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/28722.
  32. Fabio Furini, Virginie Gabrel, and Ian-Christopher Ternier. An improved DSATUR-based branch-and-bound algorithm for the vertex coloring problem. Networks, 69(1):124-141, 2017. URL: https://doi.org/10.1002/NET.21716.
  33. Graeme Gange, Geoffrey Chu, and Peter J. Stuckey. Certifying optimality in constraint programming. Manuscript. Available at https://people.eng.unimelb.edu.au/pstuckey/papers/certified-cp.pdf, 2023.
  34. Assefaw Hadish Gebremedhin, Fredrik Manne, and Alex Pothen. What color is your Jacobian? graph coloring for computing derivatives. SIAM Review, 47(4):629-705, 2005. URL: https://doi.org/10.1137/S0036144504444711.
  35. 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.
  36. Stephan Gocht, Ruben Martins, Jakob Nordström, and Andy Oertel. Certified CNF translations for pseudo-Boolean solving. 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 16:1-16:25, August 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.16.
  37. 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.
  38. 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.
  39. 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.
  40. 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.
  41. 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.
  42. 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
  43. Justin S. Gray, Tristan A. Hearn, and Bret A. Naylor. Using graph coloring to compute total derivatives more efficiently in OpenMDAO. In AIAA Aviation 2019 Forum, pages 3108:1-3108:15, June 2019. Google Scholar
  44. Stefano Gualandi and Federico Malucelli. Exact solution of graph coloring problems via constraint programming and column generation. INFORMS Journal on Computing, 24(1):81-100, 2012. URL: https://doi.org/10.1287/IJOC.1100.0436.
  45. Emmanuel Hebrard and George Katsirelos. Constraint and satisfiability reasoning for graph coloring. Journal of Artificial Intelligence Research, 69:33-65, 2020. URL: https://doi.org/10.1613/JAIR.1.11313.
  46. Stephan Held, William Cook, and Edward C. Sewell. Maximum-weight stable sets and safe lower bounds for graph coloring. Mathematical Programming Computation, 4(4):363-381, 2012. URL: https://doi.org/10.1007/S12532-012-0042-3.
  47. Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, and Armin Biere. PRuning through satisfaction. In 13th International Haifa Verification Conference (HVC '17), volume 10629 of Lecture Notes in Computer Science, pages 179-194. Springer, November 2017. URL: https://doi.org/10.1007/978-3-319-70389-3_12.
  48. 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.
  49. Adalat Jabrayilov and Petra Mutzel. New integer linear programming models for the vertex coloring problem. In Michael A. Bender, Martín Farach-Colton, and Miguel A. Mosteiro, editors, LATIN 2018: Theoretical Informatics, pages 640-652. Springer International Publishing, 2018. URL: https://doi.org/10.1007/978-3-319-77404-6_47.
  50. David S. Johnson and Michael A. Trick. Introduction to the second DIMACS challenge: Cliques, coloring, and satisfiability. In Cliques, Coloring and Satisfiability: Second DIMACS Implementation Challenge, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 1-10. American Mathematical Society, 1996. Google Scholar
  51. Richard M. Karp. Reducibility among combinatorial problems. In Complexity of Computer Computations, The IBM Research Symposia Series, pages 85-103. Springer, 1972. URL: https://doi.org/10.1007/978-1-4684-2001-2_9.
  52. Daniela Kaufmann and Armin Biere. Fuzzing and delta debugging and-inverter graph verification tools. In Proceedings of the 16th International Conference on Tests and Proofs (TAP '22), volume 13361 of Lecture Notes in Computer Science, pages 69-88. Springer, July 2022. URL: https://doi.org/10.1007/978-3-031-09827-7_5.
  53. 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 Proceedings of the 31st International Conference on Principles and Practice of Constraint Programming (CP '25), volume 340 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:27, August 2025. URL: https://doi.org/10.4230/LIPIcs.CP.2025.21.
  54. 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.
  55. 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.
  56. Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. A framework for certified Boolean branch-and-bound optimization. Journal of Automated Reasoning, 46(1):81-102, January 2011. URL: https://doi.org/10.1007/S10817-010-9176-Z.
  57. Vahid Lotfi and Sanjiv Sarin. A graph coloring algorithm for large scale scheduling problems. Computers & Operations Research, 13(1):27-32, 1986. URL: https://doi.org/10.1016/0305-0548(86)90061-4.
  58. Enrico Malaguti, Michele Monaci, and Paolo Toth. An exact approach for the vertex coloring problem. Discrete Optimization, 8(2):174-190, 2011. URL: https://doi.org/10.1016/J.DISOPT.2010.07.005.
  59. Ross M. McConnell, Kurt Mehlhorn, Stefan Näher, and Pascal Schweitzer. Certifying algorithms. Computer Science Review, 5(2):119-161, May 2011. URL: https://doi.org/10.1016/J.COSREV.2010.09.009.
  60. Ciaran McCreesh, William Pettersson, and Patrick Prosser. Understanding the empirical hardness of random optimisation problems. 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 333-349. Springer, September 2019. URL: https://doi.org/10.1007/978-3-030-30048-7_20.
  61. Colin McDiarmid. Colouring random graphs. Annals of Operations Research, 1(3):183-200, October 1984. URL: https://doi.org/10.1007/BF01874388.
  62. 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.
  63. 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.
  64. 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.
  65. Anuj Mehrotra and Michael A. Trick. A column generation approach for graph coloring. INFORMS Journal on Computing, 8(4):344-354, 1996. URL: https://doi.org/10.1287/ijoc.8.4.344.
  66. António Morgado and João P. Marques-Silva. On validating Boolean optimizers. In Proceedings of the 23rd IEEE International Conference on Tools with Artificial Intelligence (ICTAI '12), pages 924-926, November 2011. URL: https://doi.org/10.1109/ICTAI.2011.157.
  67. 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.
  68. Jan Mycielski. Sur le coloriage des graphs. Colloquium Mathematicae, 3(2):161-162, 1955. Google Scholar
  69. Aina Niemetz, Mathias Preiner, and Clark W. Barrett. Murxla: A modular and highly extensible API fuzzer for SMT solvers. In Proceedings of the 34th International Conference on Computer Aided Verification (CAV '22), volume 13372 of Lecture Notes in Computer Science, pages 92-106. Springer, August 2022. URL: https://doi.org/10.1007/978-3-031-13188-2_5.
  70. 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.
  71. Tobias Paxian and Armin Biere. MaxSAT fuzzing and delta debugging. Journal of Artificial Intelligence Research, 85, February 2026. URL: https://doi.org/10.1613/JAIR.1.19716.
  72. Aaron Potechin and Jeff Xu. Sum-of-squares lower bounds for coloring random graphs. In Proceedings of the 57th Annual ACM Symposium on Theory of Computing (STOC '25), pages 84-95, June 2025. URL: https://doi.org/10.1145/3717823.3718151.
  73. Matthieu Py, Mohamed Sami Cherif, and Djamal Habet. Towards bridging the gap between SAT and Max-SAT refutations. In Proceedings of the 32nd IEEE International Conference on Tools with Artificial Intelligence (ICTAI '20), pages 137-144, November 2020. URL: https://doi.org/10.1109/ICTAI50040.2020.00032.
  74. Matthieu Py, Mohamed Sami Cherif, and Djamal Habet. Proofs and certificates for Max-SAT. Journal of Artificial Intelligence Research, 75:1373-1400, December 2022. URL: https://doi.org/10.1613/JAIR.1.13811.
  75. Konrad Slind and Michael Norrish. A brief overview of HOL4. In Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs '08), volume 5170 of Lecture Notes in Computer Science, pages 28-32. Springer, August 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_6.
  76. 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.
  77. 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
  78. Cesare Tinelli. Scalable proof production and checking in SMT. 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 2:1-2:2, August 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.2.
  79. Raoul Van Doren, Timos Antonopoulos, and Ruzica Piskac. Efficient and verifiable proof logging for MaxSAT solving. In Proceedings of the 2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE '25), pages 1325-1337, November 2025. URL: https://doi.org/10.1109/ASE63991.2025.00113.
  80. 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.
  81. 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.
  82. Emre Yolcu, Xinyu Wu, and Marijn J. H. Heule. Mycielski graphs and PR proofs. In International Conference on Theory and Applications of Satisfiability Testing, pages 201-217. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_15.
  83. Lintao Zhang and Sharad Malik. Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In Proceedings of the Conference on Design, Automation and Test in Europe (DATE '03), pages 880-885, March 2003. Google Scholar
  84. David Zuckerman. Linear degree extractors and the inapproximability of max clique and chromatic number. Theory of Computing, 3(6):103-128, August 2007. Preliminary version in STOC '06. URL: https://doi.org/10.4086/TOC.2007.V003A006.
  85. Alexander Aleksandrovich Zykov. On some properties of linear complexes. Matematicheskii Sbornik, 66(2):163-188, 1949. Google Scholar
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact