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