this repo has no description
dekker.one
1.. _ch-solution-checkers:
2
3Automatic Solution Checking, Model Validation, and Benchmarking
4===============================================================
5
6MiniZinc supports checking the correctness of solutions of a model in two ways.
7First, it is the *autonomous checking* where compiler substitutes solution values into the model
8and tries to find inconsistencies, possibly invoking a solver to a much smaller instance.
9Second, it is by using a *checker model*. This latter method can also be seen as model validation.
10
11Autonomous Automatic Solution Checking and Benchmarking
12-------------------------------------------------------
13
14For this method, compiler needs the values of as many variables as possible,
15ideally all variables without the right-hand side. For all top-level variables (not those inside let constructs)
16the values can be output using ``--output-mode dzn`` compiler option. For optimization problems, when no explicit
17objective variable exists, a variable named ``_objective`` is added by ``--output-objective``.
18Then, each produced solution can be copied into a ``.dzn`` and compiled together with the original instance,
19adding ``--allow-multiple-assignments`` option if ``--output-objective`` was used. In the case that
20some variables inside let constructs need to be assigned, a solver has to be invoked for the
21smaller instance remaining after fixing the supplied values. For example, for the following model:
22
23.. code-block:: none
24
25 var int: a;
26 var float: b = a;
27 solve
28 maximize a-b;
29 output
30 [ "a+b is \(a+b)\n" ];
31
32running it with ``minizinc --solver gecode test_output_mode.mzn --output-mode dzn --output-objective`` ignores
33the provided output annotation and prints
34
35.. code-block:: none
36
37 a = -2147483646;
38 _objective = 0.0;
39 ----------
40 ==========
41
42which can be added as an extra ``.dzn`` file. The process of compilation for autonomous checking and re-solving
43with the output variables fixed,
44is automated by a Python script ``tests/benchmarking/mzn-test.py``. To solve an instance with autonomous
45checking by variable value substitution, run, e.g.,
46
47.. code-block:: bash
48
49 mzn-test.py --solver GECODE model.mzn data.dzn
50
51Moreover, ``mzn-test.py`` provides facility to run a list of instances and compare results
52from various test runs and different solvers.
53
54
55Model Validation: Automatic Solution Checking with a Checker Model
56------------------------------------------------------------------
57
58This approach has two main applications:
59
60- Instructors can provide checker models for student assignments. This provides students with immediate, detailed feedback on their modelling attempts.
61- A simplified checker model can be used to verify a complex model used for solving. This can be useful when experimenting with new decompositions of constraints, or for post-processing solutions if some constraints cannot be added to the original model (e.g. in case the solver does not support certain constructs).
62
63Running MiniZinc with solution checking is easy. On the command line, simply pass the name of the checker model in addition to the problem model:
64
65.. code-block:: bash
66
67 minizinc model.mzn model.mzc.mzn data.dzn
68
69Checker models can be pre-compiled in order to obfuscate their contents (e.g. if they contain clues to students how to model the problem):
70
71.. code-block:: bash
72
73 minizinc --compile-solution-checker model.mzc.mzn
74
75This will create the compiled checker model ``model.mzc``, which can be used instead of the clear text version for checking:
76
77.. code-block:: bash
78
79 minizinc model.mzn model.mzc data.dzn
80
81The MiniZinc IDE has built-in support for solution checkers. Whenever the current project contains a file with the same file name as the current model but file extension ``.mzc`` or ``.mzc.mzn``, the "Run" button turns into a "Run+Check" button.
82
83The rest of this section describes how to implement checker models.
84
85
86Basic checker models
87~~~~~~~~~~~~~~~~~~~~
88
89At its core, a checker model takes each solution that a solver produces as input, and outputs whether the solution is correct or not. Let's use the simple map colouring model from the tutorial as an example. Here is the model again:
90
91.. literalinclude:: examples/aust.mzn
92 :language: minizinc
93 :caption: A MiniZinc model :download:`aust.mzn <examples/aust.mzn>` for colouring the states and territories in Australia
94 :name: ex-aust-2
95
96A checker model for this model requires the values of the variables :mzn:`wa`, :mzn:`nt`, and so on, for each solution, and then has to test whether all constraints hold. The output of the checker model should contain a line starting with ``CORRECT`` if the solution passes the test, or ``INCORRECT`` if it doesn't.
97
98Since these values will be fixed in any solution, checker models simply declare parameters with the same name as the model variables:
99
100.. literalinclude:: examples/aust.mzc.mzn
101 :language: minizinc
102 :caption: A MiniZinc checker model :download:`aust.mzc.mzn <examples/aust.mzc.mzn>` for the map colouring problem
103 :name: ex-aust-check
104
105Running the model and the checker will produce output like this:
106
107.. code-block:: none
108
109 wa=3 nt=2 sa=1
110 q=3 nsw=2 v=3
111 t=3
112 % Solution checker report:
113 % CORRECT
114 ----------
115
116The solution checker report is embedded as comments in the original output.
117
118
119Detailed feedback
120~~~~~~~~~~~~~~~~~
121
122The basic checker model above only reports whether the solutions satisfy the constraints, but it doesn't provide any insights into the nature of the error if a constraint is violated.
123
124We can use standard MiniZinc functionality to provide much more detailed feedback. The following checker model introduces a helper function :mzn:`check` which outputs a detailed error message if a constraint doesn't hold. The results of all the checks are combined, and if any of the constraints was violated, the output is ``INCORRECT``, otherwise it is ``CORRECT``.
125
126.. literalinclude:: examples/aust-2.mzc.mzn
127 :language: minizinc
128 :caption: A checker model :download:`aust-2.mzc.mzn <examples/aust-2.mzc.mzn>` for the map colouring problem with more detailed error messages
129 :name: ex-aust-check-2
130
131However, the checker model will only report the first violated constraint, since the conjunction operator short-circuits the evaluation when one of its arguments is false. For example, if we remove all constraints from the original model, the output would be:
132
133.. code-block:: none
134
135 wa=3 nt=3 sa=3
136 q=3 nsw=3 v=3
137 t=3
138 % Solution checker report:
139 % ERROR: wa and nt have the same colour
140 % INCORRECT
141 ----------
142
143In order to get all error messages, we can force the evaluation of all checkers by creating an auxiliary array of check results:
144
145.. literalinclude:: examples/aust-3.mzc.mzn
146 :language: minizinc
147 :caption: A checker model :download:`aust-3.mzc.mzn <examples/aust-3.mzc.mzn>` for the map colouring problem without short-circuit evaluation
148 :name: ex-aust-check-3
149
150Now the output contains all error messages (for the case where the model has no constraints):
151
152.. code-block:: none
153
154 wa=3 nt=3 sa=3
155 q=3 nsw=3 v=3
156 t=3
157 % Solution checker report:
158 % ERROR: nsw and v have the same colour
159 % ERROR: q and nsw have the same colour
160 % ERROR: sa and v have the same colour
161 % ERROR: sa and nsw have the same colour
162 % ERROR: sa and q have the same colour
163 % ERROR: nt and q have the same colour
164 % ERROR: nt and sa have the same colour
165 % ERROR: wa and sa have the same colour
166 % ERROR: wa and nt have the same colour
167 % INCORRECT
168 ----------
169
170
171Instance data in checker models
172~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
173
174The map colouring example was quite simple because the model did not contain any parameter declarations. For a model that is parameterised, the checker model simply contains the same parameter declarations. MiniZinc will then pass the actual parameters of the instance being solved to the checker model.
175
176For example, the following checker model could be used for the *n*-Queens problem.
177
178.. literalinclude:: examples/nqueens.mzc.mzn
179 :language: minizinc
180 :caption: A checker model :download:`nqueens.mzc.mzn <examples/nqueens.mzc.mzn>` for the n-Queens problem
181 :name: ex-nqueens-check
182
183The checker model first makes sure that the solution has the right dimensions (correct array index set, and each variable is assigned a value in the correct domain), and then uses standard MiniZinc constructs to check each constraint.
184
185
186Checking optimisation problems
187~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
188
189Optimisation problems pose a difficulty for automatic checking. When a solver claims to prove optimality, we cannot easily verify this claim without solving the problem again (using a different model that is known to be correct). At the moment, solution checking for optimisation problems is restricted to checking that the objective has been computed correctly.
190
191To check that the objective value is calculated correctly, define a parameter called :mzn:`_objective` of the appropriate type (:mzn:`int` or :mzn:`float`) in the checker. The example in the next section illustrates this.
192
193
194Hidden variables
195~~~~~~~~~~~~~~~~
196
197For many models, the decision variables which describe the solution may not be the variables that are natural to describe the constraints. There may be other internal variables which are functionally defined by the decision variables, and which are likely to be used in the model for building constraints and/or are much more natural for describing the correctness of a candidate solution.
198
199Consider the problem of lining up *n* people numbered from 1 to *n* for a photo
200in a single line. We want to make sure that there are no more than two people of
201the same gender (male, female or other) in sequence in the line. We want to
202minimize the total distance between the pairs of people who are numbered
203consecutively. The decisions are an array :mzn:`pos` which for each person
204gives their position in the line. A correct model for this is given in :numref:`ex-photo`.
205
206.. literalinclude:: examples/photo.mzn
207 :language: minizinc
208 :caption: A model :download:`photo.mzn <examples/photo.mzn>` for the photo lineup problem
209 :name: ex-photo
210
211A critical part of learning how to model this problem is to realise
212that it is worth introducing the inverse of the :mzn:`pos` variables, called :mzn:`who` in this model. The :mzn:`who` array makes it much easier to specify that no more than two people of the same gender can be
213adjacent. The checker model **should not** include the :mzn:`who` variables, because that would effectively give away the key to the solution.
214
215The use of hidden variables (such as :mzn:`who`) makes checking harder in two
216ways. First, we may need to define these in the checker model as decision variables (rather than parameters), and MiniZinc will then need to invoke a solver to generate the values of these variables in order to check a given solution. Second, given an incorrect candidate solution, there may be
217no possible value for these hidden variables, hence we have to guard the
218checking to ensure we do not assume that there is some value for the hidden
219variables.
220
221Consider this data file for the photo problem:
222
223.. code-block:: minizinc
224
225 n = 9;
226 g = [M,M,M,M,F,F,F,M,M];
227
228and assume that an incorrect model returns the erroneous candidate solution
229:mzn:`pos = [1,2,3,4,5,6,7,2,9]; _objective=25;`. If we simply assert :mzn:`inverse(pos,who)` in the checker model, then this constraint will
230fail since there is no inverse of this position array, because persons 2 and
2318 are both at position 2. Hence the checker must guard the inverse
232constraint, and only when that succeeds use the computed values of the
233:mzn:`who` variables for checking the solution. A checking model for the photo problem might look like this:
234
235.. literalinclude:: examples/photo.mzc.mzn
236 :language: minizinc
237 :caption: A checker model :download:`photo.mzc.mzn <examples/photo.mzc.mzn>` for the photo lineup problem
238 :name: ex-photo-checker
239
240The checker model first tests whether the given :mzn:`pos` array satisfies the :mzn:`alldifferent` property (using a custom :mzn:`test` for :mzn:`alldifferent` on a par array). If it passes the test, the :mzn:`inverse` constraint is applied. Otherwise, the :mzn:`who` array is simply fixed to a list of ones.
241
242The check for the :mzn:`alldifferent` constraint is a good example for a checker that tries to give a detailed description of the error.