MF
M.L. Flippo
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
5 records found
1
Conference paper
(2026)
-
Maarten Flippo, Konstantin Sidorov, Tip ten Brink, Clément Pit-Claudel, Emir Demirović
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.
...
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.
From Literals to Atomic Constraints
Generalising Conflict-Driven Clause Learning for Constraint Programming
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.
...
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.
In the field of Explainable Constraint Solving, it is common to explain to a user why a problem is unsatisfiable. A recently proposed method for this is to compute a sequence of explanation steps. Such a step-wise explanation shows individual reasoning steps involving constraints from the original specification, that in the end explain a conflict. However, computing a step-wise explanation is computationally expensive, limiting the scope of problems for which it can be used. We investigate how we can use proofs generated by a constraint solver as a starting point for computing step-wise explanations, instead of computing them step-by-step. More specifically, we define a framework of abstract proofs, in which both proofs and step-wise explanations can be represented. We then propose several methods for converting a proof to a step-wise explanation sequence, with special attention to trimming and simplification techniques to keep the sequence and its individual steps small. Our results show our method significantly speeds up the generation of step-wise explanation sequences, while the resulting step-wise explanation has a quality similar to the current state-of-the-art.
...
In the field of Explainable Constraint Solving, it is common to explain to a user why a problem is unsatisfiable. A recently proposed method for this is to compute a sequence of explanation steps. Such a step-wise explanation shows individual reasoning steps involving constraints from the original specification, that in the end explain a conflict. However, computing a step-wise explanation is computationally expensive, limiting the scope of problems for which it can be used. We investigate how we can use proofs generated by a constraint solver as a starting point for computing step-wise explanations, instead of computing them step-by-step. More specifically, we define a framework of abstract proofs, in which both proofs and step-wise explanations can be represented. We then propose several methods for converting a proof to a step-wise explanation sequence, with special attention to trimming and simplification techniques to keep the sequence and its individual steps small. Our results show our method significantly speeds up the generation of step-wise explanation sequences, while the resulting step-wise explanation has a quality similar to the current state-of-the-art.
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.
...
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.
Conference paper
(2024)
-
Maarten Flippo, Konstantin Sidorov, Imko Marijnissen, Jeff Smits, Emir Demirović
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.
...
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.