Document Open Access Logo

From Literals to Atomic Constraints: Generalising Conflict-Driven Clause Learning for Constraint Programming

Authors Imko Marijnissen , Maarten Flippo , Emir Demirović

PDF

File

Thumbnail PDF
PDF
LIPIcs.CP.2026.42.pdf
  • Filesize: 1.04 MB
  • 21 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
Keywords
  • LCG
  • CP
  • CDCL
  • Lazy Literal
  • Conflict Analysis
  • Nogood Propagation

Metrics

Abstract

Conflict‑Driven Clause Learning (CDCL) is central to the success of SAT solvers, and its adaptation to Constraint Programming (CP) through Lazy Clause Generation (LCG) has been a major breakthrough for CP solving. A core requirement of LCG is to maintain both a CP and SAT view of the problem. Because maintaining a full SAT encoding is impractical, solvers rely on partial and solver‑specific encodings - an approach that has evolved as folklore rather than formal design. We present the first systematic analysis of how leading LCG solvers maintain their SAT encodings, based on source‑code inspection and developer correspondence. Our analysis reveals substantial differences in explanation lifting, backwards explanations, linking clauses, and nogood minimisation, all driven by the need to preserve a SAT view. To overcome these compromises, we propose a native CDCL framework for CP. We replace SAT literals with atomic constraints, enabling conflict analysis, nogood learning, and nogood propagation directly at the CP level. This results in cleaner algorithmic design, eliminates SAT‑specific complications, and allows us to introduce extended nogood propagation, a generalisation of SAT‑based clause propagation, as well as CPIP nogoods, a generalisation of SAT-based learned nogoods. Our implementation of the framework in Pumpkin demonstrates competitive performance in the MiniZinc Challenge 2025. Additionally, we empirically show that extended nogood propagation combined with CPIP nogoods can significantly reduce failures, especially on problems with constraints that reason over domain holes. Overall, our framework provides a principled and semantically rich generalisation of CDCL for CP.

Cite As Get BibTex

Imko Marijnissen, Maarten Flippo, and Emir Demirović. From Literals to Atomic Constraints: Generalising Conflict-Driven Clause Learning for Constraint Programming. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 42:1-42:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CP.2026.42

Author Details

Imko Marijnissen
  • Delft University of Technology, Netherlands
Maarten Flippo
  • Delft University of Technology, Netherlands
Emir Demirović
  • Delft University of Technology, Netherlands

Funding

  • Marijnissen, Imko: Supported by the NWO/OCW, as part of the Quantum Software Consortium programme (project number 024.003.037 / 3368).
  • Flippo, Maarten: Supported by the project "Towards a Unification of AI-Based Solving Paradigms for Combinatorial Optimisation" (OCENW.M.21.078) of the research programme "Open Competition Domain Science - M" which is financed by the Dutch Research Council (NWO).

Acknowledgements

We would like to thank Peter Stuckey and Jip Dekker for their correspondence regarding Chuffed and Huub, Frédéric Didier for their correspondence regarding OR-Tools, Emmanuel Hebrard for their correspondence concerning Tempo, and Graeme Gange for their correspondence regarding Geas.

Supplementary Materials

References

  1. Gilles Audemard, Christophe Lecoutre, and Emmanuel Lonca. Proceedings of the 2024 XCSP3 competition. CoRR, abs/2412.00117, 2024. URL: https://doi.org/10.48550/arXiv.2412.00117.
  2. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In Craig Boutilier, editor, IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009, pages 399-404, 2009. URL: http://ijcai.org/Proceedings/09/Papers/074.pdf.
  3. Robbin Baauw, Maarten Flippo, and Emir Demirović. Conflict Analysis Based on Cutting-Planes for Constraint Programming. In Maria Garcia de la Banda, editor, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025), volume 340 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1-4:19, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CP.2025.4.
  4. Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. Symbolic model checking without bdds. In W. Rance Cleaveland, editor, Tools and Algorithms for the Construction and Analysis of Systems, pages 193-207, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-49059-0_14.
  5. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009. Google Scholar
  6. Geoffrey Chu, Peter J. Stuckey, Andreas Schutt, Thorsten Ehlers, Graeme Gange, and Kathryn Francis. Chuffed: The chuffed cp solver. URL: https://github.com/chuffed/chuffed.
  7. Rina Dechter. Enhancement schemes for constraint processing: Backjumping, learning, and cutset decomposition. Artif. Intell., 41(3):273-312, 1990. URL: https://doi.org/10.1016/0004-3702(90)90046-3.
  8. Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey, and Allen Z. Zhong. Towards modern and modular SAT for LCG (short paper). In Maria Garcia de la Banda, editor, 31st International Conference on Principles and Practice of Constraint Programming, CP 2025, Glasgow, Scotland, August 10-15, 2025, volume 340 of LIPIcs, pages 42:1-42:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CP.2025.42.
  9. Delft High Performance Computing Centre (DHPC). DelftBlue Supercomputer (Phase 2). https://www.tudelft.nl/dhpc/ark:/44463/DelftBluePhase2, 2024.
  10. Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. IPASIR-UP: user propagators for CDCL. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, Alghero, Italy, July 4-8, 2023, volume 271 of LIPIcs, pages 8:1-8:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.8.
  11. Nick Feng and Fahiem Bacchus. Clause size reduction with all-uip learning. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 28-45. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_3.
  12. Thibaut Feydy, Andreas Schutt, and Peter J. Stuckey. Semantic learning for lazy clause generation. In TRICS workshop, held alongside Principles and Practice of Constraint Programming. Citeseer, 2013. Google Scholar
  13. Thibaut Feydy and Peter J. Stuckey. Lazy clause generation reengineered. In Ian P. Gent, editor, Principles and Practice of Constraint Programming - CP 2009, 15th International Conference, CP 2009, Lisbon, Portugal, September 20-24, 2009, Proceedings, volume 5732 of Lecture Notes in Computer Science, pages 352-366. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04244-7_29.
  14. Mathias Fleury and Armin Biere. Efficient all-uip learned clause minimization. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, volume 12831 of Lecture Notes in Computer Science, pages 171-187. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_12.
  15. Maarten Flippo, Konstantin Sidorov, Imko Marijnissen, Jeff Smits, and Emir Demirović. A Multi-Stage Proof Logging Framework to Certify the Correctness of CP Solvers. In Paul Shaw, editor, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024), volume 307 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1-11:20, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CP.2024.11.
  16. Graeme Gange, Jeremias Berg, Emir Demirović, and Peter J. Stuckey. Core-guided and core-boosted search for CP. In Emmanuel Hebrard and Nysret Musliu, editors, Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 17th International Conference, CPAIOR 2020, Vienna, Austria, September 21-24, 2020, Proceedings, volume 12296 of Lecture Notes in Computer Science, pages 205-221. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58942-4_14.
  17. Ian P. Gent, Chris Jefferson, and Ian Miguel. Watched literals for constraint propagation in minion. In Frédéric Benhamou, editor, Principles and Practice of Constraint Programming - CP 2006, pages 182-197, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  18. Gael Glorian, Jean-Marie Lagniez, and Christophe Lecoutre. Nacre - a nogood and clause reasoning engine. In Elvira Albert and Laura Kovacs, editors, LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 73 of EPiC Series in Computing, pages 249-259. EasyChair, 2020. URL: https://doi.org/10.29007/dxnb.
  19. Emmanuel Hebrard. Disjunctive scheduling in tempo. In Maria Garcia de la Banda, editor, 31st International Conference on Principles and Practice of Constraint Programming, CP 2025, Glasgow, Scotland, August 10-15, 2025, volume 340 of LIPIcs, pages 13:1-13:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CP.2025.13.
  20. Pascal Van Hentenryck and Jean-Philippe Carillon. Generality versus specificity: an experience with ai and or techniques. In Proceedings of the Seventh AAAI National Conference on Artificial Intelligence, AAAI'88, pages 660-664. AAAI Press, 1988. URL: http://www.aaai.org/Library/AAAI/1988/aaai88-117.php.
  21. Siddhartha Jain, Eoin O'Mahony, and Meinolf Sellmann. A complete multi-valued SAT solver. In David Cohen, editor, Principles and Practice of Constraint Programming - CP 2010 - 16th International Conference, CP 2010, St. Andrews, Scotland, UK, September 6-10, 2010. Proceedings, volume 6308 of Lecture Notes in Computer Science, pages 281-296. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15396-9_24.
  22. George Katsirelos and Fahiem Bacchus. Generalized nogoods in csps. In Manuela M. Veloso and Subbarao Kambhampati, editors, Proceedings, The Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference, July 9-13, 2005, Pittsburgh, Pennsylvania, USA, pages 390-396. AAAI Press / The MIT Press, 2005. URL: http://www.aaai.org/Library/AAAI/2005/aaai05-062.php.
  23. Mikael Z. Lagerkvist and Christian Schulte. Advisors for incremental propagation. In Christian Bessière, editor, Principles and Practice of Constraint Programming - CP 2007, pages 409-422, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-74970-7_30.
  24. Jean-Louis Laurière. A language and a program for stating and solving combinatorial problems. Artif. Intell., 10(1):29-127, 1978. URL: https://doi.org/10.1016/0004-3702(78)90029-2.
  25. Inês Lynce and João Marques-Silva. Sat in bioinformatics: Making the case with haplotype inference. In Armin Biere and Carla P. Gomes, editors, Theory and Applications of Satisfiability Testing - SAT 2006, pages 136-141, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11814948_16.
  26. João Marques-Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 133-182. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200987.
  27. Kimbal Marriott and Peter Stuckey. Programming with Constraints: An Introduction. The MIT Press, February 1998. URL: https://doi.org/10.7551/mitpress/5625.001.0001.
  28. Fabio Massacci and Laura Marraro. Logical cryptanalysis as a sat problem. Journal of Automated Reasoning, 24(1):165-203, February 2000. URL: https://doi.org/10.1023/A:1006326723002.
  29. Mzn-Challenge: An archive repository containing the minizinc instances used for the minizinc challenge. URL: https://github.com/MiniZinc/mzn-challenge.
  30. Neil CA Moore. C-learning: Further generalised g-nogood learning. In ERCIM Workshop on Constraint Solving and Constraint Logic Programming, 2011, page 103, 2011. Google Scholar
  31. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001, pages 530-535. ACM, 2001. URL: https://doi.org/10.1145/378239.379017.
  32. Olga Ohrimenko, Peter J. Stuckey, and Michael Codish. Propagation via lazy clause generation. Constraints An Int. J., 14(3):357-391, 2009. URL: https://doi.org/10.1007/S10601-008-9064-X.
  33. Laurent Perron and Frédéric Didier. Cp-sat [online]. URL: https://developers.google.com/optimization/cp/cp_solver/.
  34. Charles Prud'homme and Jean-Guillaume Fages. Choco-solver: A java library for constraint programming. Journal of Open Source Software, 7(78):4708, 2022. URL: https://doi.org/10.21105/joss.04708.
  35. J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23-41, January 1965. URL: https://doi.org/10.1145/321250.321253.
  36. Francesca Rossi, Peter van Beek, and Toby Walsh, editors. Handbook of Constraint Programming, volume 2 of Foundations of Artificial Intelligence. Elsevier, 2006. URL: https://www.sciencedirect.com/science/bookseries/15746526/2.
  37. Thomas Schiex and Gérard Verfaillie. Nogood recording for static and dynamic constraint satisfaction problems. Int. J. Artif. Intell. Tools, 3(2):187-208, 1994. URL: https://doi.org/10.1142/S0218213094000108.
  38. Christian Schulte. Comparing trailing and copying for constraint programming. In Danny De Schreye, editor, Logic Programming: The 1999 International Conference, Las Cruces, New Mexico, USA, November 29 - December 4, 1999, pages 275-289. MIT Press, 1999. Google Scholar
  39. Andreas Schutt, Thibaut Feydy, Peter J. Stuckey, and Mark G. Wallace. Explaining the cumulative propagator. Constraints, 16(3):250-282, July 2011. URL: https://doi.org/10.1007/s10601-010-9103-2.
  40. Mohamed Siala, Christian Artigues, and Emmanuel Hebrard. Two clause learning approaches for disjunctive scheduling. In Gilles Pesant, editor, Principles and Practice of Constraint Programming - 21st International Conference, CP 2015, Cork, Ireland, August 31 - September 4, 2015, Proceedings, volume 9255 of Lecture Notes in Computer Science, pages 393-402. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23219-5_28.
  41. João P. Marques Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers, 48(5):506-521, 1999. URL: https://doi.org/10.1109/12.769433.
  42. Niklas Sörensson and Armin Biere. Minimizing learned clauses. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, volume 5584 of Lecture Notes in Computer Science, pages 237-243. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_23.
  43. Peter J. Stuckey, Ralph Becket, and Julien Fischer. Philosophy of the minizinc challenge. Constraints An Int. J., 15(3):307-316, 2010. URL: https://doi.org/10.1007/S10601-010-9093-0.
  44. Peter J. Stuckey, Thibaut Feydy, Andreas Schutt, Guido Tack, and Julien Fischer. The minizinc challenge 2008-2013. AI Mag., 35(2):55-60, 2014. URL: https://doi.org/10.1609/AIMAG.V35I2.2539.
  45. Michael Veksler and Ofer Strichman. A proof-producing CSP solver. In Maria Fox and David Poole, editors, Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2010, Atlanta, Georgia, USA, July 11-15, 2010, pages 204-209. AAAI Press, 2010. URL: https://doi.org/10.1609/AAAI.V24I1.7543.
  46. Michael Veksler and Ofer Strichman. Learning general constraints in CSP. Artif. Intell., 238:135-153, 2016. URL: https://doi.org/10.1016/J.ARTINT.2016.06.002.
  47. Lintao Zhang, Conor F. Madigan, Matthew W. Moskewicz, and Sharad Malik. Efficient conflict driven learning in boolean satisfiability solver. In Rolf Ernst, editor, Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2001, San Jose, CA, USA, November 4-8, 2001, pages 279-285. IEEE Computer Society, 2001. URL: https://doi.org/10.1109/ICCAD.2001.968634.
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