<Model> ::= [ <BoolExpr> ( , <BoolExpr>)* ], minimize= <IntExpr>
<BoolExpr> ::= | <Bool> | <BoolVar> | ¬ \lnot ¬ ∧ \land ∧ ∨ \lor ∨ ⇒ \Rightarrow ⇒ ⇔ \Leftrightarrow ⇔ ≤ \leq ≤ ≥ \geq ≥ = = = ≠ \neq = <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 + y x+y x + y 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 } \{\emph{false},\emph{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 ( ¬ \neg ¬ ∧ \wedge ∧ ∨ \vee ∨ ⇒ \Rightarrow ⇒ ⇔ \Leftrightarrow ⇔ ≤ , < , ≥ , > , = \leq,<,\geq,>,= ≤ , < , ≥ , > , = ≠ \neq = + + + − - − 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 ) \neg(x+y) ¬ ( x + y ) x + y x+y x + y 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 \mbox A l l D i f f e r e n t ( x 1 , … , x n ) \mbox{{AllDifferent}}(x_{1},\ldots,x_{n}) \mbox A l l D i f f er e n t ( x 1 , … , x n ) ⋀ 1 ≤ i < j ≤ n x i ≠ x j . \bigwedge_{1\leq i<j\leq n}x_{i}\neq x_{j}. ⋀ 1 ≤ i < j ≤ n x i = x j . 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 .
Figure 1 . Examples of constraints in our constraint language and their corresponding expression trees. 4. Transformations
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.