MiniZinc Geocode 未在启用 "all" 解决方案的情况下将所有解决方案打印到 CSP

Question

问题

使用solve minimize我只得到一个解决方案，即使有多个最佳解决方案。我在求解器配置中启用了多个解决方案的打印输出。其他最佳解决方案与 solve satisfy 以及非最佳解决方案一起找到。

可能的原因

可能是基数函数card()在两个集合大小相等的情况下按枚举值排名？也就是说card(A, B) > card(B, C)？如果是这样，我是否必须切换顶点的表示？

计划

我正在创建一个 MiniZinc 程序来查找给定图形的最小顶点覆盖。本例中的图形是这样的：

最小顶点覆盖解决方案是： [{A, B, C, E}, {A, B, E, F}, {A, C, D, E}, {B, C, D, E}, {B, C, D, F}, {B, D, E, F}]。 我的代码只输出{A, B, C, E}.

数据文件：

VERTEX = {A, B, C, D, E, F};
       
edges = [|1, 0, 1, 0, 0, 0, 0, 0, 0
         |1, 1, 0, 1, 1, 0, 0, 0, 0
         |0, 1, 0, 0, 0, 1, 1, 0, 0
         |0, 0, 1, 1, 0, 0, 0, 1, 0
         |0, 0, 0, 0, 1, 1, 0, 1, 1
         |0, 0, 0, 0, 0, 0, 1, 0, 1|];

求解器程序：

% Vertices in graph
enum VERTEX;

% Edges between vertices
array[VERTEX, int] of int: edges;

int: num_edges = (length(edges) div card(VERTEX));

% Set of vertices to find
var set of VERTEX: span;

% Number of vertices connected to edge resulting from span
array[1..num_edges] of var 0..num_edges: conn;

% All edges must be connected with at least one vertex from span
constraint forall(i in 1..num_edges)
           (conn[i] >= 1);

% The number of connections to each edge is the number of vertices 
% in span with a connection to that edge
constraint forall(i in 1..num_edges)
           (conn[i] = sum([edges[vert,i]| vert in span]));
           
% Minimize the number of vertices in span
solve minimize card(span);

Answer 1

solve minimize 只显示一个最优解（在某些情况下，也可能显示中间值）。

如果您想要所有最优解，您必须使用 solve satisfy 和添加具有最优值的约束：

constraint card(span) = 4;

然后模型输出所有6个最优解：

card(cpan): 4
span: {A, B, C, E}
conn: [2, 2, 1, 1, 2, 2, 1, 1, 1]
----------
card(cpan): 4
span: {B, C, D, F}
conn: [1, 2, 1, 2, 1, 1, 2, 1, 1]
----------
card(cpan): 4
span: {A, C, D, E}
conn: [1, 1, 2, 1, 1, 2, 1, 2, 1]
----------
card(cpan): 4
span: {B, C, D, E}
conn: [1, 2, 1, 2, 2, 2, 1, 2, 1]
----------
card(cpan): 4
span: {A, B, E, F}
conn: [2, 1, 1, 1, 2, 1, 1, 1, 2]
----------
card(cpan): 4
span: {B, D, E, F}
conn: [1, 1, 1, 2, 2, 1, 1, 2, 2]
----------
==========

注意：我添加了 output 部分以显示所有值：

output [
   "card(cpan): \(card(span))\n",
   "span: \(span)\n",
   "conn: \(conn)"
];

Answer 2

另一种解决方案是使用 OptiMathSAT (v. 1.6.3)。

在优化模式下求所有解时，求解器returns所有解（相对于输出变量）具有相同的最优值。

示例：

~$ mzn2fzn test.mzn test.dzn                                        # your instance
~$ optimathsat -input=fzn -opt.fzn.all_solutions=True < test.fzn 
% allsat model
span = {2, 4, 5, 6};
conn = array1d(1..9, [1, 1, 1, 2, 2, 1, 1, 2, 2]);
----------
% allsat model
span = {1, 3, 4, 5};
conn = array1d(1..9, [1, 1, 2, 1, 1, 2, 1, 2, 1]);
----------
% allsat model
span = {1, 2, 3, 5};
conn = array1d(1..9, [2, 2, 1, 1, 2, 2, 1, 1, 1]);
----------
% allsat model
span = {1, 2, 5, 6};
conn = array1d(1..9, [2, 1, 1, 1, 2, 1, 1, 1, 2]);
----------
% allsat model
span = {2, 3, 4, 5};
conn = array1d(1..9, [1, 2, 1, 2, 2, 2, 1, 2, 1]);
----------
% allsat model
span = {2, 3, 4, 6};
conn = array1d(1..9, [1, 2, 1, 2, 1, 1, 2, 1, 1]);
----------
=========

主要优势在于。接受的答案中提出的方法是 OptiMathSAT 是增量，这意味着该工具无需重新启动即可搜索其他解决方案，因此它可以 re-use 任何有用的信息先前生成到 speed-up 搜索（例如理论引理）。 [注意：这可能与小实例无关；此外，其他 MiniZinc 求解器可能仍然更快，具体取决于输入问题]

注意：请注意OptiMathSAT不会打印每个VERTEX的标签，因为mzn2fzn 编译器在编译文件时删除了这些标签。但是，数字和标签之间的映射应该是显而易见的。

披露：我是这个工具的开发者之一。

MiniZinc Geocode 未在启用 "all" 解决方案的情况下将所有解决方案打印到 CSP

MiniZinc Geocode not printing all solutions to CSP with "all" solutions enabled

minizinc

optimathsat