用Minizinc优化只打印最优解

Question

现在我正在仔细看看Minizinc。当求解模型时，Minizinc正在输出窗口中显示我的模型的所有有效解决方案。我有点困惑，因为我没有要求minizinc作为一个满意的问题来解决这个模型。是否有可能只显示最优解？谢谢你的回答。

诚挚的问候

Answer 1

你的solve声明是什么？如果是solve satisfy，那么您需要所有的解决方案。如果是solve minimize x或solve maximize x，则求解器将显示最优解的级数，最后给出最优解。

Answer 2

使用OptiMathSAT版本1.5.1，您现在可以使用选项打印给定FlatZinc公式的所有相同成本的最优解。

-opt.fzn.all_solutions=[BOOL]

，例如，接受以下test.fzn文件

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;

并将其解决如下：

~$ ../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;
----------
=========

x的最大值是3，因此求解器输出x等于3的所有和唯一的test.fzn模型。

当然，正如@hakank在他的回答中提到的那样，人们可能对向最优解的进展感兴趣。这也可以在OptiMathSAT中使用以下选项来完成

-opt.fzn.partial_solutions=[BOOL]

在上面的例子中，这将产生

~$ ../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;
----------
=========

在这里，优化搜索可以找到两个不同的模型:一个初始模型x等于2，另一个最优模型x等于3。后一次模型被打印两次:第一次被发现，第二次当求解者能够证明它实际上是问题的最优解时。