PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Tias Guns, Ignace Bleukx, Hendrik Bierlee, Jo Devriendt, Emilio Gamba, Orestis Lomis, Wout Piessens, Thomas Sergeys, Dimos Tsouros, Wout Vanroose, Hélène Verhaeghe

arXiv:2608.15143v1cs.AI

TL;DR

Constraint models use constructs that different solver paradigms do not uniformly support, making cross-solver comparison require manual remodeling. This paper presents a modular translation waterfall implemented in CPMpy, showing on 250 XCSP3 optimization instances that targeted transformation optimizations can reduce model size and improve solving behavior.

  • Problem

    Different constraint-solving paradigms support different constraints and variables, limiting direct reuse of high-level models across solvers.

  • Method

    A modular end-to-end waterfall incrementally rewrites finite-domain models for CP, SMT, ILP, PB, MaxSAT, and SAT solvers.

  • Results

    250 XCSP3 optimization instances show that transformation optimizations can significantly reduce model size and improve solving behavior for ILP, PB, and SAT-based backends.

  • Takeaways & Limitations

    Effective solver translation depends on backend-specific transformations, including ILP-friendly decompositions, direct categorical encodings, and positive-context decompositions.

  • Takeaways & Limitations

    The same transformations do not necessarily benefit (Max)SAT encodings as they do ILP and PB solvers.

Abstract

from arXiv · show

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.

1 Introduction

The paper presents CPMpy as a Python-embedded modeling language and modular transformation pipeline for translating finite-domain integer constraint models across CP, SMT, ILP, PB, and (Max)SAT solvers. Its central contribution is a hierarchical waterfall that reuses shared rewrites while allowing solver-specific decompositions and linearizations.

  • Scope and modeling language: CPMpy targets discrete finite-domain integer models with Boolean and finite-domain integer decision variables for applications such as scheduling, packing, assignment, allocation, and routing.The modeling language supports logical and arithmetic operators, comparisons, global constraints, and global functions.
  • Scope and modeling language: Global constraints provide compact abstractions and can enable specialized CP propagation, while requiring translation for solvers that do not support them.Examples include AllDifferent, Table, Circuit, NoOverlap, Cumulative, and LexLess.
  • Transformation approach: The framework treats solver APIs as accepting language subsets and minimally rewrites expressions until only supported constructs remain.This yields a hierarchical waterfall in which lower-level paradigms reuse transformations from higher-level paradigms.
  • Transformation approach: The modular pipeline covers five constraint-solving paradigms: CP, SMT, ILP, PB, and (Max)SAT.Shared rewrites address global constraints, linearizations, and conversions of integer decision variables for solver families with overlapping requirements.
  • Solver-specific transformations: Solver-specific rewrite choices can substantially affect performance, particularly for ILP solvers benefiting from decompositions that produce strong LP relaxations.The approach therefore supports custom decompositions, including direct Boolean encodings of categorical integers.

2 Background

This section defines CSPs and COPs, their solutions and optimization objectives, and the reformulation-based transformations used to rewrite models while preserving their semantics. It also distinguishes total and partial functional constraints, which uniquely define outputs for all or only some input assignments.

  • Constraint problems: A CSP consists of decision variables, finite discrete domains, and constraints; this modeling language restricts integer domains to contiguous intervals [lb(x)..ub(x)].Boolean variables have domain {true, false}.
  • Constraint problems: A solution satisfies every CSP constraint, whereas a CSP with no solution is unsatisfiable; solution sets can also be projected onto selected variables.The notation sols(X, D, C), sols(C), and solsX(C) denotes these solution sets.
  • Constraint problems: A COP extends a CSP with a numerical objective function that scores complete assignments and supports searching for an optimal solution, defined here as one minimizing the objective.A COP is represented as (X, D, C, f).
  • Reformulations and transformations: A constraint reformulation preserves the solutions projected onto the original variables, may introduce auxiliary variables, and rewrites the original model through a transformation.For example, Min(x,y,z) ≤10 can be reformulated as Min(x,y,z)=m with m≤10.
  • Functional constraints: A total functional constraint has exactly one output assignment for every input assignment, while a partial functional constraint has at most one and may be undefined for some inputs.Division is partial because its output is undefined when the denominator is 0.

3 Language

The language defines a finite-domain integer modeling core with Boolean and bounded integer variables, typed logical and arithmetic expressions, and comparisons. It extends this core with decomposable global constraints and functions, treating integer-valued functions explicitly to avoid unnecessary auxiliary variables.

  • Core language: The core language supports Boolean variables and integer variables defined by names, lower bounds, and upper bounds.Boolean variables have the implicit domain {false, true}.
  • Core language: Boolean expressions support negation, conjunction, disjunction, implication, and equivalence, while integer expressions support linear arithmetic and comparisons.The comparisons are ≤, <, ≥, >, =, and ≠; arithmetic includes addition, subtraction, and multiplication by an integer constant.
  • Core language: Boolean expressions can be used as integers with False and True interpreted as 0 and 1, but integers cannot be cast to Boolean expressions.Thus, an expression such as ¬(x + y) is invalid even when x + y is bounded to 0 or 1.
  • Global constraints and functions: Global constraints and functions are additional operators that can be rewritten into semantically equivalent core constraints or functions.Examples include AllDifferent, GlobalCardinalityCount, Cumulative, Table, Xor, Min, Abs, and Element.
  • Global constraints and functions: Treating global functions as integer-valued functions rather than embedding them in equality constraints helps avoid unnecessary auxiliary variables.The framework supports global functions such as Min, Abs, and Element.

4 Transformations · 4.1 Eliminating Partial Functions

The framework uses a modular transformation pipeline that reformulates high-level constraints into solver-accepted primitive constraints, reusing higher-level transformations where possible. Its first step eliminates partial functions by safeguarding undefined cases with guards and safe replacement variables.

  • 4 Transformations: The pipeline transforms each input constraint into primitive constraints accepted by the targeted solver, with stages dedicated to specific reformulations.Lower-level solvers can reuse transformations shared with higher-level solvers.
  • 4 Transformations: All solvers first eliminate partial functions so subsequent transformations and solver interfaces can assume every global function is total.Negation removal and decomposition of unsupported global constraints follow this initial step.
  • 4 Transformations: After decomposition, SMT solvers can receive nested expression trees, whereas CP solvers require further flattening into constraints whose arguments are variables or constants.Transformations may be skipped when the target solver natively supports an operator or constraint.
  • 4 Transformations: The main transformation challenges are handling negation of arbitrary Boolean expressions and avoiding unnecessary auxiliary variables through Common Subexpression Elimination.The framework also reformulates numerical objectives according to solver-specific requirements.
  • 4.1 Eliminating Partial Functions: Partial functions, such as division and array lookup, are unsafe when their domains permit undefined values, including division by zero or out-of-bounds indices.The framework handles undefinedness using relational semantics for constraint modeling languages.
  • 4.1 Eliminating Partial Functions: Safening a nested partial function introduces a guard for definedness and replaces the potentially invalid argument with a safe alternative within its nearest Boolean context.This approach handles partial functions whose nearest Boolean context is not top-level.
  • 4.1.1 Safening partial functions using guards.: For range-defined functions such as X[y], safening uses the guard (1 ≤ y ≤ |X|), a variable y_safe ∈[1..|X|], and equality with y when in bounds.This models array lookup while preserving the original index whenever the lookup is defined.
  • 4.1.1 Safening partial functions using guards.: For functions undefined at one value, such as Div(x,y) and Modulo(x,y) when y=0, safening uses y≠0 and models both sides of the contiguous domain separately.Auxiliary variables are constrained to the original y when y differs from zero, while the division constraint is enforced.

4.2 Eliminating negation

The framework eliminates negation by pushing it down expression trees using comparison rewrites and De Morgan’s laws, while specialized reformulations handle some negated global constraints. Unsupported negated global constraints remain explicit, and later transformations must eliminate any negations they introduce immediately.

  • Core transformation: Negation is pushed down expression trees using standard simplifications, including mapping = to ≠, ≤ to >, and < to ≥.Logical operators are simplified using De Morgan’s laws.
  • Global constraints: Some negated global constraints are reformulated using other constraints, such as ¬Table as NegativeTable and ¬AllDifferent as NValue(X) < |X|.The implemented list also covers Regular for complete automata and Xor.
  • Global constraints: Global constraints without specialized negation remain negated in the expression tree, so the resulting grammar permits negated Boolean variables and negated global constraints.All other negation operators are eliminated.
  • Transformation invariants: Later transformations may not explicitly introduce unreduced negations; for example, ¬(x≤y) is immediately rewritten as x>y.This rule applies when decomposing IfThen constraints.

4.3 Decomposing unsupported global constraints and functions

Unsupported global constraints and functions are decomposed into equivalent lower-level expressions, using defining and value constraints when auxiliary variables are necessary. The framework avoids explicitly introducing functionally defined auxiliaries where possible, postponing flattening and reducing duplicate variables through common-subexpression elimination.

  • 4.3 Decomposing unsupported global constraints and functions: Unsupported global constraints and functions must be decomposed before models are posted to solvers.Solvers support different subsets of global constraints, and CP solvers generally restrict them to top-level use.
  • 4.3 Decomposing unsupported global constraints and functions: Decompositions return defining constraints T(X,A) for auxiliary variables and value constraints V(X,A) replacing the original global constraint.For Min(x,y,z) ≥ 3, an auxiliary variable m is defined by constraints and then substituted as m ≥ 3.
  • 4.3 Decomposing unsupported global constraints and functions: Functionally defined auxiliary variables are often avoided by using the defining subexpression directly in the decomposition.ArgMin(X,i) can be reformulated as X[i] = Min(X), eliminating the explicit auxiliaries w and v.
  • 4.3 Decomposing unsupported global constraints and functions: Postponing auxiliary-variable introduction reduces variables for solvers supporting nested expressions and lets flattening apply common-subexpression elimination and tight bounds.This also allows an auxiliary variable created later for a repeated subexpression to replace that subexpression elsewhere.
  • 4.3 Decomposing unsupported global constraints and functions: ILP reformulations require specialized decompositions because ILP solvers typically accept only linear inequalities, making standard CP-style decompositions unsuitable.Most global constraints therefore require decomposition when translating to ILP, aside from occasional numerical functions such as Min or Abs.

4.4 Flattening by substituting expressions with auxiliary variables

Flattening converts nested constraint expressions into solver-compatible flat constraints by replacing subexpressions with auxiliary variables while simplifying operators and reusing equivalent subexpressions. The resulting flat normal form supports linear expressions, clauses, global constraints, and global functions in comparisons, including reified contexts.

  • Flattening procedure: Flattening traverses the expression tree and replaces nested arguments of primitive operators and global constraints with fresh auxiliary variables.This produces constraints whose arguments are constants or variables, as required by solvers that accept only flat constraints.
  • Operator simplification: Associative operators are merged in place to avoid auxiliary variables, including weighted-sum simplification after decomposing nested Count constraints.For example, 2a + Count({x,y,z},1) ≥ 3 becomes a single weighted sum after Count is decomposed.
  • Operator simplification: Boolean distributivity and rewriting rules simplify nested ⇒, ∨, and ∧ operators before auxiliary variables are introduced.These reformulation rules are listed in Table 2 and target unnecessary auxiliary variables.
  • Common subexpression elimination: Common subexpression elimination uses a csemap cache to prevent duplicate auxiliary variables for repeated subexpressions.Expressions are normalized so syntactically different but semantically equivalent forms can share a variable, including canonical comparison and multiplication operand orderings.
  • Flat normal form: The resulting flat normal form permits linear expressions, clauses, global constraints, and global functions in comparisons, with each expression still usable in a reified context.Algorithm 2 implements common subexpression elimination and produces a form closely resembling the APIs of most CP solvers.

4.5 Linearization

The linearization phase converts flat normal-form expressions into ILP-compatible constraints, primarily using big-M reformulations for half-reifications and disequalities. It also avoids costly big-M constraints through direct or order encodings for frequently occurring integer comparisons, while eagerly choosing direct encoding when both equality and inequality expressions occur.

  • Half-reification: Half-reified linear inequalities are transformed with a big-M reformulation that relaxes the constraint when the Boolean antecedent is false and asserts it when true.The reformulation adds M·¬b to the left-hand side, where M is sufficiently large to ensure satisfaction when b is false.
  • Disequalities: Disequalities x≠y are decomposed into two half-reifications, b⇒x−y≤−1 and ¬b⇒x−y≥1, producing two big-M constraints.An auxiliary Boolean variable b selects which strict inequality is enforced.
  • Encoding optimizations: Direct encoding reuses Boolean indicators for categorical integer values, avoiding separate reification linearizations and their weak-relaxation big-M constraints.For x=3, the encoding represents x as a weighted sum of value indicators and reuses the existing indicator for value 3.
  • Encoding optimizations: Order encoding is selected for integer variables appearing frequently in comparisons of the form IntVar≥Int, avoiding big-M linearization of reified inequalities.When both equality and greater-than-or-equal expressions occur for one variable, the implementation currently eagerly selects direct encoding; channeling two encodings is left as future work.

4.6 Encoding All Integer Variables as Boolean Literals

The encoding step converts all integer variables into Boolean literals for pseudo-Boolean solvers, reusing the ILP transformation stack and supporting direct, order, and log encodings. It outputs pseudo-Boolean constraints through a modular module that can support future multiple-encoding improvements.

  • Encoding framework: All integer variables are encoded into Boolean literals using direct, order, or log encoding, while reusing most of the ILP transformation stack.The final conversion of negative to positive literals is omitted for pseudo-Boolean solvers.
  • Direct encoding: Direct encoding introduces one Boolean literal per domain value and represents weighted terms as weighted sums of value-indicator literals.Equality and disequality use matching literals, while inequalities conjoin literals for excluded domain values; consistency constraints enforce a valid encoding.
  • Order encoding: Order encoding introduces literals Jx≥iK for domain thresholds, represents inequalities directly, and requires monotonic consistency constraints.The encoding uses |D_x| − 1 literals, while equality and disequality are rewritten into combinations of ≤ and ≥ constraints.
  • Log encoding: Log encoding represents integer values with offset-binary bit literals, substitutes the resulting weighted sum into comparisons, and enforces the variable’s upper bound.It uses ⌈log2(|D_x|)⌉ literals to encode x.
  • Encoding framework: The encoding module outputs pseudo-Boolean constraints and is designed to support multiple encodings of one integer variable based on its constraint usage.The paper identifies this modularity as enabling future improvements to the encoding step.

4.7 To Conjunctive Normal Form (CNF)

The CNF transformation reuses the Pseudo-Boolean pipeline, supports half-reified constraints without Big-M encoding, then converts implications and weighted linear constraints into CNF.

  • To Conjunctive Normal Form (CNF): SAT translation reuses the modular transformations for Pseudo-Boolean solvers, while marking half-reified constraints as supported during linearisation.This avoids encoding half-reified constraints with Big-M constraints.
  • To Conjunctive Normal Form (CNF): After Pseudo-Boolean transformation, implications are rewritten as disjunctions and weighted linear constraints are formulated into CNF.The formulation of weighted linear constraints into CNF is described as well studied.

5 Experimental results

Experiments on 250 XCSP3 COP instances examine how CPMpy models change through the transformation stack and how optimizations affect ILP, PB, and Max-SAT solving. Decompositions and flattening substantially expand models, while optimization effects differ across solver paradigms.

  • Experimental setup: The evaluation uses all 250 instances from the 2024 XCSP3 COP competition, covering diverse models with global constraints and functions.Instances are parsed into CPMpy v1.0.0 using built-in datasets and IO tools.
  • Experimental setup: Experiments run Gurobi 13.0.2, Exact 2.3.0, and RC2 via PySAT 1.9.dev5 on one CPU thread with an 8GB memory limit.Runtime is measured until proven optimal, with a one-hour time limit.
  • Model transformations: Global-constraint decomposition and flattening introduce many auxiliary constraints and variables, whereas linearization adds no new integer variables.Flattening creates an auxiliary variable for each nested expression, while linearization mainly adds big-M and disequality-encoding constraints and Boolean variables.
  • Model transformations: The final Boolean encoding increases constraints and Boolean variables only moderately relative to the linear formulation, making categorical-variable detection essential to avoid an encoding explosion.The transformation results are reported for interfacing with a pseudo-Boolean solver.
  • Solver performance: ILP-friendly and positive decompositions generally improve solving performance over the baseline, while adding positive decompositions provides little additional benefit on top of ILP-friendly decompositions.The ILP-friendly decompositions produce the most instances solved to optimality overall.
  • Solver performance: Optimization effects are smaller for PB solvers, whereas ILP-friendly decompositions can degrade Max-SAT performance; the best Max-SAT combination uses eager categorical encoding with standard CP-style decompositions.For PB, the full optimization combination is only marginally better than the baseline.

6 Conclusion

The paper presents a modular waterfall that incrementally transforms finite-domain constraint models for CP, SMT, ILP, PB, MaxSAT, and SAT solvers. Experiments on 250 XCSP3 optimization instances show substantial model changes and the importance of solver-specific transformation optimizations.

  • Contributions: The pipeline incrementally rewrites high-level Boolean and integer expressions into solver-supported forms for CP, SMT, ILP, PB, MaxSAT, and SAT.It is organized as a waterfall of reusable transformations.
  • Transformation challenges: The main challenges are preserving the semantics of negated and nested expressions while avoiding unnecessary auxiliary variables.Partial functions must be safened before later transformations, and decompositions must remain valid in nested contexts.
  • Evaluation: 250 optimization instances from the XCSP3 competition were used to evaluate the transformation pipeline.The models change substantially throughout the stack, especially during decomposition, flattening, and linearization.
  • Evaluation: Transformation optimizations significantly affect solving performance, including ILP-friendly decompositions, direct encodings for categorical integer variables, and positive-context decompositions.The conclusion emphasizes that optimization choices are important for ILP and PB solving performance.
  • Future work: Future work includes extending the input language, improving normalization, half-reification-aware decompositions, and CSE, and investigating alternative hierarchical architectures.The paper also notes that (Max)SAT may not benefit from the same transformations as ILP/PB solvers.

A Pseudocode for Normalization of Arguments During Flattening

The normalization pseudocode recursively processes Boolean and numeric expressions during flattening, preserving variables and constants while introducing or reusing variables for subexpressions. It separately handles Boolean connectives, negated global constraints, negation, unary minus, linear sums, and global-function arguments.

  • NormalizeBoolExpr and NormalizeNumExpr: Normalization returns variables and constants unchanged, with no decomposition data.This base case appears in both Boolean and numeric normalization procedures.
  • NormalizeBoolExpr: Boolean normalization recursively processes implications and equivalences by normalizing their subexpressions and combining returned decomposition data.The displayed cases include implication and biconditional expressions, with decomposition sets unioned across recursive results.
  • NormalizeBoolExpr and NormalizeNumExpr: Boolean normalization includes a dedicated case for negating global constraints, while global-function arguments are converted with GetOrMakeVar during numeric normalization.The pseudocode explicitly labels negation of a global constraint and applies GetOrMakeVar to each global-function argument.
  • NormalizeNumExpr: Numeric normalization converts Boolean expressions into variables through GetOrMakeVar.The numeric procedure explicitly delegates Boolean expressions to GetOrMakeVar.
Loading 2608.15143v1…