对 MiniZinc 中“失败”求解器统计的澄清

Clarification on `failures` solver statistic in MiniZinc

我一直在 MiniZinc 中玩弄一个简单的 n 皇后模型:

include "globals.mzn";
int: n_queens = 8;
array[1..n_queens] of var 1..n_queens: queens;

constraint alldifferent(queens);
constraint alldifferent(i in 1..n_queens) (queens[i] + i);
constraint alldifferent(i in 1..n_queens) (queens[i] - i);
solve satisfy;

MiniZinc handbook 提到 failures 作为“失败的叶节点数”。以下是 运行 模型之后的统计数据:

%%%mzn-stat: initTime=0.000576
%%%mzn-stat: solveTime=0.000822
%%%mzn-stat: solutions=1
%%%mzn-stat: variables=24
%%%mzn-stat: propagators=19
%%%mzn-stat: propagations=1415
%%%mzn-stat: nodes=47
%%%mzn-stat: failures=22
%%%mzn-stat: restarts=0
%%%mzn-stat: peakDepth=5
%%%mzn-stat-end

有22次失败。作为约束编程的初学者,我的理解是范式的全部目的是尽可能地修剪和避免叶节点。我特别困惑,因为搜索树的峰值深度被报告为 5(而不是 8)。

我对这些统计数据的理解正确吗?如果是,为什么模型中会出现叶节点故障?我会通过尝试减少这些失败来创建更好的模型吗?

这些值取决于搜索策略,有时您无法避免叶节点,因为它尚未被 p运行ed,这意味着,在它告诉求解器该节点将要到达之前什么也没有是一个失败,以不同的方式建模可以防止一些失败,并且还可以防止在优化问题的情况下的次优解决方案。

这些是在 minizinc 默认搜索策略的搜索树上被评估的前三个节点,我按照它们被评估的顺序将它们标记在 image of the Search Tree 中,4 和 5 显示到达可行的解决方案。

其中蓝点是仍然存在不确定性的节点,红色方块是失败的,白点是未评估的节点,大三角形是搜索仅导致失败的整个分支,绿色菱形表示可行解决方案,橙色菱形表示 non-best-but-feasible 解决方案(仅在优化问题中)。

每个标记节点的解释是

0:根节点:所有变量未赋值

什么都没发生,这些都是决策变量及其完整域
queens = array1d(1..8, [[1..8], [1..8], [1..8], [1..8], [1..8], [1..8], [1..8], [1..8]]);

1:第一个决定

然后它选择最后一个变量域中的最小值并进行第一次拆分,求解器认为 queens[8] = 1(根的左侧 child)或 queens[8] = [2..8] (根的右 child),它将首先评估 queens[8] = 1 并使第一个节点存在,
queens = array1d(1..8, [[2..7], {2..6,8}, {2..5,7..8}, {2..4,6..8}, {2..3,5..8}, {2,4..8}, [3..8], 1]); 其中决策 queens[8] = 1 已经传播到其他变量并从其域中删除了值。

2:搜索继续

然后它再次在 queens[7] 处分裂,这是左 child 节点,其中 queens[7] = 3,该变量域中的最小值,以及该决策的传播其他变量。 queens = array1d(1..8, [{2,4..7}, {2,4..6}, {2,4..5,8}, {2,4,7..8}, {2,6..8}, [5..8], 3, 1]);

事后看来(更像是通过查看 image of the Search Tree 作弊)我们知道搜索的整个分支都会失败,但我们无法在搜索时知道这一点,因为在某些方面仍然存在不确定性变量,要知道我们必须评估所有可能性,这些可能性 可能 可行,可能发生或不发生,希望我们能在此之前找到令人满意的解决方案,但在继续之前通过搜索,请注意已经有一些 p运行ing 以不存在的节点形式完成,例如 queens[4] 此时只能取值 2,4,7,8,我们还没有对它做出任何决定,它只是求解器从它知道肯定会导致失败的变量中消除值,如果我们在哪里进行强力搜索,这个变量将具有与根节点相同的域[1..8] 因为我们还没有做出决定,所以我们正在通过传播约束来进行更智能的搜索。

3:第一次失败:但我们继续

继续使用相同的策略,它对 queens[6] 进行拆分,这次是最小值 queens[6] = 5,当传播到未定变量时,但是没有满足所有约束的解决方案(这里给了两个皇后8的值),所以这是一个死胡同,必须回溯。
queens = array1d(1..8, [7, 2, 4, 8, 8, 5, 3, 1]); ---> 失败

所以搜索的前三个节点导致失败。

搜索就这样继续,因为 queens[6] = 5 的选择导致失败,它会转到下一个值 queens[6] = [6..8],该搜索也会导致 queens[6] = 5 中用红色圈出的失败=45=].

正如您现在可能猜到的那样,搜索策略类似于 go in the order of the variablessplit the domain of the variables by picking the smallest value available and put the rest of the domain in another node,这在 minizinc 搜索注释中称为 input_orderindomain_min

现在我们将搜索快进到标记为 4.

的节点

4:解决方案的前奏:我们到了吗?

在这里你可以看到 queens[8] = 1(保持不变),queens[7] = 5 而在节点 2 中是 queens[7] = 3,那意味着 queens[8] = 1queens[7] = [3..4] 的所有可能性,无论是评估还是 p运行ed,但都会导致失败。
queens = array1d(1..8, [{2,4,6..7}, {2..3,6}, {2..4,7}, {3..4,7}, {2,6}, 8, 5, 1]);

然后这个节点进入queens[6] = 2(左child)导致更多失败和queens[6] = 6(右child)

5:我们挖到了金子:一个可行的解决方案!!

queens[2] = 6传播了,结果满足了所有的约束,所以我们有解,我们停止搜索。 queens = array1d(1..8, [4, 2, 7, 3, 6, 8, 5, 1]);

P运行ing

只需要 47 个巨大的节点 Whole Search Tree, the area inside the blue line is the search tree is the Search Tree 就可以得到解决方案,其中标记为 0,1,2,3,4,5 的节点是巨大的甚至 p运行ed 对于这个具有全局约束的 8 个基数为 8 的决策变量的相对较小的实例,这肯定会大大减少搜索树的跨度,因为它可以更有效地相互传达变量的域比求解器的约束存储。整个搜索树总共只有723个节点(节点和叶子),其中只有362个是叶子,而暴力搜索可以生成所有可能的8^8个叶子节点方向ly(同样,它可能不会,但它可以),那就是搜索 space 16.777.216 种可能性(它就像 8 个八进制数字,因为它的 8 个变量的基数为 8),当你比较一下,在求解器的 16.777.216 中,只有 362 个有意义,在可行的情况下有 92 个,它不到整个搜索 space 组合的 0.0001%,例如,随机生成生成[1..8]范围内的8个随机数字,然后评估其可行性的解决方案,大海捞针。

P运行ing 基本上意味着减少搜索 space,任何比评估所有组合更好的东西,即使删除一个单一的可能性也被认为是 p运行ed 搜索space。由于这是一个满意度问题而不是优化问题,p运行ing 只是从变量域中删除不可行的值。
在优化问题中有两种类型的 p运行ing,像以前一样满足 p运行ing,消除不可能的解决方案,以及 p运行ing 由 objective 函数,当 objective 函数的边界可以在所有变量达到一个值之前确定并且被确定为 “最差” 比当前 "best" 到目前为止找到的值(即在最小化优化中 objective 可以在分支中采用的最小值大于目前在可行解决方案中找到的最小值)你可以 p运行e 那个分支,它肯定包含可行(但不是很好)的解决方案以及不可行的解决方案,并节省一些工作,而且你仍然必须 p运行e 或评估所有如果你想找到最优解并且证明它是最优的。

要像图像那样探索搜索树,您可以使用 minizinc IDE 中的 gecode-gist 求解器 运行 您的代码,或者使用 minizinc --Solver gecode-gist <modelFile> <dataFile>命令行,双击其中一个节点后,您将看到决策变量的状态,就像 post.

中的一样

甚至进一步使用 solve :: int_search( pos, varChoise, valChoise, complete) satisfy; 来测试这种不同的搜索策略

% variable selections:
ann : varChoise
%          = input_order
%          = first_fail
%            = smallest
%          = largest
;

% value selections:
ann : valChoise
%          = indomain_min
%          = indomain_max
%          = indomain_median
%          = indomain_random
%          = indomain_split
%            = indomain_reverse_split
;

只需将其粘贴到您的模型中并取消注释一个 varChoise 注释和一个 valChoise 以测试变量选择和值选择的组合,并查看一种策略是否找到具有更少失败、更少节点或更少传播的解决方案。您可以在 minizinc 文档中阅读更多关于它们的信息。