Satisfiability Testing Procedures
Systematic, complete procedures
Depth-first backtrack search (Davis, Putnam, & Loveland 1961)
unit propagation, shortest clause heuristic
State-of-the-art implementation: ntab (Crawford & Auton 1997)
and many others! See SATLIB 1998 / Hoos & Stutzle.
Stochastic, incomplete procedures
GSAT (Selman et. al 1993)
Current fastest: Walksat (Selman & Kautz 1993)
greedy local search + noise to escape local minima