Sicstus CLPFD 标记时间差异

Question

我正在使用 Sicstus Prolog 来解决 Advent of Code 2024 Day 13，我发现同一约束模型的不同实例之间的标签时间存在令人惊讶的差异。我有：

minCost(Ax, Bx, P, A, B) :-
    A in 0..sup, B in 0..sup,
    P #= A*Ax + B*Bx,
    Cost #= A+B,
    labeling([minimize(Cost)], [A,B,Cost]) -> true; (A=nil, B=nil).

大多数情况（SAT 或 UNSAT）都在 1 毫秒内完成。例如：

?- minCost(27, 60, 100003443, A, B).
A = 9,
B = 1666720 ? 

随着

fd_statistics

显示：

Time:0, Resumps:148, Entailmnts:8, Prunings:157, Backtracks:1, Constrnts:4 

但在某些情况下，AoC 第 13 天的数据集（同样是 SAT 或 UNSAT）中大约 10% 的数据集需要大量时间。例如，这大约需要 3 秒：

minCost(48, 16, 100017648, A, B).
A = 2083701,
B = 0 ? 

随着

fd_statistics

显示：

Time:2722, Resumps:25004424, Entailmnts:8334812, Prunings:27088128, Backtracks:0, Constrnts:4 

注意恢复和修剪增加了 10^4 倍。此外，

A

非常高，

B

非常低，这是慢速 SAT 实例的模式。 还有很多缓慢的 UNSAT 实例，例如：

minCost(18, 21, 100001860, A, B).
A = nil,
B = nil ? 

随着

fd_statistics

显示：

Time:1273, Resumps:19047989, Entailmnts:2, Prunings:14285996, Backtracks:1, Constrnts:3

我将相同的数据集带到 SWI Prolog 的 CLPZ，总的来说它比 Sicstus 更快，但更重要的是它没有相同的差异。我尝试了一个名为 Minion 的非 prolog 求解器，它在总时间上的表现与 SWI 的 CLPZ 类似，并且没有这么大的差异。

我的问题是，即使对于如此小的模型，约束求解器的求解时间差异如此之大是否正常？也许 Sicstus 的求解器针对小数字进行了优化，而这些大整数超出了该范围？ （请注意，它们仍然小于 Sicstus/CLPFD 支持的最大整数）。或者我偶然发现了一个可能的错误？

注意：我尝试了 Sicstus 4.7.1 和 4.9.0，同样的问题。以上测量数据来自 4.9.0。

Answer 1

我是 SICStus Prolog 的主要作者。

你重新发现了 NP 难问题的一个特点：即使平均运行时间很短，但总会有异常实例需要花费大量时间。

您的数据中令人惊讶的是回溯计数较低。就好像搜索没有出错，所有时间都花在了约束传播上。

可能造成 SICStus 和其他求解器之间差异的因素是您使用“A in 0..sup, B in 0..sup”，这表示 A 和 B 没有上限。大多数其他求解器要么需要给定的上限，要么施加一些 MAXINT 界限。

为了能够提供更多评论，我需要您的代码。介意发一下吗？我很想深入挖掘。