Composing constraint solvers

Global Difference Constraint Propagation for Constraint Programming

This paper describes how to build a (bounds consistent) global propagator for difference constraints that treats them all simultaneously, and shows how to explain propagations by a global difference constraint propagator, in order to use it within a lazy clause generation solver.

LLM-Guided Evolutionary Search for Constraint Model Reformulation to Improve Solver Efficiency

Combinatorial problems appear in numerous industrial applications. A common approach is to formulate these problems as declarative constraint models that can subsequently be compiled to and solved by a range of back-end solvers. Recent work shows that Large Language Models (LLMs) can produce correct models from natural language, but even a correct model can be expensive to solve because performance remains sensitive to modelling choices. In this work, we investigate whether LLMs can automate performance-oriented model reformulation. Inspired by Automatic Heuristic Design (AHD), we use an evolutionary framework in which an LLM proposes candidate reformulations that are verified and benchmarked against the user-defined baseline model. We compare AHD-adapted search strategies that control which prior attempts, instructions, and measured feedback enter each prompt. Existing retention strategies prioritize recency or performance, but do not explicitly diversify the context. To cover this gap, we introduce Profile-Diverse Retention (PDR), which applies Maximal Marginal Relevance (MMR) to instance-level runtime vectors to retain behaviourally diverse attempts. We systematically evaluate the strategies on eight CSPLib problems using validation-based final model selection. The results show that: (i) iterative reformulation can produce substantial held-out speedups; (ii) strategies that keep the retained context diverse outperform those that retain only recent or the fastest attempts; and (iii) validation-based selection improves the held-out speedup of every strategy.

Efficient Reformulations of Half-reified Global Constraints using Auxiliary Variables

A set of reformulation rules are proposed that allow the use of half-reification of a global constraint with any CP solver that supports the “normal” global constraint propagator, and expand the range of available solvers and constraint models that can be used in XCP techniques or for solving CSPs with compound constraints.

From LLM Suggestions to Lean Proofs: Verified Redundant Constraints for MiniZinc

This work presents a pipeline that combines LLM-based constraint generation with empirical evaluation and formal verification, and handles MiniZinc’s partial semantics by requiring the base model to be safe and separately proving that the proposed constraint is well-defined for all instances and solutions of the base model.

Sustainable Benchmarking Tool

Improving Constraint Models with LLM Agents

This work introduces an agentic framework that reformulates a constraint model from an open-ended space and establishes correctness empirically rather than by construction, and demonstrates that autonomous agentic methods can support the improvement of constraint models.