Conclusions
Unit propagation vital to SAT
Davis Putnam (DP/DLL/DPLL) successful
- = depth first + unit propagation
Need heuristics, especially variable ordering
Three design principles help
Not yet clear which is the best
Heuristic design is still a black art