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

Question

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.

Answer 1

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.

Answer 2

With the (semi-official) contracting/1 predicate, you can minimize some domains in one fell swoop. In your case:

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

And now by adding a single goal:

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

In other words, a more consistent version of your predicate constr/3 would be:

constr_better(X, Y, Z) :-
   constr(X, Y, Z),
   clpz:contracting([Z]).

Above I used SICStus with library(clpz) which is the successor to library(clpfd) of SWI which has clpfd:contracting/1, too.