Unit propagation

Unit resolution (English unit propagation ) is to simplify a procedure to a set of clauses in mathematical logic. To apply a unit resolution, a unit clause must be included in the given set of clauses, that is, a clause consisting only of a single literal. A literal is a variable or its negation, which stands alone in a clause. Unit resolution is used among others by the DPLL algorithm and is an important component of many SAT solvers.

Method

Be given a unit clause in the set of clauses. Then you simplify other clauses from the given set of clauses by two rules:

Example

Given the following set of clauses:

In this set of clauses is a unit clause. If the clause contained in the set of clauses, then this would also be a unit clause. These clauses can be simplified by applying these two rules, the unit clause. The result is the set of clauses:

All clauses that contained, have been completely removed from the set of clauses. These were the clauses and. In addition, the literal has been removed from all clauses. This was done in the remaining two clauses and.