Information Technology Reference
In-Depth Information
Figure 11.15.
An unsatisfiability program
unsat.pl
% Dclauses in DL are unsat, after making N copies of them.
unsat(N,DL) :- copies(N,DL,DL2), nopick(DL2,[]).
% copies(N,X,Y): Y is the result of making N copies of list X.
copies(0,_,[]).
copies(N,X,Y) :-
N>0, N1 is N-1, copies(N1,X,L), copy_term(X,X2), append(X2,L,Y).
% nopick(DL,P): there is no way to pick literals from the
% dclauses in DL, given that the ones in P have been picked.
nopick([[]|_],_).
nopick([[L|D]|T],P) :- unpickable(L,T,P), nopick([D|T],P).
% The literal L cannot be picked.
unpickable(L,_,P) :- member_neg(L,P).
% Negation of L is picked.
unpickable(L,T,P) :- nopick(T,[L|P]).
% Cannot add L to picked.
% As before
member_neg(A,P) :- member(not(A),P).
member_neg(not(A),P) :- member(A,P).
%------------------------------------------------------------------
% Dclauses DL entails Q using unsat.
estunsat(N,DL,Q) :- negs(Q,NQ), unsat(N,[NQ|DL]).
% As before
negs([],[]).
negs([not(A)|T],[A|NT]) :- negs(T,NT).
negs([A|T],[not(A)|NT]) :- \+ A=not(_), negs(T,NT).
there is no literal to choose when
X
is
a
. (Specifically, the CNF formula without
variables,
[[not(p(a))],[not(q(a))],[p(a),q(a)]]
, is unsatisfiable according to
what was done before.) One complication here is that
more than one value
per vari-
able may have to be considered to handle cases like the following: the formula
[[not(p(a)),not(p(b))],[p(X)],[p(Y)]]
is unsatisfiable (when
X
is
a
and
Y
is
b
),
and so
[[not(p(a)),not(p(b))],[p(X)]]
is unsatisfiable too.
This suggests that for first-order reasoning it is easier to work with unsatisfiability
than with satisfiability:
A set of dclauses (with variables) is unsatisfiable if and only if there are (possibly
multiple) values for the variables such that the resulting set of dclauses without
variables is not satisfiable.
A program that realizes this definition appears in figure 11.15. To deal with the multi-
ple values for variables, it begins by making
copies
of all the dclauses using the built-in
