[ Please note: The project has been discontinued as of May 31, 2005 and is superseded by the projects of the ii Labs. There won't be further updates to these pages. ]

(Related publication: [PUBLink])

The problem of propositional satisfiability (SAT) is to decide whether a propositional formula is satisfiable or not. A propositional formula consists of two-valued variables (true and false) that are related via the operators not, and and or. Most solvers require that the problem be stated as a conjunctive normal form (a conjunction of disjunctions).

SAT-solving techniques include refinement approaches like the Davis-Putnam procedure [PUBLink] and Satz-Rand [PUBLink], as well as local-search methods like GSAT [PUBLink] [PUBLink], Walksat [PUBLink], HSAT [PUBLink], Novelty [PUBLink] and SDF [PUBLink]. Most of the SAT-based planning applications are based on the problem encodings of Kautz and Selman [PUBLink].

For questions, comments or suggestions, please contact us.

Last update:
May 19, 2001 by Alexander Nareyek