The goal is to translate high-level constraint satisfaction and optimization problems into any lower-level formalism, including CP, SMT QF-LIA, ILP, PB and (Max)SAT, and to present a modular framework for transforming the high-level modeling language to CP/SMT/ILP/PB and (Max)SAT solvers.
Abstract
Constraint solving is a declarative approach for solving combinatorial satisfaction and optimization problems. The user specifies their problem through constraints and decision variables, and a generic solver is used to find a solution. Several constraint-solving technologies exist, and certain solvers perform well on certain problems. Therefore, it is useful to try different solvers given a particular application. However, each solving paradigm supports different types of constraints and decision variables. Our goal is to translate high-level constraint satisfaction and optimization problems into any lower-level formalism, including CP, SMT QF-LIA, ILP, PB and (Max)SAT. This allows for comparing different solving technologies for a particular problem, without requiring a user to manually remodel it for each solving paradigm. We define a high-level language of logical and arithmetic operations, and useful additional functions and constraints, which are known as global constraints in the CP community. We then present a modular framework for transforming our high-level modeling language to CP/SMT/ILP/PB and (Max)SAT solvers. While many transformations are partly described in the literature, we observe that they can be implemented through a modular waterfall of smaller components, where lower-level paradigms reuse the transformations of higher-level paradigms. Two recurring challenges are handling the negation of arbitrary subexpressions and avoiding the introduction of auxiliary variables. Additionally, we take special care linearizing non-linear operators for ILP, PB and SAT-solvers. The transformation waterfall is implemented and evaluated in the open-source CPMpy library. Our results show that constraint models significantly change throughout the transformations, and that optimizations to the linearization of constraints are essential for ILP and PB solvers.
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.
Ignace Bleukx, Hélène Verhaeghe, Dimos Tsouros et al.· Journal of Artificial Intell...· 1 citation
A simple but general semantics for timed Petri nets is presented in this paper. Based on this semantics, an optimization formulation is introduced and implemented in a recently developed optimization solver, where a satisfiability (SAT) solver is integrated with constraint programming (CP). The solver, called CP-SAT, is a part of Google’s OR-Tools. The optimization formulation includes both concurrent and alternative sequences of operations, involving shared as well as alternative resources. The proposed optimization strategy is compared with the SAT/SMT-based solver Z3Opt and Gurobi’s mixed integer linear programming (MILP) solver. The conclusion is that the computation time for CP-SAT is much shorter than for Z3Opt, while MILP is able to handle deep problems, including long sequences with many transitions, with similar computational performance as CP-SAT. On the other hand, CP-SAT is much faster than MILP for wide problems, including many parallel sequences. An evaluation of an industrial-sized flexible manufacturing system, which involves uncontrollable events, also demonstrates how efficient and easy to implement the proposed strategy is compared to existing results. In addition, it is also demonstrated how basic functionality in SAT and constraint programming are related and integrated in CP-SAT. The conclusion is that the strength of CP-SAT depends on its successful integration of search, inference, and OR-based relaxation on top of a satisfiability solver.
B. Lennartson· Discrete event dynamic syste...· 0 citations
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.
This work introduces a framework that addresses both verification levels in the Lean theorem prover, and can be used to prove formulation-level properties, such as equivalence, equisatisfiability, and the correctness of symmetry-breaking constraints, parametrically for entire problem families.
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.
Kostis Michailidis, Dimos Tsouros, D. Nguyen et al.· 0 citations
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.
Philipp Danzinger, Nysret Musliu· International Conference on...· 0 citations