Depth First + Unit Propagation
Unit propagation is vital in SAT
Whenever there is a not-yet-satisfied unit clause
- set the corresponding variable to True if literal positive
- false if literal negative
Use this to override all other heuristics
Later in lecture will think about other heuristics to use as well
Next we will look at another algorithm