CLP(FD)中的具体化谓词可以用来检查逻辑表达式的相等性吗？

Question

根据文档（第A.9.12节），可以具体化CLP(FD)约束，例如

#>

、

#=

、

#/\

等。

约束

#<==>/2

应该是

当 P 和 Q 相等时为真

根据同一节，其中

P

和

Q

表示可具体化的约束或布尔变量。但我似乎无法理解它应该如何使用。我希望能够确定使用 CLP(FD) 约束的两个布尔表达式是否等效，并且我希望

#<==>

能够做到这一点。

然而，

#<==>

在明显相互排斥的约束下取得了成功：

?- ((X #> 0) #\/ (X #< 0)) #<==> (X #= 0).  
_A in 0..1,
X#=0#<==>_A,
_B#\/_C#<==>_A,
_B in 0..1,
X#>=1#<==>_B,
X+1#=_D,
_C in 0..1,
0#>=_D#<==>_C.

我可以使具体化谓词在我的情况下发挥作用吗？ 如果没有，

\+ (A, #\ B)

形式的暗示（这似乎是我想要的）是这里的解决方案吗？

Answer 1

我希望能够确定使用 CLP(FD) 约束的两个布尔表达式是否等效，并且我希望 #<==> 能够做到这一点。

我不认为它能做到这一点；相反，它作用于左右表达式是否成立，并使代码可以进行推理； “双方都必须持有，否则双方都不持有”。

使用

(X#>5 #<==> B#=1)

作为演示，具有两个不同的变量：

固定 X=6，因此左侧成立，然后通过

#<==>

右侧必须成立，给出 B=1：

?- (X#>5 #<==> B#=1), X = 6.
B = 1,
X = 6

反之亦然，固定右侧 B=1，则左侧必须保持 X>5：

?- (X#>5 #<==> B#=1), B = 1.
B = 1,
X in 6..sup

或者用X=2固定左边

不

成立，然后通过

#<==>

右边也一定不成立，B不能是1：

?- (X#>5 #<==> B#=1), X = 2.
X = 2,
B in inf..0\/2..sup

同样修复右侧在 B=5 时不成立且左侧一定不成立的问题：

?- (X#>5 #<==> B#=1), B = 5.
B = 5,
X in inf..5