SAT Solvers
Stochastic local search solvers (walksat)
when they work, scale well
cannot show unsat
fail on certain domains
must use very simple (fast) heuristics
Systematic solvers (Davis Putnam Loveland style)
complete
fail on (often different) domains
might use more sophisticated (costly) heuristics
often to scale badly
Can we combine best features of each approach?