Unit Propagation
e.g. clauses (aBC), (abc),
- set A = upper case, B = lower case
- what unit clause remains?
A = upper gives (BC), (bc)
B = lower case satisfies (bc)
We should set C = upper case
- irrespective of other clauses in the problem
setting one unit clause can create a new one …
- leading to a cascade/chain reaction called unit propagation