Back to AI Research

AI Research

LeanCSP: A Framework for Certifying Constraint Refo... | AI Research

Key Takeaways

  • LeanCSP is a framework designed to provide formal, end-to-end verification for constraint satisfaction problems (CSPs).
  • Constraint programming is a core technology for solving complex combinatorial problems in scheduling, planning, configuration, and verification.
  • Trusting its results therefore demands guarantees at two levels: that reformulations applied beforehand are semantics-preserving, and that solvers produce correct answers.
  • Combining both levels yields an end-to-end workflow that establishes the satisfiability or unsatisfiability of a constraint problem without trusting the external solver.
  • By integrating the Lean theorem prover, the framework ensures that both the reformulation of a problem—such as adding...
Paper AbstractExpand

Constraint programming is a core technology for solving complex combinatorial problems in scheduling, planning, configuration, and verification. Trusting its results therefore demands guarantees at two levels: that reformulations applied beforehand are semantics-preserving, and that solvers produce correct answers. In this work, we introduce a framework that addresses both verification levels in the Lean theorem prover: it can be used to prove formulation-level properties, such as equivalence, equisatisfiability, and the correctness of symmetry-breaking constraints, parametrically for entire problem families; and to check solver-produced certificates for individual instances via translation backends to external formats such as MiniZinc, SMT-LIB, and OPB. Combining both levels yields an end-to-end workflow that establishes the satisfiability or unsatisfiability of a constraint problem without trusting the external solver. Experimental results show that our framework's verified symmetry breaking also pays off in practice: a single parametric proof per problem family, reused across all instance sizes, reduces solver search effort by a factor of up to 2x10^7, while the entire in-Lean certification stays affordable, taking at most a few minutes for our largest instances.

LeanCSP is a framework designed to provide formal, end-to-end verification for constraint satisfaction problems (CSPs). By integrating the Lean theorem prover, the framework ensures that both the reformulation of a problem—such as adding symmetry-breaking constraints—and the final answers provided by external solvers are mathematically correct. This allows users to establish the satisfiability or unsatisfiability of complex combinatorial problems without needing to trust the external software used to solve them.

Verifying Problem Reformulation

Practitioners often modify CSPs to improve solver performance, such as by adding symmetry-breaking constraints. However, these modifications can contain subtle errors that silently change the problem's solution. LeanCSP addresses this by allowing users to prove properties like equivalence and equisatisfiability directly within Lean. Because these proofs are parametric, they are established once for an entire problem family—such as the n-queens problem—and automatically apply to every instance of that problem regardless of size.

Certified Solver Execution

To solve specific instances, LeanCSP translates CSPs formulated in Lean into formats compatible with external solvers, including MiniZinc, SMT-LIB, and OPB. When a solver returns an answer, the framework verifies the result against the original problem specification. For unsatisfiable problems, the framework uses the pseudo-Boolean solver RoundingSat to generate proofs that are checked inside Lean using PBLean. This process ensures that any potential bugs in the external solver result in a failed check rather than an incorrect guarantee.

Performance and Practical Impact

The framework’s approach to verified symmetry breaking significantly reduces the computational burden on solvers. By applying a single parametric proof to a problem family, the authors observed a reduction in solver search effort by a factor of up to 2 × 10⁷. Despite the rigor of the formal verification process, the in-Lean certification remains efficient, requiring only a few minutes for the largest instances tested. The authors successfully used this pipeline to certify combinatorial results, including the Schur number S(4) = 44 and bounds for Ramsey and van der Waerden numbers.

Scope and Limitations

LeanCSP currently supports a library of over 40 constraint types, including comparison, arithmetic, and global constraints. The framework is specifically designed for CSPs where variables range over finite types and values are integers. While the framework provides a robust method for certifying results, it relies on the user to provide the initial formalization in Lean. The authors note that this approach distinguishes their work from standard proof-logging, which typically validates the low-level formula the solver works on, rather than establishing a theorem about the original CSP itself.

Comments (0)

No comments yet

Be the first to share your thoughts!