# Boolean Satisfiability

Given a Boolean formula over many variables, how should the variables
be set in order to make the formula true? This is a
fundamental--indeed, the original--NP-complete problem. Many
practical problems, such as planning, circuit synthesis, circuit
verification, and scheduling can be expressed naturally as Boolean
formulas.
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.

## More Information

*Back to Glossary Index*