'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 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，即 necessarily holds.

另一方面，正确检测到具有非复合参数的单个等式的蕴涵，如第二个示例。

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

潜伏的问题当然是 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]).

上面我将 SICStus 与 library(clpz) 一起使用，它是 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).

constr(3,Y,Z) 给出 Z in 1..2 但是 constrChoice(3,Y,Z,Xout,Yout,Zout) 给出 Zout=[1] ，所以不需要使用 contracting/1 因为 setof/3 和 indomain/1 一起使用就可以了。也不需要重写序言谓词。
现在，如果我有 AND #/\ 而不是 OR #\/，none 调用 constr(3,Y,Z)，constrChoice(3,Y,Z,Xout,Yout,Zout) 或 constrChoiceBetter(3,Y,Z,Xout,Yout,Zout) 给出 Z 必须是 1。我实际上已经知道 Y 是 21 或 42，但 Z 被告知是 1 或 2。什么有效：直接写 Y mod 21 #= 0，然后也不需要使用 contracting/1。

感谢您的评论。

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

Mandatory reification when using the 'mod' operator together with 'or'?

prolog

clpfd