将“mod”运算符与“or”一起使用时强制具体化？

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

一切都按预期进行。

但是这种物化是强制性的吗？我的意思是，每次我的约束中有这种模式时，我是否必须创建一个具体化变量：

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

提前感谢您的想法。

Answer 1

这是一个非常好的观察和问题！首先，请注意，这绝不是 mod/2 特有的。例如：

?- B # X #= Y+Z, X #= Y+Z。 B 在 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包含，即必然持有。

另一方面，与第二个示例一样，可以正确检测到单个等式与非复合参数的蕴涵。

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

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

Answer 2

使用（半官方）contracting/1 谓词，您可以一举减少某些域。在你的情况下：

| ?- constr(3,Y,Z).
clpz:(Z#=1#<==>_A),
clpz:(_B#=0#<==>_C),
clpz:(_D#=0#<==>_E),
clpz:(_F#=0#<==>_G),
clpz:(_H#=0#<==>_I),
clpz:(_C#\/_E#<==>1),
clpz:(_G#\/_I#<==>_A),
clpz:(Y mod 3#=_B),
clpz:(Y mod 3#=_F),
clpz:(Y mod 7#=_D),
clpz:(Y mod 7#=_H),
clpz:(Y in 3\/5\/7),
clpz:(Z in 1..2),
clpz:(_C in 0..1),
clpz:(_B in 0..2),
clpz:(_E in 0..1),
clpz:(_D in 0..6),
clpz:(_A in 0..1),
clpz:(_G in 0..1),
clpz:(_F in 0..2),
clpz:(_I in 0..1),
clpz:(_H in 0..6) ? ;
no

现在添加一个目标：

| ?- constr(3,Y,Z), clpz:contracting([Z]).
Z = 1,
clpz:(_A#=0#<==>_B),
clpz:(_C#=0#<==>_D),
clpz:(_E#=0#<==>_F),
clpz:(_G#=0#<==>_H),
clpz:(_B#\/_D#<==>1),
clpz:(_F#\/_H#<==>1),
clpz:(Y mod 3#=_A),
clpz:(Y mod 3#=_E),
clpz:(Y mod 7#=_C),
clpz:(Y mod 7#=_G),
clpz:(Y in 3\/5\/7),
clpz:(_B in 0..1),
clpz:(_A in 0..2),
clpz:(_D in 0..1),
clpz:(_C in 0..6),
clpz:(_F in 0..1),
clpz:(_E in 0..2),
clpz:(_H in 0..1),
clpz:(_G in 0..6) ? ;
no

换句话说，您的谓词constr/3 的更一致版本将是：

constr_better(X, Y, Z) :-
   constr(X, Y, Z),
   clpz:contracting([Z]).

上面我使用了带有library(clpz) 的SICStus，它是SWI 的library(clpfd) 的继承者，也有clpfd:contracting/1。

Answer 3

在尝试了很多东西之后，我最终得出了这些结论，如果我错了，请告诉我（对不起，我是初学者）。

让我们考虑这个示例：

:- use_module(library(clpfd)).

constr(X,Y,Z) :-
   X in {1,2,3,4,5,6,7},
   Y in {3,5,7,21,42},
   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_better(X,Y,Z) :- constr(X,Y,Z), clpfd:contracting([X,Y,Z]).

res(X,L) :- setof(X, indomain(X), L).

constrChoice(X,Y,Z,XOut,YOut,ZOut) :-
   constr(X,Y,Z),
   res(X,XOut),res(Y,YOut),res(Z,ZOut).

constrChoiceBetter(X,Y,Z,XOut,YOut,ZOut) :-
   constr_better(X,Y,Z),
   res(X,XOut),res(Y,YOut),res(Z,ZOut).

1. constr(3,Y,Z) 给出 Z in 1..2 但是 constrChoice(3,Y,Z,Xout,Yout,Zout) 给出 Zout=[1] ，所以不需要使用 contracting/1 因为 setof/3 与 indomain/1 一起使用工作。也不需要重写 prolog 谓词。

1234563或 42，但 Z 被告知为 1 或 2。 什么有效：直接写Y mod 21 #= 0，然后也不需要使用contracting/1。

感谢您的 cmets。