this repo has no description
dekker.one
1.. _sec-efficient:
2
3Effective Modelling Practices in MiniZinc
4=========================================
5
6There are almost always multiple
7ways to model the same problem, some of which generate models which are
8efficient to solve, and some of which are not.
9In general it is very hard to tell a priori which models are the most
10efficient
11for solving a particular problem, and indeed it may critically depend on
12the underlying solver used, and search strategy. In this chapter we
13concentrate
14on modelling practices that avoid inefficiency in generating models
15and generated models. For solver-specific recommendations see User
16Manual/Solver Backends.
17
18Variable Bounds
19---------------
20
21.. index::
22 single: variable; bound
23
24Finite domain propagation engines, which are the principle type of solver
25targeted by MiniZinc, are more effective the tighter the bounds on the
26variables involved. They can also behave badly with problems which
27have subexpressions that take large integer values, since they may
28implicitly limit the size of integer variables.
29
30.. literalinclude:: examples/grocery.mzn
31 :language: minizinc
32 :name: ex-grocery
33 :caption: A model with unbounded variables (:download:`grocery.mzn <examples/grocery.mzn>`).
34
35The grocery problem shown in :numref:`ex-grocery` finds 4 items
36whose prices in dollars add up to 7.11 and multiply up to 7.11.
37The variables are declared unbounded. Running
38
39.. code-block:: bash
40
41 $ minizinc --solver chuffed grocery.mzn
42
43yields
44
45.. code-block:: none
46
47 =====UNSATISFIABLE=====
48
49This is because the
50intermediate expressions in the multiplication
51are also :mzn:`var int`
52and are given default bounds in the solver
53:math:`-1,000,000 \dots 1,000,000`,
54and these ranges are too small to hold the
55values that the intermediate expressions may need to take.
56
57Modifying the model so that the items are declared with tight bounds
58
59.. code-block:: minizinc
60
61 var 1..711: item1;
62 var 1..711: item2;
63 var 1..711: item3;
64 var 1..711: item4;
65
66results in a better model, since now MiniZinc can infer bounds on the
67intermediate expressions and use these rather than the default bounds.
68With this modification, executing the model gives
69
70.. code-block:: none
71
72 {120,125,150,316}
73 ----------
74
75Note however that even the improved model may be too difficult for
76some solvers.
77Running
78
79.. code-block:: bash
80
81 $ minizinc --solver g12lazy grocery.mzn
82
83does not return an answer, since the solver builds a huge representation
84for the intermediate product variables.
85
86.. defblock:: Bounding variables
87
88 .. index::
89 single: variable; bound
90
91 Always try to use bounded variables in models.
92 When using :mzn:`let`
93 declarations to introduce new variables, always try to define them
94 with correct and tight bounds. This will make your model more efficient,
95 and avoid the possibility of unexpected overflows.
96 One exception is when you introduce a new variable which is
97 immediately defined as equal to an expression. Usually MiniZinc will be
98 able to infer effective bounds from the expression.
99
100
101Effective Generators
102--------------------
103
104.. index::
105 single: generator
106
107Imagine we want to count the number of triangles (:math:`K_3` subgraphs)
108appearing in a graph. Suppose the graph is defined by
109an adjacency matrix: :mzn:`adj[i,j]` is true if nodes :mzn:`i` and :mzn:`j` are
110adjacent. We might write
111
112.. code-block:: minizinc
113
114 int: count = sum ([ 1 | i,j,k in NODES where i < j /\ j < k
115 /\ adj[i,j] /\ adj[i,k] /\ adj[j,k]]);
116
117which is certainly correct, but it examines all triples of nodes.
118If the graph is sparse we can do better by realising that some
119tests can be applied as soon as we select :mzn:`i` and :mzn:`j`.
120
121.. code-block:: minizinc
122
123 int: count = sum ([ 1 | i,j in NODES where i < j /\ adj[i,j],
124 k in NODES where j < k /\ adj[i,k] /\ adj[j,k]]);
125
126You can use the builitin :mzn:`trace` :index:`function <trace>` to help
127determine what is happening inside generators.
128
129.. defblock:: Tracing
130
131 The function :mzn:`trace(s,e)` prints the string :mzn:`s` before
132 evaluating the expression :mzn:`e` and returning its value.
133 It can be used in any context.
134
135For example, we can see how many times the test is performed in the inner
136loop for both versions of the calculation.
137
138.. literalinclude:: examples/count1.mzn
139 :language: minizinc
140 :lines: 8-15
141
142Produces the output:
143
144.. code-block:: none
145
146 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
147 ----------
148
149indicating the inner loop is evaluated 64 times while
150
151.. literalinclude:: examples/count2.mzn
152 :language: minizinc
153 :lines: 13-14
154
155Produces the output:
156
157.. code-block:: none
158
159 ++++++++++++++++
160 ----------
161
162indicating the inner loop is evaluated 16 times.
163
164Note that you can use the dependent strings in :mzn:`trace` to
165understand what is happening during model creation.
166
167.. literalinclude:: examples/count3.mzn
168 :language: minizinc
169 :lines: 13-15
170
171will print out each of triangles that is found in the calculation.
172It produces the output
173
174.. code-block:: none
175
176 (1,2,3)
177 ----------
178
179We have to admit that we cheated a bit here: In certain circumstances, the MiniZinc compiler is in fact able to re-order the arguments in a ``where`` clause automatically, so that they are evaluated as early as possible. In this case, adding the ``trace`` function in fact *prevented* this optimisation. In general, it is however a good idea to help the compiler get it right, by splitting the ``where`` clauses and placing them as close to the generators as possible.
180
181
182Redundant Constraints
183---------------------
184
185.. index::
186 single: constraint; redundant
187
188The form of a model will affect how well the constraint solver can solve it.
189In many cases adding constraints which are redundant, i.e. are logically
190implied by the existing model, may improve the search for
191solutions by making more information available to the solver earlier.
192
193Consider the magic series problem from :ref:`sec-complex`.
194Running this for :mzn:`n = 16` as follows:
195
196.. code-block:: bash
197
198 $ minizinc --solver gecode --all-solutions --statistics magic-series.mzn -D "n=16;"
199
200might result in output
201
202.. code-block:: none
203
204 s = [12, 2, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0];
205 ----------
206 ==========
207
208and the statistics showing 117 failures required.
209
210We can add redundant constraints to the model to improve the performance.
211Since each number
212in the sequence counts the number of occurrences of a number, we know
213that they sum up to :mzn:`n`. Similarly we know that the sum of
214:mzn:`s[i] * i` must also add up to :mzn:`n` because the sequence is magic.
215
216.. index::
217 single: redundant_constraint; example
218
219These constraints do not actually constrain the model further: any solution of the original model is still a solution of the new model that includes the redundant constraints. It is good practice to make the MiniZinc compiler aware that a constraint is redundant. That way, the compiler can decide to ignore the constraint for particular solvers, since not all solvers benefit from redundant constraints. We therefore wrap redundant constraints in a call to the library predicate :mzn:`redundant_constraint`.
220
221The magic sequence model with these redundant constraints is shown in
222:numref:`ex-magic-series2`.
223
224.. literalinclude:: examples/magic-series2.mzn
225 :language: minizinc
226 :name: ex-magic-series2
227 :caption: Model solving the magic series problem with redundant constraints (:download:`magic-series2.mzn <examples/magic-series2.mzn>`).
228
229Running the same problem as before
230
231.. code-block:: bash
232
233 $ minizinc --solver gecode --all-solutions --statistics magic-series2.mzn -D "n=16;"
234
235results in the same output, but with statistics showing just 14 failures
236explored. The redundant constraints have allowed the solver to prune the
237search much earlier.
238
239Because we wrapped the redundant constraints in the special predicate, we can now switch them off easily on the command line by setting the flag :mzn:`mzn_ignore_redundant_constraints=true`:
240
241.. code-block:: bash
242
243 $ minizinc --solver gecode --all-solutions --statistics magic-series2.mzn -D "n=16;mzn_ignore_redundant_constraints=true;"
244
245Modelling Choices
246-----------------
247
248There are many ways to model the same problem in MiniZinc,
249although some may be more natural than others.
250Different models may have very different efficiency of solving, and worse
251yet, different models may be better or worse for different solving backends.
252There are however some guidelines for usually producing better models:
253
254.. defblock:: Choosing between models
255
256 The better model is likely to have some of the following features
257
258 - smaller number of variables, or at least those that are not
259 functionally defined by other variables
260 - smaller domain sizes of variables
261 - more succinct, or direct, definition of the constraints of the model
262 - uses global constraints as much as possible
263
264 In reality all this has to be tempered by how effective the search is for
265 the model. Usually the effectiveness of search is hard to judge except by
266 experimentation.
267
268Consider the problem of finding permutations of :math:`n` numbers
269from 1 to :math:`n` such that the differences between adjacent numbers
270also form a permutation of numbers 1 to :math:`n-1`.
271Note that the :mzn:`u` variables are functionally defined by
272the :mzn:`x` variables so the raw search space is :math:`n^n`.
273The obvious way to model this problem is shown in :numref:`ex-allint`.
274
275.. literalinclude:: examples/allinterval.mzn
276 :language: minizinc
277 :name: ex-allint
278 :caption: A natural model for the all interval series problem ``prob007`` in CSPlib (:download:`allinterval.mzn <examples/allinterval.mzn>`).
279
280In this model the array :mzn:`x` represents the permutation of the :mzn:`n`
281numbers and the constraints are naturally represented using :mzn:`alldifferent`.
282
283Running the model
284
285.. code-block:: bash
286
287 $ minizinc --solver gecode --all-solutions --statistics allinterval.mzn -D "n=10;"
288
289finds all solutions in 16077 nodes and 71ms
290
291An alternate model uses array :mzn:`y` where :mzn:`y[i]` gives the
292position of the number :mzn:`i` in the sequence.
293We also model the positions of the differences using variables
294:mzn:`v`. :mzn:`v[i]` is the position in the sequence where the absolute difference
295:mzn:`i` occurs. If the values of :mzn:`y[i]` and :mzn:`y[j]` differ by one
296where :mzn:`j > i`, meaning the
297positions are adjacent, then :mzn:`v[j-i]` is constrained to be the earliest
298of these positions.
299We can add two redundant constraints to this model:
300since we know that a difference of :mzn:`n-1` must result, we know that
301the positions of 1 and :mzn:`n` must be adjacent (:mzn:`abs( y[1] - y[n] ) = 1`),
302which also tell us that the position of difference :mzn:`n-1` is
303the earlier of :mzn:`y[1]` and :mzn:`y[n]`, i.e.
304:mzn:`v[n-1] = min(y[1], y[n])`.
305With this we can model the problem
306as shown in :numref:`ex-allint2`. The output statement recreates the
307original sequence :mzn:`x` from the array of positions :mzn:`y`.
308
309.. literalinclude:: examples/allinterval2.mzn
310 :language: minizinc
311 :name: ex-allint2
312 :caption: An inverse model for the all interval series problem ``prob007`` in CSPlib (:download:`allinterval2.mzn <examples/allinterval2.mzn>`).
313
314The inverse model has the same size as the original model, in terms of
315number of variables and domain sizes. But the inverse model has a much more
316indirect way of modelling the relationship between the :mzn:`y` and :mzn:`v` variables
317as opposed to the relationship between :mzn:`x` and :mzn:`u` variables.
318Hence we might expect the original model to be better.
319
320The command
321
322.. code-block:: bash
323
324 $ minizinc --solver gecode --all-solutions --statistics allinterval2.mzn -D "n=10;"
325
326finds all the solutions in 98343 nodes and 640 ms.
327So the more direct modelling of the constraints is clearly paying off.
328
329Note that the inverse model prints out the answers using the same :mzn:`x` view of
330the solution. The way this is managed is using :mzn:`output_only` annotations.
331The array :mzn:`x` is defined as a fixed array and annotated as :mzn:`output_only`.
332This means it will only be evaluated, and can only be used in output statements.
333Once a solution for :mzn:`y` is discovered the value of :mzn:`x` is calculated
334during output processing, and hence can be displayed in the output.
335
336.. defblock:: Output_only annotation
337
338 .. index::
339 single: output_only
340
341 The :mzndef:`output_only` annotation can be applied to variable definitions.
342 The variable defined must not be a :mzn:`var` type, it can only be :mzn:`par`.
343 The variable must also have a right hand side definition giving its value.
344 This right hand side definition can make use of :mzn:`fix` functions to access
345 the values of decision variables, since it is evaluated at solution processing
346 time
347
348
349.. _sec-multiple-modelling-and-channels:
350
351Multiple Modelling and Channels
352-------------------------------
353
354When we have two models for the same problem it may be
355useful to use both models together by tying the variables in the two models
356together, since each can give different information to the solver.
357
358.. literalinclude:: examples/allinterval3.mzn
359 :language: minizinc
360 :name: ex-allint3
361 :caption: A dual model for the all interval series problem ``prob007`` in CSPlib (:download:`allinterval3.mzn <examples/allinterval3.mzn>`).
362
363:numref:`ex-allint3` gives a dual model combining features of
364:download:`allinterval.mzn <examples/allinterval.mzn>` and :download:`allinterval2.mzn <examples/allinterval2.mzn>`.
365The beginning of the model is taken from :download:`allinterval.mzn <examples/allinterval.mzn>`.
366We then introduce the :mzn:`y` and :mzn:`v` variables from :download:`allinterval2.mzn <examples/allinterval2.mzn>`.
367We tie the variables together using the
368global
369:mzn:`inverse` constraint:
370:mzn:`inverse(x,y)` holds if :mzn:`y` is the inverse function of :mzn:`x` (and vice versa),
371that is :mzn:`x[i] = j <-> y[j] = i`. A definition
372is shown in :numref:`ex-inverse`.
373The model does not include the constraints relating the
374:mzn:`y` and :mzn:`v` variables, they are redundant (and indeed propagation
375redundant)
376so they do not add information for a
377propagation solver. The :mzn:`alldifferent` constraints are also missing since
378they are made redundant (and propagation redundant) by the inverse
379constraints.
380The only constraints are the relationships of the :mzn:`x` and :mzn:`u` variables
381and the redundant constraints on :mzn:`y` and :mzn:`v`.
382
383.. literalinclude:: examples/inverse.mzn
384 :language: minizinc
385 :name: ex-inverse
386 :caption: A definition of the ``inverse`` global constraint (:download:`inverse.mzn <examples/inverse.mzn>`).
387
388One of the benefits of the dual model is that there is more scope for
389defining different search strategies.
390Running the dual model,
391
392.. code-block:: bash
393
394 $ minizinc --solver g12fd --all-solutions --statistics allinterval3.mzn -D "n=10;"
395
396which uses the search strategy of
397the inverse model, labelling the :mzn:`y` variables,
398finds all solutions in 1714 choice points and 0.5s.
399Note that running the same model with labelling on the :mzn:`x` variables
400requires 13142 choice points and 1.5s.
401
402Symmetry
403--------
404
405Symmetry is very common in constraint satisfaction and optimisation problems. To illustrate this, let us look again at the n-queens problem from :numref:`ex-queens`. The top left chess board in :numref:`fig-queens-sym` shows a solution to the 8-queens problems (labeled "original"). The remaining chess boards show seven symmetric variants of the same solution: rotated by 90, 180 and 270 degrees, and flipped vertically.
406
407.. _fig-queens-sym:
408
409.. figure:: figures/queens_symm.*
410
411 Symmetric variants of an 8-queens solution
412
413
414If we wanted to enumerate *all* solutions to the 8-queens problem, we could obviously save the solver some work by only enumerating *non-symmetric* solutions, and then generating the symmetric variants ourselves. This is one reason why we want to get rid of symmetry in constraint models. The other, much more important reason, is that the solver may also **explore symmetric variants of non-solution states!**
415
416For example, a typical constraint solver may try to place the queen in column 1 into row 1 (which is fine), and then try to put the column 2 queen into row 3, which, at first sight, does not violate any of the constraints. However, this configuration cannot be completed to a full solution (which the solver finds out after a little search). :numref:`fig-queens-sym-unsat` shows this configuration on the top left chess board. Now nothing prevents the solver from trying, e.g., the second configuration from the left in the bottom row of :numref:`fig-queens-sym-unsat`, where the queen in column 1 is still in row 1, and the queen in column 3 is placed in row 2. Therefore, even when only searching for a single solution, the solver may explore many symmetric states that it has already seen and proven unsatisfiable before!
417
418.. _fig-queens-sym-unsat:
419
420.. figure:: figures/queens_symm_unsat.*
421
422 Symmetric variants of an 8-queens unsatisfiable partial assignment
423
424Static Symmetry Breaking
425~~~~~~~~~~~~~~~~~~~~~~~~
426
427The modelling technique for dealing with symmetry is called *symmetry breaking*, and in its simplest form, involves adding constraints to the model that rule out all symmetric variants of a (partial) assignment to the variables except one. These constraints are called *static symmetry breaking constraints*.
428
429The basic idea behind symmetry breaking is to impose an *order*. For example, to rule out any vertical flips of the chess board, we could simply add the constraint that the queen in the first column must be in the top half of the board:
430
431.. code-block:: minizinc
432
433 constraint q[1] <= n div 2;
434
435Convince yourself that this would remove exactly half of the symmetric variants in :numref:`fig-queens-sym`. You can tell the compiler that a particular constraint is a symmetry breaking constraint by wrapping it in a special call:
436
437.. index::
438 single: symmetry_breaking_constraint; example
439
440.. code-block:: minizinc
441
442 constraint symmetry_breaking_constraint(q[1] <= n div 2);
443
444This has the advantage that solvers can ignore the constraint or treat it differently. It also means that you can easily switch off symmetry breaking by setting :mzn:`mzn_ignore_symmetry_breaking_constraints=true`, either in your model, or a data file, or as extra data using the ``-D`` command line option.
445
446In order to remove *all* symmetry in the n-queens problem, we need to work a bit harder. Whenever we can express all symmetries as permutations of the array of variables, a set of *lexicographic ordering constraints* can be used to break all symmetry. For example, if the array of variables is called :mzn:`x`, and reversing the array is a symmetry of the problem, then the following constraint will break that symmetry:
447
448.. code-block:: minizinc
449
450 constraint symmetry_breaking_constraint(lex_lesseq(x, reverse(x)));
451
452How about two-dimensional arrays? Lexicographic ordering works just the same, we only have to coerce the arrays into one dimension. For example, the following breaks the symmetry of flipping the array along one of the diagonals (note the swapped indices in the second comprehension):
453
454.. code-block:: minizinc
455
456 array[1..n,1..n] of var int: x;
457 constraint symmetry_breaking_constraint(
458 lex_lesseq([ x[i,j] | i,j in 1..n ], [ x[j,i] | i,j in 1..n ])
459 );
460
461The great thing about using lexicographic ordering constraints is that we can add multiple ones (to break several symmetries simultaneously), without them interfering with each other, as long as we keep the order in the first argument the same.
462
463For the n-queens problem, unfortunately this technique does not immediately apply, because some of its symmetries cannot be described as permutations of the :mzn:`q` array. The trick to overcome this is to express the n-queens problem in terms of Boolean variables that model, for each field of the board, whether it contains a queen or not. Now all the symmetries can be modeled as permutations of this array. Since the main constraints of the n-queens problem are much easier to express with the integer :mzn:`q` array, we simply use both models together and add channeling constraints between them, as explained in :ref:`sec-multiple-modelling-and-channels`.
464
465The full model, with added Boolean variables, channeling constraints and symmetry breaking constraints is shown in :numref:`ex-queens-sym`. We can conduct a little experiment to check whether it successfully breaks all the symmetry. Try running the model with increasing values for :mzn:`n`, e.g. from 1 to 10, counting the number of solutions (e.g., by using the ``-s`` flag with the Gecode solver, or selecting "Print all solutions" as well as "Statistics for solving" in the IDE). You should get the following sequence of numbers of solutions: 1, 0, 0, 1, 2, 1, 6, 12, 46, 92. To verify the sequence, you can search for it in the *On-Line Encyclopedia of Integer Sequences* (http://oeis.org).
466
467.. literalinclude:: examples/nqueens_sym.mzn
468 :language: minizinc
469 :name: ex-queens-sym
470 :start-after: % Symmetry breaking
471 :end-before: % search
472 :caption: Partial model for n-queens with symmetry breaking (full model: :download:`nqueens_sym.mzn <examples/nqueens_sym.mzn>`).
473
474
475Other Examples of Symmetry
476~~~~~~~~~~~~~~~~~~~~~~~~~~
477
478Many other problems have inherent symmetries, and breaking these can often make a significant difference in solving performance. Here is a list of some common cases:
479
480- Bin packing: when trying to pack items into bins, any two bins that have
481 the same capacity are symmetric.
482- Graph colouring: When trying to assign colours to nodes in a graph such
483 that adjacent nodes must have different colours, we typically model
484 colours as integer numbers. However, any permutation of colours is again a
485 valid graph colouring.
486- Vehicle routing: if the task is to assign customers to certain vehicles,
487 any two vehicles with the same capacity may be symmetric (this is similar
488 to the bin packing example).
489- Rostering/time tabling: two staff members with the same skill set may be
490 interchangeable, just like two rooms with the same capacity or technical
491 equipment.