Prolog boolean equation solve

Question

I have gotten this program to work so far in GNU prolog

not(X) :- \+ X.  
and(X, Y):-  X , Y.  
or(X, Y):-   X ; Y. 
implies(X, Y):- \+ X ; Y.  

p.
q.

:- initialization(main).

main :- 
    write('Program start'), nl.

You can type in and(p,q), and get yes, as well as and(p,not(q)) and get no. Now i'd like to do something like this:

I sett p to true, (by initializing it with p.) , and (and(p,q)) to true (but without initializing q), and i want prolog to say: One solution exists: "q" must be true

If i set p and (or(p,q)) to true i want prolog to say: Two solutions exists, "q" can be true or false. Which is the best way to do it?

Answer 1

I suggest that you use variables instead of p and q and wrap it in some term, e.g.

and(prop(P),prop(Q))

Additionally, I would implement two predicates, one for solving true statements, one for solving false statements. Using \+ is not the right approach since it doesn't allow you to bind variables. Here is a little bit of example code:

formula_true(prop(true)).
formula_true(and(A,B)) :- formula_true(A),formula_true(B).
formula_true(not(A)) :- formula_false(A).
...

formula_false(prop(false)).
formula_false(and(A,B)) :- formula_false(A);formula_false(B).
...

Your example query would then be:

P=true,formula_true(and(prop(P),prop(Q))).

And maybe you have a better name than formula_true resp. formula_false. :)

If you have a Boolean constraint solver, that would of course be more efficient.

Answer 2

Consider using a Prolog system with a Boolean constraint solver. For example, in SICStus and SWI-Prolog:

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

?- P = 1, sat(P * Q).
P = Q, Q = 1.

?- P = 1, sat_count(P + Q, Count).
Count = 2,
P = 1.

?- P = 1, sat(P + Q), labeling([P,Q]).
P = 1,
Q = 0 ;
P = Q, Q = 1.

You can also use the finite domain constraint solver of GNU Prolog, since Boolean values are a special case of integers.