Unit Propagation
One heuristic in SAT is vital to success
When we have a unit clause …
- e.g. +A
- we must set A = true
- if we set A = false the clause is unsatisfied, so is the whole problem
A unit clause might be in the original problem
or contain only one unset variable after simplification
- e.g. clauses (aBC), (abc),
- set A = upper case, B = lower case
- what unit clause remains?