Information Technology Reference
In-Depth Information
to compute whether a certain set of sentences (formed by adding the negation of
S
to
the other
S
i
) is satisfiable or not.
But how does one test for satisfiability? For a set of dclauses without variables,
there is a very simple account of satisfiability:
A set of dclauses (without variables) is satisfiable if and only if there is a way to pick
a literal from each dclause without picking both an atom and its negation.
This derives from the fact that a disjunction will be true if one of the disjuncts is true
(that is, the literal chosen for that dclause), and a conjunction will be true if all of the
conjuncts are true (that is, all the dclauses are true). So, for example, the CNF formula
[ [p], [not(p),not(q)], [not(q)] ]
is satisfiable: pick
p
from the first dclause,
not(q)
from the second, and
not(q)
(already picked) from the third. This means that the dclauses can all be true: it
happens when
p
is true and
q
is false.
However, the CNF formula
[ [p], [not(p),not(q)], [q] ]
is unsatisfiable: pick
p
from the first dclause, which forces the choice of
not(q)
from
the second (to avoid having an atom and its negation), and then there is nothing to
pick from the third. (In other words, the first two dclauses logically entail
not(q)
.)
Similarly, the CNF formula
[ [p,q], [not(p),q], [not(q),p], [not(p),not(q)] ]
is unsatisfiable: no matter what is chosen for the first three dclauses, both
p
and
q
are
picked, with nothing left to choose from the last one. (In other words, the first three
dclauses logically entail both
p
and
q
.)
11.4.3 Computing satisfiability
A predicate for testing whether a list of dclauses (without variables) is satisfiable is
presented in figure 11.13. It uses the predicate
satpick
to go though the dclauses,
picking a literal from each one using the predicate
pickone
. For each dclause, there
are three possibilities (and so three clauses for the
pickone
predicate):
No new picking is needed if the head of the dclause has already been picked.
The head of the dclause can be picked if its negation has not been picked.
A literal from the tail of the dclause can also be picked.
