this repo has no description
dekker.one
1More Complex Models
2===================
3
4In the last section we introduced the basic structure of a MiniZinc
5model. In this section we introduce the array and set data structures,
6enumerated types and
7more complex constraints.
8
9.. _sec-arrayset:
10
11Arrays and Sets
12---------------
13
14Almost always we are interested in building models where the number of
15constraints and variables is dependent on the input data.
16In order to do so we will usually use :index:`arrays <array>`.
17
18Consider a simple finite element model for modelling temperatures on a
19rectangular sheet of metal. We approximate the temperatures across the
20sheet by breaking the sheet into a finite number of elements in a
21two-dimensional matrix.
22A model is shown in :numref:`ex-laplace`.
23It declares the width ``w`` and height ``h``
24of the finite element model.
25The declaration
26
27.. literalinclude:: examples/laplace.mzn
28 :language: minizinc
29 :lines: 5-9
30
31declares four fixed sets of integers describing the dimensions of the finite
32element model: ``HEIGHT`` is the whole height of the model, while ``CHEIGHT`` is
33the centre of the height omitting the top and bottom,
34``WIDTH`` is the whole width of the model, while
35``CWIDTH`` is the centre of the width omitting the left and right sides.
36Finally a two dimensional array of float variables ``t``
37with rows numbered
38:math:`0` to :math:`h` (``HEIGHT``) and columns :math:`0` to :math:`w` (``WIDTH``),
39to represent the temperatures at each
40point in the metal plate.
41We can access the element of the array in the :math:`i^{th}` row and :math:`j^{th}` column
42using an expression :mzn:`t[i,j]`.
43
44
45Laplace's
46equation states that when the plate reaches a steady state
47the temperature at each internal point is the average of its orthogonal
48neighbours. The constraint
49
50.. literalinclude:: examples/laplace.mzn
51 :language: minizinc
52 :lines: 16-18
53
54ensures that each internal point :math:`(i,j)` is the
55average of its four orthogonal neighbours.
56The constraints
57
58.. literalinclude:: examples/laplace.mzn
59 :language: minizinc
60 :lines: 20-24
61
62restrict the temperatures on each edge to be equal, and
63gives these temperatures names: ``left``, ``right``, ``top``
64and ``bottom``.
65While the constraints
66
67.. literalinclude:: examples/laplace.mzn
68 :language: minizinc
69 :lines: 26-30
70
71ensure that the corners (which are irrelevant) are set to 0.0.
72We can determine the temperatures in a plate broken into 5 :math:`\times` 5
73elements with left, right and bottom temperature 0 and top temperature 100
74with the model shown in :numref:`ex-laplace`.
75
76
77.. literalinclude:: examples/laplace.mzn
78 :language: minizinc
79 :name: ex-laplace
80 :caption: Finite element plate model for determining steady state temperatures (:download:`laplace.mzn <examples/laplace.mzn>`).
81
82Running the command
83
84.. code-block:: bash
85
86 $ minizinc --solver cbc laplace.mzn
87
88gives the output
89
90.. code-block:: none
91
92 -0.00 100.00 100.00 100.00 -0.00
93 -0.00 42.86 52.68 42.86 -0.00
94 -0.00 18.75 25.00 18.75 -0.00
95 -0.00 7.14 9.82 7.14 -0.00
96 -0.00 -0.00 -0.00 -0.00 -0.00
97 ----------
98
99.. defblock:: Sets
100
101 .. index::
102 single: set
103
104 Set variables are declared with a declaration of the form
105
106 .. code-block:: minizincdef
107
108 set of <type-inst> : <var-name> ;
109
110 where sets of integers, enums (see later), floats or Booleans are allowed.
111 The only type allowed for decision variable sets are variable sets of
112 integers or enums.
113 Set literals are of the form
114
115 .. code-block:: minizincdef
116
117 { <expr-1>, ..., <expr-n> }
118
119 or are :index:`range` expressions over either integers, enums or floats of the form
120
121 .. code-block:: minizincdef
122
123 <expr-1> .. <expr-2>
124
125 The standard :index:`set operations <operator; set>`
126 are provided: element membership
127 (:mzn:`in`),
128 (non-strict) subset relationship (:mzn:`subset`),
129 (non-strict) superset relationship (:mzn:`superset`), union
130 (:mzn:`union`),
131 intersection (:mzn:`intersect`),
132 set difference (:mzn:`diff`),
133 symmetric set difference (:mzn:`symdiff`)
134 and the number of elements in the
135 set (:mzn:`card`).
136
137 As we have seen set variables and set literals (including ranges) can be
138 used as an implicit type in variable declarations in which case the variable
139 has the type of the elements in the set and the variable is implicitly
140 constrained to be a member of the set.
141
142
143Our cake baking problem is an example of a very simple kind of production
144planning problem. In this kind of problem we wish to determine how much of
145each kind of product to make to maximise the profit where manufacturing a
146product consumes varying amounts of some fixed resources. We can generalise
147the MiniZinc model in :numref:`ex-cakes2` to handle this kind of problem
148with a model that is generic in the kinds of resources and products. The
149model is shown in :numref:`ex-prod-planning` and a sample data file (for
150the cake baking example) is shown in :numref:`fig-prod-planning-data`.
151
152
153.. literalinclude:: examples/prod-planning.mzn
154 :language: minizinc
155 :name: ex-prod-planning
156 :caption: Model for simple production planning (:download:`prod-planning.mzn <examples/prod-planning.mzn>`).
157
158.. literalinclude:: examples/prod-planning-data.dzn
159 :language: minizinc
160 :name: fig-prod-planning-data
161 :caption: Example data file for the simple production planning problem (:download:`prod-planning-data.dzn <examples/prod-planning-data.dzn>`).
162
163The new feature in this model is the use of :index:`enumerated
164types <type; enumerated>`.
165These allow us to treat the choice of resources and products as parameters to
166the model.
167The first item in the model
168
169.. code-block:: minizinc
170
171 enum Products;
172
173declares ``Products`` as an *unknown* set of products.
174
175.. defblock:: Enumerated Types
176
177 .. index::
178 single: enumerated type
179 single enum
180
181 Enumerated types, which we shall refer to as ``enums``,
182 are declared with a declaration of the form
183
184 .. code-block:: minizincdef
185
186 enum <var-name> ;
187
188 An enumerated type is defined by an assignment of the form
189
190
191 .. code-block:: minizincdef
192
193 enum <var-name> = { <var-name-1>, ..., <var-name-n> } ;
194
195 where :mzndef:`<var-name-1>`, ..., :mzndef:`<var-name-n>` are the elements of
196 the enumerated type, with name :mzndef:`<var-name>`.
197 Each of the elements of the enumerated type is also effectively declared by
198 this definition as a new constant of that type.
199 The declaration and definition can be combined into one line as usual.
200
201The second item declares an array of integers:
202
203.. code-block:: minizinc
204
205 array[Products] of int: profit;
206
207The :index:`index set <array; index set>`
208of the array ``profit`` is ``Products``.
209This means that only elements of the set ``Products``
210can be used to index the array.
211
212The elements of an enumerated type of :math:`n` elements
213act very similar to the integers :math:`1\dots n`. They can be compared, they are
214ordered, by the order they appear in the enumerated type definition,
215they can be iterated over, they can appear as indices of arrays, in fact
216they can appear anywhere an integer can appear.
217
218In the example data file we have initialized the array using a list of
219integers
220
221.. code-block:: minizinc
222
223 Products = { BananaCake, ChocolateCake };
224 profit = [400,450];
225
226meaning the profit for a banana cake is 400, while for a chocolate cake it
227is 450. Internally ``BananaCake`` will be treated like the integer 1,
228while ``ChocolateCake`` will be treated like the integer 2.
229The expression :mzn:`[400,500]` represents a literal one-dimensional array. In MiniZinc, the index set of literal arrays always starts at 1 (this is similar to other mathematically inspired languages such as MATLAB, Julia or Mathematica).
230While MiniZinc does not provide an explicit list type, one-dimensional
231arrays with an index set :mzn:`1..n` behave like lists, and we will sometimes
232refer to them as :index:`lists <list>`.
233
234In a similar fashion, in the next two items we declare a set of resources
235``Resources``, and an array ``capacity`` which gives the amount of
236each resource that is available.
237
238More interestingly, the item
239
240.. code-block:: minizinc
241
242 array[Products, Resources] of int: consumption;
243
244declares a 2-D array ``consumption``. The value of
245:mzn:`consumption[p,r]` is the amount of resource :mzn:`r` required to
246produce one unit of product :mzn:`p`. Note that the first index is the row
247and the second is the column.
248
249The data file contains an example initialization of a 2-D array:
250
251.. code-block:: minizinc
252
253 consumption= [| 250, 2, 75, 100, 0,
254 | 200, 0, 150, 150, 75 |];
255
256Notice how the delimiter ``|`` is used to separate rows. As for one-dimensional array literals, indexing of two-dimensional array literals also starts at 1.
257
258.. defblock:: Arrays
259
260 .. index:
261 single: array
262
263 Thus, MiniZinc provides one- and multi-dimensional arrays
264 which are declared using the type:
265
266 .. code-block:: minizincdef
267
268 array [ <index-set-1>, ..., <index-set-n> ] of <type-inst>
269
270 MiniZinc requires that the array declaration contains the index set of each
271 dimension and that the index set is either an integer range, a set
272 variable initialised to an integer range, or an :index:`enumeration type <enumerated type>`.
273 Arrays can contain any of the base
274 types: integers, enums, Booleans, floats or strings. These can be fixed or unfixed
275 except for strings which can only be parameters. Arrays can also contain
276 sets but they cannot contain arrays.
277
278 :index:`One-dimensional array literals <array; literal; 1D>` are of form
279
280 .. code-block:: minizincdef
281
282 [ <expr-1>, ..., <expr-n> ]
283
284 and their index sets are :mzn:`1..n`,
285 while :index:`two-dimensional array literals <array; literal; 2D>` are of form
286
287 .. code-block:: minizincdef
288
289 [| <expr-1-1>, ..., <expr-1-n> |
290 ... |
291 <expr-m-1>, ..., <expr-m-n> |]
292
293 where the array has ``m`` rows and ``n`` columns, with index sets :mzn:`1..m` for the first and :mzn:`1..n` for the second dimension.
294
295 The family of built-in functions :mzn:`array1d`,
296 :mzn:`array2d`, etc,
297 can be used to initialise an array of any dimension from a list (or more
298 exactly a one-dimensional array). The call:
299
300 .. code-block:: minizincdef
301
302 array<n>d(<index-set-1>, ..., <index-set-n>, <list>)
303
304 returns an ``n`` dimensional array with index sets given by the first ``n``
305 arguments and the last argument contains the elements of the array. For
306 instance, :mzn:`array2d(1..3, 1..2, [1, 2, 3, 4, 5, 6])` is equivalent to
307 :mzn:`[|1, 2 |3, 4 |5, 6|]`.
308
309 Array elements are :index:`accessed <array; access>` using bracket syntax: :mzn:`a[i,j]` gives the
310 element at row index :math:`i^{th}` and column index :math:`j^{th}`.
311
312 .. \pjs{New array functions!}
313
314
315 The concatenation operator ``++``
316 can be used to concatenate two
317 one-dimensional arrays together. The result is a list, i.e. a
318 one-dimensional array whose elements are indexed from 1. For instance
319 :mzn:`[4000, 6] ++ [2000, 500, 500]` evaluates to :mzn:`[4000, 6, 2000, 500, 500]`.
320 The built-in function
321 :mzn:`length` returns the length
322 of a one-dimensional array.
323
324The next item in the model defines the parameter :mzn:`mproducts`. This is
325set to an upper-bound on the number of products of any type that can be
326produced. This is quite a complex example of nested
327array comprehensions and aggregation operators. We shall introduce these
328before we try to understand this item and the rest of the model.
329
330First, MiniZinc provides list comprehensions similar to those provided in
331many functional programming languages, or Python. For example, the list comprehension
332:mzn:`[i + j | i, j in 1..3 where j < i]` evaluates to :mzn:`[2 + 1, 3 + 1, 3 + 2]`
333which is :mzn:`[3, 4, 5]`. Of course :mzn:`[3, 4, 5]` is
334simply an array with index set :mzn:`1..3`.
335
336MiniZinc also provides set comprehensions which have a similar syntax: for
337instance, :mzn:`{i + j | i, j in 1..3 where j < i}` evaluates to the set
338:mzn:`{3, 4, 5}`.
339
340.. defblock:: List and Set Comprehensions
341
342 .. index:
343 single: comprehension
344 single: comprehension; list
345
346 The generic form of a list comprehension is
347
348 .. code-block:: minizincdef
349
350 [ <expr> | <generator-exp> ]
351
352 The expression :mzndef:`<expr>` specifies how to construct elements in the
353 output list from the elements generated by :mzndef:`<generator-exp>`.
354 The generator :mzndef:`<generator-exp>` consists of a comma separated sequence of
355 generator expressions optionally followed by a Boolean expression. The two forms are
356
357 .. code-block:: minizincdef
358
359 <generator>
360 <generator> where <bool-exp>
361
362 The optional :mzndef:`<bool-exp>` in the second form acts as a filter on
363 the generator expression: only elements satisfying the Boolean expression
364 are used to construct elements in the output list. A :index:`generator <comprehension; generator>`
365 :mzndef:`<generator>`
366 has the form
367
368 .. code-block:: minizincdef
369
370 <identifier>, ..., <identifier> in <array-exp>
371
372 Each identifier is an *iterator*
373 which takes the values
374 of the array expression in turn, with the last identifier varying most rapidly.
375
376 The generators of a list comprehension and :mzndef:`<bool-exp>`
377 usually do not involve decision variables.
378 If they do involve decision variables
379 then the list produced is a list of :mzndef:`var opt <T>` where :mzndef:`<T>` is the type
380 of the :mzndef:`<expr>`. See the discussion of :index:`option types <option type>`
381 in :ref:`sec-optiontypes` for more details.
382
383 :index:`Set comprehensions <comprehension; set>`
384 are almost identical to list comprehensions: the only
385 difference is the use of ``{`` and ``}`` to enclose the
386 expression rather than ``[`` and ``]``.
387 The elements generated by a set comprehension must be
388 :index:`fixed`, i.e. free of decision variables.
389 Similarly the generators and optional :mzndef:`<bool-exp>`
390 for set comprehensions must be fixed.
391
392
393.. index::
394 single: forall
395
396Second, MiniZinc provides a number of built-in functions that take a
397one-dimensional array and aggregate the elements. Probably the most useful
398of these is :mzn:`forall`.
399This takes an array of Boolean expressions
400(that is, constraints) and returns a single Boolean expression which is the
401logical conjunction of the Boolean expressions in the array.
402
403For example, consider the expression
404
405.. code-block:: minizinc
406
407 forall( [a[i] != a[j] | i,j in 1..3 where i < j])
408
409where ``a`` is an arithmetic array with index set ``1..3``. This
410constrains the elements in ``a`` to be pairwise different. The list
411comprehension evaluates to :mzn:`[ a[1] != a[2], a[1] != a[3], a[2] != a[3] ]`
412and so the :mzn:`forall` function returns the logical
413conjunction :mzn:`a[1] != a[2] /\ a[1] != a[3] /\ a[2] != a[3]`.
414
415.. defblock:: Aggregation functions
416
417 .. index::
418 single: aggregation function
419 single: sum
420 single: product
421 single: min
422 single: max
423 single: forall
424 single: exists
425 single: xorall
426 single: iffall
427 single: aggregation function; sum
428 single: aggregation function; product
429 single: aggregation function; min
430 single: aggregation function; max
431 single: aggregation function; forall
432 single: aggregation function; exists
433 single: aggregation function; xorall
434 single: aggregation function; iffall
435
436 The *aggregation functions* for arithmetic arrays are:
437 :mzn:`sum` which adds the elements, :mzn:`product` which multiplies them together,
438 and :mzn:`min` and :mzn:`max` which respectively return the least and
439 greatest element in the array. When applied to an empty array, :mzn:`min` and
440 :mzn:`max` give a run-time error, :mzn:`sum` returns 0 and :mzn:`product`
441 returns 1.
442
443 MiniZinc provides four aggregation functions for arrays containing Boolean
444 expressions. As we have seen, the first of these,
445 :mzn:`forall`, returns
446 a single constraint which is the logical conjunction of the
447 constraints.
448 The second function, :mzn:`exists`,
449 returns the logical
450 disjunction of the constraints. Thus, :mzn:`forall` enforces that all
451 constraints in the array hold, while :mzn:`exists` ensures that at least
452 one of the constraints holds.
453 The third function, :mzn:`xorall`,
454 ensures that an odd number of constraints hold.
455 The fourth function, :mzn:`iffall`,
456 ensures that an even number of constraints holds.
457
458The third, and final, piece in the puzzle is that MiniZinc allows a special
459syntax for aggregation functions when used with an array
460comprehension. Instead of writing
461
462.. code-block:: minizinc
463
464 forall( [a[i] != a[j] | i,j in 1..3 where i < j])
465
466the modeller can instead write the more mathematical looking
467
468.. code-block:: minizinc
469
470 forall (i,j in 1..3 where i < j) (a[i] != a[j])
471
472The two expressions are completely equivalent: the modeller is free to use
473whichever they feel looks most natural.
474
475.. defblock:: Generator call expressions
476
477 .. index::
478 single: generator call
479 single: expression; generator call
480
481 A *generator call expression* has form
482
483 .. code-block:: minizincdef
484
485 <agg-func> ( <generator-exp> ) ( <exp> )
486
487 The round brackets around the generator expression
488 :mzndef:`<generator-exp>` and the constructor expression
489 :mzndef:`<exp>` are not optional: they must be there. This is
490 equivalent to writing
491
492 .. code-block:: minizincdef
493
494 <agg-func> ( [ <exp> | <generator-exp> ] )
495
496 The :index:`aggregation function` :mzndef:`<agg-func>` is any MiniZinc
497 function expecting a single array as argument.
498
499
500We are now in a position to understand the rest of the simple production
501planning model shown in :numref:`ex-prod-planning`. For the moment ignore
502the item defining :mzn:`mproducts`. The item afterwards:
503
504.. code-block:: minizinc
505
506 array[Products] of var 0..mproducts: produce;
507
508defines a one-dimensional array :mzn:`produce` of decision variables. The
509value of :mzn:`produce[p]` will be set to the amount of product :mzn:`p`
510in the optimal solution.
511The next item
512
513.. code-block:: minizinc
514
515 array[Resources] of var 0..max(capacity): used;
516
517defines a set of auxiliary variables that record how much of each resource
518is used.
519The next two constraints
520
521.. code-block:: minizinc
522
523 constraint forall (r in Resources)
524 (used[r] = sum (p in Products) (consumption[p, r] * produce[p]));
525 constraint forall (r in Resources)(used[r] <= capacity[r] );
526
527compute in :mzn:`used[r]` the total consumption of the
528resource :mzn:`r` and ensure it is less than the available amount.
529Finally, the item
530
531.. code-block:: minizinc
532
533 solve maximize sum (p in Products) (profit[p]*produce[p]);
534
535indicates that this is a maximisation problem and that the objective to be maximised is the total profit.
536
537
538We now return to the definition of :mzn:`mproducts`. For each product
539:mzn:`p` the expression
540
541.. code-block:: minizinc
542
543 (min (r in Resources where consumption[p,r] > 0)
544 (capacity[r] div consumption[p,r]))
545
546determines the maximum amount of :mzn:`p` that can be produced taking into
547account the amount of each resource :mzn:`r` and how much of :mzn:`r` is
548required to produce the product. Notice the use of the filter
549:mzn:`where consumption[p,r] > 0` to ensure that only resources required to make the
550product are considered so as to avoid a division by zero error. Thus, the
551complete expression
552
553.. code-block:: minizinc
554
555 int: mproducts = max (p in Products)
556 (min (r in Resources where consumption[p,r] > 0)
557 (capacity[r] div consumption[p,r]));
558
559computes the maximum amount of *any* product that can be produced, and
560so this can be used as an upper bound on the domain of the decision
561variables in :mzn:`produce`.
562
563Finally notice the output item is more complex,
564and uses :index:`list comprehensions <comprehension; list>`
565to create an understandable output. Running
566
567.. code-block:: bash
568
569 $ minizinc --solver gecode prod-planning.mzn prod-planning-data.dzn
570
571results in the output
572
573.. code-block:: none
574
575 BananaCake = 2;
576 ChocolateCake = 2;
577 Flour = 900;
578 Banana = 4;
579 Sugar = 450;
580 Butter = 500;
581 Cocoa = 150;
582 ----------
583 ==========
584
585
586Global Constraints
587------------------
588
589.. \index{constraint!global|see{global constraint}}
590.. \index{global constraint}
591
592MiniZinc includes a library of global constraints which can also be used
593to define models. An example is the :mzn:`alldifferent`
594constraint which requires
595all the variables appearing in its argument to be pairwise different.
596
597
598.. literalinclude:: examples/send-more-money.mzn
599 :language: minizinc
600 :name: ex-smm
601 :caption: Model for the cryptarithmetic problem SEND+MORE=MONEY (:download:`send-more-money.mzn <examples/send-more-money.mzn>`)
602
603The SEND+MORE=MONEY problem requires assigning a different
604digit to each letter so that the arithmetic constraint holds.
605The model shown in :numref:`ex-smm` uses the constraint expression
606:mzn:`alldifferent([S,E,N,D,M,O,R,Y])`
607to ensure that each letter takes a different digit value.
608The global constraint is made available
609in the model using include item
610
611.. code-block:: minizinc
612
613 include "alldifferent.mzn";
614
615which makes
616the global constraint :mzn:`alldifferent` usable by the model.
617One could replace this line by
618
619.. code-block:: minizinc
620
621 include "globals.mzn";
622
623which includes all globals.
624
625A list of all the global constraints
626defined for MiniZinc is included in the
627release documentation. See :ref:`sec-globals` for
628a description of some important global constraints.
629
630
631Conditional Expressions
632-----------------------
633
634.. \index{expression!conditional}
635
636MiniZinc provides a conditional *if-then-else-endif*
637expression.
638An example of its use is
639
640.. code-block:: minizinc
641
642 int: r = if y != 0 then x div y else 0 endif;
643
644which sets :mzn:`r` to :mzn:`x` divided by :mzn:`y` unless :mzn:`y` is zero in which case
645it sets it to zero.
646
647.. defblock:: Conditional expressions
648
649 .. index::
650 single: expression; conditional
651
652 The form of a conditional expression is
653
654 .. code-block:: minizincdef
655
656 if <bool-exp> then <exp-1> else <exp-2> endif
657
658 It is a true expression rather than a control flow statement and so can be used in other expressions.
659 It evaluates to :mzndef:`<exp-1>` if the Boolean expression :mzndef:`<bool-exp>` is true and
660 :mzndef:`<exp-2>` otherwise. The type of the conditional expression is that of
661 :mzndef:`<exp-1>` and :mzndef:`<exp-2>` which must have the same
662 type.
663
664 If the :mzndef:`<bool-exp>` contains decision variables, then the
665 type-inst
666 of the expression is :mzndef:`var <T>` where :mzndef:`<T>` is the type of
667 :mzndef:`<exp-1>` and :mzndef:`<exp-2>` even if both
668 expressions are fixed.
669
670.. literalinclude:: examples/sudoku.mzn
671 :language: minizinc
672 :name: ex-sudoku
673 :caption: Model for generalized Sudoku problem (:download:`sudoku.mzn <examples/sudoku.mzn>`)
674
675
676.. literalinclude:: examples/sudoku.dzn
677 :language: minizinc
678 :name: ex-sudokud
679 :caption: Example data file for generalised Sudoku problem (:download:`sudoku.dzn <examples/sudoku.dzn>`)
680
681.. _fig-sudoku:
682
683.. figure:: figures/sudoku.*
684
685 The problem represented by data file :download:`sudoku.dzn <examples/sudoku.dzn>`
686
687Conditional expressions are very useful in building complex models, or
688complex output. Consider the model of Sudoku problems shown in
689:numref:`ex-sudoku`. The initial board positions are given by the
690:mzn:`start` parameter where 0 represents an empty
691board position. This is converted to constraints on the decision variables
692:mzn:`puzzle` using the conditional expression
693
694.. code-block:: minizinc
695
696 constraint forall(i,j in PuzzleRange)(
697 if start[i,j] > 0 then puzzle[i,j] = start[i,j] else true endif );
698
699Conditional expressions are also very useful for
700defining complex :index:`output`.
701In the Sudoku model of :numref:`ex-sudoku` the expression
702
703.. code-block:: minizinc
704
705 if j mod S == 0 then " " else "" endif
706
707inserts an extra space between groups of size :mzn:`S`.
708The output expression also uses conditional expressions to
709add blank lines
710after each :mzn:`S` lines. The resulting output is highly readable.
711
712The remaining constraints ensure that the numbers appearing in each
713row and column and :math:`S \times S` subsquare are all different.
714
715.. index::
716 single: runtime flag; -a
717 single: runtime flag; --all-solutions
718 single: solution; all
719
720One can use MiniZinc to search
721for all solutions to a satisfaction problem (:mzn:`solve satisfy`). In the MiniZinc IDE, this can be achieved by setting the number of solutions to zero in the "User-defined behavior" part of the solver configuration pane (see :numref:`ide_solver_config`). On the command line, one can use the flag ``-a``
722or ``--all-solutions``. Running
723
724.. code-block:: bash
725
726 $ minizinc --solver gecode --all-solutions sudoku.mzn sudoku.dzn
727
728results in
729
730.. code-block:: none
731
732 5 9 3 7 6 2 8 1 4
733 2 6 8 4 3 1 5 7 9
734 7 1 4 9 8 5 2 3 6
735
736 3 2 6 8 5 9 1 4 7
737 1 8 7 3 2 4 9 6 5
738 4 5 9 1 7 6 3 2 8
739
740 9 4 2 6 1 8 7 5 3
741 8 3 5 2 4 7 6 9 1
742 6 7 1 5 9 3 4 8 2
743 ----------
744 ==========
745
746The line ``==========``
747is output when the system has output all possible
748solutions, here verifying that there is exactly one.
749
750.. _sec-enum:
751
752Enumerated Types
753----------------
754
755.. index::
756 single: type; enumerated
757
758Enumerated types allows us to build models that depend on a set of objects
759which are part of the data, or are named in the model, and hence make models
760easier to understand and debug.
761We have introduce enumerated types or enums briefly, in this subsection we
762will explore how we can use them more fully, and show some of the built in
763functions for dealing with enumerated types.
764
765Let's revisit the problem of coloring the graph of Australia from :ref:`sec-modelling`.
766
767
768.. literalinclude:: examples/aust-enum.mzn
769 :language: minizinc
770 :name: ex-aust-enum
771 :caption: Model for coloring Australia using enumerated types (:download:`aust-enum.mzn <examples/aust-enum.mzn>`).
772
773The model shown in :numref:`ex-aust-enum` declares an enumerated type
774:mzn:`Color` which must be defined in the data file. Each of the state
775variables is declared to take a value from this enumerated type.
776Running this program using
777
778.. code-block:: bash
779
780 $ minizinc --solver gecode -D"Color = { red, yellow, blue };" aust-enum.mzn
781
782might result in output
783
784.. code-block:: none
785
786 wa = blue;
787 nt = yellow;
788 sa = red;
789 q = blue;
790 nsw = yellow;
791 v = blue;
792 t = red;
793
794
795.. defblock:: Enumerated Type Variable Declarations
796
797 .. index::
798 single: variable; declaration; enum
799
800 An enumerated type parameter is declared as either:
801
802 .. code-block:: minizincdef
803
804 <enum-name> : <var-name>
805 <l>..<u> : <var-name>
806
807 where :mzndef:`<enum-name>` is the name of an enumerated type, and
808 :mzndef:`<l>` and :mzndef:`<u>` are fixed enumerated type expressions of the same
809 enumerated type.
810
811 An enumerated type decision variable is declared
812 as either:
813
814 .. code-block:: minizincdef
815
816 var <enum-name> : <var-name>
817 var <l>..<u> : <var-name>
818
819 where :mzndef:`<enum-name>` is the name of an enumerated type, and
820 :mzndef:`<l>` and :mzndef:`<u>` are fixed enumerated type expressions of the same
821 enumerated type.
822
823A key behaviour of enumerated types is that they are automatically coerced
824to integers when they are used in a position expecting an integer.
825For example, this allows us to use global constraints defined on integers,
826such as
827
828.. code-block:: minizinc
829
830 global_cardinality_low_up([wa,nt,sa,q,nsw,v,t],
831 [red,yellow,blue],[2,2,2],[2,2,3]);
832
833This requires at least two states to be colored each color and three to be
834colored blue.
835
836
837.. defblock:: Enumerated Type Operations
838
839 There are a number of built in operations on enumerated types:
840
841 - :mzn:`enum_next(X,x)`: returns the next value after :mzn:`x` in the
842 enumerated type :mzn:`X`. This is a partial function, if :mzn:`x` is the last value in
843 the enumerated type :mzn:`X` then the function returns :math:`\bot` causing the Boolean
844 expression containing the expression to evaluate to :mzn:`false`.
845 - :mzn:`enum_prev(X,x)`:
846 returns the previous value before :mzn:`x` in the
847 enumerated type :mzn:`X`. Similarly :mzn:`enum_prev` is a partial function.
848 - :mzn:`to_enum(X,i)`: maps an integer expression :mzn:`i` to an
849 enumerated type value in type :mzn:`X` or evaluates to :math:`\bot` if :mzn:`i` is less
850 than or equal to 0 or greater than the number of elements in :mzn:`X`.
851
852 Note also that a number of standard functions are applicable to enumerated
853 types:
854
855 - :mzn:`card(X)`: returns the cardinality of an enumerated type :mzn:`X`.
856 - :mzn:`min(X)`: returns the minimum element of of an enumerated type :mzn:`X`.
857 - :mzn:`max(X)`: returns the maximum element of of an enumerated type :mzn:`X`.
858
859It is often useful to define an enumerated type by *extending* another enumerated type. A good example for this is adding a "don't care" value to a type. For instance, consider a typical assignment problem, where we have to assign chores to flatmates. The names of the flatmates are given as an enumerated type :mzn:`Flatmates`, and the chores as an enumerated type :mzn:`Chores`.
860
861In the case where not every flatmate needs to be assigned a job, and not every chore needs to be assigned to a flatmate, we need to introduce a value that signals "no assignment". We can then use the :mzn:`alldifferent_except` constraint to constrain the assignment.
862
863.. literalinclude:: examples/assignment-extend-enum.mzn
864 :language: minizinc
865 :name: ex-assignment-extend-enum
866 :caption: Model for an assignment problem using extended enumerated types (:download:`assignment-extend-enum.mzn <examples/assignment-extend-enum.mzn>`).
867
868The model is shown in :numref:`ex-assignment-extend-enum`. It introduces a new enumerated type :mzn:`ChoreOrNothing`, which is a combination of the :mzn:`Chores` type and a new constructor :mzn:`Nothing`. The :mzn:`Chores` type is *injected* into the new type via a *constructor function*. In this case, we chose the name :mzn:`C` for the constructor function, but you can use any valid identifier you like. The constructor function can then be used to coerce a value of type :mzn:`Chores` into a value of the new type :mzn:`ChoreOrNothing`. For example, we could write a constraint such as
869
870.. code-block:: minizinc
871
872 constraint assignment[Bert] = C(Vacuuming);
873
874This is required because the type :mzn:`ChoreOrNothing` is considered different from the type :mzn:`Chores` by the compiler, in order to avoid any ambiguities or accidental type conversions. The compiler also generates inverses of all constructor functions, to map back from the extended types into the base types. This can be seen in the output item, where :mzn:`C^-1` is used to map from :mzn:`ChoreOrNothing` back to :mzn:`Chores`. The inverse function can be written as ASCII using the :mzn:`^-1` notation, or using the unicode symbols :mzn:`⁻¹`, as in :mzn:`C⁻¹`.
875
876In the example above, we could have used option types, instead of adding a new value that acts essentially like the absent value :mzn:`<>`. However, extended enum types have some advantages in this scenario. For example, we can extend a type by multiple extra values (say, different reasons for not being assigned any chore). We can also combine multiple enumerated types into one. Consider the scenario in :numref:`ex-assignment-combine-enums` where we can assign chores to flatmates and/or robots. Flatmates have preferences for certain chores, while robots have integer benefits. The model also shows how to test if a value of the extended enum in fact belongs to the underlying enum: In the output item, the test :mzn:`w in F(Flatmates)` uses the :mzn:`F` constructor to translate the set :mzn:`Flatmates` into the :mzn:`Worker` type, which enables the use of the :mzn:`in` operator.
877
878.. literalinclude:: examples/assignment-combine-enums.mzn
879 :language: minizinc
880 :name: ex-assignment-combine-enums
881 :caption: Model for an assignment problem using combined enumerated types (:download:`assignment-combine-enums.mzn <examples/assignment-combine-enums.mzn>`).
882
883
884.. _sec-complex:
885
886Complex Constraints
887-------------------
888
889.. index::
890 single: constraint; complex
891
892Constraints are the core of the MiniZinc model.
893We have seen simple relational expressions but constraints can be considerably more powerful than this.
894A constraint is allowed to be any Boolean expression.
895Imagine a scheduling problem in which we have
896two tasks that cannot overlap in time.
897If :mzn:`s1` and :mzn:`s2` are the corresponding start times
898and :mzn:`d1` and :mzn:`d2` are the corresponding
899durations
900we can express this as:
901
902.. code-block:: minizinc
903
904 constraint s1 + d1 <= s2 \/ s2 + d2 <= s1;
905
906which ensures that the tasks do not overlap.
907
908
909.. defblock:: Booleans
910
911 .. index::
912 single: Boolean
913 single: expression; Boolean
914 single: true
915 single: false
916 single: operator; Boolean
917 single: bool2int
918
919 Boolean expressions in MiniZinc can be written using a standard mathematical syntax.
920 The Boolean literals are :mzn:`true` and
921 :mzn:`false`
922 and the Boolean
923 operators
924 are
925 conjunction, i.e. and (``/\``),
926 disjunction, i.e. or (``\/``),
927 only-if (:mzn:`<-`),
928 implies (:mzn:`->`),
929 if-and-only-if (:mzn:`<->`) and
930 negation (:mzn:`not`).
931 Booleans can be automatically coerced to integers, but to make this
932 coercion explicit the
933 built-in function :mzn:`bool2int` can be used: it
934 returns 1 if its argument is true and 0 otherwise.
935
936.. literalinclude:: examples/jobshop.mzn
937 :language: minizinc
938 :name: ex-jobshop
939 :caption: Model for job-shop scheduling problems (:download:`jobshop.mzn <examples/jobshop.mzn>`).
940
941.. literalinclude:: examples/jdata.dzn
942 :language: minizinc
943 :name: ex-jdata
944 :caption: Data for job-shop scheduling problems (:download:`jdata.dzn <examples/jdata.dzn>`).
945
946The job shop scheduling model given in :numref:`ex-jobshop`
947gives a realistic example of the use of this disjunctive modelling
948capability. In job shop scheduling we have a set of jobs, each consisting
949of a sequence of tasks on separate machines: so task :mzn:`[i,j]` is the
950task in the :math:`i^{th}` job performed on the :math:`j^{th}` machine.
951Each sequence of tasks must be completed in order,
952and no two tasks on the same machine can overlap in time.
953Even for small instances of this problem it can be quite challenging to find
954optimal solutions.
955
956The command
957
958.. code-block:: bash
959
960 $ minizinc --solver gecode --all-solutions jobshop.mzn jdata.dzn
961
962solves a small job shop scheduling problem, and illustrates the behaviour of
963``--all-solutions`` for optimisation problems (note that when running this in the MiniZinc IDE, ``--all-solutions`` is the default behaviour for optimisation problems). Here the solver outputs increasingly better solutions as it finds them, rather than all possible optimal
964solutions. The output from this command is:
965
966.. code-block:: none
967
968 end = 39
969 5 9 13 22 30
970 6 13 18 25 36
971 0 4 8 12 16
972 4 8 12 16 22
973 9 16 25 27 38
974 ----------
975 end = 37
976 4 8 12 17 20
977 5 13 18 26 34
978 0 4 8 12 16
979 8 12 17 20 26
980 9 16 25 27 36
981 ----------
982 end = 34
983 0 1 5 10 13
984 6 10 15 23 31
985 2 6 11 19 27
986 1 5 10 13 19
987 9 16 22 24 33
988 ----------
989 end = 30
990 5 9 13 18 21
991 6 13 18 25 27
992 1 5 9 13 17
993 0 1 2 3 9
994 9 16 25 27 29
995 ----------
996 ==========
997
998indicating an optimal solution with end time 30 is finally found,
999and proved optimal.
1000We can generate all *optimal solutions*
1001by adding a constraint that
1002:mzn:`end = 30` and changing the solve item to :mzn:`solve satisfy`
1003and then executing
1004
1005.. code-block:: bash
1006
1007 $ minizinc --solver gecode --all-solutions jobshop.mzn jobshop.dzn
1008
1009For this problem there are 3,444,375 optimal solutions. In the MiniZinc IDE, you would have to select "User-defined behavior" in the configuration pane and set the number of solutions to zero in order to display all solutions of this satisfaction problem.
1010
1011.. literalinclude:: examples/stable-marriage.mzn
1012 :language: minizinc
1013 :name: ex-stable-marriage
1014 :caption: Model for the stable marriage problem (:download:`stable-marriage.mzn <examples/stable-marriage.mzn>`).
1015
1016.. literalinclude:: examples/stable-marriage.dzn
1017 :language: minizinc
1018 :name: ex-sm-data
1019 :caption: Example data for the stable marriage problem (:download:`stable-marriage.dzn <examples/stable-marriage.dzn>`).
1020
1021Another powerful modelling feature in MiniZinc is
1022that decision variables
1023can be used for :index:`array access <array; access>`.
1024As an example, consider the
1025(old-fashioned) *stable marriage problem*. We have :mzn:`n` (straight) women and :mzn:`n` (straight)
1026men. Each man has a ranked list of women and vice versa. We want to find a
1027husband/wife for each women/man so that all marriages are *stable* in
1028the sense that:
1029
1030- whenever :mzn:`m` prefers another women :mzn:`o` to his wife :mzn:`w`, :mzn:`o` prefers her husband to :mzn:`m`, and
1031- whenever :mzn:`w` prefers another man :mzn:`o` to her husband :mzn:`m`, :mzn:`o` prefers his wife to :mzn:`w`.
1032
1033This can be elegantly modelled in
1034MiniZinc.
1035The model and sample data is shown in :numref:`ex-stable-marriage` and :numref:`ex-sm-data`.
1036
1037The first three items in the model declare the number of men/women and the
1038set of men and women. Here we introduce the use of *anonymous enumerated types*.
1039Both :mzn:`Men` and :mzn:`Women` are sets of size
1040:mzn:`n`, but we do not wish to mix them up so we use an anonymous enumerated
1041type. This allows MiniZinc to detect modelling errors where we use
1042:mzn:`Men` for :mzn:`Women` or vice versa.
1043
1044
1045The matrices :mzn:`rankWomen` and :mzn:`rankMen`,
1046respectively, give the women's ranking of the men and the men's ranking of the women.
1047Thus, the entry :mzn:`rankWomen[w,m]`
1048gives the ranking by woman :mzn:`w` of man :mzn:`m`. The lower the number in the ranking, the more the man or women is preferred.
1049
1050There are two arrays of decision variables: :mzn:`wife` and
1051:mzn:`husband`. These, respectively, contain the wife of each man and the
1052husband of each women.
1053
1054The first two constraints
1055
1056.. literalinclude:: examples/stable-marriage.mzn
1057 :language: minizinc
1058 :lines: 13-14
1059
1060ensure that the assignment of husbands and wives is consistent: :mzn:`w` is the
1061wife of :mzn:`m` implies :mzn:`m` is the husband of :mzn:`w` and vice versa. Notice how in
1062:mzn:`husband[wife[m]]` the index expression :mzn:`wife[m]` is a
1063decision variable, not a parameter.
1064
1065The next two constraints are a direct encoding of the stability condition:
1066
1067.. literalinclude:: examples/stable-marriage.mzn
1068 :language: minizinc
1069 :lines: 16-22
1070
1071This natural modelling of the stable marriage problem is made possible by
1072the ability to use decision variables as array indices and to construct
1073constraints using the standard Boolean connectives.
1074The alert reader may
1075be wondering at this stage, what happens if the array index variable takes a
1076value that is outside the index set of the array. MiniZinc treats this as
1077failure: an array access :mzn:`a[e]` implicitly adds the constraint
1078:mzn:`e in index_set(a)`
1079to the closest surrounding Boolean context where
1080:mzn:`index_set(a)`
1081gives the index set of :mzn:`a`.
1082
1083.. defblock:: Anonymous Enumerated Types
1084
1085 .. index::
1086 single: type; enumerated; anonymous
1087
1088 An *anonymous enumerated type*
1089 is of the form :mzndef:`anon_enum(<n>)` where :mzndef:`<n>` is a fixed integer
1090 expression defining the size of the enumerated type.
1091
1092 An anonymous enumerated type is just like any other enumerated type except
1093 that we have no names for its elements. When printed out, they are given
1094 unique names based on the enumerated type name.
1095
1096Thus for example, consider the variable declarations
1097
1098.. code-block:: minizinc
1099
1100 array[1..2] of int: a= [2,3];
1101 var 0..2: x;
1102 var 2..3: y;
1103
1104The constraint :mzn:`a[x] = y`
1105will succeed with :math:`x=1 \wedge y=2` and :math:`x=2 \wedge y=3`.
1106And the constraint :mzn:`not a[x] = y` will succeed with
1107:math:`x=0 \wedge y=2`, :math:`x=0 \wedge y=3`, :math:`x=1 \wedge y=3` and :math:`x=2 \wedge y=2`.
1108
1109In the case of invalid array accesses by a parameter, the formal semantics
1110of MiniZinc treats this as failure so as to ensure that the treatment of
1111parameters and decision variables is consistent, but a warning is issued
1112since it is almost always an error.
1113
1114.. literalinclude:: examples/magic-series.mzn
1115 :language: minizinc
1116 :name: ex-magic-series
1117 :caption: Model solving the magic series problem (:download:`magic-series.mzn <examples/magic-series.mzn>`).
1118
1119.. index::
1120 single: bool2int
1121 single: constraint; higher order
1122
1123The coercion function
1124:mzn:`bool2int`
1125can be called with any Boolean
1126expression. This allows the MiniZinc
1127modeller to use so called *higher order constraints*.
1128As a simple example consider the *magic series problem*:
1129find a list of numbers :math:`s= [s_0,\ldots,s_{n-1}]`
1130such that :math:`s_i` is the number
1131of occurrences of :math:`i` in :math:`s`. An example is :math:`s = [1,2,1,0]`.
1132
1133A MiniZinc
1134model for this problem
1135is shown in :numref:`ex-magic-series`. The use of
1136:mzn:`bool2int` allows us to sum up the number of times the constraint
1137:mzn:`s[j]=i` is satisfied.
1138Executing the command
1139
1140.. code-block:: bash
1141
1142 $ minizinc --solver gecode --all-solutions magic-series.mzn -D "n=4;"
1143
1144leads to the output
1145
1146.. code-block:: none
1147
1148 s = [1, 2, 1, 0];
1149 ----------
1150 s = [2, 0, 2, 0];
1151 ----------
1152 ==========
1153
1154indicating exactly two solutions to the problem (the effect of ``--all-solutions`` can be achieved in the MiniZinc IDE using the "User-defined behavior" option in the solver configuration pane).
1155
1156Note that MiniZinc will automatically coerce Booleans
1157to integers and integers to floats when required.
1158We could replace the the constraint item in :numref:`ex-magic-series`
1159with
1160
1161.. code-block:: minizinc
1162
1163 constraint forall(i in 0..n-1) (
1164 s[i] = (sum(j in 0..n-1)(s[j]=i)));
1165
1166and get identical results, since the Boolean expression
1167:mzn:`s[j] = i` will be automatically coerced to an
1168integer, effectively by the MiniZinc system automatically adding the
1169missing :mzn:`bool2int`.
1170
1171.. defblock:: Coercion
1172
1173 .. index::
1174 single: coercion; automatic
1175 single: coercion; bool2int
1176 single: coercion; int2float
1177
1178 In MiniZinc one can *coerce* a Boolean value to
1179 an integer value using the :mzn:`bool2int` function.
1180 Similarly one can coerce an integer value to a float value using
1181 :mzn:`int2float`.
1182 The instantiation of the coerced value is the same as the argument,
1183 e.g. :mzn:`par bool` is coerced to :mzn:`par int`, while
1184 :mzn:`var bool` is coerced to :mzn:`var int`.
1185
1186 MiniZinc automatically coerces Boolean expressions to integer
1187 expressions and integer expressions to float expressions,
1188 by inserting :mzn:`bool2int` and :mzn:`int2float` in the model
1189 appropriately.
1190 Note that it will also coerce Booleans to floats using two steps.
1191
1192
1193Set Constraints
1194---------------
1195
1196.. index::
1197 single: constraint; set
1198
1199Another powerful modelling feature of MiniZinc
1200is that it allows sets
1201containing integers to be decision variables:
1202this means that when the model is evaluated the solver will find which elements are in the set.
1203
1204As a simple example, consider the *0/1 knapsack problem*. This is a
1205restricted form of the knapsack problem in which we can either choose to
1206place the item in the knapsack or not. Each item has a weight and a profit
1207and we want to find which choice of items leads to the maximum profit
1208subject to the knapsack not being too full.
1209
1210It is natural to model this in MiniZinc with a single decision variable: :mzn:`var set of ITEM: knapsack`
1211where :mzn:`ITEM` is the set of possible items. If the arrays
1212:mzn:`weight[i]` and :mzn:`profit[i]` respectively give the weight and
1213profit of item :mzn:`i`, and the maximum weight the knapsack can carry is
1214given by :mzn:`capacity` then a natural model is given in
1215:numref:`ex-knapsack-binary`.
1216
1217.. literalinclude:: examples/knapsack.mzn
1218 :language: minizinc
1219 :name: ex-knapsack-binary
1220 :caption: Model for the 0/1 knapsack problem (:download:`knapsack.mzn <examples/knapsack.mzn>`).
1221
1222Notice that the :mzn:`var`
1223keyword comes before the :mzn:`set`
1224declaration indicating that the
1225set itself is the decision variable.
1226This contrasts with an array in which the :mzn:`var` keyword
1227qualifies the elements in the array rather than the array itself since the
1228basic structure of the array is fixed, i.e. its index set.
1229
1230.. literalinclude:: examples/social-golfers.mzn
1231 :language: minizinc
1232 :name: ex-social-golfers
1233 :caption: Model for the social golfers problems (:download:`social-golfers.mzn <examples/social-golfers.mzn>`).
1234
1235
1236As a more complex example of set constraint consider the social golfers
1237problem shown in :numref:`ex-social-golfers`.
1238The aim is to schedule a golf tournament over :mzn:`weeks`
1239using :mzn:`groups` :math:`\times` :mzn:`size` golfers. Each week we have to
1240schedule :mzn:`groups` different groups each of size :mzn:`size`.
1241No two pairs of golfers should ever play in two groups.
1242
1243The variables in the model are sets of golfers :mzn:`Sched[i,j]`
1244for the :math:`i^{th}` week and :mzn:`j^{th}` group.
1245
1246The constraints shown in lines 11-32
1247first enforces an ordering on the first
1248set in each week to remove symmetry in swapping weeks. Next they
1249enforce an ordering on the sets in each week, and make each set have a
1250cardinality of :mzn:`size`.
1251They then ensure that each week is a partition of the set of golfers
1252using the global constraint
1253:mzn:`partition_set`.
1254Finally the last constraint ensures that no two players play in two
1255groups together (since the cardinality of the intersection of any two groups
1256is at most 1).
1257
1258.. index::
1259 single: symmetry; breaking
1260
1261There are also symmetry breaking
1262initialisation constraints shown in lines 34-46:
1263the first week
1264is fixed to have all players in order; the second week is made up of the
1265first players of each of the first groups in the first week; finally the
1266model forces the first :mzn:`size` players to appear in their corresponding
1267group number for the remaining weeks.
1268
1269Executing the command
1270
1271.. code-block:: bash
1272
1273 $ minizinc --solver gecode social-golfers.mzn social-golfers.dzn
1274
1275where the data file defines a problem with 4 weeks, with 4 groups
1276of size 3 leads to the output
1277
1278.. code-block:: none
1279
1280 1..3 4..6 7..9 10..12
1281 {1,4,7} {2,9,12} {3,5,10} {6,8,11}
1282 {1,6,9} {2,8,10} {3,4,11} {5,7,12}
1283 {1,5,8} {2,7,11} {3,6,12} {4,9,10}
1284 ----------
1285
1286Notice hows sets which are ranges may be output in range format.
1287
1288
1289Putting it all together
1290-----------------------
1291
1292We finish this section with a complex example illustrating most
1293of the features introduced in this chapter including
1294enumerated types, complex constraints, global constraints,
1295and complex output.
1296
1297.. literalinclude:: examples/wedding.mzn
1298 :language: minizinc
1299 :name: ex-wedding
1300 :caption: Planning wedding seating using enumerated types (:download:`wedding.mzn <examples/wedding.mzn>`).
1301
1302The model of :numref:`ex-wedding` arranges seats at the wedding table.
1303The table has 12 numbered seats in order around the table, 6 on each side.
1304Males must sit in odd numbered seats, and females in even.
1305Ed cannot sit at the end of the table because of a phobia,
1306and the bride and groom must
1307sit next to each other. The aim is to maximize the distance between known
1308hatreds. The distance between seats is the difference in seat number
1309if on the same side, otherwise its the distance to the opposite seat
1310+ 1.
1311
1312Note that in the output statement we consider each seat :mzn:`s` and search for a
1313guest :mzn:`g` who is assigned to that seat. We make use of the built in function
1314:mzn:`fix` which checks if a decision variable is fixed and returns its
1315fixed value, and otherwise aborts.
1316This is always safe to use in output statements, since by the
1317time the output statement is run all decision variables should be fixed.
1318
1319
1320Running
1321
1322.. code-block:: bash
1323
1324 $ minizinc --solver gecode wedding.mzn
1325
1326Results in the output
1327
1328.. code-block:: none
1329
1330 ted bride groom rona ed carol ron alice bob bridesmaid bestman clara
1331 ----------
1332 ==========
1333
1334The resulting table placement is illustrated in :numref:`fig-wedding`
1335where the lines indicate hatreds. The total distance is 22.
1336
1337.. _fig-wedding:
1338
1339.. figure:: figures/wedding.*
1340
1341 Seating arrangement at the wedding table
1342
1343
1344.. \pjs{Move the fix definition elsewhere!}
1345
1346.. defblock:: Fix
1347
1348 .. index::
1349 single: fix
1350 single: fixed
1351
1352 In output items the built-in function :mzn:`fix` checks that
1353 the value of a decision variable is fixed
1354 and coerces the instantiation from
1355 decision variable to parameter.
1356
1357.. % oil-blending
1358.. %arrays floats sum forall
1359.. %more complex datafile
1360..
1361.. %suduko
1362.. %2-D array
1363.. %complex transformation from data file
1364..
1365.. %jobshop
1366.. %disjunction,
1367..
1368.. %talk about other complex constraints--IC example?
1369..
1370.. %magic sequence
1371.. %reification
1372..
1373.. %warehouse placement
1374.. %reification more complex example
1375..
1376.. %0/1 knapsack
1377.. %set constraint
1378..
1379.. %social golfers
1380.. %more complex set constraint
1381..
1382.. %finish with larger example from Mark
1383