SAT solving
Unit propagation
Assigning the only remaining value that can keep a clause true.
Definition
Unit propagation
Unit propagation forces a literal when every other literal in its clause is already false.
The forced value can make other clauses unit, so propagation repeats until no unit clause remains or a conflict appears. CDCL records the clause responsible for each propagated value.
01
Example
If a is false in the clause a or b, unit propagation forces b to true.
02
Important distinction
Propagation derives forced values from clauses. A search decision chooses a value that the current clauses have not forced.
After reading this article, you should be able to
- Define Unit propagation in the sense used on this site.
- Carry out repeated unit propagation on a small set of clauses.