使用 Minizinc 进行优化 - 仅打印最佳解决方案

Question

目前我正在仔细研究 Minizinc。求解模型时，Minizinc 在输出 window 中显示了我的模型的所有有效解。我有点困惑，因为我没有要求 minizinc 将模型作为满足问题来解决。是否有可能只显示最佳解决方案？感谢您的回答。

此致

Answer 1

你的solve声明是什么？如果它是 solve satisfy 那么你要求所有的解决方案。如果是 solve minimize x 或 solve maximize x 那么求解器将显示最优解的进展，最后显示最优解。

Answer 2

使用 OptiMathSAT 版本 1.5.1，现在可以使用选项

打印给定 FlatZinc 公式的所有 same-cost 最优解

-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，因此求解器打印 all-and-only test.fzn 的那些模型，其中 x 等于 3.

自然地，正如 @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 等于 [=20] 的最佳模型=].后一个模型被打印两次：第一次是在找到它时，第二次是在求解器能够证明它实际上是问题的最优解时。

使用 Minizinc 进行优化 - 仅打印最佳解决方案

Optimization with Minizinc - Only print optimal solutions

minizinc

optimathsat