Boolean unification in Prolog?

Admin 1
Viewed 112

I am struggling alreay for a long time with the following problem. I want to make the usual unification of Prolog more smart.

Basically I want that certain variables understand that for example 0 = ~1 and 1 = ~0. This doesn't work normally:

?- op(300, fy, ~).
true.

?- X = ~Y, Y = 0.
X = ~0,
Y = 0.

I know that that CLP(B) can do it:

Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.7)

:- use_module(library(clpb)).
true.

?- sat(X=:= ~Y), Y = 0.
X = 1,
Y = 0.

But I require something more lightweight than loading a full CLP(B) library. Any ideas?

sat prolog constraints
1 Answers

It seems that SWI-Prologs when/2 does the job. I am using the Quine algorithm from here to partially evaluate a boolean expression. I can then define a Boolean let/2 predicate:

let(X, Y) :-
   eval(Y, H),
   term_variables(H, L),
   ( L== [] -> X = H;
      cond(L, R),
      when(R, let(X, H))).

cond([X], nonvar(X)) :- !.
cond([X,Y|Z], (nonvar(X);T)) :-
   cond([Y|Z], T).

The above predicate will reevaluate the expression assigned to the variable X when ever some variable inside the expression changes. The expression is associate with the variable X through when/2. Since we see when/2 in the top-level, we see the associated expression:

?- let(X, ~Y).
when(nonvar(Y), let(X, ~Y))

?- let(X, Y+Z).
when((nonvar(Y); nonvar(Z)), let(X, Y+Z))

And we can also do our use case and even more:

?- let(X, ~Y), Y = 0.
X = 1,
Y = 0.

?- let(X, Y+Z), Y = 0.
Y = 0,
when(nonvar(Z), let(X, Z))

?- let(X, Y+Z), Y = 0, Z = 1.
X = 1,
Y = 0,
Z = 1
Admin1
Related