Can reification predicates from CLP(FD) be used to check equality of logic expressions?

Question

According to the documentation (section A.9.12), CLP(FD) constraints such as #>, #=, #/\ etc. can be reified.

Constraint #<==>/2 is supposed to be

True iff P and Q are equivalent

according to the same section, where P and Q denote reifiable constraints or Boolean variables. But I can't seem to understand how it is supposed to be used. I would like to be able to determine whether two boolean expressions that use constraints from CLP(FD) are equivalent, and I expected #<==> to do exactly that.

However, #<==> succedes with clearly mutually exclusive constraints:

?- ((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.

Can I make reification predicates work in my case?

If not, will implication in the form of \+ (A, #\ B) (that seems to do what I want) be the solution here? (Update: it fails if expressions contain multiple variables)

Answer 1

I would like to be able to determine whether two boolean expressions that use constraints from CLP(FD) are equivalent, and I expected #<==> to do exactly that.

No, I do not think it can do this. From the documentation you linked, in "Let P and Q denote reifiable constraints or Boolean variables" read P and Q as Booleans, then "True iff P and Q are equivalent" says that P and Q must be both true or both false. It does not say what you want, that "the constraints are equivalent" but instead that "the truth value of the constraints, whether they hold or not, are equivalent".

The problem reification solves is that you can constrain X to be positive or negative, non-zero, but then you cannot write code to use that result - further reason one way if X is negative, a different way if X is positive - because you do not yet know which is correct. Reifying the result turns it into something you can code against - "if X turns out to be negative, then this new constraint must hold".

The reification operators go through the various options "either constraint must hold", "both must hold", etc. and "if one holds, it implies the other must hold" going left, right, or both ways.

e.g. Using (X#>5 #<==> B#=1) as a demo, with two different variables:

If, in the process of labelling the variables, Prolog finds X is solved to be six, then the left side of #<==> is known to hold, so through #<==> the right side must now hold and B must be solved to 1:

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

or vice-versa, if B becomes solved to 1 on the right, then through #<==> the constraint on the left must hold and X must be greater than 5:

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