Paper deep dive
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
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 92%
Last extracted: 8/18/2026, 5:44:45 AM
Summary
This paper introduces CPMpy, an open-source Python library that provides a modular framework for translating high-level finite-domain integer constraint satisfaction and optimization models into various lower-level solver formalisms, including Constraint Programming (CP), Satisfiability Modulo Theories (SMT QF-LIA), Integer Linear Programming (ILP), Pseudo-Boolean (PB), and (Max)SAT. The system defines a high-level language with logical, arithmetic, and global constraints, implementing a modular 'waterfall' transformation pipeline that reuses components across paradigms to handle challenges like negation, auxiliary variable minimization, and linearization of non-linear operators.
Entities (12)
Relation Signals (11)
CPMpy → supportstranslationto → Pseudo-Boolean
confidence 95% · Our goal is to translate high-level constraint satisfaction and optimization problems into any lower-level formalism, including ... PB
CPMpy → supportstranslationto → SMT
confidence 95% · Our goal is to translate high-level constraint satisfaction and optimization problems into any lower-level formalism, including ... SMT QF-LIA
CPMpy → supportstranslationto → Integer Linear Programming
confidence 95% · Our goal is to translate high-level constraint satisfaction and optimization problems into any lower-level formalism, including ... ILP
CPMpy → supportstranslationto → SAT
confidence 95% · Our goal is to translate high-level constraint satisfaction and optimization problems into any lower-level formalism, including ... (Max)SAT
CPMpy → supportstranslationto → Constraint Programming
confidence 95% · Our goal is to translate high-level constraint satisfaction and optimization problems into any lower-level formalism, including CP
CPMpy → affiliatedwith → KU Leuven
confidence 90% · Affiliation: KU Leuven , Belgium
CPMpy → developedby → Tias Guns
confidence 90% · Authors list includes Tias Guns from KU Leuven, and the paper describes the CPMpy library.
CPMpy → →
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2608.15143v1
- Canonical: https://arxiv.org/abs/2608.15143v1
Trouble viewing inline? Open PDF directly →
Full Text
123,957 characters extracted from source content.
Expand or collapse full text
TBD Translating finite-domain integer constraint models to CP/SMT/ILP/PB/SAT solvers with CPMpy08DOI: TBD Tias Guns OrcID: 0000-0002-2156-2155 email: tias.guns@kuleuven.be Affiliation: KU Leuven , Belgium , Ignace Bleukx OrcID: 0000-0001-7810-8351 email: ignace.bleukx@kuleuven.be Affiliation: KU Leuven , Belgium , Hendrik Bierlee OrcID: 0000-0001-6766-5435 email: bierlee.henk@gmail.com Affiliation: KU Leuven , Belgium , Jo Devriendt OrcID: 0000-0002-6346-3665 email: jo.devriendt@nonfictionsoftware.com Affiliation: Nonfiction Software , Belgium , Emilio Gamba OrcID: 0000-0003-1720-9428 email: emilio.gamba@flandersmake.be Affiliation: Flanders Make , Belgium , Orestis Lomis OrcID: 0009-0006-2934-0510 email: orestis.lomis@kuleuven.be Affiliation: KU Leuven , Belgium , Wout Piessens OrcID: 0009-0005-5608-2097 email: wout.piessens@kuleuven.be Affiliation: KU Leuven , Belgium , Thomas Sergeys OrcID: 0009-0003-3817-4516 email: thomas.sergeys@kuleuven.be Affiliation: KU Leuven , Belgium , Dimos Tsouros OrcID: 0000-0002-3040-0959 email: dtsouros@uowm.gr Affiliation: University of Western Macedonia , Greece , Wout Vanroose OrcID: 0009-0004-8945-0442 email: wout@vanroose.be Affiliation: KU Leuven , Belgium and Hélène Verhaeghe OrcID: 0000-0003-0233-4656 email: helene.verhaeghe@uclouvain.be Affiliation: UCLouvain , Belgium 2026; © c; Received 07/08/2026 Abstract. Background: 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. Objectives: 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. Methods: 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. Results: 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. Keywords: modeling languages, constraint reformulation, constraint solving, constraint satisfaction 1. Introduction A prevalent AI approach to solving combinatorial satisfaction and optimization problems is the model + solve paradigm. In this paradigm, the user first describes their problem in a constraint model in terms of constraints over decision variables, optionally with an objective function over a subset of the decision variables. This declarative problem specification is then given to a highly optimized constraint solver, which searches for an (optimal) solution, where the constraints are used to effectively reduce the search space. Many generic solvers have been developed, differing in the type of constraints and decision variables they support. For example, SAT solvers support Boolean variables and clauses as constraints 16. MaxSAT solvers additionally support a weighted linear sum as an objective function 39. Pseudo-Boolean solvers support linear constraints over Boolean variables 52. There are also Integer Linear Programming (ILP) solvers, Mixed continuous-Integer Linear Programming (MILP) and non-linear programming solvers, Constraint Programming (CP) 51 solvers with global constraints, and SAT Modulo Theories (SMT) solvers with arbitrary theories including quantified formulas and unbounded variables 9. We here focus on discrete, finite-domain integer constraint models, which have a wide range of real-life applications, including scheduling, packing, assignment, allocation, routing, and more 53; 22; 35; 60; 26. The supported decision variables are Boolean and finite-domain integer. Constraint solvers are typically categorized by the types of constraints they support, that is, relations they can enforce to be satisfied (such as a∨ba b, 2x+3y≤42x+3y≤ 4, x≠yx≠ y). In contrast, SMT solvers and modeling languages are defined by the expressions they support, where basic expressions can be combined into nested expressions, which together with a comparison or Boolean operator become a constraint that must be satisfied (such as a⇒(¬(b∧c)∨d)a ( (b c) d) or x⋅y+3⋅(z=0)≤r10x· y+3·(z=0)≤ r10). What we will describe is a modeling language, with a practical implementation that is embedded in the Python programming language, with the following types of expressions: • Boolean logical operators (and, or, not, implication, equivalence, exclusive-or) • Integer arithmetic operators (+, -, multiplication, integer-division, modulo, power, max, min, abs) • Integer comparison (=,≠,>,≥,<,≤=,≠,>,≥,<,≤) • Integer “global” constraints (AllDifferent, Table, Circuit, NoOverlap, Cumulative, LexLess …) • Integer “global” functions (Array-Lookup, Count, Among, NValue …) The “global” constraints are constructs from the constraint programming community 12 that offer two benefits: 1) they provide meaningful abstractions that users can use to compactly write down their problem specification; 2) many CP solvers have specialized reasoning methods (propagators) to efficiently reduce the search space based on the semantics of the global constraint. For solvers that do not support such global constraints, there are well-known translations into basic Boolean and integer operators (called decompositions). The integer global constraints are Boolean-valued (they can be true or false). The “global” functions are integer-valued functions that have a corresponding global constraint, e.g., the Count(,) Count(Arr,Val) operator has CountEquals(,,) CountEquals(Arr,Val,Cnt). Our choice of language follows from the combinatorial scheduling, routing, and assignment type of applications we target. A number of modeling languages and transformation libraries exist for combinatorial problems, including MiniZinc 43, Essence Prime 4 in combination with Savile Row 44, PicatSAT 67, and Pyomo 36. They differ in 1) the type of expressions they support, and 2) the type of solvers they can translate to. Table 1. Comparison of different constraint modeling systems and their capabilities. Solvers Language Global constraints Global functions Variables Savile Row CP/SMT/SAT Text-based ✓ ✓ Bool/int MiniZinc CP/ILP/FZN-based Text-based ✓ ✓ Bool/int/float PyCSP3 CP Python ✓ ✓ Bool/int PicatSAT SAT Text-based ✓ - Bool/int Pyomo ILP/SMT Python - - Bool/int/float OR-Tools API CP Python ✓ ✓ Bool/int Gurobi API ILP Python - - Bool/int/float CPMpy (ours) CP/SMT/ILP/PB/SAT Python ✓ ✓ Bool/int The system closest to CPMpy that we will describe here is the Savile Row system for the Essence Prime language. The Savile Row system translates constraint models in the Essence language to CP solvers, SAT solvers and SMT solvers. However, Essence Prime is a text-based modeling language, whereas our CPMpy modeling language is embedded in Python. Another important difference is that Savile Row has different backends for the 3 types of solvers, where they reuse low-level components up to some extent, which corresponds to how it has been developed over time. In contrast, we describe a holistic, hierarchical approach that aims to maximize the number of transformations that can be reused for different solver paradigms and solvers. Another highly related technology is PyCSP3, which, like CPMpy, is also a Python-embedded system, but it only translates to the XML-based CP language XCSP3, not to other solver paradigms. The Pyomo system is also relevant to our framework. While it is embedded in Python and translates to multiple MIP, ILP, and SMT solvers, the system does not compile “down” to PB or SAT solvers. Additionally, global constraints and operators are not supported by the Pyomo framework as they are specific to CP modeling. Finally, the well-known MiniZinc system 43 is highly related as well. Together with Essence Prime, it has been an inspiration both conceptually and academically, based on the different papers and reports published on these systems. MiniZinc is a text-based language that also supports floating-point decision variables and floating-point arithmetic. Its main output language is the text-based FlatZinc constraint language, which supports (custom definable) flat (= non-nested) constraints over floating-point, integer, and Boolean decision variables. The key difference is that the MiniZinc compiler does not translate directly to the language of a specific solver. Rather, it translates to a flat intermediate language, and this intermediate language must then be reformulated to a specific solver in a separate program (e.g., PicatSAT 67, fzn2omt 23…). The latter requires rebuilding certain data structures and modeling patterns, and potentially undoing some of the flattening done by the MiniZinc compiler. The translation to integer linear and mixed integer programming solvers can be handled by MiniZinc through configuration options that change how different constraints are decomposed/rewritten 43; 13. We propose a more holistic approach, and adopt the view that solvers (or solver APIs, more specifically) accept a subset of our language as input, and our goal is to minimally rewrite our expressions so that only supported expressions remain. Furthermore, multiple families of solvers require the same rewrite operations: only CP solvers support global constraints, both ILP and PB solvers benefit from good linearizations, and both PB and SAT solvers require the conversion of integer decision variables to Boolean decision variables. As we will describe below, the result is a hierarchical waterfall of transformations that can effectively rewrite models in the above language to any of the mentioned solvers. Technically, some solver families will benefit from different rewrite choices than others, most notably integer linear programming solvers, which benefit from global constraint decompositions that lead to strong LP relaxations, for example, that reason over a direct Boolean encoding of the categorical integers. The proposed approach is modular and allows for such custom decompositions as we describe in Section 4.5. In general, the performance of lower-level solvers can be greatly impacted by the choice of rewrites and the encodings used 65; 59; 66. While the transformations we describe are based on techniques described and validated in the literature, we make no attempt to claim they are the optimal choice. Indeed, determining the optimal choice of encodings is an ongoing active research topic in the specific solver fields of research 4. Instead, we believe that constraint-solving communities can benefit from having accessible libraries that offer good baseline encodings. As the knowledge of encoding choices further develops, modeling system developers can take over the best practices and make them more widely available. Furthermore, the modular nature of the proposed approach makes modeling systems a good framework for investigating the effect of different encodings. Our key contribution is hence not any specific transformation, but the presentation of a modular end-to-end translation pipeline that covers five different constraint-solving paradigms and that has been validated in real applications 20; 33 and competitions 6; 7. 2. Background A Constraint Satisfaction Problem (CSP) is a triple (,,)(X,D,C) 51. Here, X is a set of decision variables and D is a set of finite and discrete domains, which detail the allowed values for each variable. For any integer variable x, Dx⊂ℤD_x and Boolean variables have a domain ,\true,false\. In our constraint modeling language, only contiguous domains are allowed, and each variable x has a domain where (x)lb(x) and (x)ub(x) are the lower and upper bounds of x, respectively. An assignment maps a variable to a value in its domain, which we write as x↦vx v. C is a set of constraints, where each constraint c∈c maps an assignment to true or false. A constraint is typically written as a mathematical expression or predicate and often only contains a subset of the variables in the full CSP. E.g., the constraint x+2y−8z≥3x+2y-8z≥ 3 only contains variables x,yx,y and z. These variables are said to be in the scope of the constraint. To refer to the set of variables occurring in c, we write (c)scope(c). If an assignment is mapped to true by the constraint, we say the assignment satisfies the constraint. An assignment α projected to a subset of variables X is written as α| _| X. An assignment that satisfies all constraints in the CSP is a solution of the CSP. If there exists no solution to the CSP, it is said to be unsatisfiable. The set of solutions of a CSP is written as (,,)sols(X,D,C) or, when the variables and domains are clear from the context, we write ()sols(C) in short. The set of solutions of a set of constraints, projected to a set of variables X is written as ()sols_X(C). A Constraint Optimization Problem (COP) generalizes the definition of a CSP to also include an objective function f. That is, a COP is a quadruple (,,,f)(X,D,C,f) where f is a numerical expression that maps a full assignment α to a numerical value. This allows us to score or rank the set of solutions to a constraint problem and allows searching for an optimal solution of the problem. An optimal solution (w.l.o.g.) minimizes the objective value. That is, a solution α∗α^* is optimal if for each α∈()α (C), f(α)f(α) is greater than or equal to f(α∗)f(α^*). 2.1. Constraint reformulations A constraint satisfaction or optimization problem (hereafter referred to as “constraint problem”) can be modeled in multiple ways by choosing a particular set of variables and constraints. We will be interested in semantically equivalent formulations of a constraint problem. We say two CSPs are semantically equivalent to a set of decision variables if they have the same set of solutions when projected onto that set of decision variables. We say two such CSPs are constraint reformulations of one another, as formalized by 15. Definition 0 (Constraint reformulation). A CSP (′,′,′)(X ,D ,C ) is a constraint reformulation of another CSP (,,)(X,D,C) if and only if both CSPs are semantically equivalent with respect to the set of original decision variables X. That is, if (,,)=(′,′,′)sols_X(X,D,C)=sols_X(X ,D ,C ) and ⊆′X . An example of a constraint reformulation for Min(x,y,z)≤10\ Min(x,y,z)≤ 10\ is Min(x,y,z)=m,m≤10\ Min(x,y,z)=m,m≤ 10\ where =x,y,zX=\x,y,z\ and ′=x,y,z,mX =\x,y,z,m\. To write a CSP to a reformulated CSP, we say it has to be transformed into the new CSP. Therefore, we will refer to the process of rewriting a CSP to a constraint reformulation as a transformation. Transformations can introduce new variables into the CSP, such as m in the reformulation of the constraint above, and ′∖X in general. These fresh variables are introduced by the modeling system and do not belong to the set of user-defined variables. We call such variables auxiliary variables 55. The values of these auxiliary variables do not need to be uniquely determined by a solution over X. In this case, for an original solution there may exist multiple extensions to a solution of the reformulated CSP. In general, the reformulation must be sound and complete with respect to CSP (,,)(X,D,C): every solution of the reformulated CSP must project onto a solution of the original CSP, and every solution of the original CSP must admit at least one extension to a solution of the reformulated CSP. A constraint reformulation generalizes to optimization problems as well. That is, a COP (′,′,′,f′)(X ,D ,C ,f ) is a reformulation of (,,,f)(X,D,C,f) if the set of constraints are semantically equivalent to X and for each solution α∈(′,′,′)α (X ,D ,C ), it holds that f′(α)=f(α|)f (α)=f( _|X) Note that in practice, constraint modeling systems can also remove variables from the input CSP when transforming it to a CSP suitable for a particular solver. We distinguish three cases where variables are removed: (1) Unconstrained variables, also known as free variables, can be removed from the model. (2) Constant variables with a singleton domain can be replaced by that single value in their domain. (3) Functionally defined variables whose value is determined by a set of (auxiliary) variables ′X . Whenever such variables are removed during the transformation process, we assume the modeling system keeps a mapping from the remaining variables to the removed variables. The modeling system then only posts the relevant part of the transformed CSP to the solver (e.g., only Boolean encoding literals of integer variables for SAT solvers), and derives the value for all removed decision variables after the solver has found a solution. 2.2. Functional constraints Some constraints used in constraint models represent a function. That is, they define the value of one or more “output” variables, given a value to the “input” variables. Functional constraints can be either total or partial. Definition 0 (Total function constraint). A functional constraint F(X,Y)F(X,Y) is total if and only if for each assignment to X, there exists exactly one assignment to Y that satisfies the constraint. Total function constraints with a single input and output variable are sometimes also referred to as views in constraint programming nomenclature 61. An example of such a total function with a single “output” variable is the Min(X,m) Min(X,m) constraint, as for assignment to the set of variables X, the minimum value always exists and is unique. Another example is the GlobalCardinality(X,V,O) GlobalCardinality(X,V,O) constraint, which enforces the number of occurrences of each value viv_i in the array of X to be exactly oio_i. The open version of this constraint allows values in X to take a value not occurring in V, i.e. it allows ∑oj∈Ooj≤|X| _o_j∈ Oo_j≤|X| 63. This constraint is an example of a total function constraint with multiple output variables O. Indeed, for any value assigned to the variables in X and a fixed set of values C, the number of occurrences OvO_v of value v in X is always defined and unique. Definition 0 (Partial function constraint). A functional constraint F(X,Y)F(X,Y) is partial if for each assignment to X, there exists at most one assignment to Y that satisfies the constraint. This means the output of a partial function may be undefined for some input values. An example of a partial function is the Division function, for which the output is undefined when the denominator is 0. Note that the closed version of GlobalCardinality(X,V,O) GlobalCardinality(X,V,O), which enforces values of X to be assigned to a value in V, can be interpreted as a partial function. Indeed, given an assignment to X, the constraint only defines the number of occurrences for each value in V when all variables X take a value occurring in V. Section 4.1 elaborates further on the semantics of (nested) partial functions in constraint models. 3. Language Grammar 1 The constraint modeling language. <Model> ::= [ <BoolExpr> (, <BoolExpr>)* ], minimize= <IntExpr> <BoolExpr> ::= | <Bool> | <BoolVar> | ¬ <BoolExpr> | <BoolExpr> ∧ | ∨ | ⇒ | ⇔ <BoolExpr> | <IntExpr> ≤ | < | ≥ | > | == | ≠ <IntExpr> | <GlobalConstraint> [ <Arg> (, <Arg>)* ] <IntExpr> ::= | <Int> | <IntVar> | <BoolExpr> | - <IntExpr> | <IntExpr> + | - <IntExpr> | <Int>×<IntExpr> | <GlobalFunction> [ <Arg> (, <Arg>)* ] <BoolVar> ::= <String> <IntVar> ::= <String> <Int> <Int> <Arg> ::= <BoolExpr> | <IntExpr> | [ <Arg> (, <Arg>)* ] We now formally define the constraint modeling language as shown in Section 3, which is used throughout the remainder of this paper. The modeling language consists of Boolean and integer expressions, which can be arbitrarily nested to form complex expressions. We say a Boolean expression is a constraint when it is ‘top-level”, i.e., if it occurs in the list of Boolean expressions in the model definition. If a Boolean expression occurs as a subexpression, we say it is ‘nested”. Naturally, integer expressions only occur as a subexpression, as they cannot be enforced to true at the top-level of the model. E.g., x+yx+y is not a constraint. 3.1. Core language We first define the core language of finite-domain integer modeling, that is, everything in Grammar 3 except global constraints and functions. The language allows for two types of decision variables: Boolean variables and integer variables. Each integer variable is defined with a name, a lower bound, and an upper bound. Boolean variables are defined with a name, and the implicit domain false,true\ false, true\ Similar to variables, each expression has either a Boolean or an integer return type. Boolean variables (and expressions) can be used in logic operators from propositional logic: negation (¬ ), conjunction (∧ ), disjunction (∨ ), implication (⇒ ), and reification/equivalence (⇔ ). Integer variables (and expressions) can be used as arguments to the comparisons ≤,<,≥,>,=≤,<,≥,>,= and ≠. Operators with an integer return type are the linear arithmetic operators plus (++) and minus (−-) and the multiplication operator × to ‘scale” an integer expression with a constant. Other Boolean and integer operators will be implemented through global constraints and global functions. Note that our language does not support casting from integer to Boolean. That is, Boolean variables and expressions can be used as an integer (where False and True are interpreted as 0 and 1, respectively), but not vice versa. E.g., it is not valid to write ¬(x+y) (x+y), even if the expression x+yx+y is bounded to only take values 0 or 1. This is similar to the format supported by SMT-solvers 8; 9. However, in contrast to the language supported in SMT, our constraint modeling language includes the use of global constraints and global functions, as described in the next section. 3.2. Global constraints and functions We now extend the core language with additional Boolean and integer operators and functions. What differentiates them from the core operators is that they can be decomposed, i.e., rewritten into (a conjunction of) core operators. To stay somewhat close to constraint programming nomenclature, we will call these additional operators and functions ‘global constraints” if they have a Boolean return type, and when they have an integer return type we will call them ‘global functions”. Definition 0 (Global constraint). A global constraint is a Boolean predicate that can be reformulated to a semantically equivalent (see Definition 2.1) set of constraints in the core language. For example, the global constraint AllDifferent(x1,…,xn) AllDifferent(x_1,…,x_n) holds if all variables take pairwise distinct values. It can be decomposed into the following conjunction of core constraints: ⋀1≤i<j≤nxi≠xj. _1≤ i<j≤ nx_i≠ x_j. Other examples of well-known global constraints are GlobalCardinalityCount, Cumulative, Table and Xor. In Section 4.3 we elaborate on the semantics of these constraints and their decompositions implemented in our framework. Definition 0 (Global function). A global function is an integer-valued function that can be reformulated to a semantically equivalent function and set of supporting constraints in the core language. Examples of global functions supported in our language are the Min, ˛and Element functions. Note that our use of ‘global functions” is often not described in existing papers on constraint modeling languages; they often consider the operator together with an equality operator as a global constraint and silently extract it when the function is used as a subexpression. However, treating it as a function is a first key aspect in avoiding unnecessary introductions of auxiliary variables 57. ⇔ ∨ ≤++x∧ 3 (a) (a∨b)⇔(x+(p∧q)≤3)(a b) (x+(p q)≤ 3) AllDifferentaaDivbbcc+d3 (b) AllDifferent(a,Div(b,c),d+3) AllDifferent(a, Div(b,c),d+3) Figure 1. Examples of constraints in our constraint language and their corresponding expression trees. 4. Transformations modelNo partial functionsEliminate negationDecompose globalFlattenLinearizeInteger to BoolTo CNF SMT-solvers CP-solvers ILP-solvers PB-solvers SAT-solvers Figure 2. Transformation pipeline. We now describe the modular transformation pipeline that allows us to translate the described language to different solver paradigms. The goal of our transformation process is to transform each constraint in the input constraint model to a set of primitive constraints for the targeted solver. A primitive constraint is a constraint the solver accepts as input. Naturally, each solver (paradigm) has a certain set of such primitive constraints. Each stage in the transformation pipeline shown in Figure 2 has a specific purpose of reformulating certain types of constraints. Each box corresponds to a particular subsection describing the transformation. A key insight of our transformation pipeline is that lower-level solvers can re-use transformations that are shared with higher-level solvers. The first step for all solvers is to eliminate partial functions, which is described in Section 4.1. This ensures all subsequent transformations and solver interfaces can assume every global function in the constraint model is a total function. Next, negation operators are removed from the expression tree as described in Section 4.2. More specifically, we follow a set of standard reformulation rules that allow to ‘push down” any negation operator into its arguments. Note that this step is omitted for SMT solvers, as they typically have their own set of simplification rules for eliminating negation from the expression tree. As a third general transformation step, we decompose all unsupported global constraints and functions (Section 4.3). Here, we replace every unsupported global constraint with a Boolean expression consisting of only supported operators by the solver at hand, and all global functions are replaced with a numerical expression. After eliminating all these global constraints and functions, we can post the constraint model to SMT-solvers, which accept nested expression trees as input. For CP-solvers, however, further flattening of the expression tree is required, as CP-solvers only support flat constraints or their reification (Section 4.4). That is, constraints in which each argument is a variable or a constant. For ILP solvers, further linearization of the flattened constraints is required (Section 4.5). Indeed, these solvers only support linear inequality constraints, so all logical constraints should be linearized as such. Pseudo-Boolean (PB) solvers also support linear inequality constraints, but only over Boolean variables. Hence, all integer variables must be encoded with an appropriate Boolean encoding. Section 4.6 describes which encodings are currently implemented in our framework. Finally, SAT-solvers only support clauses of Boolean literals. Hence, the set of constraints suited for PB-solvers must be processed further before it can be posted to a SAT-solver. For this final step, our framework largely relies on external libraries such as PyPBlib 47 and Pindakaas 18. Note that, given a target solver to transform the input model to, certain steps in the transformation may be skipped. E.g., if a CP-solver supports the AllDifferent constraint, then naturally it should not be decomposed by the transformation stack. Similarly, some ILP solvers support the use of an implication constraint in their API; this means the linearization of implications is skipped in our transformation stack. In practice, we implement this using an ‘exclude” set, which lists the operators that are left unchanged during a particular transformation. Two key challenges for transforming a high-level constraint model will be to 1) correctly handle negation of arbitrary Boolean expressions and 2) avoid introducing superfluous auxiliary variables. The first challenge will largely be handled during safening of partial functions, and subsequent elimination of negation constraints. To avoid introducing unnecessary auxiliary variables, we apply Common Subexpression Elimination (CSE) 50 during flattening and subsequent transformations. This ensures all semantically equivalent subexpressions are channeled to the same auxiliary variable. For constraint optimization problems, the objective function may also need to be reformulated given a particular solver. For example, several CP-solvers only support minimizing the value of a single variable, while ILP-solvers only support weighted linear objective functions. Therefore, we apply the same reformulations to the numerical objective function as we do for the constraints, before posting the objective function to a solver. The architecture of every transformation is designed such that it can take both Boolean and numerical expressions as input. 4.1. Eliminating Partial Functions Our constraint modeling language allows the use of global functions. These functions map a set of ‘input” variables to a single output variable. However, some of the global functions implemented in our system are ‘partial” functions, for which the output can be undefined (see Definition 2.3). Common examples of partial function constraints in constraint programming models are the division constraint (Div(x,y)=z Div(x,y)=z) and the Element constraint (written as X[i]=vX[i]=v). Indeed, division is undefined when (y=0)(y=0) and an array lookup is undefined when the index is out-of-bounds (i.e., i<1i<1 or i>|X|i> X ). When the domains of the variables in a partial function allow it to be undefined, we say the function is unsafe, and it should be safened. We handle undefinedness using the relational semantics for constraint modeling languages 34. That is, when the result of a numerical function is undefined, it asserts its nearest Boolean context to false. In the context of our modeling language, this means the nearest Boolean parent expression is asserted to be false. Both MiniZinc and Savile Row also implement the relational semantics for handling partial functions 57; 44. In Figure 3 we show different expression trees that contain a partial function, in this case Division. We focus on partial functions for which the nearest Boolean context is not top-level (e.g., Figures 2(c) and 2(d)). Indeed, solvers supporting top-level partial function constraints will exclude any unsafe value from the domains themselves, e.g., through root-level propagation for CP-solvers. =Divxxyyzz (a) Top-level =+Divxxyyddzz (b) Nested in ⟨⟩~ IntExpr ~ ∨ =Divxxyyzzpp (c) Nested in a disjunction ¬ =Divxxyyzz (d) Nested in a negation Figure 3. In Figure 2(a), the nearest Boolean context of the division is the top-level == constraint, so the model forbids y↦0y 0. The same holds for Figure 2(b), where the only intermediate parent is Sum (numerical). In Figure 2(c), the nearest Boolean context is the comparison within the top-level disjunction, so y↦0y 0 causes the left-hand side to evaluate to false, requiring p to be true. In Figure 2(d), the nearest Boolean context is the negation, allowing solutions where the division is false or where y↦0y 0. 4.1.1. Safening partial functions using guards The general idea of safening a nested partial function is to introduce a guard, which determines whether the partial function is defined or not, and to replace the argument that can cause the function to be undefined with a safe alternative. This guard is placed in conjunction with the nearest Boolean context 34. We observe that for our modeling framework, two kinds of guards can be needed, depending on the domain for which the partial function is defined. Both cases are discussed below. Case 1: Safening to a range of values The first type of partial functions is only defined for a contiguous range of values. We will use the array lookup function X[y]X[y] as an example, which is only defined when the index y∈y∈. Hence, a natural guard is (1≤y≤|X|)(1≤ y≤ X ). To safen the constraint, we introduce a new integer variable y∈y_safe∈, and we ensure the original decision variable y is equal to y_safe whenever the function is defined. Example 4.1 (Safening of an Element constraint). Consider the constraint (X[i]=v)∨p(X[i]=v) p. After safening, this constraint is reformulated as a conjunction of the constraints: (1) ((X[y]=v)∧(1≤y≤|X|))∨p ((X[y_safe]=v) (1≤ y≤ X ) ) p ∧ (2) (1≤y≤|X|)⇒(y=y) (1≤ y≤ X ) (y=y_safe) ∧ (3) y∈ y_safe∈ where constraint 1 is the original, safe constraint and 2 ensures the new index is equal to the original index variable whenever it is in the bounds of the array. Case 2: Excluding a single value from the domain The second type of partial functions are undefined for a single value in the domain of one of their arguments. Common examples are the Div(x,y) Div(x,y) and Modulo(x,y) Modulo(x,y) functions, which are both undefined when y=0y=0. A natural guard is y≠0y≠ 0. As our modeling language only allows integer variables with a contiguous domain (see Section 3), we need to model both sides of the domain around the excluded value separately. More specifically, we introduce two auxiliary variables y_neg and y_pos to represent the safe negative and positive parts of the domain of y, respectively. Example 4.2 (Safening a nested division constraint). Consider the unsafe constraint (Div(x,y)=v)∨p( Div(x,y)=v) p as introduced previously. After safening, this expression becomes a conjunction: (4) ((z=v)∧(y≠0))∨p ((z=v) (y≠ 0) ) p ∧ (5) (y<0)⇒(Div(x,y)=z∧y=y) (y<0) ( Div(x,y_neg)=z y=y_neg) ∧ (6) (y>0)⇒(Div(x,y)=z∧y=y) (y>0) ( Div(x,y_pos)=z y=y_pos) ∧ (7) y∈∧y∈ y_neg∈ y_pos∈ Where constraint 4 is the original, but now safe constraint; and constraints 5 and 6 ensure the auxiliary variables are asserted to the original y when y takes a value that is different from 0; and that the division constraint holds. 4.2. Eliminating negation After eliminating partial functions, we focus on eliminating negation from the expression tree. More specifically, we traverse the expression tree and ‘push down” any ¬ operator into its arguments. For this, we follow a set of standard simplification rules. To rewrite the negation of a comparison, we can simply replace the comparison with its negative counterpart. That is, == is mapped to ≠, ≤ to >> and << to ≥. For logical operators, we follow De Morgan’s laws 27: ¬(a∧b) (a b) is simplified to (¬a)∨(¬b)( a) ( b), ¬(a∨b) (a b) to (¬a)∧(¬b)( a) ( b), and ¬(a⇒b) (a b) to a∧(¬b)a ( b). When a or b is an expression, negation is further eliminated recursively. Finally, negating global constraints is non-trivial, and no generic system exists for (efficiently) negating them. However, for some global constraints, it is possible to define their negation in terms of other global constraints, as observed by 30. Below is a non-exhaustive list of constraint reformulations for negated global constraints as implemented in our system: • ¬Table(X,T) Table(X,T) is mapped to NegativeTable(X,T) NegativeTable(X,T) • ¬AllDifferent(X) AllDifferent(X) is mapped to NValue(X)<|X| NValue(X)< X • ¬Regular(X,N,T,s,A) Regular(X,N,T,s,A) is mapped to Regular(X,N,T,s,N∖A) Regular(X,N,T,s,N A) for complete automata • ¬Xor(x1,x2,…,xn) Xor(x_1,x_2,…,x_n) is mapped to Xor(¬x1,x2,…,xn) Xor( x_1,x_2,…,x_n) For global constraints where no specialized negation is implemented, we keep the negated global constraint in the expression tree. This is shown in Section 4.2, where all negation operators are eliminated, apart from negated Boolean variables and negated global constraints. Note that no transformations further down the transformation stack are allowed to explicitly introduce the negation of an expression. E.g., when the decomposition of a global constraint requires negating one of its arguments, that negation operator must immediately be eliminated using the transformation described in this section. For example, the decomposition of IfThen(x≤y,z=2,z=3) IfThen(x≤ y,z=2,z=3) is (x≤y)⇒(z=2),¬(x≤y)⇒(z=3))\(x≤ y) (z=2), (x≤ y) (z=3))\. The latter of these constraints is then further rewritten as (x>y)⇒(z=3)(x>y) (z=3) to eliminate the negation operator from the new expression. Grammar 2 Boolean expressions after eliminating negation. <BoolExpr> ::= | <Bool> | <BoolVar> | ¬ <BoolVar> | <BoolExpr> ∧ | ∨ | ⇒ | ⇔ <BoolExpr> | <IntExpr> ≤ | < | ≥ | > | == | ≠ <IntExpr> | <GlobalConstraint> [ <Arg> (, <Arg>)* ] | ¬ <GlobalConstraint> [ <Arg> (, <Arg>)* ] 4.3. Decomposing unsupported global constraints and functions Our constraint modeling language supports the use of global constraints 62; 12 to model constraint satisfaction or optimization problems. However, not all solvers support (all) global constraints. Indeed, while most CP-solvers support a variety of global constraints and functions, SMT or ILP solvers rarely support them (apart from some common functions such as Min or ˛). Hence, for all solvers, the unsupported global constraints and functions must be decomposed before posting the model to the solver. Note that in our language, global constraints can be used as any other Boolean expression, and thus they can occur as a nested expression in the model. However, CP-solvers typically do not support such arbitrary nesting of global constraints. Instead, they only support using the global constraints at the ‘top-level” of the constraint model, where the solver will maintain its satisfaction during search. Hence, we define two general types of ‘supportedness” of global constraints: they are either supported at the top-level, or supported as a nested expression. Each solver interface is configured using two sets, Supp and SuppNested, that list the set of global constraints supported at the top-level and in a nested context, respectively. In this transformation, we avoid decomposing the same global constraint or global function multiple times by keeping a cache of decomposed expressions. This generally reduces the number of expressions and auxiliary variables in the decomposed constraint model. While it may be uncommon for a user to write the exact same global constraint twice, decompositions or other reformulations may introduce the same expression in various places. 4.3.1. Decomposing top-level global constraints Each solver will support a subset of global constraints that are supported at the ‘top-level” of the constraint model. This is the most common case where global constraints occur: e.g., AllDifferent constraints in allocation problems or Cumulative constraints in many scheduling problems. Any top-level global constraint that is not listed in Supp, will need to be decomposed into a conjunction of expressions that is equivalent to the original global constraint. For example, given a constraint solver that does not support the constraint AllDifferent(x,y,z) AllDifferent(x,y,z), we can replace it with the conjunction (x≠y)∧(x≠z)∧(y≠z)(x≠ y) (x≠ z) (y≠ z). However, note that global constraints may be decomposed into other global constraints. This means that we need to recursively check whether all unsupported global constraints and functions are eliminated. An example is the decomposition of the GlobalCardinalityCount constraint, as shown in Figure 4, which is decomposed using Count functions. GlobalCardinality((x,y,z),(7,9),(c1,c2)) GlobalCardinality((x,y,z),(7,9),(c_1,c_2))Count((x,y,z),7)=c1 Count((x,y,z),7)=c_1(x=7)+(y=7)+(z=7)=c1(x=7)+(y=7)+(z=7)=c_1Count((x,y,z),9)=c2 Count((x,y,z),9)=c_2(x=9)+(y=9)+(z=9)=c2(x=9)+(y=9)+(z=9)=c_2c1+c2≤3c_1+c_2≤ 3 Figure 4. Decomposing the GlobalCardinalityCount constraint into two global functions, which are in turn decomposed into nested arithmetic constraints. As we will discuss in this section, some global constraints require the introduction of auxiliary variables to formulate the relation represented by the constraint. Following 11, our framework returns two sets of constraints as the decomposition of a global constraint G()G(X): a set of defining constraints (,)T(X,A) and a set of value constraint(s) (,)V(X,A). The defining constraints determine the value of the auxiliary variables A, using the decision variables X. The value constraints represent the truth value of the global constraint. Note that this decomposition scheme is compatible with decomposing global functions as well. Indeed, while for global constraints, the value constraint is a set of constraints representing a single Boolean-valued conjunction, for global functions it is an integer-valued expression. Example 4.3 (Decomposition of Min using an auxiliary variable). Consider the constraint Min(x,y,z)≥3 Min(x,y,z)≥ 3. If the solver does not support the global function Min, we decompose it using an auxiliary variable m. More specifically, the defining constraints become (x,y,z,m)=(m≤x)∧(m≤y)∧(m≤z)∧((m≥x)∨(m≥y)∨(m≥z))T(\x,y,z\,\m\)= (m≤ x ) (m≤ y ) (m≤ z ) ((m≥ x) (m≥ y) (m≥ z) ) and the value expression is the auxiliary variable: (x,y,z,m)=mV(\x,y,z\,\m\)=m. As part of the decomposition procedure, the value expression m is put in place of the original Min constraint: m≥3m≥ 3. Example 4.4 (Decomposition of MDD using auxiliary variables). Consider the following MDD constraint: MDD((x,y),(S,1,A),(S,2,B),(A,1,F),(B,1,F),(B,2,F),F) MDD((x,y),(S,1,A),(S,2,B),(A,1,F),(B,1,F),(B,2,F),F) with starting node S and accepting state F. This constraint is satisfied if the paths defined by the transitions of the MDD represent an accepting path through the MDD. The decomposition uses a Boolean edge variable ⟦X→Y⟧ X \!i\!Y for each edge X→YX→ Y with label i in the MDD; and enforces a ‘flow” to the accepting state 3. Its defining and value constraints are: E= E= ⟦S→A⟧,⟦S→B⟧,⟦A→F⟧,⟦B→F⟧,⟦B→F⟧ ~\ S \!1\!A , S \!2\!B , A \!1\!F , B \!1\!F , B \!2\!F \ (x,y,E)= (\x,y\,E)= ((x=1)⇔⟦S→A⟧)∧((x=2)⇔⟦S→B⟧)∧ ~ ((x=1) S \!1\!A ) ((x=2) S \!2\!B ) ((y=1)⇔⟦A→F⟧∨⟦B→F⟧)∧((y=2)⇔⟦B→F⟧)∧ ~ ((y=1) A \!1\!F B \!1\!F ) ((y=2) B \!2\!F ) (⟦S→A⟧=⟦A→F⟧)∧ ~ ( S \!1\!A = A \!1\!F ) (⟦S→B⟧=⟦B→F⟧+⟦B→F⟧) ~ ( S \!2\!B = B \!1\!F + B \!2\!F ) (x,y,E)= (\x,y\,E)= (⟦S→A⟧+⟦S→B⟧=1)∧ ~ ( S \!1\!A + S \!2\!B =1 ) (⟦A→F⟧+⟦B→F⟧+⟦B→F⟧=1) ~ ( A \!1\!F + B \!1\!F + B \!2\!F =1 ) SSAABBFFxxyy12112 Here, the channeling constraints determine the value of the auxiliary variables and the consistency of flow are the defining constraints, and the constraints enforcing that there is a non-zero flow from the starting node to the accepting state are the value constraints. While the auxiliary variables cannot be avoided in the previous two examples to reformulate the constraint, for many decompositions, we can circumvent explicitly introducing auxiliary variables in the decomposition. Avoiding introduction of functionally defined auxiliary variables For many decompositions, the auxiliary variables used in the decomposition are functionally defined by the user-defined decision variables. In general, we try to avoid explicitly introducing auxiliary variables that represent a subexpression used in the decomposition. Instead, we use the subexpression itself as an argument to build the complex expression that represents the decomposition. We will call this the functional form of decomposing global constraints. Example 4.5 (Functional decomposition of ArgMin). Consider the following naive decomposition of the constraint ArgMin(X,i) ArgMin(X,i): (X[i]=w)∧(Min(X)=v)∧(w=v)(X[i]=w) ( Min(X)=v) (w=v) 10. This decomposition introduces two auxiliary variables w and v, to define the relation. However, their value is functionally defined. An equivalent reformulation which avoids the explicit use of auxiliary variables is (X[i]=Min(X))(X[i]= Min(X)). Solvers that support nested expressions will benefit from an explicitly nested structure. For other solvers, the flattening will introduce the auxiliary variables automatically, but it will use Common Subexpression Elimination (CSE) to avoid creating duplicates and will compute tight bounds on the variables automatically. This scheme is also compatible with the decomposition of global functions, as the following example shows. Example 4.6 (Decomposing NValue). The standard decomposition for the constraint NValue(x,y,z)=n NValue(x,y,z)=n introduces a Boolean variable Bv=iB_v=i for each of the domain values x,yx,y and z 14. The decomposition then enforces the constraints: ∀v∈x,y,z∀i∈Dv:Bv=i⇔(v=i)∀ v∈\x,y,z\∀ i∈ D_v:B_v=i (v=i) and n=∑i∈Dx∪Dy∪Dz(Bx=i∨By=i∨Bz=i)n= _i∈ D_x∪ D_y∪ D_z(B_x=i B_y=i B_z=i). However, it is easier to formulate the decomposition over the subexpressions directly, which avoids explicitly introducing any auxiliary variables at this stage: n=∑i∈Dx∪Dy∪Dz((x=i)∨(y=i)∨(z=i))n= _i∈ D_x∪ D_y∪ D_z((x=i) (y=i) (z=i)). Avoiding the introduction of auxiliary variables at decomposition time has several advantages. First, it reduces the overall number of variables for solvers that support nested expressions (see Section 4.4). Indeed, some solvers (e.g., most SMT-solvers) directly support the nested constraints as shown in the example. Secondly, given the ArgMin constraint from Example 4.5, it is not unthinkable that the user will use the expression X[i]X[i] elsewhere in the constraint model – say in constraint C2C_2. If at some point in the transformation stack, an auxiliary variable is made for this other occurrence in the model (e.g., during flattening of C2C_2), then it can be used to replace the subexpression in the decomposition as well. Hence, by postponing the introduction of auxiliary variables as long as possible in the transformation stack, we can localize all CSE-logic into the flattening transformation and potentially enable more opportunities to do CSE 50. ILP-friendly decompositions When reformulating a CSP for an Integer Linear Programming (ILP) solver, virtually all global constraints in the model must be decomposed. Indeed, apart from occasional support for numerical global functions such as Min or ˛constraints, ILP solvers typically only support linear inequalities as input language. Standard ‘CP-style” decompositions of global constraints are often unsuited for ILP solvers. A prime example is the AllDifferent constraint, whose standard decomposition is a set of n(n−1)n(n-1) binary disequality constraints 64. However, to linearize disequality constraints, we need to use big-M style constraints (see Section 4.5), which are generally unwanted for performant ILP models. 13 proposes that many global constraints can instead be decomposed in an ‘ILP-friendly” way. These specialized decompositions (implicitly) use a Boolean encoding variable Bx=vB_x=v to represent that a categorical variable x is assigned to value v. Below, we show several examples of such decompositions. Example 4.7 (ILP-friendly flow decomposition of AllDifferent). Given the constraint AllDifferent(X) AllDifferent(X) with a set of integer variables X, the flow-based decomposition is ⋀v∈..∑xi∈X(xi=v)≤1 _v∈lb..ub _x_i∈ X(x_i=v)≤ 1 Example 4.8 (ILP-friendly decomposition of Element). Given an array A of integer constants, and an index variable i the constraint A[i]=vA[i]=v can be decomposed as the linear constraint ∑j=1..|A|aj×(i=j)=v _j=1.. A a_j×(i=j)=v. The linear relaxation of this constraint ensures the bounds of variable v are [(A),(A)][min(A),max(A)]. Our framework currently implements specialized linear decompositions for AllDifferent, Element, Table, Regular and Circuit constraints. Interestingly, by avoiding explicitly creating auxiliary variables when decomposing global constraints, several CP-style decompositions already work well for ILP solvers, as they are further processed by the linearize transformation down the transformation stack. For example, we decompose the function Count(X,v) Count(X,v) as ∑x∈X(x=v) _x∈ X(x=v) for all solvers. When targeting a CP-solver, our transformation pipeline will introduce Boolean variables Bx=vB_x=v used in ∑x∈XBx=v _x∈ XB_x=v and reification constraints Bx=v⇔(x=v)B_x=v (x=v). For ILP solvers, the decomposition will be the same ∑x∈XBx=v _x∈ XB_x=v but the direct encodings Bx=vB_x=v can be done in a more ILP-friendly way. Section 4.5 further elaborates on the implementation of this feature. 4.3.2. Decomposing nested global constraints We now focus on the case of fully reified global constraints, but the techniques are valid for any nesting of global constraints in Section 3. When introducing auxiliary variables to decompose a nested global constraint, we need to ensure their value is at all times functionally defined by the decision variables 11. That is, given any value to the decision variables, there is exactly one satisfying assignment to the auxiliary variables. We say the auxiliary variables are totally defined by the decision variables. In practice, this means the defining constraints (,)T(X,A) must represent a total function, written as F(,)T_F(X,A), which can and should be enforced at the top-level of the constraint model: b ⇔G()G(X) ≡ F(,)T_F(X,A) ∧b ⇔(,)V(X,A) Indeed, enforcing the definition of auxiliary variables as part of the nested expression is not valid, as shown in the following example. Example 4.9 (Invalid decomposition of a reified constraint using auxiliary variables). Consider the constraint b⇔Count((x,y,z),1)≤2b Count((x,y,z),1)≤ 2, which enforces that the number of occurrences of the value 11 is at most two, if and only if b is true. An invalid decomposition would be b⇔((x=1)+(y=1)+(z=1)=c∧c≤2)b ((x=1)+(y=1)+(z=1)=c c≤ 2). Indeed, the assignment b↦false,x↦1,y↦2,z↦3,c↦3\b false,x 1,y 2,z 3,c 3\ satisfies the reformulation, but clearly does not satisfy the original reified constraint: the Boolean reification variable is false, but the original comparison with the Count constraint on the right-hand side is satisfied by the assignment. For this example of the Count constraint, it is easy to see that the auxiliary variable c is functionally defined by the variables x,yx,y, and z. However, for other decompositions, this is less trivial, as the value of the auxiliary variables is defined through several constraint, as shown in the following example of a reified MDD constraint. Example 4.10 (Decomposition of a reified MDD constraint). Consider again the constraint from Example 4.4, but now as a reification: b⇔MDD((x,y),(S,1,A),(S,2,B),(A,1,F),(B,1,F),(B,2,F),F)b MDD((x,y),(S,1,A),(S,2,B),(A,1,F),(B,1,F),(B,2,F),F). Our previous decomposition is not suited to decompose this reified MDD constraint. Indeed, the assignment b↦false,x↦3,y↦2\b false,x 3,y 2\ is not allowed by the decomposition introduced in the previous example, as it enforces variables x and y to take either value 1 or 2. To circumvent this issue, the MDD must be expanded with a ‘garbage state” G for each layer in the MDD. This allows to include all remaining domain values from each of the nodes. For Dx=Dy=D_x=D_y= we get: E= E=\ ⟦S→A⟧,⟦S→B⟧,⟦A→F⟧,⟦B→F⟧,⟦B→F⟧, S \!1\!A , S \!2\!B , A \!1\!F , B \!1\!F , B \!2\!F , ⟦S→Gx⟧,⟦A→Gy⟧,⟦A→Gy⟧,⟦B→Gy⟧, [rgb]0,0,1 S \!3\!G_x , [rgb]0,0,1 A \!2\!G_y , A \!3\!G_y , [rgb]0,0,1 B \!3\!G_y , ⟦Gx→Gy⟧,⟦Gx→Gy⟧,⟦Gx→Gy⟧ [rgb]0,0,1 G_x \!1\!G_y , G_x \!2\!G_y , G_x \!3\!G_y \ F(x,y,E)= _F(\x,y\,E)= ((x=1)⇔⟦S→A⟧)∧ ((x=1) S \!1\!A ) ((x=2)⇔⟦S→B⟧)∧ ((x=2) S \!2\!B ) ((x=3)⇔⟦S→Gx⟧)∧ [rgb]0,0,1 ((x=3) S \!3\!G_x ) ((y=1)⇔⟦A→F⟧∨⟦B→F⟧∨⟦Gx→Gy⟧)∧ ((y=1) A \!1\!F B \!1\!F [rgb]0,0,1 G_x \!1\!G_y ) ((y=2)⇔⟦B→F⟧∨⟦A→Gy⟧∨⟦Gx→Gy⟧)∧ ((y=2) B \!2\!F [rgb]0,0,1 A \!2\!G_y G_x \!2\!G_y ) ((y=3)⇔⟦B→Gy⟧∨⟦A→Gy⟧∨⟦Gx→Gy⟧)∧ [rgb]0,0,1 ((y=3) B \!3\!G_y A \!3\!G_y G_x \!3\!G_y ) (⟦S→A⟧=⟦A→F⟧+⟦A→Gy⟧+⟦A→Gy⟧)∧ ( S \!1\!A = A \!1\!F + [rgb]0,0,1 A \!2\!G_y + A \!3\!G_y ) (⟦S→B⟧=⟦B→F⟧+⟦B→F⟧+⟦B→Gy⟧)∧ ( S \!2\!B = B \!1\!F + B \!2\!F + [rgb]0,0,1 B \!3\!G_y ) (⟦S→Gx⟧=⟦Gx→Gy⟧+⟦Gx→Gy⟧+⟦Gx→Gy⟧) [rgb]0,0,1 ( S \!3\!G_x = G_x \!1\!G_y + G_x \!2\!G_y + G_x \!3\!G_y ) SSAABBGxG_xFFGyG_yxxyy1211,231,2,32,33 Now, all edge variables are uniquely defined given any value to the decision variables x and y. The value constraints can be kept as before, as they enforce a flow matching the MDD constraint. Indeed, if any blue edge is activated, the constraints below cannot be satisfied. (x,y,E)= (\x,y\,E)= (⟦S→A⟧+⟦S→B⟧=1)∧ ( S \!1\!A + S \!2\!B =1 ) (⟦A→F⟧+⟦B→F⟧+⟦B→F⟧=1) ( A \!1\!F + B \!1\!F + B \!2\!F =1 ) Note that much of the complexity of decomposing reified or nested global constraints as described in related works 10; 11; 30 can be avoided by not introducing auxiliary variables at all. Indeed, when the auxiliary variables can be defined directly using a simple expression, we adopt the functional form of writing the decomposition for a global constaint or function. For solvers that do not accept nested expressions, the flattening transformation described in Section 4.4 then handles all logic for introducing auxiliary variables and determining their value based on the decision variables. The example below shows how such a functional decomposition can simplify nested decompositions. Example 4.11 (Decomposing reified ArgMin constraint). Consider the reified constraint b⇔(ArgMin(X)=i)b ( ArgMin(X)=i). Using the naive decomposition with two auxiliary variables, the decomposition of the reification becomes: (X[i]=v)∧(Min(X)=w)∧(b⇔(v=w))(X[i]=v) ( Min(X)=w) (b (v=w) ) where the definition of v and w is enforced at top-level. However, by writing the decomposition functionally, we obtain b⇔(Min(X)=X[i])b ( Min(X)=X[i]), which makes the defining expression empty, and we can simply replace the nested global constraint with its (nested) value expression. As described previously, we can use specialized decompositions for some global constraints when targeting an ILP solver. More generally, we allow a solver to specify a set of ‘custom” decompositions, allowing solvers to deviate from the default decomposition for specific global constraints or functions. However, some of these decompositions, e.g., the decomposition of Circuit by 42, are only valid when the constraint is at the top-level of the constraint model, not when nested in another expression. Hence, when a Circuit constraint occurs in a nested context, we always decompose it using its ‘traditional CP” decomposition using order variables instead. We next describe how to detect and use the more efficient decomposition when possible. 4.3.3. Decomposing global constraints in positive context As discussed previously, our system supports arbitrary nesting of global constraints. We observe that for some nestings, the global constraint occurs in positive context in the expression tree. Common examples of such nesting are half-reified constraints 31 or constraints occurring in a disjunction 38. In such cases, the global constraint is never enforced to be false. Hence, when decomposing a global constraint in a nested positive context, we can simply re-use the decomposition as if the constraint were posted top-level (Section 4.3.1). Clearly, this is advantageous for many global constraints, as it avoids the requirement that auxiliary variables are functionally defined, and this can avoid extra variables and/or constraints, as Examples 4.4 and 4.10 have shown. Reformulation of half-reified global constraints As a final optimization to the decomposition transformation, we consider the case where a CP solver supports a global constraint at the top-level of the model, but not in a nested context. When the global constraint occurs in a positive context, 21 observed that one can avoid decomposing the global constraint, and instead introduce a set of auxiliary variables and a channeling constraint that uses the original (efficient) global constraint in a non-nested way. To illustrate this, consider the top-level constraint b⇒AllDifferent(x,y,z)b AllDifferent(x,y,z). If the solver does not support the AllDifferent constraint in a nested expression, but does support the top-level AllDifferent constraint (which is the case for most CP solvers), then we can reformulate the constraint as: AllDifferent(x′,y′,z′)∧(b⇒(x=x′∧y=y′∧z=z′)) AllDifferent(x ,y ,z ) (b (x=x y=y z=z )) where x′,y′x ,y and z′z are auxiliary variables. When the Boolean variable b is set to true, the reified channeling constraint ensures the auxiliary variables are equal to the original decision variables, and the global constraint is asserted to be true. When the indicator variable is set to false, the auxiliary variables are free, and the reformulation is valid as long as AllDifferent(x′,y′,z′) AllDifferent(x ,y ,z ) is satisfiable. This approach can be implemented generically for any global constraint, with several optimizations possible for functional or total relation constraints 21. Using the Supp and SuppNested configured for each solver, we can easily determine which global constraints to reformulate using this method. 4.4. Flattening by substituting expressions with auxiliary variables Many (CP) solvers do not accept nested expressions, but rather accept only flat constraints. That is, constraints where all arguments are either constants or variables (= leaf nodes in the expression tree). This step of the transformation pipeline is responsible for eliminating any subexpressions from the arguments of primitive operators and global constraints. This algorithm traverses the entire expression tree of the constraint model and substitutes any nested expression with a freshly introduced auxiliary variable. Then, the auxiliary variable is asserted to be equal to the subexpression it replaces, which is implemented in the helper function GetOrMakeVar shown in Algorithm 2. For Boolean subexpressions, this results in a new reification constraint; for integer subexpressions, an equality constraint links the auxiliary variable with the subexpression it replaces. To avoid introducing unnecessary auxiliary variables, we implement two well-known optimizations: in-place simplification of operators and Common Subexpression Elimination (CSE) over normalized expressions. An implementation with a CSE-map and simplify procedure is shown in Algorithm 1, where F collects the flat constraints and C′C those that have to be recursively flattened. The algorithm first tries to simplify the expression by checking its immediate subexpressions and merging/rewriting associative operators. It then checks if it is already in flat normal form; it then normalizes reifications, comparisons, negated global constraints, and other Boolean expressions to the flat normal form described in Section 4.4. This normalization iterates over the arguments of a subexpression and replaces any subexpression with a fresh auxiliary variable. The pseudocode for NormalizeBoolExpr and NormalizeNumExpr is shown in Appendix A. Algorithm 1 Flatten(C, csemap) 1: Input: set of constraints C, CSE map csemap 2: Output: set of flat constraints 3: F←∅F← ; C′←∅C ← 4: for c∈Cc∈ C do 5: c←SimplifyOperators(c)c← SimplifyOperators(c) 6: if c is a ⟨⟩~ FnfBoolExpr ~ then 7: F←F∪cF← F∪\c\ continue 8: if c is 1∘2expr_1 _2 with ∘∈⇔,⇒ ∈\ , \ then 9: 1′,d1←GetOrMakeVar(1,)expr_1 ,d_1← GetOrMakeVar(expr_1,csemap) 10: 2′,d2←NormalizeBoolExpr(2,)expr_2 ,d_2← NormalizeBoolExpr(expr_2,csemap) 11: F←F∪1′∘2′F← F∪\expr_1 _2 \ 12: C′←C′∪d1∪d2C ← C ∪ d_1∪ d_2 13: else if c is expr1∘2expr_1 _2 with ∘∈=,≠,<,>,≤,≥ ∈\=,≠,<,>,≤,≥\ then 14: 1′,d1←GetOrMakeVar(1,)expr_1 ,d_1← GetOrMakeVar(expr_1,csemap) 15: 2′,d2←NormalizeNumExpr(2,)expr_2 ,d_2← NormalizeNumExpr(expr_2,csemap) 16: F←F∪1′∘2′F← F∪\expr_1 _2 \ 17: C′←C′∪d1∪d2C ← C ∪ d_1∪ d_2 18: else if c is ¬ \,expr then ⊳ expr can only be a global constraint after eliminating negation 19: ′,d←NormalizeBoolExpr(′,)expr ,d← NormalizeBoolExpr(expr ,csemap) 20: F←F∪¬F← F∪\ \,expr\ 21: C′←C′∪dC ← C ∪ d 22: else⊳ other ⟨⟩~ BoolExpr ~ 23: c′,d←NormalizeBoolExpr(c,CLOSE,c ,d← NormalizeBoolExpr(c,csemap,) 24: F←F∪c′F← F∪\c \ 25: C′←C′∪dC ← C ∪ d 26: if C′≠∅C ≠ then F←F∪Flatten(C′,)F← F∪ Flatten(C ,csemap) 27: return F In-place simplifications operators A first optimization is to detect associative n-ary operators (+,−,∨,∧+,-, , ) being used as a subexpression to the same operator. For example, when a Sum constraint uses another Sum as a subexpression, they can clearly be merged, without introducing an auxiliary variable. While it is uncommon for users to explicitly write such nested sum constraints, they are often the result of previous transformations. Additional care is taken to turn a sum where at least one of the terms is a multiplication of a constant and a variable, into a weighted sum, as well as to merge nestings of weighted and unweighted sums into a single weighted sum. Example 4.12 (Nested Sum after decomposing Count). Consider the user-constraint 2a+Count(x,y,z,1)≥32a+ Count(\x,y,z\,1)≥ 3. If the solver does not support the Count constraint, it will be decomposed in-place by the previous transformation. This results in the expression 2a+((x=1)+(y=1)+(z=1))≥32a+((x=1)+(y=1)+(z=1))≥ 3. The simplification method at line 4 in Algorithm 1 will then merge the left-hand side of the sum constraint to a single weighted sum, instead of introducing an auxiliary variable for the decomposition of Count. Secondly, for Boolean operators ⇒ and ∨ and ∧ , we also apply distributivity and rewriting rules when they occur together. Table 2 lists all such simplification rules implemented in our flattening transformation. Table 2. Reformulation rules for nested ⇒,∨ , and ∧ operators to avoid unnecessary auxiliary variables Input Output a∨(b⇒c)a (b c) a∨¬b∨ca b c (a∨b)⇒c(a b) c (¬c⇒¬a)∧(¬c⇒¬b)( c a) ( c b) Input Output (a⇒b)⇒c(a b) c (¬c⇒a)∧(¬c⇒¬b)( c a) ( c b) (a∧b)⇒c(a b) c ¬a∨¬b∨c a b c Common Subexpression Elimination In constraint programming models, it is common to use a particular subexpression in multiple places in the model. During the flattening process, we generate new auxiliary variables for each subexpression we encounter. To avoid making duplicate variables, we keep a cache of already introduced auxiliary variables in a ‘Common Subexpression Elimination Map”, which we refer to as csemap. This map keeps track of which (sub)expression is related to which auxiliary variable. Hence, whenever a new variable needs to be introduced, we first check whether a variable for the expression already exists in the map. To avoid creating separate auxiliary variables for two expressions that are syntactically different but semantically equivalent, we normalize expressions into a normal form. The two simplest normalizations are that a comparison between a constant and an expression always has the constant on the right-hand side; and a multiplication between a constant and an expression has the constant as first argument. The in-place reformulation for associative operators is also performed as part of the normalization. We also implement normalization of expressions of the form ⟨⟩⟨⟩⟨⟩~ Intvar ~~ Comparison ~~ Constant ~. That is, all comparisons of this form are converted to either ⟨⟩=⟨⟩~ Intvar ~=~ Constant ~ or ⟨⟩≥⟨⟩~ Intvar ~≥~ Constant ~. For example, when flattening (x≠3)+y≤5(x≠ 3)+y≤ 5, we introduce a new Boolean variable to represent x=3x=3, say Bx=3B_x=3, and reformulate the constraint to ¬Bx=3+y≤5 B_x=3+y≤ 5. This approach also improves the linearization of categorical variables, as we will describe later in Section 4.5. Algorithm 2 GetOrMakeVar(,expr,csemap) 1: if expr is a variable then return ,∅expr, 2: ←Normalize()expr← Normalize(expr) 3: if ∈expr then 4: return .(),∅ csemap.get(expr), 5: if IsBoolExpr() IsBoolExpr(expr) then 6: v←()v () 7: d≔v⇔d v 8: else 9: v←((),())v (lb(expr),ub(expr)) 10: d≔v=d v=expr 11: .(,v) csemap.put(expr,v) 12: return v,dv,d Algorithm 2 shows the pseudocode for our lightweight implementation of common subexpression elimination 50. The resulting output is described in Section 4.4, and closely resembles the language most CP solvers accept in their API. That is, we allow linear expressions, clauses, global constraints, and global functions in a comparison. Note that each of these expressions can still occur in a reified context. The following two sections describe two additional post-flattening transformations that solvers can choose to activate or not. Grammar 3 Flat normal form <Model> ::= [ <FnfBoolExpr> (, <FnfBoolExpr>)* ], minimize= <Int> + <LinExpr> <Lit> ::= <BoolVar> | ¬ <BoolVar> <FnfBoolExpr> ::= | <PrimitiveExpr> | <Lit> ⇒ <PrimitiveExpr> | <Lit> ⇔ <PrimitiveExpr> <PrimitiveExpr> ::= | False | <Lit> (∨ <Lit>)* | <LinExpr> <Comparison> <Int> | <IntVar> <Comparison> <GlobalFunction> [ <FnfArg> (, <FnfArg>)* ] | <GlobalConstraint> [ <FnfArg> (, <FnfArg>)* ] | ¬ <GlobalConstraint> [ <FnfArg> (, <FnfArg>)* ] <LinExpr> ::= | <Var> (+ <Var>)* | <Int>×<Var> (+ <Int>×<Var>)* <Var> ::= <BoolVar> | <IntVar> <Comparison> ::= ≤ | < | ≥ | > | == | ≠ <FnfArg> ::= <Int> | <Var> | [ <FnfArg> (, <FnfArg>)* ] 4.4.1. Normalize global functions The flat normal form allows global functions to be used in arbitrary comparisons and in reified comparisons. E.g., the constraint b⇔max(x,y,z)≤pb (x,y,z)≤ p is a valid flat constraint. However, most CP-solvers don’t directly support such constraints. Indeed, reified global constraints are rarely supported, and global functions are typically not supported in arbitrary comparisons. Instead, solvers implement a separate global constraint MaxEqual((x,y,z),p) MaxEqual((x,y,z),p), which forces p to be the maximum value among variables x,y,zx,y,z. This transformation introduces a fresh auxiliary variable (again through GetOrMakeVar) for each global function that should be rewritten to a top-level equality constraint: F(X) ⟨Comparison ⟩ Y ≡ (F(X) = Y’) ∧(Y’ ⟨Comparison ⟩ Y) and b ⇔F(X) ⟨Comparison ⟩ Y ≡ (F(X) = Y’) ∧(b ⇔Y’ ⟨Comparison ⟩ Y) This latter reformulation was first proposed by 11 as a reformulation for reified total function constraints. Note that some non-equality comparisons are supported by CP-solvers for certain global functions. For example, the constraint NValue(X)≤c NValue(X)≤ c maps to the global constraint AtMostNValue(X,c) AtMostNValue(X,c), which is supported by several CP-solvers. Hence, the implementation for normalizing global functions is a separate modular transformation that accepts a list of global functions for which only equality is supported. Section 4.4.1 describes the resulting set of allowed constraints in case all global functions only support equality. Grammar 4 Primitive expressions after normalizing global functions <PrimitiveExpr> :: = | False | <Lit> (∨ <Lit>)* | <LinExpr> <Comparison> <Int> | <IntVar> == <GlobalFunction> [ <FnfArg> (, <FnfArg>)* ] | <GlobalConstraint> [ <FnfArg> (, <FnfArg>)* ] | ¬ <GlobalConstraint> [ <FnfArg> (, <FnfArg>)* ] 4.4.2. Reification to two implications In this second post-flatten transformation, we transform all reification constraints into a conjunction of two half-reification constraints for solvers that only support the latter. That is, for a reified constraint ⟨⟩⇔⟨⟩~ Lit ~ ~ PrimitiveExpr ~, we introduce two constraints ⟨⟩⇒⟨⟩~ Lit ~ ~ PrimitiveExpr ~ and ¬⟨⟩⇒¬⟨⟩ ~ Lit ~ ~ PrimitiveExpr ~. Note that the negations in the second half-reification are immediately passed to the eliminate negation transformation described in Section 4.2 to ensure everything remains in flat normal form. Additionally, as unsupported nested global constraints have already been decomposed before, introducing the negation of a supported nested global constraint at this stage in the transformation stack does not cause any issues, as the downstream solver supports nested (and hence also negated) global constraints (e.g., Choco 49). 5 describes the set of constraints allowed after this normalization step. For ILP, PB, and SAT solvers, we pass a flag to this transformation that keeps fully reified comparisons between an integer variable and a constant. More precisely, we allow ⟨⟩⇔⟨⟩⟨⟩⟨⟩~ Lit ~ ~ Intvar ~~ Comparison ~~ Int ~ constraints to remain. This allows for detecting integer variable encodings, which will benefit the ‘linearize” transformation described in the next section. Grammar 5 Flat Boolean expressions after normalizing reification. <FnfBoolExpr> ::= | <PrimitiveExpr> | <Lit> ⇒ <PrimitiveExpr> | <Lit> ⇔ <IntVar> <Comparison> <Int> 4.5. Linearization We now describe how to further transform a set of flat normal form expressions into a format suitable for ILP-solvers. The output of this transformation phase will also serve as input for further processing required for PB and SAT solvers, which we describe in Section 4.6 We will assume any global constraints not supported by the ILP solver at hand are already decomposed in previous stages, that all full-reification constraints (except for ⟨⟩⟨⟩⟨⟩~ Var ~~ Comparison ~~ Constant ~) have been split up into half-reifications, and that supported global functions are only used in compatible comparisons. E.g., ILP solvers like SCIP 2 and Gurobi 45 allow to post a Max-equality constraint and a limited set of other global operators and constraints. Disjunctions are trivially linearized by transforming to greater than 1 comparison, e.g., x∨y∨z≡x+y+z≥1x y z≡ x+y+z≥ 1. Strictly less-than and greater-than comparisons are eliminated by offsetting the right-hand side of the integer comparison with +1 and -1, respectively. This leaves us with disequality constraints between a linear expression and a constant, half-reified linear constraints, and fully-reified equals and not-equals comparisons between a variable and a constant. In the following two subsections we discuss how to linearlize these remaining constraints. Grammar 6 Linear normal form <Model> ::= [ <LinCons> (, <LinCons>)* ], minimize= <Int> + <LinExpr> <LinCons> ::= | False | <LinExpr> <Comparison> <Int> <LinExpr> ::= | <Var> (+ <Var>)* | <Int>×<Var> (+ <Int>×<Var>)* <Var> ::= <BoolVar> | <IntVar> <Comparison> ::= == | ≤ | ≥ 4.5.1. Linearization of half-reified linear inequality constraints We first consider implication constraints of the form ⟨⟩⇒⟨⟩≥⟨⟩~ Lit ~ ~ LinExpr ~≥~ Int ~. As a generalization for any linear expression, we will write such a constraint as b⇒∑i=1..nwixi≥vb _i=1..nw_ix_i≥ v in this section. Thus, we assume that the right-hand side of any half-reification in the output of the flat normal form in Section 4.4 is already linearized by rewriting unsupported comparisons or by rewriting disjunctions to a linear constraint, and we just focus on linearizing the half-reification itself. To linearize this constraint, we rely on a big-M reformulation 24. The main idea is to convert the expression above to M⋅¬b+∑i=1..nwixi≥vM· b+ _i=1..nw_ix_i≥ v. Here, M is a large integer constant that ensures the inequality is satisfied when b is false, regardless of the values assigned to decision variables xix_i. When b is true, the first term of the sum on the left-hand side of the inequality is 0, and the right-hand side of the half-reification is asserted to hold. 4.5.2. Linearization of disequality Constraints of the form x≠yx≠ y are reformulated using two half-reification constraints. That is, we linearize any disequality constraint by introducing an auxiliary Boolean variable b, and introduce the constraints b⇒x−y≤−1b x-y≤-1 and ¬b⇒x−y≥1 b x-y≥ 1. These constraints are then linearized using a big-M reformulation as described above. This results in two big-M constraints, one for each side of the disequality. 4.5.3. Encoding categorical integer variables During flattening, we introduce an auxiliary Boolean variable for any comparison that is used as a subexpression in a constraint. E.g., after decomposing, Count((x,y,z),3)=1 Count((x,y,z),3)=1 to (x=3)+(y=3)+(z=3)=1(x=3)+(y=3)+(z=3)=1, it is flattened to a1+a2+a3=1,a1⇔(x=3),a2⇔(y=3),a3⇔(z=3)\a_1+a_2+a_3=1,a_1 (x=3),a_2 (y=3),a_3 (z=3)\. Such structures are common when integer variables are used as categorical variables, and each integer value represents an item of an enumerated type 58. Naively linearizing each of the reification constraints separately would introduce 4 big-M constraints for each reification. Indeed, let’s consider the first constraint a1⇔(x=3)a_1 (x=3). This requires two big-M constraints to model the half-reifications a1⇒x≤3a_1 x≤ 3 and a1⇒x≥3a_1 x≥ 3, and another two big-M constraints, and an auxiliary variable to linearize ¬a1⇒x≠3 a_1 x≠ 3: a1⇔(x=3)≡(a1⇒(x≤3))∧(a1⇒(x≥3))∧(¬a1⇒(x≠3)) a_1 (x=3)≡ (a_1 (x≤ 3) ) (a_1 (x≥ 3) ) ( a_1 (x≠ 3) ) and a1⇒(x≤3) a_1 (x≤ 3) ≡M1¬a1+x≤3 ≡ M_1 a_1+x≤ 3 a1⇒(x≥3) a_1 (x≥ 3) ≡M2¬a1+x≥3 ≡ M_2 a_1+x≥ 3 ¬a1⇒(x≠3) a_1 (x≠ 3) ≡(¬a1⇒(b⇒x≤2))∧(¬a1⇒(¬b⇒x≥4)) ≡ ( a_1 (b x≤ 2) ) ( a_1 ( b x≥ 4) ) ≡(¬a1⇒(M3¬b+x≤2))∧(¬a1⇒(M4b+x≥4)) ≡ ( a_1 (M_3 b+x≤ 2) ) ( a_1 (M_4b+x≥ 4) ) ≡(M5a1+M3¬b+x≤2)∧(M6a1+M4b+x≥4) ≡ (M_5a_1+M_3 b+x≤ 2 ) (M_6a_1+M_4b+x≥ 4 ) As these Big-M constraints can hurt performance in ILP solvers due to their weak linear relaxation, this is to be avoided. Instead, we wish to detect and use the direct encoding for integer variables whenever a categorical integer variable is used. That is, instead of linearizing the expression a1⇔(x=3)a_1 (x=3), we encode the variable x as 1⋅⟦x=1⟧+2⋅⟦x=2⟧+3⋅a1+4⋅⟦x=4⟧+5⋅⟦x=5⟧=x1· x=1 +2· x=2 +3· a_1+4· x=4 +5· x=5 =x. Notice that we do not introduce another variable ⟦x=3⟧ x=3 , but simply reuse the already introduced variable a1a_1 to represent that x is equal to 3. In practice, this involves iterating over the csemap and extracting all auxiliary Boolean variables that map to an expression of the form ⟨⟩=⟨⟩~ IntVar ~=~ Int ~. We allow the user to set the minimum number of values before the direct encoding is created; by default, this is set to 2. We implement a similar optimization for integer variables that occur frequently in a ≤ comparison to a constant. That is, given enough ⟨⟩≥⟨⟩~ IntVar ~≥~ Int ~ expressions for the same integer variable in the csemap, we encode the integer variable using its order encoding (see Section 4.6). This again avoids linearizing reified inequality constraints with Big-M constraints when such inequalities are used in logical constraints. An example of such a case is when using the time-decomposition of the Cumulative constraint 32. Currently, we eagerly select the direct encoding when for a single integer variable both ⟨⟩=⟨⟩~ IntVar ~=~ Int ~ and ⟨⟩≥⟨⟩~ IntVar ~≥~ Int ~ expressions are present. Future optimization could include encoding the integer variable twice and channeling the encodings to achieve better solving times 19. Note that most ILP solvers do not support negated Boolean variables (i.e., negative literals). Hence, as an additional transformation, we replace any literals ¬b b with (1−b)(1-b). This is trivial to do for linear constraints, as weighted terms of a sum can simply be multiplied by −1-1, and constants can be subtracted from the right-hand side of the comparisons. E.g., 3(¬x)+4y≥23( x)+4y≥ 2 can be rewritten to 3(1−x)+4y≥23(1-x)+4y≥ 2 and normalized to −3x+4y≥−1-3x+4y≥-1. 4.6. Encoding All Integer Variables as Boolean Literals To transform constraints in our language for (Pseudo-)Boolean solvers, all integer variables must be encoded into Boolean literals. For this, we reuse most of the modular transformation stack as done for ILP solvers, without the final conversion of negative to positive literals. We currently support the most common encodings: direct encoding 66, order encoding 59, and log-encoding (also known as binary encoding) 29. These are all implemented through a common interface with three main functionalities: (1) Encoding a term of the form ⟨⟩×⟨⟩~ Int ~×~ Var ~, (2) encoding a comparison of the form ⟨⟩⟨⟩⟨⟩~ Var ~~ Comparison ~~ Int ~ and (3) formulating the consistency constraints to ensure the encoding is valid. Direct encoding The direct encoding of integer variables introduces a Boolean literal for each of the values in the integer variable domain. To encode a term k×xk× x, we simply return the weighted sum k×∑i∈Dx(i×⟦x=i⟧)k× _i∈ D_x(i× x=i ) Encoding a == or ≠ constraint is as trivial as returning the matching Boolean literal, to encode a ≤ or ≥ constraint, we construct a conjunction of negative literals of the excluded part of the domain. To ensure the encoding is consistent, we add the constraint ∑i∈Dx⟦x=i⟧=1 _i∈ D_x x=i =1. This results in a total of |Dx| D_x literals. Order encoding The order (or thermometer) encoding of an integer variable uses a Boolean ‘inequality” variable for each value in the domain. That is, we introduce a literal ⟦x≥i⟧ x≥ i to represent that x is greater than or equal to the value i. Similar to the direct encoding, encoding a weighted term involves simply weighting each literal in the encoding: k×((x)+∑i∈⟦x≥i⟧)k×(lb(x)+ _i∈ x≥ i ). The encodings for ≤ and ≥ constraints are now a single literal, while == and ≠ constraints are encoded by first rewriting them to combinations of ≤ and ≥ constraints. To ensure consistency of the encoding, we require ⟦x≥i⟧⇒⟦x≥i−1⟧ x≥ i x≥ i-1 for all values i in DxD_x. This results in a total of |Dx|−1 D_x -1 literals. Log encoding The log encoding for integer variables is based on the binary representation of the value assigned to the integer. That is, we use a list of m Boolean literals, where ⟦(x,i)⟧ (x,i) is set to true if the offset binary representation of the value of x is set to true 56. To encode a term, we construct the sum ∑0..m−1(k×2i×⟦(x,i)⟧)+(x) _0..m-1(k× 2^i× (x,i) )+lb(x). Comparisons are encoded as-is, by using the above sum as the left-hand side in place of the integer variable. For consistency, we ensure the encoding is always smaller than or equal to the upper bound of the integer variable. This results in ⌈log2(|Dx|)⌉ _2( D_x ) literals to encode x. The output of the encoding step is a set of pseudo-Boolean constraints. Our modular encoding module allows for future improvements to this encoding step, for example, to use multiple encodings of the same integer variable depending on which types of constraints it is used in 19; 56. 4.7. To Conjunctive Normal Form (CNF) For SAT solvers, which require CNF input, we reuse the modular transformations as for Pseudo-Boolean solvers, except that in the linearisation transformation we indicate that half-reified constraints are supported and hence need not be encoded with Big-M constraints. After the transformation to Pseudo-Boolean, what is left to do is to rewrite the implications as disjunctions and to formulate the weighted linear constraints into CNF. This step has been well studied 41; 48; 17; 1, and in our framework, we use external libraries that implement this, such as PyPBlib 47 and Pindakaas 18. The to-CNF transformation allows indicating that unweighted sums (cardinality constraints) are supported and hence need not be encoded for SAT solvers that support this natively, such as Minicard 40. 5. Experimental results We use our implementation of the above transformations to investigate the following experimental questions. EQ1. How does the model for a finite domain constraint model change throughout the transformation stack? EQ2. What is the impact of the transformation optimizations on solving time for ILP, PB and SAT solvers? EQ2.1. What is the impact of using ILP-friendly decompositions for global constraints? EQ2.2. What is the effect of encoding categorical integer variables with a direct Boolean encoding? EQ2.3. What is the impact of using positive-only decompositions for global constraints? We consider all 250 instances of the COP track of the 2024 edition of the XCSP3 competition. These optimization models consider a wide variety of constraints, including global constraints and functions. The instances are parsed into CPMpy v1.0.0 using the built-in datasets and IO tools 54. To answer the second experimental question, we run these benchmark instances on three different solvers integrated in the framework: MIP solver Gurobi v.13.0.2 45, Pseudo-Boolean solver Exact v2.3.0 28, and MaxSAT solver RC2 via PySAT v1.9.dev5 37. All experiments were run on a single thread of an Intel(R) Xeon(R) Silver 4514Y and with a memory limit of 8GB. 5.1. EQ1: effect of transformation stack on constraint model In this first experimental question, we transform each of the instances in the benchmark set using the entire transformation stack as described in Section 4. Figure 5 shows the distribution of the number of constraints and variables after each step in the transformation stack. Note that both safening of partial functions and elimination of negation do not introduce any new constraints or variables into the model. Indeed, for the XCSP3 instances, all partial functions are at the top-level of the constraint model, and hence do not need to be safened before they are decomposed. For eliminating negation, we identify only one case where additional constraints can be introduced: namely, applying DeMorgan’s law of rewriting negated disjunctions. For the XCSP3 instances we considered, this rule was never applied, and hence no new constraints or variables were introduced by the transformation. As expected, decomposing global constraints introduced a large number of additional constraints and variables into the model. While in general we try to avoid introducing functionally defined variables as discussed in Section 4.3, for some global constraints and functions we are required to use auxiliary variables. During flattening, we introduce an auxiliary variable for each nested expression in the model. Hence, we notice a significant increase in both the number of variables and the number of constraints in the model in Figure 5. Clearly, a large number of these constraints are reification constraints for when Boolean expressions were used as subexpressions (e.g., as part of a decomposition). This is also confirmed by the resulting number of constraints after applying our detection algorithm for categorical variables (see Section 4.5.3). Indeed, after encoding all categorical variables, all constraints of the form ⟨⟩⇔⟨⟩⟨⟩⟨⟩~ Lit ~ ~ IntVar ~~ Comparison ~~ Int ~ are eliminated, and we instead post a single constraint that channels the integer variable to a Boolean encoding. Interestingly, as shown in Table 3, the number of Boolean variables increased by only a minor amount after constructing the Boolean encoding. This means that almost all values in the integer variable’s domain are already used in a variable-equals-value subexpression elsewhere in the model. Still, the average number of constraints is reduced by 63% for the models we tested. Note that the number of integer variables also slightly decreases after this transformation. Indeed, when interfacing to a purely Boolean solver, we do not post the channeling constraint between the Boolean encoding and the integer variable at this stage of the transformation stack. Hence, if an integer variable only occurs in reified comparisons with a constant, it will be removed from the model after encoding the categorical variables with a direct encoding. During linearization of the constraints, no new integer variables are introduced, as all linear constraints can easily be normalized by altering the coefficients of linear terms and/or by swapping comparisons. All constraints and Boolean variables introduced by this transformation are due to introducing big-M constraints for linearizing half-reified linear inequalities and encoding disequality constraints, as discussed in Section 4.5. In the final step of the transformation waterfall, we encode all integer variables with an appropriate Boolean encoding. Interestingly, both the number of constraints and Boolean variables increase only moderately compared to the linear formulation of the constraint model. Overall, we conclude that reformulating a high-level constraint model to a low-level formulation such as Pseudo-Boolean constraints can significantly increase the number of constraints and auxiliary variables, and that detecting categorical variables as part of the linearization transformation is essential to avoid an explosion in the number of constraints and Boolean variables during the final encoding step. Table 3. Average increase in number of top-level constraints and variables compared to the input and previous transformation stage. Top-level conjunctions are split into their individual arguments and counted as individual constraints. Number of constraints Number of integer variables Number of Boolean variables Compared to Input Previous Input Previous Input Previous Input ×1.0× 1.0 ×1.0× 1.0 ×1.0× 1.0 ×1.0× 1.0 ×1.0× 1.0 ×1.0× 1.0 No partial functions ×1.0× 1.0 ×1.0× 1.0 ×1.0× 1.0 ×1.0× 1.0 ×1.0× 1.0 ×1.0× 1.0 Eliminate negation ×1.0× 1.0 ×1.0× 1.0 ×1.0× 1.0 ×1.0× 1.0 ×1.0× 1.0 ×1.0× 1.0 Decompose global ×3.9× 3.9 ×3.9× 3.9 ×1.4× 1.4 ×1.4× 1.4 ×4.9× 4.9 ×4.9× 4.9 Flatten ×27.5× 27.5 ×7.0× 7.0 ×1.8× 1.8 ×1.3× 1.3 ×53.7× 53.7 ×11.1× 11.1 Detect categorical ×10.3× 10.3 ×0.4× 0.4 ×1.8× 1.8 ×1.0× 1.0 ×54.5× 54.5 ×1.0× 1.0 Linearize ×31.1× 31.1 ×3.0× 3.0 ×1.8× 1.8 ×1.0× 1.0 ×57.2× 57.2 ×1.1× 1.1 Integer to Boolean ×32.8× 32.8 ×1.1× 1.1 ×0.0× 0.0 ×0.0× 0.0 ×85.2× 85.2 ×1.5× 1.5 Figure 5. Cumulative distribution plots on the number of constraints (left), number of integer variables (center), and number of Boolean variables (right) after each stage in the transformation waterfall when interfacing to a pseudo-Boolean solver. 5.2. EQ2: impact of transformation optimizations on solve time for ILP, PB and SAT Solvers In this second experimental question, we evaluate the impact of the transformation optimizations described in Section 4 on the solving time of lower-level solvers. Figure 6 shows the runtime until proven optimal for the constraint optimization models in our benchmark. The time limit was set to 1h. We now discuss the effects of different optimizations for each solver. Integer Linear Programming solvers We first focus on the results for ILP solvers on the left-side of Figure 6. Here we generally notice a positive effect for any of the optimizations we implemented. Indeed, compared to the baseline (blue), using specialized positive decompositions improves the solving performance, as well as using specialized ILP-friendly decompositions that are known to have a good linear relaxation. Interestingly, this is even the case without automatically encoding the categorical variables using their direct encoding (Section 4.5.3). Note that Gurobi supports implication constraints in their API and does the big-M encoding of these constraints internally. Therefore, it is likely that Gurobi encodes some of the categorical variables itself when the solver detects it. Still, combining our own direct encoding for categorical variables, in combination with the ILP-friendly decompositions result in the most instances solved to optimality overall. Adding the specialized positive decompositions on top have little to no impact, as most ILP-friendly decompositions work in both positive and nested contexts. Pseudo-Boolean solvers Compared to the results for ILP solvers, the optimizations implemented in our pipeline have a smaller impact on the result for PB solvers. Indeed, even the combination of all optimizations perform only marginally better compared to the baseline. Note that Exact also supports to use an LP-solver during the solving process, which is used to solve the linear relaxation of the constraint model to provide (strong) bounds. When we allow the solver to spend 10% of the solving time in the LP-solver (lp = 0.1), the solving time is slightly improved when using all optimizations in our pipeline. Max-SAT solvers Finally, we discuss the results for Max-SAT solvers as shown on the right-hand side of Figure 6. A surprising result here is the negative impact of using ILP-friendly decompositions for global constraints. Indeed, especially in the absence of eagerly encoding categorical variables using a direct encoding, the solver performance degrades compared to the baseline CP-style decompositions. This is likely due to the large domains that can be induced by some ILP-friendly decompositions. For example, our pipeline rewrites constraint [10,20,30][i]≥r[10,20,30][i]≥ r to 10⟦i=1⟧+20⟦i=2⟧+30⟦i=3⟧=r′,r′≥r\10 i=1 +20 i=2 +30 i=3 =r ,r ≥ r\, the auxiliary variable r′r will have domain , and the direct encoding will make a Boolean literal for each of these domain values. Naturally, while the consistency constraints will exclude all except 10, 20 and 30 from its domain, the Boolean literals are still posted to the solver. Further optimizations to the transformation pipeline could include automatically detecting such cases and already shrinking the domain of r′r during the reformulation process. Overall, the current best combination is to use the eager encoding for categorical variables in combination with standard CP-style decompositions. Figure 6. Runtime to proven optimal solution when enabling different optimizations in the transformation pipeline. 6. Conclusion We presented a modular end-to-end transformation pipeline for finite-domain constraint models. It can target CP, SMT, ILP, PB, MaxSAT, and SAT solvers by incrementally rewriting high-level Boolean and integer expressions into the subset of the language supported by each solver. The pipeline is organized as a waterfall of reusable transformations: eliminating partial functions, eliminating negation, decomposing unsupported global constraints and functions, flattening nested expressions, linearizing constraints, encoding integer variables as Boolean literals, and translating pseudo-Boolean constraints to CNF as needed. The main challenges involved correctly preserving the semantics of negated and nested expressions, while avoiding unnecessary creation of auxiliary variables. In particular, partial functions must be safened before later transformations change their Boolean context and decompositions must remain valid when global constraints occur in nested contexts. To keep the reformulated models compact, we delayed the explicit introduction of auxiliary variables where possible, used functional decompositions for global functions and constraints, and applied common subexpression elimination and normalization throughout. We experimentally evaluated the transformation pipeline on 250 optimization instances from the XCSP3 competition. The results show that constraint models change substantially throughout the transformation stack, especially during decomposition, flattening, and linearization. We also observe that transformation optimizations are important for solving performance: ILP-friendly decompositions, direct encodings for categorical integer variables, and positive-context decompositions can significantly reduce model size and improve solving behavior for ILP, PB, and SAT-based backends. Future work can extend the input language, for example to floating-point decision variables. It can also improve individual transformations, such as normalization, half-reification-aware decompositions, and CSE, or investigate different hierarchical transformation architectures altogether. As the experimental results show, the encoding to (Max)SAT does not necessarily benefit from the same transformations as ILP/PB solvers. Hence, a more direct path from integer expressions, like PicatSAT 67 implements, could be of benefit. Finally, we notice a trend that more and more solvers support limited forms of nested expressions, for example nested affine transformations of integers for OR-Tools CP-SAT 46, nested integer expressions for Gurobi 13 45, and nested Boolean expressions for PySDD 25 and Paramita 5. This encourages further reducing the importance and work of the flatten step, which has been a central component of previous CP modeling languages. Acknowledgements. This research is partly funded by the European Research Council (ERC) under the EU Horizon 2020 research and innovation programme (Grant No 101002802, CHAT-Opt). Additionally, this research received funding from the framework of H.F.R.I call “4th Call for H.F.R.I.’s Research Projects to Support Postdoctoral Researchers” (H.F.R.I. Project Number: 28553). References Aavani (2011) A. Aavani Translating pseudo-boolean constraints into CNF. In SAT, Lecture Notes in Computer Science, Vol. 6695, p. 357–359. Cited by: §4.7. Achterberg et al. (2008) T. Achterberg, T. Berthold, T. Koch, and K. Wolter Constraint integer programming: a new approach to integrate cp and mip. In Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, L. Perron and M. A. Trick (Eds.), Berlin, Heidelberg, p. 6–20. External Links: ISBN 978-3-540-68155-7, Document Cited by: §4.5. Ahuja et al. (1993) R. K. Ahuja, T. L. Magnanti, and J. B. Orlin Network flows - theory, algorithms and applications. Prentice Hall. Cited by: Example 4.4. Akgün et al. (2022) Ö. Akgün, A. M. Frisch, I. P. Gent, C. Jefferson, I. Miguel, and P. Nightingale Conjure: automatic generation of constraint models from problem specifications. Artificial Intelligence 310, p. 103751. Cited by: §1, §1. Alòs et al. (2026) J. Alòs, C. Ansótegui, J. L. Esteban, and E. Torres Paramita: an extensible framework for satisfiability solving. In ModRef 2026, Cited by: §6. Audemard et al. (2024) G. Audemard, C. Lecoutre, and E. Lonca Proceedings of the 2024 XCSP3 competition. CoRR abs/2412.00117. Cited by: §1. Audemard et al. (2025) G. Audemard, C. Lecoutre, and E. Lonca Proceedings of the 2025 XCSP3 competition. CoRR abs/2511.06918. Cited by: §1. Barrett et al. (2010) C. Barrett, A. Stump, C. Tinelli, et al. The SMT-LIB standard: version 2.0. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK), Vol. 13, p. 14. Cited by: §3.1. Barrett et al. (2021) C. W. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli Satisfiability modulo theories. In Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, Vol. 336, p. 1267–1329. Cited by: §1, §3.1. Beldiceanu et al. (2012a) N. Beldiceanu, M. Carlsson, P. Flener, and J. Pearson On the reification of global constraints. Technical report Technical Report T2012:02. Cited by: Example 4.10, Example 4.5. Beldiceanu et al. (2013) N. Beldiceanu, M. Carlsson, P. Flener, and J. Pearson On the reification of global constraints. Constraints An Int. J. 18 (1), p. 1–6. Cited by: §4.3.1, §4.3.2, §4.4.1, Example 4.10. Beldiceanu et al. (2012b) N. Beldiceanu, M. Carlsson, and J. Rampon Global constraint catalog, (revision a). Swedish Institute of Computer Science. Cited by: §1, §4.3. Belov et al. (2016) G. Belov, P. J. Stuckey, G. Tack, and M. Wallace Improved linearization of constraint programming models. In CP, Lecture Notes in Computer Science, Vol. 9892, p. 49–65. Cited by: §1, §4.3.1. Bessiere et al. (2010) C. Bessiere, G. Katsirelos, N. Narodytska, C. Quimper, and T. Walsh Decomposition of the nvalue constraint. In International Conference on Principles and Practice of Constraint Programming, p. 114–128. Cited by: Example 4.6. Bessiere and Van Hentenryck (2003) C. Bessiere and P. Van Hentenryck To be or not to be… a global constraint. In International Conference on Principles and Practice of Constraint Programming, p. 789–794. Cited by: §2.1. A. Biere, M. Heule, H. van Maaren, and T. Walsh (Eds.) (2021) A. Biere, M. Heule, H. van Maaren, and T. Walsh (Eds.) Handbook of satisfiability - second edition. Frontiers in Artificial Intelligence and Applications, Vol. 336, IOS Press. Cited by: §1. Bierlee et al. (2025) H. Bierlee, J. J. Dekker, and P. J. Stuckey Revisiting pseudo-boolean encodings from an integer perspective. In CPAIOR (1), Lecture Notes in Computer Science, Vol. 15762, p. 113–133. Cited by: §4.7. [18] Pindakaas External Links: Link, Document Cited by: §4.7, §4. Bierlee et al. (2022) H. Bierlee, G. Gange, G. Tack, J. J. Dekker, and P. J. Stuckey Coupling different integer encodings for SAT. In CPAIOR, Lecture Notes in Computer Science, p. 44–63. Cited by: §4.5.3, §4.6. Bleukx et al. (2025) I. Bleukx, R. Boumazouza, T. Guns, N. Laage, and G. Povéda Modeling and explaining an industrial workforce allocation and scheduling problem. In CP, LIPIcs, Vol. 340, p. 6:1–6:24. Cited by: §1. Bleukx et al. (2026) I. Bleukx, H. Verhaeghe, D. Tsouros, and T. Guns Efficient reformulations of half-reified global constraints using auxiliary variables. J. Artif. Intell. Res.. Note: to appear Cited by: §4.3.3. Clautiaux et al. (2008) F. Clautiaux, A. Jouglet, J. Carlier, and A. Moukrim A new constraint programming approach for the orthogonal packing problem. Comput. Oper. Res. 35 (3), p. 944–959. Cited by: §1. Contaldo et al. (2020) F. Contaldo, P. Trentin, and R. Sebastiani From minizinc to optimization modulo theories, and back. In CPAIOR, Lecture Notes in Computer Science, Vol. 12296, p. 148–166. Cited by: §1. Dantzig (1963) G. B. Dantzig Linear programming and extensions. Princeton university press, Princeton (N.J.) (eng). External Links: LCCN 59-50559 Cited by: §4.5.1. Darwiche et al. (2017) A. Darwiche, P. Marquis, D. Suciu, and S. Szeider Recent trends in knowledge compilation (dagstuhl seminar 17381). Dagstuhl Reports 7 (9), p. 62–85. Cited by: §6. De Backer et al. (2000) B. De Backer, V. Furnon, P. Shaw, P. Kilby, and P. Prosser Solving vehicle routing problems using constraint programming and metaheuristics. J. Heuristics 6 (4), p. 501–523. Cited by: §1. De Morgan (1864) A. De Morgan "On the syllogism", no. i., "and on logic in general". Transactions of the Cambridge Philosophical Society 10 (1), p. 173– (eng). Cited by: §4.2. Devriendt (2023) J. Devriendt Exact solver. External Links: Link Cited by: §5. Ernst et al. (1997) M. D. Ernst, T. D. Millstein, and D. S. Weld Automatic sat-compilation of planning problems. In IJCAI, p. 1169–1177. Cited by: §4.6. Fages and Soliman (2012) F. Fages and S. Soliman Reifying global constraints. Ph.D. Thesis, INRIA. Cited by: §4.2, Example 4.10. Feydy et al. (2011) T. Feydy, Z. Somogyi, and P. J. Stuckey Half reification and flattening. In CP, Lecture Notes in Computer Science, Vol. 6876, p. 286–301. Cited by: §4.3.3. Feydy et al. (2009) T. Feydy, P. J. Stuckey, and M. Wallace Why cumulative decomposition is not as bad as it sounds. In Principles and Practice of Constraint Programming - CP 2009, 15th International Conference, CP 2009, Lisbon, Portugal, September 20-24, 2009, Proceedings, I. P. Gent (Ed.), Lecture Notes in Computer Science, Vol. 5732, p. 746–761. External Links: Document Cited by: §4.5.3. Foschini et al. (2026) M. Foschini, E. Gamba, L. Kletzander, and T. Guns From CP modeling to preference elicitation in HMLV assembly problems. In CP, LIPIcs. Note: to appear Cited by: §1. Frisch and Stuckey (2009) A. M. Frisch and P. J. Stuckey The proper treatment of undefinedness in constraint languages. In International Conference on Principles and Practice of Constraint Programming, p. 367–382. Cited by: §4.1.1, §4.1. Fromherz (2001) M. P. J. Fromherz Constraint-based scheduling. In ACC, p. 3231–3244. Cited by: §1. Hart et al. (2011) W. E. Hart, J. Watson, and D. L. Woodruff Pyomo: modeling and solving mathematical programs in python. Math. Program. Comput. 3 (3), p. 219–260. Cited by: §1. Ignatiev et al. (2018) A. Ignatiev, A. Morgado, and J. Marques-Silva PySAT: A python toolkit for prototyping with SAT oracles. In SAT, Lecture Notes in Computer Science, Vol. 10929, p. 428–437. Cited by: §5. Jefferson et al. (2010) C. Jefferson, N. C. A. Moore, P. Nightingale, and K. E. Petrie Implementing logical connectives in constraint programming. Artif. Intell. 174 (16-17), p. 1407–1429. Cited by: §4.3.3. Li and Manyà (2021) C. M. Li and F. Manyà MaxSAT, hard and soft constraints. In Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, Vol. 336, p. 903–927. Cited by: §1. Liffiton and Maglalang (2012) M. H. Liffiton and J. C. Maglalang A cardinality solver: more expressive constraints for free - (poster presentation). In SAT, Lecture Notes in Computer Science, Vol. 7317, p. 485–486. Cited by: §4.7. Marques-Silva and Lynce (2007) J. Marques-Silva and I. Lynce Towards robust CNF encodings of cardinality constraints. In CP, Lecture Notes in Computer Science, Vol. 4741, p. 483–497. Cited by: §4.7. Miller et al. (1960) C. E. Miller, A. W. Tucker, and R. A. Zemlin Integer programming formulation of traveling salesman problems. J. ACM 7 (4), p. 326–329. Cited by: Example 4.10. Nethercote et al. (2007) N. Nethercote, P. J. Stuckey, R. Becket, S. Brand, G. J. Duck, and G. Tack MiniZinc: towards a standard cp modelling language. In International Conference on Principles and Practice of Constraint Programming, p. 529–543. Cited by: §1, §1. Nightingale (2022) P. Nightingale Savile row manual. CoRR abs/2201.03472. Cited by: §1, §4.1. Optimization (2026) G. Optimization Gurobi Optimizer Reference Manual. External Links: Link Cited by: §4.5, §5, §6. Perron and Furnon (2022) OR-tools Google. External Links: Link Cited by: §6. Philipp and Steinke (2015) T. Philipp and P. Steinke PBLib – a library for encoding pseudo-boolean constraints into CNF. In Theory and Applications of Satisfiability Testing – SAT 2015, M. Heule and S. Weaver (Eds.), Lecture Notes in Computer Science, Vol. 9340, p. 9–16. External Links: ISBN 978-3-319-24317-7, Document Cited by: §4.7, §4. Prestwich (2021) S. D. Prestwich CNF encodings. In Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, Vol. 336, p. 75–100. Cited by: §4.7. Prud’homme et al. (2016) C. Prud’homme, J. Fages, and X. Lorca Choco solver documentation. TASC, INRIA Rennes, LINA CNRS UMR 6241, p. 102–106. Cited by: §4.4.2. Rendl et al. (2008) A. Rendl, I. P. Gent, and I. Miguel Eliminating common subexpressions during flattening. URL: http://w-circa. mcs. st-and. ac. uk/Preprints/ERCIMCSE08. pdf. Cited by: §4.3.1, §4.4, §4. F. Rossi, P. van Beek, and T. Walsh (Eds.) (2006) F. Rossi, P. van Beek, and T. Walsh (Eds.) Handbook of constraint programming. Foundations of Artificial Intelligence, Vol. 2, Elsevier. External Links: Link, ISBN 978-0-444-52726-4 Cited by: §1, §2. Roussel and Manquinho (2021) O. Roussel and V. Manquinho Pseudo-boolean and cardinality constraints. In Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, Vol. 336, p. 1087–1129. Cited by: §1. Schwerin and Wäscher (1997) P. Schwerin and G. Wäscher The bin-packing problem: a problem generator and some numerical experiments with ffd packing and mtp. International transactions in operational research 4 (5-6), p. 377–389. Cited by: §1. Sergeys et al. (2026) T. Sergeys, I. Bleukx, and T. Guns Unified programmatic access to co benchmarks, to connect constraint solving communities. In SAT, LIPIcs. Note: to appear Cited by: §5. Smith (2006) B. M. Smith Modelling. In Handbook of Constraint Programming, F. Rossi, P. van Beek, and T. Walsh (Eds.), Foundations of Artificial Intelligence, Vol. 2, p. 377–406. External Links: Link, Document Cited by: §2.1. Soh et al. (2015) T. Soh, M. Banbara, and N. Tamura A hybrid encoding of CSP to SAT integrating order and log encodings. In ICTAI, p. 421–428. Cited by: §4.6, §4.6. Stuckey and Tack (2013) P. J. Stuckey and G. Tack MiniZinc with functions. In CPAIOR, Lecture Notes in Computer Science, Vol. 7874, p. 268–283. Cited by: §3.2, §4.1. Stuckey and Tack (2022) P. J. Stuckey and G. Tack Enumerated types and type extensions for minizinc. In CPAIOR, Lecture Notes in Computer Science, Vol. 13292, p. 374–389. Cited by: §4.5.3. Tamura et al. (2009) N. Tamura, A. Taga, S. Kitagawa, and M. Banbara Compiling finite linear CSP into SAT. Constraints An Int. J. 14 (2), p. 254–272. Cited by: §1, §4.6. van Beek and Chen (1999) P. van Beek and X. Chen CPlan: A constraint programming approach to planning. In AAAI/IAAI, p. 585–590. Cited by: §1. Van Hentenryck and Michel (2014) P. Van Hentenryck and L. D. Michel Domain views for constraint programming. In CP, Lecture Notes in Computer Science, p. 705–720. Cited by: §2.2. van Hoeve and Katriel (2006) W. van Hoeve and I. Katriel Global constraints. In Handbook of Constraint Programming, F. Rossi, P. van Beek, and T. Walsh (Eds.), Foundations of Artificial Intelligence, Vol. 2, p. 169–208. External Links: Document Cited by: §4.3. van Hoeve and Régin (2006) W. van Hoeve and J. Régin Open constraints in a closed world. In CPAIOR, Lecture Notes in Computer Science, Vol. 3990, p. 244–257. Cited by: §2.2. van Hoeve (2001) W. van Hoeve The AllDifferent constraint: A survey. CoRR cs.PL/0105015. Cited by: §4.3.1. Vielma (2015) J. P. Vielma Mixed integer linear programming formulation techniques. SIAM Rev. 57 (1), p. 3–57. Cited by: §1. Walsh (2000) T. Walsh SAT v CSP. In CP, Lecture Notes in Computer Science, Vol. 1894, p. 441–456. Cited by: §1, §4.6. Zhou et al. (2015) N. Zhou, H. Kjellerstrand, and J. Fruhman Constraint solving and planning with picat. Springer Briefs in Intelligent Systems, Springer. Cited by: §1, §1, §6. Appendix A Pseudocode for Normalization of Arguments During Flattening Algorithm 3 NormalizeBoolExpr(,) NormalizeBoolExpr(expr,csemap) 1: if expr is a variable or constant then 2: return (,∅expr, ) 3: else if expr is a ⟨⟩~ Comparison ~ l∘rexpr_l _r then 4: l′,dl←GetOrMakeVar(l,)expr_l ,d_l← GetOrMakeVar(expr_l,csemap) 5: r′,dr←NormalizeNumExpr(r,)expr_r ,d_r← NormalizeNumExpr(expr_r,csemap) 6: if rexpr_r is not a ⟨⟩~ GlobalFunction ~ then 7: l′,r′←CanonicalizedLinear(l′,r′)expr_l ,expr_r ← CanonicalizedLinear(expr_l ,expr_r ) 8: return (l′∘r′,dl∪dr)(expr_l _r ,\;d_l∪ d_r) 9: else if expr is 1⇒2expr_1 _2 then 10: 1′,d1←GetOrMakeVar(1,)expr_1 ,d_1← GetOrMakeVar(expr_1,csemap) 11: 2′,d2←GetOrMakeVar(2,)expr_2 ,d_2← GetOrMakeVar(expr_2,csemap) 12: return (¬1′∨2′,d1∪d2)( \,expr_1 _2 ,\;d_1∪ d_2) 13: else if expr is 1⇔2expr_1 _2 then 14: 1′,d1←GetOrMakeVar(1,)expr_1 ,d_1← GetOrMakeVar(expr_1,csemap) 15: 2′,d2←GetOrMakeVar(2,)expr_2 ,d_2← GetOrMakeVar(expr_2,csemap) 16: return (1×1′+−1×2′=0,d1∪d2)(1×expr_1 +-1×expr_2 =0,\;d_1∪ d_2) 17: else if expr is ¬0 \,expr_0 then ⊳ Negation of global constraint 18: 0′,d←NormalizeBoolExpr(0,)expr_0 ,d← NormalizeBoolExpr(expr_0,csemap) 19: return (¬0′,d)( \,expr_0 ,\;d) 20: ⊳∨ , ⇔ and global constraints 21: for each argument aia_i of expr do 22: vi,di←GetOrMakeVar(ai,)v_i,d_i← GetOrMakeVar(a_i,csemap) 23: return ([vi/ai],⋃idi)(expr[v_i/a_i],\; _id_i) Algorithm 4 NormalizeNumExpr (expr, csemap) 1: if expr is a variable or constant then 2: return (,∅)(expr, ) 3: else if expr is a Boolean expression then 4: return GetOrMakeVar(,) GetOrMakeVar(expr,csemap) 5: else if expr is −0-expr_0 then 6: 0′,d0←GetOrMakeVar(0,)expr_0 ,d_0← GetOrMakeVar(expr_0,csemap) 7: return (−1×0′,d0-1×expr_0 ,d_0) 8: else if expr is 1−2expr_1-expr_2 then 9: 1′,d1←GetOrMakeVar(1,)expr_1 ,d_1← GetOrMakeVar(expr_1,csemap) 10: 2′,d2←GetOrMakeVar(2,)expr_2 ,d_2← GetOrMakeVar(expr_2,csemap) 11: return (1×1′+−1×2′,d1∪d21×expr_1 +-1×expr_2 ,d_1∪ d_2) 12: else if expr is ∑iwi×i _iw_i×expr_i then 13: for each argument iexpr_i do 14: i′,di←GetOrMakeVar(i,)expr_i ,d_i← GetOrMakeVar(expr_i,csemap) 15: return (∑wi×i′,⋃idi)(Σ w_i×expr_i , _id_i) 16: ⊳+ + and global functions 17: for each argument aia_i of expr do 18: vi,di←GetOrMakeVar(ai,)v_i,d_i← GetOrMakeVar(a_i,csemap) 19: return ([vi/ai],⋃idi)(expr[v_i/a_i],\; _id_i)