2.9. FlatZinc and Flattening

Constraint solvers do not directly support MiniZinc models, rather in order to run a MiniZinc model, it is translated into a simple subset of MiniZinc called FlatZinc. FlatZinc reflects the fact that most constraint solvers only solve satisfaction problems of the form \(\bar{exists} c_1 \wedge \cdots \wedge c_m\) or optimization problems of the form \(\text{minimize } z \text{ subject to } c_1 \wedge \cdots \wedge c_m\), where \(c_i\) are primitive constraints and \(z\) is an integer or float expression in a restricted form.

The minizinc tool includes the MiniZinc compiler, which takes a MiniZinc model and data files and creates a flattened FlatZinc model which is equivalent to the MiniZinc model with the given data, and that appears in the restricted form discussed above. Normally the construction of a FlatZinc model which is sent to a solver is hidden from the user but you can view the result of flattening a model model.mzn with its data data.dzn as follows:

minizinc -c model.mzn data.dzn

which creates a FlatZinc model called model.fzn.

In this chapter we explore the process of translation from MiniZinc to FlatZinc.

2.9.1. Flattening Expressions

The restrictions of the underlying solver mean that complex expressions in MiniZinc need to be flattened to only use conjunctions of primitive constraints which do not themselves contain structured terms.

Consider the following model for ensuring that two circles in a rectangular box do not overlap:

Listing 2.9.1 Modelling non overlap of two circles (cnonoverlap.mzn).
float: width;          % width of rectangle to hold circles
float: height;         % height of rectangle to hold circles
float: r1;
var r1..width-r1:  x1; % (x1,y1) is center of circle of radius r1
var r1..height-r1: y1;
float: r2;
var r2..width-r2:  x2; % (x2,y2) is center of circle of radius r2
var r2..height-r2: y2;
                       % centers are at least r1 + r2 apart
constraint (x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) >= (r1+r2)*(r1+r2);
solve satisfy;

2.9.1.1. Simplification and Evaluation

Given the data file

width = 10.0;
height = 8.0;
r1 = 2.0;
r2 = 3.0;

the translation to FlatZinc first simplifies the model by replacing all the parameters by their values, and evaluating any fixed expression. After this simplification the values of parameters are not longer needed. An exception to this is large arrays of parametric values. If they are used more than once, then the parameter is retained to avoid duplicating the large expression.

After simplification the variable and parameter declarations parts of the model of Listing 2.9.1 become

var 2.0 .. 8.0: x1;
var 2.0 .. 6.0: y1;
var 3.0 .. 7.0: x2;
var 3.0 .. 5.0: y2;

2.9.1.2. Defining Subexpressions

Now no constraint solver directly handles complex constraint expressions like the one in Listing 2.9.1. Instead, each subexpression in the expression is named, and we create a constraint to construct the value of each expression. Let’s examine the subexpressions of the constraint expression. (x1 - x2) is a subexpression, if we name if FLOAT01 we can define it as constraint FLOAT01 = x1 - x2; Notice that this expression occurs twice in the model. We only need to construct the value once, we can then reuse it. This is called common subexpression elimination. The subexpression (x1 - x2)*(x1 - x2) can be named FLOAT02 and we can define it as constraint FLOAT02 = FLOAT01 * FLOAT01; We can similarly name constraint FLOAT03 = y1 - y2; and constraint FLOAT04 = FLOAT03 * FLOAT03; and finally constraint FLOAT05 = FLOAT02 * FLOAT04;. The inequality constraint itself becomes constraint FLOAT05 >= 25.0; since (r1+r2)*(r1 + r2) is calculated as 25.0. The flattened constraint is hence

constraint FLOAT01 = x1 - x2;
constraint FLOAT02 = FLOAT01 * FLOAT01;
constraint FLOAT03 = y1 - y2;
constraint FLOAT04 = FLOAT03 * FLOAT03;
constraint FLOAT05 = FLOAT02 * FLOAT04;
constraint FLOAT05 >= 25.0

2.9.1.3. FlatZinc constraint form

Flattening as its final step converts the form of the constraint to a standard FlatZinc form which is always \(p(a_1, \ldots, a_n)\) where p is the name of the primitive constraint and \(a_1, \ldots, a_n\) are the arguments. FlatZinc tries to use a minimum of different constraint forms so for example the constraint FLOAT01 = x1 - x2 is first rewritten to FLOAT01 + x2 = x1 and then output using the float_plus primitive constraint. The resulting constraint form is as follows:

constraint float_plus(FLOAT01, x2, x1);
constraint float_plus(FLOAT03, y2, y1);
constraint float_plus(FLOAT02, FLOAT04, FLOAT05);
constraint float_times(FLOAT01, FLOAT01, FLOAT02);
constraint float_times(FLOAT03, FLOAT03, FLOAT04);

2.9.1.4. Bounds analysis

We are still missing one thing, the declarations for the introduced variables FLOAT01, …, FLOAT05. While these could just be declared as var float, in order to make the solver’s task easier MiniZinc tries to determine upper and lower bounds on newly introduced variables, by a simple bounds analysis. For example since FLOAT01 = x1 - x2 and \(2.0 \leq\) x1 \(\leq 8.0\) and \(3.0 \leq\) x2 \(\leq 7.0\) then we can see that \(-5.0 \leq\) FLOAT0 \(\leq 5.0\). Given this information we can see that \(-25.0 \leq\) FLOAT02 \(\leq 25.0\) (although note that if we recognized that the multiplication was in fact a squaring we could give the much more accurate bounds \(0.0 \leq\) FLOAT02 \(\leq 25.0\)).

The alert reader may have noticed a discrepancy between the flattened form of the constraints in Defining Subexpressions and FlatZinc constraint form. In the latter there is no inequality constraint. Since unary inequalities can be fully represented by the bounds of a variable, the inequality forces the lower bound of FLOAT05 to be 25.0 and is then redundant. The final flattened form of the model of Listing 2.9.1 is:

% Variables
var 2.0 .. 8.0: x1;
var 2.0 .. 6.0: y1;
var 3.0 .. 7.0: x2;
var 3.0 .. 5.0: y2;
%
var -5.0..5.0:   FLOAT01;
var -25.0..25.0: FLOAT02;
var -3.0..3.0:   FLOAT03;
var -9.0..9.0:   FLOAT04;
var 25.0..34.0:  FLOAT05;
% Constraints
constraint float_plus(FLOAT01, x2, x1);
constraint float_plus(FLOAT03, y2, y1);
constraint float_plus(FLOAT02, FLOAT04, FLOAT05);
constraint float_times(FLOAT01, FLOAT01, FLOAT02);
constraint float_times(FLOAT03, FLOAT03, FLOAT04);
%
solve satisfy;

2.9.1.5. Objectives

MiniZinc flattens minimization or maximization objectives just like constraints. The objective expression is flattened and a variable is created for it, just as for other expressions. In the FlatZinc output the solve item is always on a single variable. See Let Expressions for an example.

2.9.2. Linear Expressions

One of the most important form of constraints, widely used for modelling, are linear constraints of the form

\[\begin{split}a_1 x_1 + \cdots + a_n x_n \begin{array}[c]{c} = \\ \leq \\ < \end{array} a_0\end{split}\]

where \(a_i\) are integer or floating point constants, and \(x_i\) are integer or floating point variables. They are highly expressive, and are the only class of constraint supported by (integer) linear programming constraint solvers. The translator from MiniZinc to FlatZinc tries to create linear constraints, rather than break up linear constraints into many subexpressions.

Listing 2.9.2 A MiniZinc model to illustrate linear constraint flattening (linear.mzn).
int:       d = -1;
var 0..10: x;
var -3..6: y;
var 3..8:  z;
constraint 3*x - y + x * z <= 19 + d * (x + y + z) - 4*d;
solve satisfy;

Consider the model shown in Listing 2.9.2. Rather than create variables for all the subexpressions \(3*x\), \(3*x - y\), \(x * z\), \(3*x - y + x*z\), \(x + y + z\), \(d * (x + y + z)\), \(19 + d * (x + y + z)\), and \(19 + d * (x + y + z) - 4*d\) translation will attempt to create a large linear constraint which captures as much as possible of the constraint in a single FlatZinc constraint.

Flattening creates linear expressions as a single unit rather than building intermediate variables for each subexpression. It also simplifies the linear expression created. Extracting the linear expression from the constraints leads to

var 0..80: INT01;
constraint 4*x + z + INT01 <= 23;
constraint INT01 = x * z;

Notice how the nonlinear expression \(x \times z\) is extracted as a new subexpression and given a name, while the remaining terms are collected together so that each variable appears exactly once (and indeed variable \(y\) whose terms cancel is eliminated).

Finally each constraint is written to FlatZinc form obtaining:

var 0..80: INT01;
constraint int_lin_le([1,4,1],[INT01,x,z],23);
constraint int_times(x,z,INT01);

2.9.3. Unrolling Expressions

Most models require creating a number of constraints which is dependent on the input data. MiniZinc supports these models with array types, list and set comprehensions, and aggregation functions.

Consider the following aggregate expression from the production scheduling example of Listing 2.2.2.

int: mproducts = max (p in Products)
                     (min (r in Resources where consumption[p,r] > 0)
                                     (capacity[r] div consumption[p,r]));

Since this uses generator call syntax we can rewrite it to equivalent form which is processed by the compiler:

int: mproducts = max([ min [ capacity[r] div consumption[p,r]
                           | r in Resources where consumption[p,r] > 0])
                     | p in Products]);

Given the data

nproducts = 2;
nresources = 5;
capacity = [4000, 6, 2000, 500, 500];
consumption= [| 250, 2, 75, 100, 0,
              | 200, 0, 150, 150, 75 |];

this first builds the array for p = 1

[ capacity[r] div consumption[p,r]
                           | r in 1..5 where consumption[p,r] > 0]

which is [16, 3, 26, 5] and then calculates the minimum as 3. It then builds the same array for p = 2 which is [20, 13, 3, 6] and calculates the minimum as 3. It then constructs the array [3, 3] and calculates the maximum as 3. There is no representation of mproducts in the output FlatZinc, this evaluation is simply used to replace mproducts by the calculated value 3.

The most common form of aggregate expression in a constraint model is forall. Forall expressions are unrolled into multiple constraints.

Consider the MiniZinc fragment

array[1..8] of var 0..9: v = [S,E,N,D,M,O,R,Y];
constraint forall(i,j in 1..8 where i < j)(v[i] != v[j])

which arises from the SEND-MORE-MONEY example of Listing 2.2.4 using a default decomposition for alldifferent. The forall expression creates a constraint for each \(i, j\) pair which meet the requirement \(i < j\), thus creating

constraint v[1] != v[2]; % S != E
constraint v[1] != v[3]; % S != N
...
constraint v[1] != v[8]; % S != Y
constraint v[2] != v[3]; % E != N
...
constraint v[7] != v[8]; % R != Y

In FlatZinc form this is

constraint int_neq(S,E);
constraint int_neq(S,N);
...
constraint int_neq(S,Y);
constraint int_neq(E,N);
...
constraint int_neq(R,Y);

Notice how the temporary array variables v[i] are replaced by the original variables in the output FlatZinc.

2.9.4. Arrays

One dimensional arrays in MiniZinc can have arbitrary indices as long as they are contiguous integers. In FlatZinc all arrays are indexed from 1..l where l is the length of the array. This means that array lookups need to be translated to the FlatZinc view of indices.

Consider the following MiniZinc model for balancing a seesaw of length 2 * l2, with a child of weight cw kg using exactly m 1kg weights.

int: cw;                               % child weight
int: l2;                               % half seesaw length
int: m;                                % number of 1kg weight
array[-l2..l2] of var 0..max(m,cw): w; % weight at each point
var -l2..l2: p;                        % position of child
constraint sum(i in -l2..l2)(i * w[i]) = 0; % balance
constraint sum(i in -l2..l2)(w[i]) = m + cw; % all weights used
constraint w[p] = cw;                  % child is at position p
solve satisfy;

Given cw = 2, l2 = 2, and m = 3 the unrolling produces the constraints

array[-2..2] of var 0..3: w;
var -2..2: p
constraint -2*w[-2] + -1*w[-1] + 0*w[0] + 1*w[1] + 2*w[2] = 0;
constraint w[-2] + w[-1] + w[0] + w[1] + w[2] = 5;
constraint w[p] = 2;

But FlatZinc insists that the w array starts at index 1. This means we need to rewrite all the array accesses to use the new index value. For fixed array lookups this is easy, for variable array lookups we may need to create a new variable. The result for the equations above is

array[1..5] of var 0..3: w;
var -2..2: p
var 1..5: INT01;
constraint -2*w[1] + -1*w[2] + 0*w[3] + 1*w[4] + 2*w[5] = 0;
constraint w[1] + w[2] + w[3] + w[4] + w[5] = 5;
constraint w[INT01] = 2;
constraint INT01 = p + 3;

Finally we rewrite the constraints into FlatZinc form. Note how the variable array index lookup is mapped to array_var_int_element.

array[1..5] of var 0..3: w;
var -2..2: p
var 1..5: INT01;
constraint int_lin_eq([2, 1, -1, -2], [w[1], w[2], w[4], w[5]], 0);
constraint int_lin_eq([1, 1, 1, 1, 1], [w[1],w[2],w[3],w[4],w[5]], 5);
constraint array_var_int_element(INT01, w, 2);
constraint int_lin_eq([-1, 1], [INT01, p], -3);

Multidimensional arrays are supported by MiniZinc, but only single dimension arrays are supported by FlatZinc (at present). This means that multidimensional arrays must be mapped to single dimension arrays, and multidimensional array access must be mapped to single dimension array access.

Consider the Laplace equation constraints defined for a finite element plate model in Listing 2.2.1:

set of int: HEIGHT = 0..h;
set of int: CHEIGHT = 1..h-1;
set of int: WIDTH = 0..w;
set of int: CWIDTH = 1..w-1;  
array[HEIGHT,WIDTH] of var float: t; % temperature at point (i,j)
var float: left;   % left   edge temperature
var float: right;  % right  edge temperature
var float: top;    % top    edge temperature
var float: bottom; % bottom edge temperature

% equation
% Laplace equation: each internal temp. is average of its neighbours
constraint forall(i in CHEIGHT, j in CWIDTH)(
              4.0*t[i,j] = t[i-1,j] + t[i,j-1] + t[i+1,j] + t[i,j+1]);

Assuming w = 4 and h = 4 this creates the constraints

array[0..4,0..4] of var float: t; % temperature at point (i,j)
constraint 4.0*t[1,1] = t[0,1] + t[1,0] + t[2,1] + t[1,2];
constraint 4.0*t[1,2] = t[0,2] + t[1,1] + t[2,2] + t[1,3];
constraint 4.0*t[1,3] = t[0,3] + t[1,2] + t[2,3] + t[1,4];
constraint 4.0*t[2,1] = t[1,1] + t[2,0] + t[3,1] + t[2,2];
constraint 4.0*t[2,2] = t[1,2] + t[2,1] + t[3,2] + t[2,3];
constraint 4.0*t[2,3] = t[1,3] + t[2,2] + t[3,3] + t[2,4];
constraint 4.0*t[3,1] = t[2,1] + t[3,0] + t[4,1] + t[3,2];
constraint 4.0*t[3,2] = t[2,2] + t[3,1] + t[4,2] + t[3,3];
constraint 4.0*t[3,3] = t[2,3] + t[3,2] + t[4,3] + t[3,4];

The 2 dimensional array of 25 elements is converted to a one dimensional array and the indices are changed accordingly: so index [i,j] becomes [i * 5 + j + 1].

array [1..25] of var float: t;
constraint 4.0*t[7] = t[2] + t[6] + t[12] + t[8];
constraint 4.0*t[8] = t[3] + t[7] + t[13] + t[9];
constraint 4.0*t[9] = t[4] + t[8] + t[14] + t[10];
constraint 4.0*t[12] = t[7] + t[11] + t[17] + t[13];
constraint 4.0*t[13] = t[8] + t[12] + t[18] + t[14];
constraint 4.0*t[14] = t[9] + t[13] + t[19] + t[15];
constraint 4.0*t[17] = t[12] + t[16] + t[22] + t[18];
constraint 4.0*t[18] = t[13] + t[17] + t[23] + t[19];
constraint 4.0*t[19] = t[14] + t[18] + t[24] + t[20];

2.9.5. Reification

FlatZinc models involve only variables and parameter declarations and a series of primitive constraints. Hence when we model in MiniZinc with Boolean connectives other than conjunction, something has to be done. The core approach to handling complex formulae that use connectives other than conjunction is by reification. Reifying a constraint \(c\) creates a new constraint equivalent to \(b \leftrightarrow c\) where the Boolean variable \(b\) is true if the constraint holds and false if it doesn’t hold.

Once we have the capability to reify constraints the treatment of complex formulae is not different from arithmetic expressions. We create a name for each subexpression and a flat constraint to constrain the name to take the value of its subexpression.

Consider the following constraint expression that occurs in the jobshop scheduling example of Listing 2.2.10.

constraint %% ensure no overlap of tasks
    forall(j in 1..tasks) (
        forall(i,k in 1..jobs where i < k) (
            s[i,j] + d[i,j] <= s[k,j] \/
            s[k,j] + d[k,j] <= s[i,j]
    ) );

Given the data file

jobs = 2;
tasks = 3;
d = [| 5, 3, 4 | 2, 6, 3 |]

then the unrolling creates

constraint s[1,1] + 5 <= s[2,1] \/ s[2,1] + 2 <= s[1,1];
constraint s[1,2] + 3 <= s[2,2] \/ s[2,2] + 6 <= s[1,2];
constraint s[1,3] + 4 <= s[2,3] \/ s[2,3] + 3 <= s[1,3];

Reification of the constraints that appear in the disjunction creates new Boolean variables to define the values of each expression.

array[1..2,1..3] of var 0..23: s;
constraint BOOL01 <-> s[1,1] + 5 <= s[2,1];
constraint BOOL02 <-> s[2,1] + 2 <= s[1,1];
constraint BOOL03 <-> s[1,2] + 3 <= s[2,2];
constraint BOOL04 <-> s[2,2] + 6 <= s[1,2];
constraint BOOL05 <-> s[1,3] + 4 <= s[2,3];
constraint BOOL06 <-> s[2,3] + 3 <= s[1,3];
constraint BOOL01 \/ BOOL02;
constraint BOOL03 \/ BOOL04;
constraint BOOL05 \/ BOOL06;

Each primitive constraint can now be mapped to the FlatZinc form. Note how the two dimensional array s is mapped to a one dimensional form.

array[1..6] of var 0..23: s;
constraint int_lin_le_reif([1, -1], [s[1], s[4]], -5, BOOL01);
constraint int_lin_le_reif([-1, 1], [s[1], s[4]], -2, BOOL02);
constraint int_lin_le_reif([1, -1], [s[2], s[5]], -3, BOOL03);
constraint int_lin_le_reif([-1, 1], [s[2], s[5]], -6, BOOL04);
constraint int_lin_le_reif([1, -1], [s[3], s[6]], -4, BOOL05);
constraint int_lin_le_reif([-1, 1], [s[3], s[6]], -3, BOOL06);
constraint bool_clause([BOOL01, BOOL02], []);
constraint bool_clause([BOOL03, BOOL04], []);
constraint bool_clause([BOOL05, BOOL06], []);

The int_lin_le_reif is the reified form of the linear constraint int_lin_le.

Most FlatZinc primitive constraints \(p(\bar{x})\) have a reified form \(\mathit{p\_reif}(\bar{x},b)\) which takes an additional final argument \(b\) and defines the constraint \(b \leftrightarrow p(\bar{x})\). FlatZinc primitive constraints which define functional relationships, like int_plus and int_plus, do not need to support reification. Instead, the equality with the result of the function is reified.

Another important use of reification arises when we use the coercion function bool2int (either explicitly, or implicitly by using a Boolean expression as an integer expression). Flattening creates a Boolean variable to hold the value of the Boolean expression argument, as well as an integer variable (restricted to 0..1) to hold this value.

Consider the magic series problem of Listing 2.2.14.

int: n;
array[0..n-1] of var 0..n: s;

constraint forall(i in 0..n-1) (
   s[i] = (sum(j in 0..n-1)(bool2int(s[j]=i))));

Given n = 2 the unrolling creates

constraint s[0] = bool2int(s[0] = 0) + bool2int(s[1] = 0);
constraint s[1] = bool2int(s[0] = 1) + bool2int(s[1] = 1);

and flattening creates

constraint BOOL01 <-> s[0] = 0;
constraint BOOL03 <-> s[1] = 0;
constraint BOOL05 <-> s[0] = 1;
constraint BOOL07 <-> s[1] = 1;
constraint INT02 = bool2int(BOOL01);
constraint INT04 = bool2int(BOOL03);
constraint INT06 = bool2int(BOOL05);
constraint INT08 = bool2int(BOOL07);
constraint s[0] = INT02 + INT04;
constraint s[1] = INT06 + INT08;

The final FlatZinc form is

var bool: BOOL01;
var bool: BOOL03;
var bool: BOOL05;
var bool: BOOL07;
var 0..1: INT02;
var 0..1: INT04;
var 0..1: INT06;
var 0..1: INT08;
array [1..2] of var 0..2: s;
constraint int_eq_reif(s[1], 0, BOOL01);
constraint int_eq_reif(s[2], 0, BOOL03);
constraint int_eq_reif(s[1], 1, BOOL05);
constraint int_eq_reif(s[2], 1, BOOL07);
constraint bool2int(BOOL01, INT02);
constraint bool2int(BOOL03, INT04);
constraint bool2int(BOOL05, INT06);
constraint bool2int(BOOL07, INT08);
constraint int_lin_eq([-1, -1, 1], [INT02, INT04, s[1]], 0);
constraint int_lin_eq([-1, -1, 1], [INT06, INT08, s[2]], 0);
solve satisfy;

2.9.6. Predicates

An important factor in the support for MiniZinc by many different solvers is that global constraints (and indeed FlatZinc constraints) can be specialized for the particular solver.

Each solver will either specify a predicate without a definition, or with a definition. For example a solver that has a builtin global alldifferent predicate, will include the definition

predicate alldifferent(array[int] of var int:x);

in its globals library, while a solver using the default decomposition will have the definition

predicate alldifferent(array[int] of var int:x) =
    forall(i,j in index_set(x) where i < j)(x[i] != x[j]);

Predicate calls \(p(\bar{t})\) are flattened by first constructing variables \(v_i\) for each argument terms \(t_i\). If the predicate has no definition we simply use a call to the predicate with the constructed arguments: \(p(\bar{v})\). If the predicate has a definition \(p(\bar{x}) = \phi(\bar{x})\) then we replace the predicate call \(p(\bar{t})\) with the body of the predicate with the formal arguments replaced by the argument variables, that is \(\phi(\bar{v})\). Note that if a predicate call \(p(\bar{t})\) appears in a reified position and it has no definition, we check for the existence of a reified version of the predicate \(\mathit{p\_reif}(\bar{x},b)\) in which case we use that.

Consider the alldifferent constraint in the SEND-MORE-MONEY example of Listing 2.2.4

constraint alldifferent([S,E,N,D,M,O,R,Y]);

If the solver has a builtin alldifferent we simply construct a new variable for the argument, and replace it in the call.

array[1..8] of var 0..9: v = [S,E,N,D,M,O,R,Y];
constraint alldifferent(v);

Notice that bounds analysis attempts to find tight bounds on the new array variable. The reason for constructing the array argument is if we use the same array twice the FlatZinc solver does not have to construct it twice. In this case since it is not used twice a later stage of the translation will replace v by its definition.

What if the solver uses the default definition of alldifferent? Then the variable v is defined as usual, and the predicate call is replaced by a renamed copy where v replaces the formal argument x. The resulting code is

array[1..8] of var 0..9: v = [S,E,N,D,M,O,R,Y];
constraint forall(i,j in 1..8 where i < j)(v[i] != v[j])

which we examined in Unrolling Expressions.

Consider the following constraint, where alldifferent appears in a reified position.

constraint alldifferent([A,B,C]) \/ alldifferent([B,C,D]);

If the solver has a reified form of alldifferent this will be flattened to

constraint alldifferent_reif([A,B,C],BOOL01);
constraint alldifferent_reif([B,C,D],BOOL02);
constraint bool_clause([BOOL01,BOOL02],[]);

Using the default decomposition, the predicate replacement will first create

array[1..3] of var int: v1 = [A,B,C];
array[1..3] of var int: v2 = [B,C,D];
constraint forall(i,j in 1..3 where i<j)(v1[i] != v1[j]) \/
           forall(i,j in 1..3 where i<j)(v2[i] != v2[j]);

which will eventually be flattened to the FlatZinc form

constraint int_neq_reif(A,B,BOOL01);
constraint int_neq_reif(A,C,BOOL02);
constraint int_neq_reif(B,C,BOOL03);
constraint array_bool_and([BOOL01,BOOL02,BOOL03],BOOL04);
constraint int_neq_reif(B,D,BOOL05);
constraint int_neq_reif(C,D,BOOL06);
constraint array_bool_and([BOOL03,BOOL05,BOOL06],BOOL07);
constraint bool_clause([BOOL04,BOOL07],[]);

Note how common subexpression elimination reuses the reified inequality B != C (although there is a better translation which lifts the common constraint to the top level conjunction).

2.9.7. Let Expressions

Let expressions are a powerful facility of MiniZinc to introduce new variables. This is useful for creating common sub expressions, and for defining local variables for predicates. During flattening let expressions are translated to variable and constraint declarations. The relational semantics of MiniZinc means that these constraints must appear as if conjoined in the first enclosing Boolean expression.

A key feature of let expressions is that each time they are used they create new variables.

Consider the flattening of the code

constraint even(u) \/ even(v);
predicate even(var int: x) =
          let { var int: y } in x = 2 * y;

First the predicate calls are replaced by their definition.

constraint (let { var int: y} in u = 2 * y) \/
           (let { var int: y} in v = 2 * y);

Next let variables are renamed apart

constraint (let { var int: y1} in u = 2 * y1) \/
           (let { var int: y2} in v = 2 * y2);

Finally variable declarations are extracted to the top level

var int: y1;
var int: y2;
constraint u = 2 * y1 \/ v = 2 * y2;

Once the let expression is removed we can flatten as usual.

Remember that let expressions can define values for newly introduced variables (and indeed must do so for parameters). These implicitly define constraints that must also be flattened.

Consider the complex objective function for wedding seating problem of Listing 2.3.10.

solve maximize sum(h in Hatreds)(
      let {  var Seats: p1 = pos[h1[h]],
             var Seats: p2 = pos[h2[h]],
             var 0..1: same = bool2int(p1 <= 6 <-> p2 <= 6) } in
      same * abs(p1 - p2) + (1-same) * (abs(13 - p1 - p2) + 1));

For conciseness we assume only the first two Hatreds, so

set of int: Hatreds = 1..2;
array[Hatreds] of Guests: h1 = [groom, carol];
array[Hatreds] of Guests: h2 = [clara, bestman];

The first step of flattening is to unroll the sum expression, giving (we keep the guest names and parameter Seats for clarity only, in reality they would be replaced by their definition):

solve maximize
      (let { var Seats: p1 = pos[groom],
             var Seats: p2 = pos[clara],
             var 0..1: same = bool2int(p1 <= 6 <-> p2 <= 6) } in
       same * abs(p1 - p2) + (1-same) * (abs(13 - p1 - p2) + 1))
      +
      (let { var Seats: p1 = pos[carol],
             var Seats: p2 = pos[bestman],
             var 0..1: same = bool2int(p1 <= 6 <-> p2 <= 6) } in
       same * abs(p1 - p2) + (1-same) * (abs(13 - p1 - p2) + 1));

Next each new variable in a let expression is renamed to be distinct

solve maximize
      (let { var Seats: p11 = pos[groom],
             var Seats: p21 = pos[clara],
             var 0..1: same1 = bool2int(p11 <= 6 <-> p21 <= 6) } in
       same1 * abs(p11 - p21) + (1-same1) * (abs(13 - p11 - p21) + 1))
      +
      (let { var Seats: p12 = pos[carol],
             var Seats: p22 = pos[bestman],
             var 0..1: same2 = bool2int(p12 <= 6 <-> p22 <= 6) } in
       same2 * abs(p12 - p22) + (1-same2) * (abs(13 - p12 - p22) + 1));

Variables in the let expression are extracted to the top level and defining constraints are extracted to the correct level (which in this case is also the top level).

var Seats: p11;
var Seats: p21;
var 0..1: same1;
constraint p12 = pos[clara];
constraint p11 = pos[groom];
constraint same1 = bool2int(p11 <= 6 <-> p21 <= 6);
var Seats p12;
var Seats p22;
var 0..1: same2;
constraint p12 = pos[carol];
constraint p22 = pos[bestman];
constraint same2 = bool2int(p12 <= 6 <-> p22 <= 6) } in
solve maximize
      same1 * abs(p11 - p21) + (1-same1) * (abs(13 - p11 - p21) + 1))
      +
      same2 * abs(p12 - p22) + (1-same2) * (abs(13 - p12 - p22) + 1));

Now we have constructed equivalent MiniZinc code without the use of let expressions and the flattening can proceed as usual.

As an illustration of let expressions that do not appear at the top level consider the following model

var 0..9: x;
constraint x >= 1 -> let { var 2..9: y = x - 1 } in
                     y + (let { var int: z = x * y } in z * z) < 14;

We extract the variable definitions to the top level and the constraints to the first enclosing Boolean context, which here is the right hand side of the implication.

var 0..9: x;
var 2..9: y;
var int: z;
constraint x >= 1 -> (y = x - 1 /\ z = x * y /\ y + z * z < 14);

Note that if we know that the equation defining a variable definition cannot fail we can extract it to the top level. This will usually make solving substantially faster.

For the example above the constraint y = x - 1 can fail since the domain of y is not big enough for all possible values of x - 1. But the constraint z = x * y cannot (indeed bounds analysis will give z bounds big enough to hold all possible values of x * y). A better flattening will give

var 0..9: x;
var 2..9: y;
var int: z;
constraint z = x * y;
constraint x >= 1 -> (y = x - 1 /\ y + z * z < 14);

Currently the MiniZinc compiler does this by always defining the declared bounds of an introduced variable to be big enough for its defining equation to always hold and then adding bounds constraints in the correct context for the let expression. On the example above this results in

var 0..9: x;
var -1..8: y;
var -9..72: z;
constraint y = x - 1;
constraint z = x * y;
constraint x >= 1 -> (y >= 2 /\ y + z * z < 14);

This translation leads to more efficient solving since the possibly complex calculation of the let variable is not reified.

Another reason for this approach is that it also works when introduced variables appear in negative contexts (as long as they have a definition). Consider the following example similar to the previous one

var 0..9: x;
constraint (let { var 2..9: y = x - 1 } in
           y + (let { var int: z = x * y } in z * z) > 14) -> x >= 5;

The let expressions appear in a negated context, but each introduced variable is defined. The flattened code is

var 0..9: x;
var -1..8: y;
var -9..72: z;
constraint y = x - 1;
constraint z = x * y;
constraint (y >= 2 /\ y + z * z > 14) -> x >= 5;

Note the analog to the simple approach to let elimination does not give a correct translation:

var 0..9: x;
var 2..9: y;
var int: z;
constraint (y = x - 1 /\ z = x * y /\ y + z * z > 14) -> x >= 5;

gives answers for all possible values of x, whereas the original constraint removes the possibility that x = 4.

The treatment of constraint items in let expressions is analogous to defined variables. One can think of a constraint as equivalent to defining a new Boolean variable. The definitions of the new Boolean variables are extracted to the top level, and the Boolean remains in the correct context.

constraint z > 1 -> let { var int: y,
                          constraint (x >= 0) -> y = x,
                          constraint (x < 0)  -> y = -x
                    } in y * (y - 2) >= z;

is treated like

constraint z > 1 -> let { var int: y,
                          var bool: b1 = ((x >= 0) -> y = x),
                          var bool: b2 = ((x < 0)  -> y = -x),
                          constraint b1 /\ b2
                    } in y * (y - 2) >= z;

and flattens to

constraint b1 = ((x >= 0) -> y = x);
constraint b2 = ((x < 0)  -> y = -x);
constraint z > 1 -> (b1 /\ b2 /\ y * (y - 2) >= z);