Unit propagation (UP) or boolean constraint propagation (BCP) or the one-literal rule (OLR) is a procedure of automated theorem proving that can simplify a set of (usually propositional) clauses.
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").
As for resolution, unit propagation is a correct inference rule, in that it never produces a new clause that was not entailed by the old ones.
The differences between unit propagation and resolution are: Resolution calculi that include subsumption can model rule one by subsumption and rule two by a unit resolution step, followed by subsumption.
Unit propagation, applied repeatedly as new unit clauses are generated, is a complete satisfiability algorithm for sets of propositional Horn clauses; it also generates a minimal model for the set if satisfiable: see Horn-satisfiability.
The unit clauses that are present in a set of clauses or can be derived from it can be stored in form of a partial model (this partial model may also contain other literals, depending on the application).
In this case, unit propagation is performed based on the literals of the partial model, and unit clauses are removed if their literal is in the model.
The resulting set of clauses is equivalent to the original one under the assumption of validity of the literals in the partial model.
The direct implementation of unit propagation takes time quadratic in the total size of the set to check, which is defined to be the sum of the size of all clauses, where the size of each clause is the number of literals it contains.
Unit propagation can however be done in linear time by storing, for each variable, the list of clauses in which each literal is contained.
For example, the set above can be represented by numbering each clause as follows: and then storing, for each variable, the list of clauses containing the variable or its negation: This simple data structure can be built in time linear in the size of the set, and allows finding all clauses containing a variable very easily.
More precisely, the total running time for doing unit propagation for all unit clauses is linear in the size of the set of clauses.