Unit Propagation

logic computation sat-solving

Definition

Unit Propagation

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

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

1. Remove from every clause of the form .
2. Replace in every clause of the form by the clause .

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

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

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

Examples

Iterated unit propagation

Consider the formula

The clause is a unit clause, so we assign :

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

Deriving a contradiction

Consider the set of clauses

The literal is a unit clause, so we apply the transformation with :

• remove the clause ;
• replace by .

This gives

Now is a unit clause, so we apply the transformation with :

• remove the clause ;
• replace by the empty clause.

This gives

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