Case Study: Other Ways of Thinking - Thinking as Computation - page 261

Figure 11.13. A satisfiability program

sat.pl

% The dclauses in DL are satisfied by picking Lits.
sat(DL,Lits) :- satpick(DL,[],Lits).
% satpick(DL,P,Lits): the dclauses in DL can be satisfied by
% picking the literals in Lits, given that those in P are taken.
satpick([],P,P).
satpick([D|DL],P1,Lits) :- pickone(D,P1,P2), satpick(DL,P2,Lits).
pickone([L|_],P,P) :- member(L,P). % L is picked.
pickone([L|_],P,[L|P]) :- \+ member_neg(L,P). % ˜L is not picked.
pickone([_|D],P,P2) :- pickone(D,P,P2). % Use D instead.

member_neg(A,P) :- member(not(A),P).
member_neg(not(A),P) :- member(A,P).

The predicate member_neg is used to check if the negation of a literal has already been
picked. It does this by either adding or removing a not on the given literal.
It is not hard to confirm that this predicate does the right thing:
?- sat([[p],[not(p),not(q)],[not(q)]],L).
L = [not(q), p]
Yes
?- sat([[p],[not(p),not(q)],[q]],L).
No
?- sat([[p,q],[not(p),q],[not(q),p],[not(p),not(q)]],_).
No

11.4.4 Logical entailment reconsidered

The notion of logical entailment can now be enlarged to deal with knowledge bases
that are lists of dclauses. Continue to assume that there are no variables in the
dclauses, and for simplicity, that the queries are as before, a list of atoms or their
negations, all of which are to be established. It is then easy to do logical entailment:
negate the literals in the query and let the sat predicate do the heavy lifting, as shown
in figure 11.14.
With this procedure, one can go beyond what was possible with back-chaining. For
example, the puzzle with Alice, Bob, and Carol can now be solved:
?- estsat([[a,b,c],[not(a),b],[a,not(c)]], [a]).
No