CLP(FD) 和 dif/2 中的重复约束

Question

在 SWI-Prolog 中，以下查询给出此结果：

?- X mod 2 #= 0, X mod 2 #= 0.
X mod 2#=0,
X mod 2#=0.

虽然正确，但显然不需要第二个约束

同样：

?- dif(X,0), dif(X,0).
dif(X, 0),
dif(X, 0).

有没有办法避免这种重复约束？（显然最正确的方法是不编写导致这种情况的代码，但这并不总是那么容易）。

Answer 1

您可以避免发布冗余约束，或者使用类似于 setof/3 的结构来删除它们。两者都是非常具体的实现。 SICStus 提供了用于此目的的最佳界面。 YAP 或 SWI 等其他实现或多或少地复制了该接口，通过省略 . A recent attempt 来克服 SWI 的缺陷而被拒绝。

避免发布限制

在 SICStus 中，您可以使用 frozen/2 来达到这个目的：

| ?- dif(X,0), frozen(X,Goal).
Goal = prolog:dif(X,0),
prolog:dif(X,0) ? ;
no
| ?- X mod 2#=0, frozen(X, Goal).
Goal = clpfd:(X in inf..sup,X mod 2#=0),
X mod 2#=0,
X in inf..sup ? ;
no

否则，copy_term/3 可能就足够了，前提是约束之间没有太多相互关联。

消除冗余约束

在这里，类似 setof 的构造与 call_residue_vars/1 and copy_term/3 一起可能是最好的方法。同样，原始实现在 SICStus 中....

Answer 2

很少有约束规划系统实现收缩也与解析定理证明中的因子相关，因为CLP标签不是SMT. Contraction is a structural rule，它的内容如下，假设约束存储在(|-)/2之前否定形式。

G, A, A |- B
------------ (Left-Contraction)
  G, A |- B

我们也可以将其扩展到两个 A 可推导等价的情况。这很可能没有实施，因为它很昂贵。例如 Jekejeke Minlog 已经实现了 CLP(FD) 的收缩，即有限域。我们发现查询类似于来自 OP 的第一个查询：

?- use_module(library(finite/clpfd)).
% 19 consults and 0 unloads in 829 ms.
Yes

?- Y+X*3 #= 2, 2-Y #= 3*X.
3*X #= -Y+2

?- X #< Y, Y-X #> 0.
X #=< Y-1

基本上我们分别归一化为 A1*X1+..+An*Xn #= B A1*X1+..+An*Xn #=< B 其中 gcd(A1,..,An)=1 和 X1, ..,Xn 是按词法排序的，然后我们检查约束存储中是否已经存在相同的约束。但是对于 CLP(H)，即 Herbrand 域名术语，我们还没有实施收缩。我们还在酝酿一个高效的算法：

?- use_module(library(term/herbrand)).
% 2 consults and 0 unloads in 35 ms.
Yes

?- neq(X,0), neq(X,0).
neq(X, 0),
neq(X, 0)

dif/2 的收缩意味着通过 dif/2 约束中定义的实例化来实现一种 (==)/2 。也就是说，我们需要在 dif/2 约束中定义的变量和项与约束存储中已有的所有其他 dif/2 约束配对之后应用递归测试。测试包容而不是收缩也会更有意义。

可能只有在某些适当的索引技术的帮助下才能为 dif/2 实现收缩或包含。在 Jekejeke Minlog for example for CLP(FD) we index on X1, but we did not yet realize some indexing for CLP(H). What we first might need to figure out is a normal form for the dif/2 constraints, see also this problem here.

Answer 3

仅对于 dif/2，可以在不借助任何内部结构的情况下测试蕴含：

difp(X,Y) :-
   (  X \= Y -> true
   ;  dif(X, Y)
   ).

CLP(FD) 和 dif/2 中的重复约束

Duplicate constraints in CLP(FD) and with dif/2

prolog

clpfd

避免发布限制

消除冗余约束