Translating finite-domain integer constraint models to CP/SMT/ILP/PB/SAT solvers with CPMpy

• URL: http://arxiv.org/abs/2608.15143v1
• Date: Sat, 15 Aug 2026 09:38:09 GMT
• Title: Translating finite-domain integer constraint models to CP/SMT/ILP/PB/SAT solvers with CPMpy
• Abstract summary: Constraint solving is a declarative approach for solving satisfaction and optimization problems.<n>Our goal is to translate high-level constraint satisfaction and optimization problems into any lower-level formalism.<n>We present a modular framework for transforming our high-level modeling language to CP/SMT/ILP/PB and (Max)SAT solvers.
• Score: 6.498850269638911
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Disciplined Bilevel Programming [9.272977870242562]
  Bilevel optimization provides a natural modeling language for hierarchical decision problems.<n>Applying existing numerical solvers usually requires substantial manual analysis and reformulation.<n>We introduce disciplined bilevel programming (DBLP), a symbolic framework that allows users to specify and solve optimistic bilevel problems.
  arXiv  Detail & Related papers  (2026-09-01T03:22:48Z)
• Complementarity by Construction: A Lie-Group Approach to Solving Quadratic Programs with Linear Complementarity Constraints [9.967127506836453]
  Many problems in robotics require reasoning over a mix of continuous dynamics and discrete events.<n>We provide an opensource solver, Marble, that is implemented in C++ with Julia.
  arXiv  Detail & Related papers  (2026-04-13T19:31:41Z)
• GPU Accelerated Compact-Table Propagation [1.7249361224827533]
  This work focuses on a specific form of constraint, the so-called table constraint, used to specify conditions on the values of variables as an enumeration of alternative options.<n>Since every condition on a set of finite domain variables can be ultimately expressed as a finite set of cases, Table can, in principle, simulate any other constraint.<n>In this paper, we deal with the Compact-Table (CT) algorithm, the state-of-the-art propagation algorithms for Table.
  arXiv  Detail & Related papers  (2025-07-24T13:53:49Z)
• Efficient QAOA Architecture for Solving Multi-Constrained Optimization Problems [3.757262277494307]
  This paper proposes a novel combination of constraint encoding methods for the Quantum Approximate Optimization Ansatz.<n>One-hot constraints are enforced through $XY$-mixers that restrict the search space to the feasible sub-space naturally.<n>Since $XY$-mixers restrict the search space, specific state vector entries are always zero and can be omitted from the simulation, saving valuable memory and computing resources.
  arXiv  Detail & Related papers  (2025-06-03T17:46:53Z)
• A Graphical Global Optimization Framework for Parameter Estimation of Statistical Models with Nonconvex Regularization Functions [0.0]
  Problems with linear norm-bound constraints arise in a variety of applications, including portfolio optimization, machine learning, feature selection.<n>We propose a novel graphbased method to globally solve these problems.
  arXiv  Detail & Related papers  (2025-05-06T18:09:54Z)
• Syzygy of Thoughts: Improving LLM CoT with the Minimal Free Resolution [59.39066657300045]
  Chain-of-Thought (CoT) prompting enhances the reasoning of large language models (LLMs) by decomposing problems into sequential steps.<n>We propose Syzygy of Thoughts (SoT)-a novel framework that extends CoT by introducing auxiliary, interrelated reasoning paths.<n>SoT captures deeper logical dependencies, enabling more robust and structured problem-solving.
  arXiv  Detail & Related papers  (2025-04-13T13:35:41Z)
• Contextual Stochastic Bilevel Optimization [50.36775806399861]
  We introduce contextual bilevel optimization (CSBO) -- a bilevel optimization framework with the lower-level problem minimizing an expectation on some contextual information and the upper-level variable. It is important for applications such as meta-learning, personalized learning, end-to-end learning, and Wasserstein distributionally robustly optimization with side information (WDRO-SI)
  arXiv  Detail & Related papers  (2023-10-27T23:24:37Z)
• Numerical Methods for Convex Multistage Stochastic Optimization [86.45244607927732]
  We focus on optimisation programming (SP), Optimal Control (SOC) and Decision Processes (MDP) Recent progress in solving convex multistage Markov problems is based on cutting planes approximations of the cost-to-go functions of dynamic programming equations. Cutting plane type methods can handle multistage problems with a large number of stages, but a relatively smaller number of state (decision) variables.
  arXiv  Detail & Related papers  (2023-03-28T01:30:40Z)
• Symmetric Tensor Networks for Generative Modeling and Constrained Combinatorial Optimization [72.41480594026815]
  Constrained optimization problems abound in industry, from portfolio optimization to logistics. One of the major roadblocks in solving these problems is the presence of non-trivial hard constraints which limit the valid search space. In this work, we encode arbitrary integer-valued equality constraints of the form Ax=b, directly into U(1) symmetric networks (TNs) and leverage their applicability as quantum-inspired generative models.
  arXiv  Detail & Related papers  (2022-11-16T18:59:54Z)
• Conditional gradient methods for stochastically constrained convex minimization [54.53786593679331]
  We propose two novel conditional gradient-based methods for solving structured convex optimization problems. The most important feature of our framework is that only a subset of the constraints is processed at each iteration. Our algorithms rely on variance reduction and smoothing used in conjunction with conditional gradient steps, and are accompanied by rigorous convergence guarantees.
  arXiv  Detail & Related papers  (2020-07-07T21:26:35Z)
• An Integer Linear Programming Framework for Mining Constraints from Data [81.60135973848125]
  We present a general framework for mining constraints from data. In particular, we consider the inference in structured output prediction as an integer linear programming (ILP) problem. We show that our approach can learn to solve 9x9 Sudoku puzzles and minimal spanning tree problems from examples without providing the underlying rules.
  arXiv  Detail & Related papers  (2020-06-18T20:09:53Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.