Mandatory confirmation when using the "mod" operator with "or"?

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

It seems to me that I need to improve the recording of my constraints when I use the mod operator with #\/ in my predicates.

A brief 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 #= 1 or Z #= 2 . This is due to the fact that some intermediate variables (relative to mod expressions) still need to be evaluated.

Of course, only Z #= 1 would be ideal.

How can I do that?

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 a binding obligation? I mean, do I need to create a reification variable every time I have this template in my constraints:

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

Thanks in advance for your ideas.

+5
source share
3 answers

This is a very good observation and a question! First, note that this in no way applies to mod/2 . For instance:

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

On the contrary, if we write it declaratively equivalent to:

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

then we get exactly as expected:

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

What's going on here? On all systems that I know about, reification usually uses the expression CLP (FD) expressions, which, unfortunately, removes important information that is not restored later. In the first example, it was not found that the restriction X #= Y+Z entails , i.e. Necessarily performed.

On the other hand, the correct detection of the occurrence of one equality with non-compositional arguments, as in the second example.

So yes, in general, you will need to rewrite your constraints in such a way as to ensure optimal occurrence detection.

The obvious question, of course, is whether the CLP (FD) system can help you detect such cases and automatically rewrite them. Also in this case, the answer is yes, at least for certain cases. However, the CLP (FD) system is usually only informed of individual constraints in a specific sequence, and re-creating and analyzing a global overview of all placed constraints to merge or combine previously decomposed constraints is usually not worth the effort.

+5
source

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 adding one 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 constr/3 predicate 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) SWI, which also has clpfd:contracting/1 .

+2
source

After trying a lot of things, I ended up with these conclusions, tell me if I am wrong (sorry, I'm new).

Consider this example:

 :- use_module(library(clpfd)). constr(X,Y,Z) :- X in {1,2,3,4,5,6,7}, Y in {3,5,7,21,42}, Z in {1,2}, (X #= 3) #==> ((Y mod 3 #= 0) #\/ (Y mod 7 #= 0)), (Z #= 1) #<==> ((Y mod 3 #= 0) #\/ (Y mod 7 #= 0)). constr_better(X,Y,Z) :- constr(X,Y,Z), clpfd:contracting([X,Y,Z]). res(X,L) :- setof(X, indomain(X), L). constrChoice(X,Y,Z,XOut,YOut,ZOut) :- constr(X,Y,Z), res(X,XOut),res(Y,YOut),res(Z,ZOut). constrChoiceBetter(X,Y,Z,XOut,YOut,ZOut) :- constr_better(X,Y,Z), res(X,XOut),res(Y,YOut),res(Z,ZOut). 
  • constr(3,Y,Z) gives Z in 1..2 , but constrChoice(3,Y,Z,Xout,Yout,Zout) gives Zout=[1] , so there is no need to use contracting/1 , because using setof/3 along with indomain/1 work. It is also not necessary to rewrite prolog predicates.

  • Now, if I have AND #/\ instead of OR #\/ , none of the calls are constr(3,Y,Z) , constrChoice(3,Y,Z,Xout,Yout,Zout) or constrChoiceBetter(3,Y,Z,Xout,Yout,Zout) does not give that Z should be 1. I really have that Y is 21 or 42, but Z say it is 1 or 2. What works: write that Y mod 21 #= 0 directly and then do not need to use contracting/1 .

Thanks for your comments.

+1
source

All Articles