Sicstus CLPFD Labeling时间差异异常问题技术咨询

问题背景 #

我使用Sicstus Prolog求解Advent of Code 2024 Day 13时，发现同一约束模型的不同实例之间，Labeling阶段的耗时存在显著差异。

约束模型代码 #

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).

性能表现差异 #

多数实例：快速求解 #

大部分可满足或不可满足的实例求解耗时低于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 

少数实例：极慢求解 #

约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值极小的模式。

同时存在大量慢的不可满足实例，例如：

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及Minion求解器时，总耗时更短，且无此类显著的性能差异。

疑问 #

• 针对如此小规模的约束模型，求解器出现这种时间差异是否正常？
• 是否因Sicstus求解器针对小整数做了优化，大整数超出其优化范围？
• 是否可能遇到了求解器的bug？

注：已在Sicstus 4.7.1和4.9.0版本测试，问题一致。

内容的提问来源于stack exchange，提问作者Görkem Paçacı