Davis-Putnam Procedure

Question

My professor gave the following to be applied to clauses when using the Davis-Putnam procedure:

(a)If literal l is in a clause but no occurrence of lc appears in any clause , delete all clauses containing l.

(b)Remove any clause which is subsumed by any other clause.

(c)If a one literal clause, say l is present, delete all clauses containing l and remove each occurrence of lc in any other clause.

(d) If (a) or (c ) cannot be applied, choose a literal l, such that l, lc appear in some clauses and replace the clause set by 2 sets of clauses.

i. The first set formed as in (c).

ii. The set of clauses with all clauses containing lc removed and l removed from all remaining.

I cannot understand the rule (b) and more specifically by what is being met by subsumed.

Thanks

Answer 1

(a) is Pure-literal rule :

Definition Let $S$ be a set of clauses. A pure literal in $S$ is a literal $l$ that appears in at least one clause of $S$, but its complement $l^c$ does not appear in any clause of $S$.

Theorem Let $S$ be a set of clauses and let $l$ be a pure literal in $S$. Let $S'$ be obtained from $S$ by deleting every clause containing $l$. Then $S$ and $S'$ are equisatisfiable [meaning that that $S$ is satisfiable if and only if $S'$ is].

(b) is the Subsumption rule.

Consider two clauses $C, C'$ such that $C \subseteq C'$; then remove $C'$.

We say that clause $C$ subsumes clause $C'$ and that $C'$ is a subsumed clause.

Because a clause is a set of atoms representing a disjunction, we have that e.g. $\{ l \} \subseteq \{ l,k \}$ corresponds to the fact that $l \vDash l \lor k$.

This in turns means that if $\{ l,k \}$ is unsatisfiable also $\{ l \}$ is; thus we can remove the first one, shortening the clause.

(d) is the Splitting rule.

See Chin-Liang Chang & Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press (1973), page 63-64.

Answer 2

A clause $C_1$ subsumes a clause $C_2$ iff $C_1 \subset C_2$

Remember that you are trying to find a truth-value assignment that satisfies each clause, i.e. that sets at least one literal in each clause to true. So if, for example, you have $C_1 = \{ A, B \}$ and $C_2 = \{ A,B,C \}$ in your clause set, then satisfying $C_1$ (i.e. setting one of $A$ and $B$ to true) will automatically satisfy $C_2$. So, there is no sense in worrying about $C_2$: its satisfaction will be guaranteed by satisfying $C_1$. That's why we can remove $C_2$ from the clause set: the original clause set is satisfiable if and only if the clause set with $C_2$ removed is satisfiable.

Thus, in general, we can remove any subsumed clauses.