Prolog CLPFD传递性

Question

“显而易见”不是一个轻率的词，但是为什么SWI-Prolog的CLPFD正确地解决了这个问题：

?- A+1 #= A*2.
A = 1.

但不是这样的：

?- B #= A + 1, B #= A * 2.
A+1#=B,
A*2#=B.

(label和indomain yield Arguments are not sufficiently instantiated。)

是不是just...the求解器没有捕捉到这种情况？(我肯定希望它能应用传递性。)或者它是某种更深层次的句法难题的症状，或者别的什么？

Answer 1

它尝试从每个变量的域中的值来求解约束！由于B和A的域是无限的，并且没有约束，在约束满足上的回溯将被延迟，程序将被停止。

这意味着它试图为约束B #= A + 1找到一些解决方案，但它找到了许多( A和B的无限值)，对于第二个约束也是如此。因此，它将在这里停止，因为A和B的可能值是无限的。但是，结果不是No。这是有两个延迟目标的Yes。

B = B{-1.0Inf .. 1.0Inf}
A = A{-1.0Inf .. 1.0Inf}
There are 2 delayed goals.

要解决此问题，您需要绑定A或B中的至少一个。例如，如果您运行此查询A::1..1000, B#=A+1, B #= A*2.，您将获得与示例中的第一个查询相同的结果。而且，clpfd中没有任何演绎来解决传递性问题，因为它使用回溯方法。

总而言之，这是您正在使用的库的缺点之一，因为当具有多个变量的约束的域具有无限大域时，它将停止，您可以通过为至少一个变量设置有界域来解决它。