Unit Propagation

logic computation sat-solving

Definition

Unit Propagation

Let $S$ be a set of clauses. Unit propagation is the repeated application of the following transformation.

If $S$ contains a unit clause, that is, a clause consisting of a single literal $L$, then:

1. Remove from $S$ every clause of the form $L\vee C$.
2. Replace in $S$ every clause of the form $\neg L\vee C$ by the clause $C$.

The process continues until no unit clause remains. At that point one of three situations holds:

• $S$ is empty: every clause was satisfied, so the original set is satisfiable.
• $S$ contains the empty clause $\square$: a contradiction was derived, so the original set is unsatisfiable.
• $S$ contains non-unit clauses only: no further simplification is possible without choosing a literal to branch on.

Intuitively, $L$ must be true, so every clause containing $L$ is already satisfied and can be discarded, while $\neg L$ is false and can be deleted from every clause that contains it.

Examples

Iterated unit propagation

Consider the formula

$$F=(\neg a\vee \neg b\vee c)\wedge (\neg b\vee \neg c\vee u)\wedge (\neg u\vee b)\wedge u$$

The clause $u$ is a unit clause, so we assign $u=\top$:

$$\begin{array}{rl}\text{I.:}& (\neg a\vee \neg b\vee c)\wedge \cancel{(\neg b\vee \neg c\vee u)}\wedge (\cancel{\neg u}\vee b)\wedge u\\ \text{II.:}& (\neg a\vee \cancel{\neg b}\vee c)\wedge b\wedge u\\ \text{III.:}& (\neg a\vee c)\wedge b\wedge u\end{array}$$

In step I, $u$ is assigned true, eliminating the clause containing $u$ and removing $\neg u$ from the third clause. In step II, this creates a new unit clause $b$, which propagates to yield the simplified formula III.

Deriving a contradiction

Consider the set of clauses

$$S=\{p,\neg p\vee q,\neg q\}.$$

The literal $p$ is a unit clause, so we apply the transformation with $L=p$:

• remove the clause $p$;
• replace $\neg p\vee q$ by $q$.

This gives

$$S^{\prime }=\{q,\neg q\}.$$

Now $q$ is a unit clause, so we apply the transformation with $L=q$:

• remove the clause $q$;
• replace $\neg q$ by the empty clause.

This gives

$$S^{\prime \prime }=\{\square \}.$$

The empty clause is unsatisfiable. Hence the original set $S$ is unsatisfiable, and unit propagation has established this without any guessing.