3.6. Automatic Solution Checking, Model Validation, and Benchmarking
MiniZinc supports checking the correctness of solutions of a model in two ways. First, it is the autonomous checking where compiler substitutes solution values into the model and tries to find inconsistencies, possibly invoking a solver to a much smaller instance. Second, it is by using a checker model. This latter method can also be seen as model validation.
3.6.1. Autonomous Automatic Solution Checking and Benchmarking
For this method, compiler needs the values of as many variables as possible, ideally all variables without the right-hand side. For all top-level variables (not those inside let constructs) the values can be output using --output-mode dzn compiler option. For optimization problems, when no explicit objective variable exists, a variable named _objective is added by --output-objective. Then, each produced solution can be copied into a .dzn and compiled together with the original instance, adding --allow-multiple-assignments option if --output-objective was used. In the case that some variables inside let constructs need to be assigned, a solver has to be invoked for the smaller instance remaining after fixing the supplied values. For example, for the following model:
var int: a;
var float: b = a;
solve
maximize a-b;
output
[ "a+b is \(a+b)\n" ];
running it with minizinc --solver gecode test_output_mode.mzn --output-mode dzn --output-objective ignores the provided output annotation and prints
a = -2147483646;
_objective = 0.0;
----------
==========
which can be added as an extra .dzn file. The process of compilation for autonomous checking and re-solving with the output variables fixed, is automated by a Python script tests/benchmarking/mzn-test.py. To solve an instance with autonomous checking by variable value substitution, run, e.g.,
mzn-test.py --solver gecode model.mzn data.dzn
Moreover, mzn-test.py provides facility to run a list of instances and compare results from various test runs and different solvers.
3.6.2. Model Validation: Automatic Solution Checking with a Checker Model
This approach has two main applications:
Instructors can provide checker models for student assignments. This provides students with immediate, detailed feedback on their modelling attempts.
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).
Running MiniZinc with solution checking is easy. On the command line, simply pass the name of the checker model in addition to the problem model:
minizinc model.mzn model.mzc.mzn data.dzn
Checker models can be pre-compiled in order to obfuscate their contents (e.g. if they contain clues to students how to model the problem):
minizinc --compile-solution-checker model.mzc.mzn
This will create the compiled checker model model.mzc, which can be used instead of the clear text version for checking:
minizinc model.mzn model.mzc data.dzn
The 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.
The rest of this section describes how to implement checker models.
3.6.2.1. Basic checker models
At 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:
% Colouring Australia using nc colours
int: nc = 3;
var 1..nc: wa; var 1..nc: nt; var 1..nc: sa; var 1..nc: q;
var 1..nc: nsw; var 1..nc: v; var 1..nc: t;
constraint wa != nt;
constraint wa != sa;
constraint nt != sa;
constraint nt != q;
constraint sa != q;
constraint sa != nsw;
constraint sa != v;
constraint q != nsw;
constraint nsw != v;
solve satisfy;
output ["wa=\(wa)\t nt=\(nt)\t sa=\(sa)\n",
"q=\(q)\t nsw=\(nsw)\t v=\(v)\n",
"t=", show(t), "\n"];
A checker model for this model requires the values of the variables wa, 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.
Since these values will be fixed in any solution, checker models simply declare parameters with the same name as the model variables:
int: wa;
int: nt;
int: sa;
int: q;
int: nsw;
int: v;
int: t;
output [
if wa!=nt /\ wa!=sa /\ nt!=sa /\ nt!=q /\ sa!=q /\
sa!=nsw /\ sa!=v /\ q!=nsw /\ nsw!=v
then "CORRECT\n"
else "INCORRECT\n"
endif
];
Running the model and the checker will produce output like this:
wa=3 nt=2 sa=1
q=3 nsw=2 v=3
t=3
% Solution checker report:
% CORRECT
----------
The solution checker report is embedded as comments in the original output.
3.6.2.2. Detailed feedback
The 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.
We can use standard MiniZinc functionality to provide much more detailed feedback. The following checker model introduces a helper function 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.
int: wa;
int: nt;
int: sa;
int: q;
int: nsw;
int: v;
int: t;
test check(bool: b,string: s) =
if b then true else trace_stdout("ERROR: "++s++"\n",false) endif;
output [
if check(wa!=nt, "wa and nt have the same colour")
/\ check(wa!=sa, "wa and sa have the same colour")
/\ check(nt!=sa, "nt and sa have the same colour")
/\ check(nt!=q, "nt and q have the same colour")
/\ check(sa!=q, "sa and q have the same colour")
/\ check(sa!=nsw, "sa and nsw have the same colour")
/\ check(sa!=v, "sa and v have the same colour")
/\ check(q!=nsw, "q and nsw have the same colour")
/\ check(nsw!=v, "nsw and v have the same colour")
then "CORRECT: all constraints hold.\n"
else "INCORRECT\n"
endif
];
However, 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:
wa=3 nt=3 sa=3
q=3 nsw=3 v=3
t=3
% Solution checker report:
% ERROR: wa and nt have the same colour
% INCORRECT
----------
In order to get all error messages, we can force the evaluation of all checkers by creating an auxiliary array of check results:
int: wa;
int: nt;
int: sa;
int: q;
int: nsw;
int: v;
int: t;
test check(bool: b,string: s) =
if b then true else trace_stdout("ERROR: "++s++"\n",false) endif;
array[int] of bool: checks = [
check(wa!=nt, "wa and nt have the same colour"),
check(wa!=sa, "wa and sa have the same colour"),
check(nt!=sa, "nt and sa have the same colour"),
check(nt!=q, "nt and q have the same colour"),
check(sa!=q, "sa and q have the same colour"),
check(sa!=nsw, "sa and nsw have the same colour"),
check(sa!=v, "sa and v have the same colour"),
check(q!=nsw, "q and nsw have the same colour"),
check(nsw!=v, "nsw and v have the same colour")
];
output [
if forall(checks)
then "CORRECT: all constraints hold.\n"
else "INCORRECT\n"
endif
];
Now the output contains all error messages (for the case where the model has no constraints):
wa=3 nt=3 sa=3
q=3 nsw=3 v=3
t=3
% Solution checker report:
% ERROR: nsw and v have the same colour
% ERROR: q and nsw have the same colour
% ERROR: sa and v have the same colour
% ERROR: sa and nsw have the same colour
% ERROR: sa and q have the same colour
% ERROR: nt and q have the same colour
% ERROR: nt and sa have the same colour
% ERROR: wa and sa have the same colour
% ERROR: wa and nt have the same colour
% INCORRECT
----------
3.6.2.3. Instance data in checker models
The 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.
For example, the following checker model could be used for the n-Queens problem.
int: n; % number of queens
set of int: ROW = 1..n;
set of int: COL = 1..n;
array[int] of int: q; % col of queen in each row
test check(bool: b,string: s) =
if b then true else trace_stdout("ERROR: "++s++"\n",false) endif;
output [
if check(index_set(q)=1..n, "ERROR: array q should have index set 1..\(n)")
/\ forall(i in 1..n)(check(q[i] in 1..n, "ERROR: q[\(i)] should have a value in 1..\(n)"))
/\ forall(r1, r2 in 1..n where r1 < r2)
(check(q[r1] != q[r2],
"queens in rows \(r1) and \(r2) are on same column\n")
/\
check(q[r1]+r1 != q[r2]+r2,
"queens in rows \(r1) and \(r2) are on same up diagonal\n")
/\
check(q[r1]-r1 != q[r2]-r2,
"queens in rows \(r1) and \(r2) are on same down diagonal\n")
)
then "CORRECT: All constraints hold"
else "INCORRECT" endif ];
The 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.
3.6.2.4. Checking optimisation problems
Optimisation 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.
To check that the objective value is calculated correctly, define a parameter called _objective of the appropriate type (int or float) in the checker. The example in the next section illustrates this.