Here is an example session with a few queries and their answers:
?- use_module(library(clpb)).
true.
?- sat(X*Y).
X = Y, Y = 1.
?- sat(X * ~X).
false.
?- taut(X * ~X, T).
T = 0,
sat(X=:=X).
?- sat(X^Y^(X+Y)).
sat(X=:=X),
sat(Y=:=Y).
?- sat(X*Y + X*Z), labeling([X,Y,Z]).
X = Z, Z = 1, Y = 0 ;
X = Y, Y = 1, Z = 0 ;
X = Y, Y = Z, Z = 1.
?- sat(X =< Y), sat(Y =< Z), taut(X =< Z, T).
T = 1,
sat(X=:=X*Y),
sat(Y=:=Y*Z).
?- sat(1#X#a#b).
sat(X=:=a#b).
The pending residual goals constrain remaining variables to Boolean
expressions and are declaratively equivalent to the original query. The
last example illustrates that when applicable, remaining variables are
expressed as functions of universally quantified variables.
