SWI Prolog Clpfd Library - Reification

Question

I have an upcoming Logic exam and have been studying some past papers from my course. I've come across a question regarding reification and have posted it below;

Illustrate reification by using it to express the property that a variable B can either take the value of 1 or 8.

After reading some resources and looking at the SWI Prolog manual, I still find the concept of reification quite confusing (primarily studying Java so the switch to learning Prolog has been difficult). It's quite confusing having to use boolean logic within the prolog query.

Without reification, I would have to write the following code (which I know is far too long to be the correct answer);

 B in 1..8, B #\= 2,B #\= 3,B #\= 4,B #\= 5,B #\= 6,B #\= 7. 

Would really appreciate if someone could show me the above query, but using reification.

Intransitive

Answer 1

From the documentation:

The constraints in/2, #=/2, #\=/2, #/2, #==/2 can be reified, which means reflecting their truth values into Boolean values represented by the integers 0 and 1. Let P and Q denote reifiable constraints or Boolean variables, then:

...
P #\/ Q True iff either P or Q
...

For you, it seems P is B #= 1 and Q is B #= 8, so you end up with:

?- B #= 1 #\/ B #= 8.
B in 1\/8.

As you see, you are not really using the reified values. You are just using reification as a round-about way of declaring the domain of your variable. The answer to your query, B in 1 \/ 8, is what you would probably use directly if you wanted to say that "B is either 1 or 8". If you look carefully at the documentation of in/2, you should see that the domain can be either an integer, a range Lower .. Upper, or the union of Domain1 \/ Domain2. In your case both domains are a single integer, 1 and 8.

PS: Once you go down that road, why not:

?- B in 1..8 #/\ #\ B in 2..7.
B in 1\/8.

B is in [1,8] AND B is not in [2,7].

The possibilities are endless :)

Vermicide

Answer 2

First, try out your query:

?- B in 1..8, B #\= 2,B #\= 3,B #\= 4,B #\= 5,B #\= 6,B #\= 7.
B in 1\/8.

This tells you that your query is equivalent to the single goal B in 1\/8.

From this, you see that you don't need reification to express that a finite domain variable is either equal to 1 or 8.

Reification allows you to reify the truth value of the constraint. For example, you can say:

?- T #<==> B in 1\/8.
T in 0..1,
B in 1\/8#<==>T.

?- T #<==> B in 1\/8, B = 3.
T = 0,
B = 3.

From the second query, you see that if B = 3, then T = 0, because the constraint B in 1\/8 doesn't hold in that case.

Reifying a constraint can be useful if you want to reason about constraints themselves. For example, this allows you to express that a certain number of list elements must be equal to a given integer. I leave solving this as a more meaningful exercise to understand reification.

Bonniebonns

... but B #= 1 #\/ B #= 8 is probably the expected answer. – Ovoviviparous

I must confess that this would never have occurred to me; however, I can still cram in a reification where it is not necessary if I write the example I gave as 1 #<==> B in 1\/8. – Bonniebonns

Answer 3

Initially I was thinking along the same lines as @Boris and @mat. But after pondering the question for a while, another possible interpretation of the task occured to me. However, keep in mind that I am not familiar with your course material, so this is highly speculative. That being said, maybe the task description is asking to write a predicate that evaluates to true if the above property holds or to false otherwise. A predicate like that could be defined as:

val_either_or_t(X,Y,Z,true) :-
   ( X#=Y ; X#=Z).
val_either_or_t(X,Y,Z,false) :-
   X #\= Y,
   X #\= Z.

I admit the name is a little clumsy but I couldn't really come up with a better one. Anyway, it does the job according to the task interpretation I described above:

   ?- val_either_or_t(X,1,8,T).
T = true,
X = 1 ? ;
T = true,
X = 8 ? ;
T = false,
X in inf..0\/2..7\/9..sup

   ?- val_either_or_t(X,Y,Z,T).
T = true,
X = Y,
X in inf..sup ? ;
T = true,
X = Z,
X in inf..sup ? ;
T = false,
X#\=Z,
X#\=Y

I came up with this idea because lately I was playing around with some reifying predicates that I found on Stackoverflow, and it popped into my mind that the task might be aimed in a direction where the described property could be used as a condition with such predicates. For example with if_/3 that I used a lot with (=)/3 in the condition, but why not use it with something like val_either_or_t/4. Consider the following minimal example:

a(condition_was_true).
b(condition_was_false).

somepredicate(X,Y) :-
   if_(val_either_or_t(X,1,8),a(Y),b(Y)).

With the respective query:

   ?- somepredicate(X,Y).
X = 1,
Y = condition_was_true ? ;
X = 8,
Y = condition_was_true ? ;
Y = condition_was_false,
X in inf..0\/2..7\/9..sup

This example is of course not very meaningful and only intended to illustrate how reification of the given property might be used. Also, I am using the atoms true and false to reify the thruth values with regard to using them with if_/3. However, you can also use 1 and 0 to reify truth values like in @mat's example. Just replace the 4th argument in the definition of val_either_or_t/4 by 1 and 0 respectively. Furthermore you might find the refinement of this idea that was suggested by @repeat in the comments interesting as well.

Incorporable

if_/3 + clpfd is a Good Thing™! Constraints don't mix well with non-monotonic constructs (!, \+, ->). – Foreman

A further refinement of val_either_or_t/4 could look like this: val_either_or_t(X,Y,Z,T) :- ( X#=Y #\/ X#=Z ) #<==> B, bool10_t(B, T). with bool10_t(1,true). bool10_t(0, false). With SICStus use (#<=>)/2 instead of SWI's (#<==>)/2. That way your code is deterministic in ground cases and non-deterministic only when required... – Foreman

Note the argument and the goal order in above suggested definition of bool10_t! (1) the true case comes before the false case. And (2) first argument indexing on the numeric value is exploited for avoiding the creation of useless choicepoints: with sufficiently instantiated data determinism is achieved. – Foreman