将'mod'运算符与'或'一起使用时必须具体化？

Question

我使用CLP(FD)和SWI-Prolog编写了一个CSP程序.

我认为当我在谓词中使用mod运算符时,我需要改进约束的写法#\/.

一个简短的例子:

:- use_module(library(clpfd)).

constr(X,Y,Z) :-
   X in {1,2,3,4,5,6,7},
   Y in {3,5,7},
   Z in {1,2},
   ((X #= 3)) #==> ((Y mod 3 #= 0) #\/ (Y mod 7 #= 0)),
   ((Z #= 1)) #<==> ((Y mod 3 #= 0) #\/ (Y mod 7 #= 0)).

如果我打电话constr(3,Y,Z).,我得到Z #= 1或Z #= 2.这是因为mod仍然需要评估一些中间变量(相对于表达式).

当然理想只是获得Z #= 1.

怎么可以这样做？

我知道如果我写的话

((X #= 3)) #==> ((Z #= 1)),
((Z #= 1)) #<==> ((Y mod 3 #= 0) #\/ (Y mod 7 #= 0)).

一切都按预期工作.

但这种具体化是强制性的吗？我的意思是,每次我在约束中使用此模式时,是否必须创建一个reification变量:

(A mod n1 #= 0) #\/ (B mod n2 #= 0) #\/ ... #\/ (Z mod n26 #= 0)

提前感谢您的想法.

Answer 1

这是一个非常好的观察和问题!首先,请注意,这绝不具体  mod/2.例如:

?- B #<==> X #= Y+Z, X #= Y+Z.
B in 0..1,
X#=_G1122#<==>B,
Y+Z#=X,
Y+Z#=_G1122.

相反,如果我们在声明上等效地写为:

?- B #<==> X #= A, A #= Y + Z, X #= A.

然后我们得到完全符合预期:

A = X,
B = 1,
Y+Z#=X.

这里发生了什么？在我所知道的所有系统中,通常使用CLP(FD)表达式的分解,遗憾的是,它删除了以后无法恢复的重要信息.在第一个例子,它是未检测到约束X #= Y+Z被entailed,即必然保持.

另一方面,正如第二个例子中那样,正确地检测到与非复合参数的单一相等的蕴含.

所以是的,一般来说,你需要以这种方式重写你的约束,以实现对蕴涵的最佳检测.

潜在的问题当然是CLP(FD)系统是否可以帮助您检测此类情况并自动执行重写.同样在这种情况下,答案是肯定的,至少对于某些情况.然而,CLP(FD)系统通常仅被告知特定序列中的各个约束,并且重新创建和分析所有发布的约束的全局概览以便合并或组合先前分解的约束通常不值得努力.