Finding consistent assignments for logical formulas

Question

I am about to implement a prover for logical terms in Prolog. My current code is not really presentable, therefore, I will just state, what I want my program to do and hopefully you can give me some good advice for that :)

It should take a list of variables (so to say the logical arguments) and secondly a logical formula containing these arguments (e.g. 'not'(A 'and' B) 'or' 'not'(B 'and' C) 'or' ... and so forth).

As output I would like my program to respond with the possible consistent assignments. The single arguments can either be true (1) or false (0).

So I aim for a return like A=0, B=0, C=0 ; A=1 and so forth.

I am happy for every help concerning my program :)

Answer 1

There are several ways one could approach this. One way that is convenient in terms of syntax would be to define operators, something like this:

:- op(500, fx, not).
:- op(600, xfx, and).
:- op(700, xfx, or).

(I am just guessing at reasonable precedence settings here, but just for illustration. See the op documentation for details.)

Having done that, you can write an expression such as: A and B and Prolog will "see" it as and(A, B):

| ?- write_canonical(A and B).
and(_23,_24)

From there, you need to have a way to evaluate an expression. There are lots of questions on SO here in this regard (do a search in this site on [prolog] boolean expression evaluation), but I'll provide a simple example. It's now all about how you want to represent a result, and about recursion.

When it comes to representing a result, you could use Prolog's success/fail mechanism since you are dealing with boolean results. Or, you can have an explicit result, such as 0 and 1. Let's try 0 and 1 since that's your representation for true and false.

% Describe a valid boolean
bool(0).
bool(1).

% The evaluation of a valid boolean is itself
exp_eval(X, X) :- bool(X).

% Evaluation of an 'and' expression
exp_eval(and(A, B), Result) :-
    exp_eval(A, ResultA),
    exp_eval(B, ResultB),
    Result #= ResultA * ResultB.

% Evaluation of an 'or' expression
exp_eval(or(A, B), Result) :-
    exp_eval(A, ResultA),
    exp_eval(B, ResultB),
    % Just a little trick to get 1 if either ResultA or ResultB or both are 1
    Result #= (ResultA + ResultB + 1) // 2.

% Evaluation of a 'not' expression
exp_eval(not(A), Result) :-
    exp_eval(A, ResultNot),
    Result #= 1 - ResultNot.  % 0 ---> 1, and 1 ---> 0

Instead of calculating "boolean" 1/0 results as I've done above, you could, instead, assert them as facts like so:

bool_not(0, 1).
bool_not(1, 0).

bool_and(0, 0, 0).
bool_and(0, 1, 0).
bool_and(1, 0, 0).
bool_and(1, 1, 1).

bool_or(0, 0, 0).
bool_or(0, 1, 1).
bool_or(1, 0, 1).
bool_or(1, 1, 1).

And then, for example, instead of Result #= (ResultA + ResultB + 1) // 2 you could just have, bool_or(ResultA, ResultB, Result).

Now that we can evaluate expressions, we want a solver:

solve(Exp) :-
    term_variables(Exp, Variables),
    maplist(bool, Variables),  % Variables should be valid booleans
    exp_eval(Exp, 1).          % We only want true results for the expression

Note that in the original problem statement, it's said that the variable list would be given as an argument, but you can use term_variables/2 to obtain the variables from an expression.

Then you can run the solver:

| ?- solve(not(A and B) or not(B and C)).

A = 0
B = 0
C = 0 ? a

A = 0
B = 0
C = 1

A = 0
B = 1
C = 0

A = 0
B = 1
C = 1

A = 1
B = 0
C = 0

A = 1
B = 0
C = 1

A = 1
B = 1
C = 0

no
| ?-

I don't know what your representation is for an expression. But whatever it is, you can map it to the above solution. What I've shown is simple and clear. You could skip the op/3 stuff and use standard term expressions, like, or(not(and(A,B)), not(and(B,C))) using the above code. If you have your input as some kind of token sequence, like, [not, (, A, and, B, ...] then you'll have to do a little list processing.