将“mod"运算符与“or"一起使用时强制具体化? [英] Mandatory reification when using the 'mod' operator together with 'or'?

问题描述

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

当我使用 mod 操作符时，我认为我需要改进我的约束编写与我谓词中的 #\/ 一起使用.

一个简短的例子:

:- use_module(library(clpfd)).constr(X,Y,Z) :-X 在 {1,2,3,4,5,6,7}，Y 在 {3,5,7}，Z 在 {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)

提前感谢您的想法.

解决方案

这是一个很好的观察和问题！首先，请注意这绝不是特定于 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是entailed，即necessively holds.

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

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

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

I have written a CSP program using CLP(FD) and SWI-Prolog.

I think I need to improve my constraints' writing when I use the mod operator together with #\/ in my predicates.

A short example :

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

If I call constr(3,Y,Z)., I get Z #= 1or Z #= 2. This is because some intermediate variables (relative to the mod expressions) still need to be evaluated.

Of course the ideal would be to only obtain Z #= 1.

How could this be done ?

I know that if I write instead

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

everything works as expected.

But is this reification mandatory ? I mean, do I have to create a reification variable each time I have this pattern in my constraints :

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

Thanks in advance for your ideas.

解决方案

That's a very good observation and question! First, please note that this is in no way specific to mod/2. For example:

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

In contrast, if we write this declaratively equivalently as:

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

then we get exactly as expected:

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

What is going on here? In all systems I am aware of, reification in general uses a decomposition of CLP(FD) expressions which unfortunately removes important information that is not recovered later. In the first example, it is not detected that the constraint X #= Y+Z is entailed, i.e., necessarily holds.

On the other hand, entailment of a single equality with non-composite arguments is correctly detected, as in the second example.

So yes, in general, you will need to rewrite your constraints in this way to enable optimal detection of entailment.

The lurking question is of course whether the CLP(FD) system could help you to detect such cases and perform the rewriting automatically. Also in this case, the answer is yes, at least for certain cases. However, the CLP(FD) system typically is told only individual constraints in a certain sequence, and recreating and analyzing a global overview of all posted constraints in order to merge or combine previously decomposed constraints is typically not worth the effort.

这篇关于将“mod"运算符与“or"一起使用时强制具体化?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！