Search Results

Documents authored by Flippo, Maarten

Document
DOI: 10.4230/LIPIcs.CP.2026.24
Formally Verified Certification of Constraint Programming Proofs

Authors: Maarten Flippo, Konstantin Sidorov, Tip ten Brink, Clément Pit-Claudel, and Emir Demirović

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

Abstract
As constraint programming (CP) solvers are increasingly used in critical applications, there is a growing need for certification of solver claims of infeasibility and optimality. Recent work has demonstrated that certification is feasible for CP solvers using a multi-stage proof-generation framework; however, the underlying proof system was informal, and verification relied on translation into an external proof format, impacting the trustworthiness. We address these issues by formalising a rigorous, solver-agnostic framework for certifying CP solver claims. We present a formal definition of DRCP, a proof system for CP over integer domains that captures core solver operations, including conflict analysis and heterogeneous propagation, by modular inference rules with precise semantics. We also develop FznDrcpCheck, a formally verified proof checker in Rocq that validates DRCP proofs directly against FlatZinc models. Our evaluation shows that our framework enables practical certification across various benchmarks with negligible overhead during solving and modest proof-checking costs.
Cite as

Maarten Flippo, Konstantin Sidorov, Tip ten Brink, Clément Pit-Claudel, and Emir Demirović. Formally Verified Certification of Constraint Programming Proofs. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 24:1-24:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{flippo_et_al:LIPIcs.CP.2026.24,
  author =	{Flippo, Maarten and Sidorov, Konstantin and ten Brink, Tip and Pit-Claudel, Cl\'{e}ment and Demirovi\'{c}, Emir},
  title =	{{Formally Verified Certification of Constraint Programming Proofs}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{24:1--24:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.24},
  URN =		{urn:nbn:de:0030-drops-266560},
  doi =		{10.4230/LIPIcs.CP.2026.24},
  annote =	{Keywords: Constraint programming, Proof systems, Certified checking}
}
Document
DOI: 10.4230/LIPIcs.CP.2026.42
From Literals to Atomic Constraints: Generalising Conflict-Driven Clause Learning for Constraint Programming

Authors: Imko Marijnissen, Maarten Flippo, and Emir Demirović

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{marijnissen_et_al:LIPIcs.CP.2026.42,
  author =	{Marijnissen, Imko and Flippo, Maarten and Demirovi\'{c}, Emir},
  title =	{{From Literals to Atomic Constraints: Generalising Conflict-Driven Clause Learning for Constraint Programming}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{42:1--42:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.42},
  URN =		{urn:nbn:de:0030-drops-266744},
  doi =		{10.4230/LIPIcs.CP.2026.42},
  annote =	{Keywords: LCG, CP, CDCL, Lazy Literal, Conflict Analysis, Nogood Propagation}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.4
Conflict Analysis Based on Cutting-Planes for Constraint Programming

Authors: Robbin Baauw, Maarten Flippo, and Emir Demirović

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
This paper introduces a novel constraint learning mechanism for Constraint Programming (CP) solvers that integrates cutting planes reasoning into the conflict analysis procedure. Drawing inspiration from Lazy Clause Generation (LCG), our approach, named Lazy Linear Generation (LLG), can generate linear integer inequalities to prune the search space, rather than propositional clauses as in LCG. This combines the strengths of constraint programming (strong propagation through global constraints) with cutting-planes reasoning. We present linear constraint explanations for various arithmetic constraints and the element constraint. An experimental evaluation shows that the improved generality of linear constraints has a practical impact on a CP solver by reducing the number of encountered conflicts in 45% of our benchmark instances. Our analysis and prototype implementation show promising results and are an important step towards a new paradigm to make constraint programming solvers more effective.
Cite as

Robbin Baauw, Maarten Flippo, and Emir Demirović. Conflict Analysis Based on Cutting-Planes for Constraint Programming. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{baauw_et_al:LIPIcs.CP.2025.4,
  author =	{Baauw, Robbin and Flippo, Maarten and Demirovi\'{c}, Emir},
  title =	{{Conflict Analysis Based on Cutting-Planes for Constraint Programming}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{4:1--4:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.4},
  URN =		{urn:nbn:de:0030-drops-238655},
  doi =		{10.4230/LIPIcs.CP.2025.4},
  annote =	{Keywords: constraint programming, learning, conflict analysis}
}
Document
DOI: 10.4230/LIPIcs.CP.2024.11
A Multi-Stage Proof Logging Framework to Certify the Correctness of CP Solvers

Authors: Maarten Flippo, Konstantin Sidorov, Imko Marijnissen, Jeff Smits, and Emir Demirović

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Proof logging is used to increase trust in the optimality and unsatisfiability claims of solvers. However, to this date, no constraint programming solver can practically produce proofs without significantly impacting performance, which hinders mainstream adoption. We address this issue by introducing a novel proof generation framework, together with a CP proof format and proof checker. Our approach is to divide the proof generation into three steps. At runtime, we require the CP solver to only produce a proof sketch, which we call a scaffold. After the solving is done, our proof processor trims and expands the scaffold into a full CP proof, which is subsequently verified. Our framework is agnostic to the solver and the verification approach. Through MiniZinc benchmarks, we demonstrate that with our framework, the overhead of logging during solving is often less than 10%, significantly lower than other approaches, and that our proof processing step can reduce the overall size of the proof by orders of magnitude and by extension the proof checking time. Our results demonstrate that proof logging has the potential to become an integral part of the CP community.
Cite as

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 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{flippo_et_al:LIPIcs.CP.2024.11,
  author =	{Flippo, Maarten and Sidorov, Konstantin and Marijnissen, Imko and Smits, Jeff and Demirovi\'{c}, Emir},
  title =	{{A Multi-Stage Proof Logging Framework to Certify the Correctness of CP Solvers}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{11:1--11:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.11},
  URN =		{urn:nbn:de:0030-drops-206969},
  doi =		{10.4230/LIPIcs.CP.2024.11},
  annote =	{Keywords: proof logging, formal verification, constraint programming}
}
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