Optimization with Minizinc - Only print optimal solutions

Question

at the moment I'm having a closer look on Minizinc. Minizinc is showing all valid solutions of my model in the output window when solving the model. I'm a bit confused because I did not ask minizinc to solve the model as a satisfaction problem. Is there a possibility that only optimal solutions are shown? Thanks for your answers.

best regards

Answer 1

What is your solve statement? If it's solve satisfy then you ask for all solutions. If it's solve minimize x or solve maximize x then the solver will show the progression of optimal solutions, with the optimal solution is shown last.

Answer 2

With OptiMathSAT version 1.5.1, one can now print all same-cost optimal solutions of a given FlatZinc formula using option

-opt.fzn.all_solutions=[BOOL]

e.g. take the following test.fzn file

var 0..3: x ::output_var;
var 0..3: y ::output_var;
var bool: r1 ::output_var;
var bool: r2 ::output_var;

constraint int_lin_le_reif([1, 1, -1], [x, y, 4], 0, r1);
constraint int_lin_le_reif([1, 1, -1], [x, y, 2], 0, r2);
constraint bool_or(r1, r2, true);

solve maximize x;

and solve it as follows:

~$ ../bin/optimathsat -input=fzn -opt.fzn.all_solutions=True < test.fzn
% allsat model
x = 3;
y = 0;
r1 = true;
r2 = false;
----------
% allsat model
x = 3;
y = 1;
r1 = true;
r2 = false;
----------
=========

The maximum value for x is 3, hence the solver prints all-and-only those models of test.fzn for which x is equal to 3.

---

Naturally, as mentioned by @hakank in his answer, one might be interested in the progression of solutions towards the optimal one. This can also be done in OptiMathSAT using the option

-opt.fzn.partial_solutions=[BOOL]

On the example above, that would yield

~$ ../bin/optimathsat -input=fzn -opt.fzn.partial_solutions=True < test.fzn
% objective: x (model)
x = 2;
y = 0;
r1 = true;
r2 = true;
----------
% objective: x (model)
x = 3;
y = 0;
r1 = true;
r2 = false;
----------
% objective: x (optimal model)
x = 3;
y = 0;
r1 = true;
r2 = false;
----------
=========

Here the optimization search finds two different models: an initial one in which x is equal to 2, and an optimal one in which x is equal to 3. The latter model gets printed twice: the first time as soon as it is found, the second time when the solver is able to prove that it is actually the optimal solution of the problem.