this repo has no description
dekker.one
1.. _sec-flattening:
2
3FlatZinc and Flattening
4=======================
5
6.. \pjs{Maybe show the toolset at this point?}
7
8Constraint solvers do not directly support MiniZinc models, rather in order
9to run a MiniZinc model, it is translated into a simple subset of MiniZinc
10called FlatZinc. FlatZinc reflects the fact that most constraint solvers
11only solve satisfaction
12problems of the form :math:`\bar{exists} c_1 \wedge \cdots \wedge c_m`
13or optimization problems of the form
14:math:`\text{minimize } z \text{ subject to } c_1 \wedge \cdots \wedge c_m`,
15where :math:`c_i` are primitive constraints and :math:`z` is an integer or float
16expression in a restricted form.
17
18.. index::
19 single: minizinc -c
20
21The ``minizinc`` tool includes the MiniZinc *compiler*, which
22takes a MiniZinc model and data files and creates
23a flattened FlatZinc model which is equivalent to the MiniZinc model with
24the given data, and that appears in the restricted form discussed above.
25Normally the construction of a FlatZinc model which is sent to a solver is
26hidden from the user but you can view the result of flattening a model
27``model.mzn`` with
28its data ``data.dzn`` as follows:
29
30.. code-block:: bash
31
32 minizinc -c model.mzn data.dzn
33
34which creates a FlatZinc model called ``model.fzn``.
35
36In this chapter we explore the process of translation from MiniZinc to FlatZinc.
37
38Flattening Expressions
39----------------------
40
41The restrictions of the underlying solver mean that complex expressions in
42MiniZinc need to be *flattened* to only use conjunctions of primitive
43constraints which do not themselves contain structured terms.
44
45Consider the following model for ensuring that two circles in a rectangular
46box do not overlap:
47
48.. literalinclude:: examples/cnonoverlap.mzn
49 :language: minizinc
50 :caption: Modelling non overlap of two circles (:download:`cnonoverlap.mzn <examples/cnonoverlap.mzn>`).
51 :name: fig-nonoverlap
52
53
54Simplification and Evaluation
55~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
56
57Given the data file
58
59.. code-block:: minizinc
60
61 width = 10.0;
62 height = 8.0;
63 r1 = 2.0;
64 r2 = 3.0;
65
66the translation to FlatZinc first simplifies the model by replacing all the
67parameters by their values, and evaluating any fixed expression.
68After this simplification the values of parameters are not longer needed.
69An exception to this is large arrays of parametric values. If they are
70used more than once, then the parameter is retained to avoid duplicating the
71large expression.
72
73After simplification the variable and parameter declarations parts of
74the model of :numref:`fig-nonoverlap` become
75
76.. literalinclude:: examples/cnonoverlap.fzn
77 :language: minizinc
78 :start-after: % Variables
79 :end-before: %
80
81.. _sec-flat-sub:
82
83Defining Subexpressions
84~~~~~~~~~~~~~~~~~~~~~~~
85
86Now no constraint solver directly handles complex constraint expressions
87like the one in :numref:`fig-nonoverlap`.
88Instead, each subexpression in the expression is named, and we create a
89constraint to construct the value of each expression. Let's examine the
90subexpressions of the constraint expression. :mzn:`(x1 - x2)` is a
91subexpression, if we name if :mzn:`FLOAT01` we can define it as
92:mzn:`constraint FLOAT01 = x1 - x2;` Notice that this expression occurs
93twice in the model. We only need to construct the value once, we can then
94reuse it. This is called *common subexpression elimination*.
95The subexpression :mzn:`(x1 - x2)*(x1 - x2)` can be named
96:mzn:`FLOAT02`
97and we can define it as
98:mzn:`constraint FLOAT02 = FLOAT01 * FLOAT01;`
99We can similarly name :mzn:`constraint FLOAT03 = y1 - y2;`
100and
101:mzn:`constraint FLOAT04 = FLOAT03 * FLOAT03;`
102and finally :mzn:`constraint FLOAT05 = FLOAT02 * FLOAT04;`.
103The inequality constraint itself becomes
104:mzn:`constraint FLOAT05 >= 25.0;` since :mzn:`(r1+r2)*(r1 + r2)`
105is calculated as :mzn:`25.0`.
106The flattened constraint is hence
107
108.. code-block:: minizinc
109
110 constraint FLOAT01 = x1 - x2;
111 constraint FLOAT02 = FLOAT01 * FLOAT01;
112 constraint FLOAT03 = y1 - y2;
113 constraint FLOAT04 = FLOAT03 * FLOAT03;
114 constraint FLOAT05 = FLOAT02 * FLOAT04;
115 constraint FLOAT05 >= 25.0
116
117.. _sec-flat-fzn:
118
119FlatZinc constraint form
120~~~~~~~~~~~~~~~~~~~~~~~~
121
122Flattening as its final step converts the form of the constraint to a
123standard FlatZinc form which is always :math:`p(a_1, \ldots, a_n)` where
124:mzn:`p` is the name of the primitive constraint and :math:`a_1, \ldots, a_n` are the
125arguments. FlatZinc tries to use a minimum of different constraint forms so
126for example the constraint :mzn:`FLOAT01 = x1 - x2` is first rewritten to
127:mzn:`FLOAT01 + x2 = x1` and then output using the :mzn:`float_plus` primitive
128constraint. The resulting constraint form is as follows:
129
130.. literalinclude:: examples/cnonoverlap.fzn
131 :language: minizinc
132 :start-after: % Constraints
133 :end-before: %
134
135Bounds analysis
136~~~~~~~~~~~~~~~
137
138We are still missing one thing, the
139declarations for the introduced variables :mzn:`FLOAT01`, ...,
140:mzn:`FLOAT05`. While these could just be declared as
141:mzn:`var float`, in order to make the solver's task easier MiniZinc tries to
142determine upper and lower bounds on newly introduced variables, by a simple
143bounds analysis. For example since :mzn:`FLOAT01 = x1 - x2`
144and :math:`2.0 \leq` :mzn:`x1` :math:`\leq 8.0` and :math:`3.0 \leq` :mzn:`x2` :math:`\leq 7.0` then we can see that
145:math:`-5.0 \leq` :mzn:`FLOAT0` :math:`\leq 5.0`. Given this information we can see that
146:math:`-25.0 \leq` :mzn:`FLOAT02` :math:`\leq 25.0` (although note that if we recognized that the
147multiplication was in fact a squaring we could give the much more accurate
148bounds :math:`0.0 \leq` :mzn:`FLOAT02` :math:`\leq 25.0`).
149
150The alert reader may have noticed a discrepancy between the flattened form
151of the constraints in :ref:`sec-flat-sub` and :ref:`sec-flat-fzn`. In
152the latter there is no inequality constraint. Since unary inequalities can
153be fully represented by the bounds of a variable, the inequality forces the
154lower bound of :mzn:`FLOAT05` to be :mzn:`25.0` and is then redundant. The final
155flattened form of the model of :numref:`fig-nonoverlap` is:
156
157.. literalinclude:: examples/cnonoverlap.fzn
158 :language: minizinc
159
160Objectives
161~~~~~~~~~~
162
163MiniZinc flattens minimization or maximization
164objectives just like constraints. The objective
165expression is flattened and a variable is created for it, just as for other
166expressions. In the FlatZinc output the solve item is always on a single
167variable. See :ref:`sec-let` for an example.
168
169.. \pjs{Do we need an example here?}
170
171Linear Expressions
172------------------
173
174One of the most important form of constraints, widely used for modelling,
175are linear constraints of the form
176
177
178.. math:: a_1 x_1 + \cdots + a_n x_n \begin{array}[c]{c} = \\ \leq \\ < \end{array} a_0
179
180where :math:`a_i` are integer or floating point constants, and
181:math:`x_i` are integer or floating point variables.
182They are highly expressive, and are the only class of constraint supported
183by (integer) linear programming constraint solvers.
184The translator from MiniZinc to FlatZinc tries to create linear
185constraints, rather than break up linear constraints into many
186subexpressions.
187
188.. \pjs{Maybe use the equation from SEND-MORE-MONEY instead?}
189
190.. literalinclude:: examples/linear.mzn
191 :language: minizinc
192 :caption: A MiniZinc model to illustrate linear constraint flattening (:download:`linear.mzn <examples/linear.mzn>`).
193 :name: fig-lflat
194
195Consider the model shown in :numref:`fig-lflat`. Rather than create
196variables for all the subexpressions :math:`3*x`, :math:`3*x - y`, :math:`x * z`, :math:`3*x - y + x*z`,
197:math:`x + y + z`, :math:`d * (x + y + z)`, :math:`19 + d * (x + y + z)`,
198and :math:`19 + d * (x + y + z) - 4*d`
199translation will attempt to create a large linear constraint which captures
200as much as possible of the constraint in a single FlatZinc
201constraint.
202
203Flattening creates linear expressions as a single unit rather than building
204intermediate variables for each subexpression. It also simplifies the linear
205expression created. Extracting the linear expression from the constraints
206leads to
207
208.. code-block:: minizinc
209
210 var 0..80: INT01;
211 constraint 4*x + z + INT01 <= 23;
212 constraint INT01 = x * z;
213
214Notice how the *nonlinear expression* :math:`x \times z` is extracted as a
215new subexpression and given a name, while the remaining terms are collected
216together so that each variable appears exactly once (and indeed variable :math:`y`
217whose terms cancel is eliminated).
218
219Finally each constraint is written to FlatZinc form obtaining:
220
221.. code-block:: minizinc
222
223 var 0..80: INT01;
224 constraint int_lin_le([1,4,1],[INT01,x,z],23);
225 constraint int_times(x,z,INT01);
226
227.. _sec-unroll:
228
229Unrolling Expressions
230---------------------
231
232Most models require creating a number of constraints which is
233dependent on the input data. MiniZinc supports these models with array
234types, list and set comprehensions, and aggregation functions.
235
236Consider the following aggregate expression from the production scheduling
237example of :numref:`ex-prod-planning`.
238
239.. code-block:: minizinc
240
241 int: mproducts = max (p in Products)
242 (min (r in Resources where consumption[p,r] > 0)
243 (capacity[r] div consumption[p,r]));
244
245Since this uses generator call syntax we can rewrite it to equivalent
246form which is processed by the compiler:
247
248.. code-block:: minizinc
249
250 int: mproducts = max([ min [ capacity[r] div consumption[p,r]
251 | r in Resources where consumption[p,r] > 0])
252 | p in Products]);
253
254Given the data
255
256.. code-block:: minizinc
257
258 nproducts = 2;
259 nresources = 5;
260 capacity = [4000, 6, 2000, 500, 500];
261 consumption= [| 250, 2, 75, 100, 0,
262 | 200, 0, 150, 150, 75 |];
263
264this first builds the array for :mzn:`p = 1`
265
266.. code-block:: minizinc
267
268 [ capacity[r] div consumption[p,r]
269 | r in 1..5 where consumption[p,r] > 0]
270
271which is :mzn:`[16, 3, 26, 5]` and then calculates the minimum as 3.
272It then builds the same array for :mzn:`p = 2` which is
273:mzn:`[20, 13, 3, 6]` and calculates the minimum as 3. It then constructs the
274array :mzn:`[3, 3]` and calculates the maximum as 3.
275There is no representation of :mzn:`mproducts` in the output FlatZinc,
276this evaluation is simply used to replace :mzn:`mproducts` by the
277calculated value 3.
278
279The most common form of aggregate expression in a constraint model is
280:mzn:`forall`. Forall expressions are unrolled into multiple constraints.
281
282Consider the MiniZinc fragment
283
284.. code-block:: minizinc
285
286 array[1..8] of var 0..9: v = [S,E,N,D,M,O,R,Y];
287 constraint forall(i,j in 1..8 where i < j)(v[i] != v[j])
288
289which arises from the SEND-MORE-MONEY example of :numref:`ex-smm`
290using a default decomposition for :mzn:`alldifferent`.
291The :mzn:`forall` expression creates a constraint for each :math:`i, j` pair which meet
292the requirement :math:`i < j`, thus creating
293
294.. code-block:: minizinc
295
296 constraint v[1] != v[2]; % S != E
297 constraint v[1] != v[3]; % S != N
298 ...
299 constraint v[1] != v[8]; % S != Y
300 constraint v[2] != v[3]; % E != N
301 ...
302 constraint v[7] != v[8]; % R != Y
303
304In FlatZinc form this is
305
306.. code-block:: minizinc
307
308 constraint int_neq(S,E);
309 constraint int_neq(S,N);
310 ...
311 constraint int_neq(S,Y);
312 constraint int_neq(E,N);
313 ...
314 constraint int_neq(R,Y);
315
316Notice how the temporary array variables :mzn:`v[i]` are replaced by the
317original variables in the output FlatZinc.
318
319Arrays
320------
321
322One dimensional arrays
323in MiniZinc can have arbitrary indices as long as they are
324contiguous integers. In FlatZinc all arrays are indexed from :mzn:`1..l`
325where :mzn:`l` is the length of the array. This means that array lookups need to
326be translated to the FlatZinc view of indices.
327
328Consider the following MiniZinc model for balancing a seesaw
329of length :mzn:`2 * l2`,
330with a child of weight :mzn:`cw` kg using exactly :mzn:`m` 1kg weights.
331
332.. code-block:: minizinc
333
334 int: cw; % child weight
335 int: l2; % half seesaw length
336 int: m; % number of 1kg weight
337 array[-l2..l2] of var 0..max(m,cw): w; % weight at each point
338 var -l2..l2: p; % position of child
339 constraint sum(i in -l2..l2)(i * w[i]) = 0; % balance
340 constraint sum(i in -l2..l2)(w[i]) = m + cw; % all weights used
341 constraint w[p] = cw; % child is at position p
342 solve satisfy;
343
344Given :mzn:`cw = 2`, :mzn:`l2 = 2`, and :mzn:`m = 3` the unrolling produces the constraints
345
346.. code-block:: minizinc
347
348 array[-2..2] of var 0..3: w;
349 var -2..2: p
350 constraint -2*w[-2] + -1*w[-1] + 0*w[0] + 1*w[1] + 2*w[2] = 0;
351 constraint w[-2] + w[-1] + w[0] + w[1] + w[2] = 5;
352 constraint w[p] = 2;
353
354But FlatZinc insists that the :mzn:`w` array starts at index 1.
355This means we need to rewrite all the array accesses to use the new index
356value. For fixed array lookups this is easy, for variable array lookups we
357may need to create a new variable. The result for the equations above is
358
359.. code-block:: minizinc
360
361 array[1..5] of var 0..3: w;
362 var -2..2: p
363 var 1..5: INT01;
364 constraint -2*w[1] + -1*w[2] + 0*w[3] + 1*w[4] + 2*w[5] = 0;
365 constraint w[1] + w[2] + w[3] + w[4] + w[5] = 5;
366 constraint w[INT01] = 2;
367 constraint INT01 = p + 3;
368
369Finally we rewrite the constraints into FlatZinc form. Note how the variable
370array index lookup is mapped to :mzn:`array_var_int_element`.
371
372.. code-block:: minizinc
373
374 array[1..5] of var 0..3: w;
375 var -2..2: p
376 var 1..5: INT01;
377 constraint int_lin_eq([2, 1, -1, -2], [w[1], w[2], w[4], w[5]], 0);
378 constraint int_lin_eq([1, 1, 1, 1, 1], [w[1],w[2],w[3],w[4],w[5]], 5);
379 constraint array_var_int_element(INT01, w, 2);
380 constraint int_lin_eq([-1, 1], [INT01, p], -3);
381
382Multidimensional arrays are supported by MiniZinc, but only single
383dimension arrays are supported by FlatZinc (at present).
384This means that multidimensional arrays must be mapped to single dimension
385arrays, and multidimensional array access must be mapped to single dimension
386array access.
387
388Consider the Laplace equation constraints defined for a finite element
389plate model in :numref:`ex-laplace`:
390
391.. literalinclude:: examples/laplace.mzn
392 :language: minizinc
393 :start-after: % arraydec
394 :end-before: % sides
395
396
397Assuming :mzn:`w = 4` and :mzn:`h = 4` this creates the constraints
398
399.. code-block:: minizinc
400
401 array[0..4,0..4] of var float: t; % temperature at point (i,j)
402 constraint 4.0*t[1,1] = t[0,1] + t[1,0] + t[2,1] + t[1,2];
403 constraint 4.0*t[1,2] = t[0,2] + t[1,1] + t[2,2] + t[1,3];
404 constraint 4.0*t[1,3] = t[0,3] + t[1,2] + t[2,3] + t[1,4];
405 constraint 4.0*t[2,1] = t[1,1] + t[2,0] + t[3,1] + t[2,2];
406 constraint 4.0*t[2,2] = t[1,2] + t[2,1] + t[3,2] + t[2,3];
407 constraint 4.0*t[2,3] = t[1,3] + t[2,2] + t[3,3] + t[2,4];
408 constraint 4.0*t[3,1] = t[2,1] + t[3,0] + t[4,1] + t[3,2];
409 constraint 4.0*t[3,2] = t[2,2] + t[3,1] + t[4,2] + t[3,3];
410 constraint 4.0*t[3,3] = t[2,3] + t[3,2] + t[4,3] + t[3,4];
411
412The 2 dimensional array of 25 elements is converted to a one dimensional
413array and the indices are changed accordingly: so index :mzn:`[i,j]` becomes
414:mzn:`[i * 5 + j + 1]`.
415
416.. code-block:: minizinc
417
418 array [1..25] of var float: t;
419 constraint 4.0*t[7] = t[2] + t[6] + t[12] + t[8];
420 constraint 4.0*t[8] = t[3] + t[7] + t[13] + t[9];
421 constraint 4.0*t[9] = t[4] + t[8] + t[14] + t[10];
422 constraint 4.0*t[12] = t[7] + t[11] + t[17] + t[13];
423 constraint 4.0*t[13] = t[8] + t[12] + t[18] + t[14];
424 constraint 4.0*t[14] = t[9] + t[13] + t[19] + t[15];
425 constraint 4.0*t[17] = t[12] + t[16] + t[22] + t[18];
426 constraint 4.0*t[18] = t[13] + t[17] + t[23] + t[19];
427 constraint 4.0*t[19] = t[14] + t[18] + t[24] + t[20];
428
429
430Reification
431-----------
432
433.. index::
434 single: reification
435
436FlatZinc models involve only variables and parameter declarations
437and a series of primitive constraints. Hence when we model in MiniZinc
438with Boolean connectives other than conjunction, something has to be done.
439The core approach to handling complex formulae that use
440connectives other than conjunction is by
441*reification*.
442Reifying a constraint :math:`c` creates a new constraint equivalent to :math:`b \leftrightarrow c`
443where the Boolean variable :math:`b` is :mzn:`true`
444if the constraint holds and :mzn:`false` if it doesn't hold.
445
446Once we have the capability to *reify* constraints the treatment of
447complex formulae is not different from arithmetic expressions. We create a
448name for each subexpression and a flat constraint to constrain the name to
449take the value of its subexpression.
450
451
452Consider the following constraint expression that occurs in the jobshop
453scheduling example of :numref:`ex-jobshop`.
454
455.. code-block:: minizinc
456
457 constraint %% ensure no overlap of tasks
458 forall(j in 1..tasks) (
459 forall(i,k in 1..jobs where i < k) (
460 s[i,j] + d[i,j] <= s[k,j] \/
461 s[k,j] + d[k,j] <= s[i,j]
462 ) );
463
464Given the data file
465
466.. code-block:: minizinc
467
468 jobs = 2;
469 tasks = 3;
470 d = [| 5, 3, 4 | 2, 6, 3 |]
471
472then the unrolling creates
473
474.. code-block:: minizinc
475
476 constraint s[1,1] + 5 <= s[2,1] \/ s[2,1] + 2 <= s[1,1];
477 constraint s[1,2] + 3 <= s[2,2] \/ s[2,2] + 6 <= s[1,2];
478 constraint s[1,3] + 4 <= s[2,3] \/ s[2,3] + 3 <= s[1,3];
479
480Reification of the constraints that appear in the disjunction
481creates new Boolean variables to define the values of each expression.
482
483.. code-block:: minizinc
484
485 array[1..2,1..3] of var 0..23: s;
486 constraint BOOL01 <-> s[1,1] + 5 <= s[2,1];
487 constraint BOOL02 <-> s[2,1] + 2 <= s[1,1];
488 constraint BOOL03 <-> s[1,2] + 3 <= s[2,2];
489 constraint BOOL04 <-> s[2,2] + 6 <= s[1,2];
490 constraint BOOL05 <-> s[1,3] + 4 <= s[2,3];
491 constraint BOOL06 <-> s[2,3] + 3 <= s[1,3];
492 constraint BOOL01 \/ BOOL02;
493 constraint BOOL03 \/ BOOL04;
494 constraint BOOL05 \/ BOOL06;
495
496Each primitive constraint can now be mapped to the FlatZinc form.
497Note how the two dimensional array :mzn:`s` is mapped to a one dimensional form.
498
499.. code-block:: minizinc
500
501 array[1..6] of var 0..23: s;
502 constraint int_lin_le_reif([1, -1], [s[1], s[4]], -5, BOOL01);
503 constraint int_lin_le_reif([-1, 1], [s[1], s[4]], -2, BOOL02);
504 constraint int_lin_le_reif([1, -1], [s[2], s[5]], -3, BOOL03);
505 constraint int_lin_le_reif([-1, 1], [s[2], s[5]], -6, BOOL04);
506 constraint int_lin_le_reif([1, -1], [s[3], s[6]], -4, BOOL05);
507 constraint int_lin_le_reif([-1, 1], [s[3], s[6]], -3, BOOL06);
508 constraint array_bool_or([BOOL01, BOOL02], true);
509 constraint array_bool_or([BOOL03, BOOL04], true);
510 constraint array_bool_or([BOOL05, BOOL06], true);
511
512The :mzn:`int_lin_le_reif` is the reified form of the linear constraint
513:mzn:`int_lin_le`.
514
515Most FlatZinc primitive constraints :math:`p(\bar{x})` have a reified form
516:math:`\mathit{p\_reif}(\bar{x},b)` which takes an additional final argument :math:`b`
517and defines the constraint :math:`b \leftrightarrow p(\bar{x})`.
518FlatZinc primitive constraints which define functional relationships,
519like :mzn:`int_plus` and :mzn:`int_plus`, do
520not need to support reification. Instead, the equality with the result of the function is reified.
521
522Another important use of reification arises when we use the coercion
523function :mzn:`bool2int` (either explicitly, or implicitly by using a Boolean
524expression as an integer expression). Flattening creates a Boolean
525variable to hold the value of the Boolean expression argument, as well as an
526integer variable (restricted to :mzn:`0..1`) to hold this value.
527
528Consider the magic series problem of :numref:`ex-magic-series`.
529
530.. literalinclude:: examples/magic-series.mzn
531 :language: minizinc
532 :end-before: solve satisfy
533
534Given :mzn:`n = 2` the unrolling creates
535
536.. code-block:: minizinc
537
538 constraint s[0] = bool2int(s[0] = 0) + bool2int(s[1] = 0);
539 constraint s[1] = bool2int(s[0] = 1) + bool2int(s[1] = 1);
540
541and flattening creates
542
543.. code-block:: minizinc
544
545 constraint BOOL01 <-> s[0] = 0;
546 constraint BOOL03 <-> s[1] = 0;
547 constraint BOOL05 <-> s[0] = 1;
548 constraint BOOL07 <-> s[1] = 1;
549 constraint INT02 = bool2int(BOOL01);
550 constraint INT04 = bool2int(BOOL03);
551 constraint INT06 = bool2int(BOOL05);
552 constraint INT08 = bool2int(BOOL07);
553 constraint s[0] = INT02 + INT04;
554 constraint s[1] = INT06 + INT08;
555
556The final FlatZinc form is
557
558.. code-block:: minizinc
559
560 var bool: BOOL01;
561 var bool: BOOL03;
562 var bool: BOOL05;
563 var bool: BOOL07;
564 var 0..1: INT02;
565 var 0..1: INT04;
566 var 0..1: INT06;
567 var 0..1: INT08;
568 array [1..2] of var 0..2: s;
569 constraint int_eq_reif(s[1], 0, BOOL01);
570 constraint int_eq_reif(s[2], 0, BOOL03);
571 constraint int_eq_reif(s[1], 1, BOOL05);
572 constraint int_eq_reif(s[2], 1, BOOL07);
573 constraint bool2int(BOOL01, INT02);
574 constraint bool2int(BOOL03, INT04);
575 constraint bool2int(BOOL05, INT06);
576 constraint bool2int(BOOL07, INT08);
577 constraint int_lin_eq([-1, -1, 1], [INT02, INT04, s[1]], 0);
578 constraint int_lin_eq([-1, -1, 1], [INT06, INT08, s[2]], 0);
579 solve satisfy;
580
581Predicates
582----------
583
584An important factor in the support for MiniZinc by many different solvers
585is that global constraints (and indeed FlatZinc constraints) can be
586specialized for the particular solver.
587
588Each solver will either specify a predicate without a definition, or with a
589definition. For example a solver that has a builtin global :mzn:`alldifferent`
590predicate, will include the definition
591
592.. code-block:: minizinc
593
594 predicate alldifferent(array[int] of var int:x);
595
596in its globals library, while a solver using the default decomposition will
597have the definition
598
599.. code-block:: minizinc
600
601 predicate alldifferent(array[int] of var int:x) =
602 forall(i,j in index_set(x) where i < j)(x[i] != x[j]);
603
604Predicate calls :math:`p(\bar{t})`
605are flattened by first constructing variables :math:`v_i` for
606each argument terms :math:`t_i`.
607If the predicate has no definition we simply use a call to the predicate
608with the constructed arguments: :math:`p(\bar{v})`.
609If the predicate has a definition :math:`p(\bar{x}) = \phi(\bar{x})`
610then we replace the predicate call :math:`p(\bar{t})`
611with the body of the predicate with the formal arguments replaced by the
612argument variables, that is :math:`\phi(\bar{v})`.
613Note that if a predicate call :math:`p(\bar{t})`
614appears in a reified position and it has no definition, we check for the
615existence of a reified version of the predicate :math:`\mathit{p\_reif}(\bar{x},b)` in which
616case we use that.
617
618Consider the :mzn:`alldifferent` constraint in the
619SEND-MORE-MONEY example of :numref:`ex-smm`
620
621.. code-block:: minizinc
622
623 constraint alldifferent([S,E,N,D,M,O,R,Y]);
624
625If the solver has a builtin :mzn:`alldifferent` we simply construct a new variable
626for the argument, and replace it in the call.
627
628.. code-block:: minizinc
629
630 array[1..8] of var 0..9: v = [S,E,N,D,M,O,R,Y];
631 constraint alldifferent(v);
632
633Notice that bounds analysis attempts to find tight bounds on the new array
634variable. The reason for constructing the array argument is if we use the
635same array twice the FlatZinc solver does not have to construct it twice.
636In this case since it is not used twice a later stage of the translation
637will replace :mzn:`v` by its definition.
638
639What if the solver uses the default definition of :mzn:`alldifferent`?
640Then the variable :mzn:`v` is defined as usual, and the predicate call is
641replaced by a renamed copy where :mzn:`v` replaces the formal argument :mzn:`x`.
642The resulting code is
643
644.. code-block:: minizinc
645
646 array[1..8] of var 0..9: v = [S,E,N,D,M,O,R,Y];
647 constraint forall(i,j in 1..8 where i < j)(v[i] != v[j])
648
649which we examined in :ref:`sec-unroll`.
650
651Consider the following constraint, where :mzn:`alldifferent` appears in a reified
652position.
653
654.. code-block:: minizinc
655
656 constraint alldifferent([A,B,C]) \/ alldifferent([B,C,D]);
657
658If the solver has a reified form of :mzn:`alldifferent` this will be flattened to
659
660.. code-block:: minizinc
661
662 constraint alldifferent_reif([A,B,C],BOOL01);
663 constraint alldifferent_reif([B,C,D],BOOL02);
664 constraint array_bool_or([BOOL01,BOOL02],true);
665
666Using the default decomposition, the predicate replacement will first create
667
668.. code-block:: minizinc
669
670 array[1..3] of var int: v1 = [A,B,C];
671 array[1..3] of var int: v2 = [B,C,D];
672 constraint forall(i,j in 1..3 where i<j)(v1[i] != v1[j]) \/
673 forall(i,j in 1..3 where i<j)(v2[i] != v2[j]);
674
675which will eventually be flattened to the FlatZinc form
676
677.. code-block:: minizinc
678
679 constraint int_neq_reif(A,B,BOOL01);
680 constraint int_neq_reif(A,C,BOOL02);
681 constraint int_neq_reif(B,C,BOOL03);
682 constraint array_bool_and([BOOL01,BOOL02,BOOL03],BOOL04);
683 constraint int_neq_reif(B,D,BOOL05);
684 constraint int_neq_reif(C,D,BOOL06);
685 constraint array_bool_and([BOOL03,BOOL05,BOOL06],BOOL07);
686 constraint array_bool_or([BOOL04,BOOL07],true);
687
688Note how common subexpression elimination reuses the
689reified inequality :mzn:`B != C` (although there is a better translation which
690lifts the common constraint to the top level conjunction).
691
692.. _sec-let:
693
694Let Expressions
695---------------
696
697Let expressions are a powerful facility of MiniZinc to introduce new
698variables. This is useful for creating common sub expressions, and for
699defining local variables for predicates.
700During flattening let expressions are translated to variable and constraint
701declarations. The relational semantics of MiniZinc means that these
702constraints must appear as if conjoined
703in the first enclosing Boolean expression.
704
705A key feature of let expressions is that each time they are used they
706create new variables.
707
708Consider the flattening of the code
709
710.. code-block:: minizinc
711
712 constraint even(u) \/ even(v);
713 predicate even(var int: x) =
714 let { var int: y } in x = 2 * y;
715
716First the predicate calls are replaced by their definition.
717
718.. code-block:: minizinc
719
720 constraint (let { var int: y} in u = 2 * y) \/
721 (let { var int: y} in v = 2 * y);
722
723Next let variables are renamed apart
724
725.. code-block:: minizinc
726
727 constraint (let { var int: y1} in u = 2 * y1) \/
728 (let { var int: y2} in v = 2 * y2);
729
730Finally variable declarations are extracted to the top level
731
732.. code-block:: minizinc
733
734 var int: y1;
735 var int: y2;
736 constraint u = 2 * y1 \/ v = 2 * y2;
737
738Once the let expression is removed we can flatten as usual.
739
740Remember that let expressions can define values for newly introduced
741variables (and indeed must do so for parameters).
742These implicitly define constraints that must also be flattened.
743
744Consider the complex objective function for wedding seating problem of
745:numref:`ex-wedding2`.
746
747.. code-block:: minizinc
748
749 solve maximize sum(h in Hatreds)(
750 let { var Seats: p1 = pos[h1[h]],
751 var Seats: p2 = pos[h2[h]],
752 var 0..1: same = bool2int(p1 <= 6 <-> p2 <= 6) } in
753 same * abs(p1 - p2) + (1-same) * (abs(13 - p1 - p2) + 1));
754
755For conciseness we assume only the first two Hatreds, so
756
757.. code-block:: minizinc
758
759 set of int: Hatreds = 1..2;
760 array[Hatreds] of Guests: h1 = [groom, carol];
761 array[Hatreds] of Guests: h2 = [clara, bestman];
762
763The first step of flattening is to unroll the :mzn:`sum` expression, giving
764(we keep the guest names and parameter :mzn:`Seats` for clarity only, in
765reality they would be replaced by their definition):
766
767.. code-block:: minizinc
768
769 solve maximize
770 (let { var Seats: p1 = pos[groom],
771 var Seats: p2 = pos[clara],
772 var 0..1: same = bool2int(p1 <= 6 <-> p2 <= 6) } in
773 same * abs(p1 - p2) + (1-same) * (abs(13 - p1 - p2) + 1))
774 +
775 (let { var Seats: p1 = pos[carol],
776 var Seats: p2 = pos[bestman],
777 var 0..1: same = bool2int(p1 <= 6 <-> p2 <= 6) } in
778 same * abs(p1 - p2) + (1-same) * (abs(13 - p1 - p2) + 1));
779
780Next each new variable in a let expression is renamed to be distinct
781
782.. code-block:: minizinc
783
784 solve maximize
785 (let { var Seats: p11 = pos[groom],
786 var Seats: p21 = pos[clara],
787 var 0..1: same1 = bool2int(p11 <= 6 <-> p21 <= 6) } in
788 same1 * abs(p11 - p21) + (1-same1) * (abs(13 - p11 - p21) + 1))
789 +
790 (let { var Seats: p12 = pos[carol],
791 var Seats: p22 = pos[bestman],
792 var 0..1: same2 = bool2int(p12 <= 6 <-> p22 <= 6) } in
793 same2 * abs(p12 - p22) + (1-same2) * (abs(13 - p12 - p22) + 1));
794
795Variables in the let expression
796are extracted to the top level and
797defining constraints are extracted to the correct
798level (which in this case is also the top level).
799
800.. code-block:: minizinc
801
802 var Seats: p11;
803 var Seats: p21;
804 var 0..1: same1;
805 constraint p12 = pos[clara];
806 constraint p11 = pos[groom];
807 constraint same1 = bool2int(p11 <= 6 <-> p21 <= 6);
808 var Seats p12;
809 var Seats p22;
810 var 0..1: same2;
811 constraint p12 = pos[carol];
812 constraint p22 = pos[bestman];
813 constraint same2 = bool2int(p12 <= 6 <-> p22 <= 6) } in
814 solve maximize
815 same1 * abs(p11 - p21) + (1-same1) * (abs(13 - p11 - p21) + 1))
816 +
817 same2 * abs(p12 - p22) + (1-same2) * (abs(13 - p12 - p22) + 1));
818
819Now we have constructed equivalent MiniZinc code without the use of let
820expressions and the flattening can proceed as usual.
821
822As an illustration of let expressions that do not appear at the top level
823consider the following model
824
825.. code-block:: minizinc
826
827 var 0..9: x;
828 constraint x >= 1 -> let { var 2..9: y = x - 1 } in
829 y + (let { var int: z = x * y } in z * z) < 14;
830
831We extract the variable definitions to the top level and the constraints to
832the first enclosing Boolean context, which here is the right hand side of
833the implication.
834
835.. code-block:: minizinc
836
837 var 0..9: x;
838 var 2..9: y;
839 var int: z;
840 constraint x >= 1 -> (y = x - 1 /\ z = x * y /\ y + z * z < 14);
841
842Note that if we know that the equation defining a variable definition
843cannot fail we can extract it to the top level. This will usually make
844solving substantially faster.
845
846For the example above the constraint :mzn:`y = x - 1` can fail since the domain
847of :mzn:`y` is not big enough for all possible values of :mzn:`x - 1`. But the
848constraint :mzn:`z = x * y` cannot (indeed bounds analysis will give :mzn:`z`
849bounds big enough to hold all possible values of :mzn:`x * y`).
850A better flattening will give
851
852.. code-block:: minizinc
853
854 var 0..9: x;
855 var 2..9: y;
856 var int: z;
857 constraint z = x * y;
858 constraint x >= 1 -> (y = x - 1 /\ y + z * z < 14);
859
860Currently the MiniZinc compiler does this by always defining the declared
861bounds of an
862introduced variable to be big enough for its defining equation to always
863hold and then adding bounds constraints in the correct context for the let
864expression. On the example above this results in
865
866.. code-block:: minizinc
867
868 var 0..9: x;
869 var -1..8: y;
870 var -9..72: z;
871 constraint y = x - 1;
872 constraint z = x * y;
873 constraint x >= 1 -> (y >= 2 /\ y + z * z < 14);
874
875This translation leads to more efficient solving since the possibly
876complex calculation of the let variable is not reified.
877
878Another reason for this approach is that it also works when introduced variables
879appear in negative contexts (as long as they have a definition).
880Consider the following example similar to the previous one
881
882.. code-block:: minizinc
883
884 var 0..9: x;
885 constraint (let { var 2..9: y = x - 1 } in
886 y + (let { var int: z = x * y } in z * z) > 14) -> x >= 5;
887
888The let expressions appear in a negated context, but each introduced
889variable is defined. The flattened code is
890
891.. code-block:: minizinc
892
893 var 0..9: x;
894 var -1..8: y;
895 var -9..72: z;
896 constraint y = x - 1;
897 constraint z = x * y;
898 constraint (y >= 2 /\ y + z * z > 14) -> x >= 5;
899
900Note the analog to the simple approach to let elimination
901does not give a correct translation:
902
903.. code-block:: minizinc
904
905 var 0..9: x;
906 var 2..9: y;
907 var int: z;
908 constraint (y = x - 1 /\ z = x * y /\ y + z * z > 14) -> x >= 5;
909
910gives answers for all possible values of :mzn:`x`, whereas the original
911constraint removes the possibility that :mzn:`x = 4`.
912
913The treatment of *constraint items* in let expressions is analogous
914to defined variables. One can think of a constraint as equivalent to
915defining a new Boolean variable. The definitions of the new Boolean variables
916are extracted to the top level, and the Boolean remains in the correct
917context.
918
919.. code-block:: minizinc
920
921 constraint z > 1 -> let { var int: y,
922 constraint (x >= 0) -> y = x,
923 constraint (x < 0) -> y = -x
924 } in y * (y - 2) >= z;
925
926is treated like
927
928.. code-block:: minizinc
929
930 constraint z > 1 -> let { var int: y,
931 var bool: b1 = ((x >= 0) -> y = x),
932 var bool: b2 = ((x < 0) -> y = -x),
933 constraint b1 /\ b2
934 } in y * (y - 2) >= z;
935
936and flattens to
937
938.. code-block:: minizinc
939
940 constraint b1 = ((x >= 0) -> y = x);
941 constraint b2 = ((x < 0) -> y = -x);
942 constraint z > 1 -> (b1 /\ b2 /\ y * (y - 2) >= z);