As with any NP-complete problem, solution techniques are based on search. Systematic search techniques (e.g., the Davis-Putnam algorithm), which guarantee that a solution will be found if one exists, are effective only for small problems. But in recent years, surprisingly difficult formulas have been solved by WALKSAT [Selman, Kautz and Cohen 1994], a simple local search method. WALKSAT works by mixing greedy hillclimbing-like moves with sideways and non-improving moves.
In the AUTON lab, the STAGE and COMIT optimization projects have both studied Boolean satisfiability as a testbed domain.