The CNF Saturation Procedure

The basic CNF saturation procedure is :
While a refutation has not been found
    Copy two clauses from the set
    Generate all logical consequences, e.g., by resolution
    Put logical consequences into the set
Note the "Copy", indicating that a clause may be used multiple times with a new set of variables each time.

Example
S = { wise(jim),
      ~wise(X) | wise(brother_of(X)),
      ~wise(brother_of(brother_of(jim))) }

~wise(X) | wise(brother_of(X)) + ~wise(brother_of(brother_of(jim)))
» ~wise(brother_of(jim))
~wise(brother_of(jim)) + ~wise(X) | wise(brother_of(X))
» ~wise(jim)
wise(jim) + ~wise(jim)
» FALSE

Example
S = { p(f(X)) | q(Y),
      ~p(X) | q(dog),
      p(f(dog)) | ~q(X),
      ~p(f(Z)) }
p(f(X)) | q(Y) + ~p(X) | q(dog) » q(dog) | q(Y)
p(f(dog)) | ~q(X) + ~p(f(Z)) » ~q(X)
q(dog) | q(Y) + ~q(X) » FALSE

Example
Axioms
∀M1,M2 (member(M1) & member(M2) & shaved(M1,M2)) => all_shaved(M1)
member(guido)
member(lorenzo)
member(petrucio)
member(cesare)
shaved(guido,cesare)
∀M1 ( all_shaved(M1) <=> ( member(M1) & ∀M2 (member(M2) => shaved(M2,M1)) ) )

Conjecture
shaved(petrucio,lorenzo)

Axioms U {~C} Converted to CNF
all_shaved(A) | ~member(B) | ~member(A) | ~shaved(A,B)
member(guido)
member(lorenzo)
member(petrucio)
member(cesare)
shaved(guido,cesare)
member(A) | ~all_shaved(A)
shaved(B,A) | ~all_shaved(A) | ~member(B)
all_shaved(A) | member(sk1(A)) | ~member(A)
all_shaved(A) | ~member(A) | ~shaved(sk1(A),A)
~shaved(petrucio,lorenzo)
Refutation
member(cesare) + all_shaved(A) | ~member(B) | ~member(A) | ~shaved(A,B)
» all_shaved(A) | ~member(A) | ~shaved(A,cesare)
member(guido) + all_shaved(A) | ~member(A) | ~shaved(A,cesare)
» all_shaved(guido) | ~shaved(guido,cesare)
shaved(guido,cesare) + all_shaved(guido) | ~shaved(guido,cesare)
» all_shaved(guido)
member(lorenzo) + shaved(B,A) | ~all_shaved(A) | ~member(B)
» shaved(lorenzo,A) | ~all_shaved(A)
all_shaved(guido) + shaved(lorenzo,A) | ~all_shaved(A)
» shaved(lorenzo,guido)
member(guido) + all_shaved(A) | ~member(B) | ~member(A) | ~shaved(A,B)
» all_shaved(A) | ~member(A) | ~shaved(A,guido)
member(lorenzo) + all_shaved(A) | ~member(A) | ~shaved(A,guido)
» all_shaved(lorenzo) | ~shaved(lorenzo,guido)
shaved(lorenzo,guido) + all_shaved(lorenzo) | ~shaved(lorenzo,guido)
» all_shaved(lorenzo)
member(petrucio) + shaved(B,A) | ~all_shaved(A) | ~member(B)
» shaved(petrucio,A) | ~all_shaved(A)
all_shaved(lorenzo) + shaved(petrucio,A) | ~all_shaved(A)
» shaved(petrucio,lorenzo)
~shaved(petrucio,lorenzo) + shaved(petrucio,lorenzo)
» FALSE

Example
A = { ∀X (p(X) => (q(X) | r(X))),
      p(a) | p(b),
      ∀Y ~q(Y) }

C = ∃X r(X)

Full resolution is refutation complete for general clauses [Robinson 1965], and binary resolution is refutation complete for Horn clauses [Henschen & Wos 1974]. This means that if the input set is unsatisfiable, then the empty clause can always be derived in this manner, given infinite time and memory (i.e., resolution is theoretically refutation complete, practically incomplete). Such a deduction is called a refutation. If the input set is satisfiable, the CNF saturation procedure may continue for ever.

Example (showing that binary resolution is not refutation complete)
S = { p(X) | q(Y) | q(X)
      ~q(a) | ~q(Z),
      ~p(a) }

Full resolution
p(X) | q(Y) | q(X) + ~q(a) | ~q(Z) » p(a)
~p(a) + p(a) » FALSE
Binary resolution
Try it, and fail


Proof Trees

A refutation can be represented as a proof tree.

Example
S2 = { ~p(X) | q(X) | r(X),
       p(a) | p(b),
       ~q(Y),
       ~r(a),
       ~r(b) }
~p(X) | q(X) | r(X) + ~q(Y) » ~p(X) | r(X)
~p(X) | r(X) + ~r(a) » ~p(a)
+ ~r(b) » ~p(b)
~p(a) + p(a) | p(b) » p(b)
p(b) + ~p(b) » FALSE

This refutation has the proof tree :

Notice that the clause ~p(X) | r(X) is used twice in the proof tree but is generated only once by resolution.



Failure Trees

A failure tree for an unsatisfiable set of clauses is a minimal finite subtree of the semantic tree of the Herbrand base, such that for each branch there is a clause that is FALSE in the sub-interpretation identified by that branch. FALSE has a single node as its failure tree.

Example
S = { wise(jim),
      ~wise(X) | wise(brother_of(X)),
      ~wise(brother_of(brother_of(jim))) }

This unsatisfiable clause set has the failure tree :

Example
S = { p(a) | q(X),
      ~p(Y) | q(f(Y)),
      p(a) | ~q(T),
      ~p(A) | ~q(W) }

A (Herbrand) unsatisfiable set of clauses has a failure tree

Proof

If a set of clauses is (Herbrand) unsatisfiable then for each branch of the semantic tree of the Herbrand base, i.e., for each Herbrand interpretation, there exists a clause in the set which has a ground instance that is FALSE in the Herbrand interpretation identified by that branch.

As there are only a finite number of literals in each clause, each branch has a smallest sub-branch such that the truth value of the corresponding clause instance is determined by the sub-interpretation identified by the sub-branch. The leaf of such a sub-branch is called a failure node for the clause. The sub-branches define a finite sub-tree of the semantic tree. Prune any descendants of failure nodes to form a minimal sub-tree, i.e. a failure tree.

Failures trees are used in the proofs of Herbrand's theorem and the completeness of resolution.


Refutation Completeness

The CNF saturation procedure is refutation complete

Proof

For a set of clauses S, let R(S) mean S U {all resolvants from S}, and Rn(S) mean R applied n times. If S is (Herbrand) unsatisfiable, then it needs to be shown that there exists n such that FALSE is an element of Rn(S).

If S is unsatisfiable, then it has a failure tree. If the tree is trivial, then FALSE is an element of S. Otherwise:

  • Pick a failure node Y of maximum depth in the failure tree. Let X be the parent of Y. X is not a failure node as a failure tree is minimal. Let Z be the other offspring, which must also be a failure node as Y is of maximum depth.
  • Let K be the Herbrand base element whose truth value is determined by the arcs X-Y (FALSE) and X-Z (TRUE).
  • As Y and Z are failure nodes, there exist clauses that are FALSE at Y and Z respectively. Since both these clauses are TRUE at X (X is not a failure node) the clauses must be of the forms C| | L1 |...| Ln and D| | ~M1 |...| ~Mn, such that they have ground instances (C| | L1 |...| Ln and (D| | ~M1 |...| ~Mn, and Liθ = Mjσ = K.
  • Then there is a resolvant (C| | D| of the clauses. (C| | D|)θσ is an instance of (C| | D| All literals of (C| | D|)θσ are FALSE at some highest node F above Y and Z. This node is a failure node for (C| | D|. The failure tree for S U {(C| | D|)γ} is thus smaller than that for S.
  • If S is unsatisfiable, then S U {(C| | D|)γ} is unsatisfiable (simply because S is unsatisfiable), so the process can be iterated. As the failure tree keeps getting smaller, it must eventually become the trivial tree. FALSE has then been inferred.
Example
The failure tree for:
S = { wise(jim),
      ~wise(X) | wise(brother_of(X)),
      ~wise(brother_of(brother_of(jim))) }
is

  • X, Y and Z are as indicated. K = wise(brother_of(brother_of(jim)))
  • The clause that is FALSE at Y is ~wise(X) | wise(brother_of(X)), and the clause that is FALSE at Z is ~wise(brother_of(brother_of(jim)))
  • With θ = {X/brother_of(jim)} and σ = {}, the ground instances of these clauses are ~wise(brother_of(jim)) | wise(brother_of(brother_of(jim))) and ~wise(brother_of(brother_of(jim))).
  • With γ = {X/brother_of(jim)} the resolvant of these clauses is ~wise(brother_of(jim)), which is FALSE at the node F.

The failure tree for

S = { wise(jim),
      ~wise(X) | wise(brother_of(X)),
      ~wise(brother_of(brother_of(jim))),
      ~wise(brother_of(jim)) }
is


The Quest for Logical Consequence

To show that C is a logical consequence of Ax, it is sufficient to: The CNF saturation procedure is refutation complete, so


Exam Style Questions

  1. Write out the basic CNF saturation procedure algorithm.
  2. What things could happen if the basic CNF saturation procedure algorithm is run on an unsatisfiable set of clauses?
  3. What things could happen if the basic CNF saturation procedure algorithm is run on a satisfiable set of clauses?
  4. In what circumstances does the basic CNF saturation procedure algorithm retain refutation completeness when using only binary resolution?
  5. Draw the proof tree for the following refutation:
    ~p(X) | q(X) | r(X) + ~q(Y) » ~p(X) | r(X)
    ~p(X) | r(X) + ~r(a) » ~p(a)
    + ~r(b) » ~p(b)
    ~p(a) + p(a) | p(b) » p(b)
    p(b) + ~p(b) » FALSE
  6. What is an axiomatic proof?
  7. Draw the failure tree for the following set of clauses:
         S = { p(f(X)) | q(Y),
               ~p(X) | q(dog),
               p(f(dog)) | ~q(X),
               ~p(f(Z)) }
         
  8. Prove that a Herbrand unsatisfiable set of clauses has a failure tree.
  9. Prove that the CNF saturation procedure is refutation complete.