MiniZinc Geocode 未将所有解决方案打印到启用“所有”解决方案的 CSP

Posted 2023-02-22

【中文标题】MiniZinc Geocode 未将所有解决方案打印到启用“所有”解决方案的 CSP

【英文标题】：MiniZinc Geocode not printing all solutions to CSP with "all" solutions enabled

【发布时间】：2019-05-12 14:09:02

【问题描述】：

问题

使用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);

【参考方案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)"
];

【讨论】：

感谢您解决此问题。我的目标是在多个示例中使用此代码 - 是否可以将 constraint card(span) 动态设置为找到的最低数字？

@Matsern 抱歉，不行，您必须先运行 minimize 然后添加约束。我建议您使用执行这些步骤的包装程序运行它。

【参考方案2】：

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

当在优化模式下要求所有解决方案时，求解器返回所有具有相同最优值的解决方案（相对于输出变量）。

示例：

~$ 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 是增量，这意味着该工具无需重新启动即可搜索其他解决方案，以便它可以重新使用之前生成的任何有用信息来加速 -搜索（例如理论引理）。 [警告：这可能与小实例无关；此外，根据输入问题，其他 MiniZinc 求解器可能仍然更快]

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

---

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