Unit propagation

Unit propagation (UP) or Boolean Constraint propagation or the one-literal rule (OLR) is a procedure of automated theorem proving that can simplify a set of (usually propositional) clauses.

The procedure is based on unit clauses, i.e. clauses that are composed of a single literal. Because each clause needs to be satisfied, we know that this literal must be true. If a set of clauses contains the unit clause ${\displaystyle l}$, the other clauses are simplified by the application of the two following rules:

The application of these two rules lead to a new set of clauses that is equivalent to the old one.

For example, the following set of clauses can be simplified by unit propagation because it contains the unit clause ${\displaystyle a}$.

Since ${\displaystyle a\vee b}$ contains the literal ${\displaystyle a}$, this clause can be removed altogether. Since ${\displaystyle \neg a\vee c}$ contains the negation of the literal in the unit clause, this literal can be removed from the clause. The unit clause ${\displaystyle a}$ is not removed; this would make the resulting set not equivalent to the original one; this clause can be removed if already stored in some other form (see section "Using a partial model"). The effect of unit propagation can be summarized as follows.

...
Wikipedia