Davis Putnam Algorithm for SAT
SAT is QBF with only one layer of existential quantifiers
- we donít need a strategy
- just find assignment satisfying all clauses
Davis Putnam is classic algorithm for SAT
- developed by D/P/Logemann/Loveland in 60ís
- at heart of many modern SAT solvers
- developing applications in model checking
Problems in clause form (=CNF)
- each clause a disjunction of literals
- all clauses must be true