Resolve and Expand

We present a novel expansion based decision procedure for quantified boolean formulas (QBF) in conjunctive normal form (CNF). The basic idea is to resolve existentially quantified variables and eliminate universal variables by expansion. This process is continued until the formula becomes propositional and can be solved by any SAT solver. On structured problems our implementation quantor is competitive with state-of-the-art QBF solvers based on DPLL. It is orders of magnitude faster on certain hard to solve instances.

• Type: Conference
• Year: 2004
• Where: SAT
• Authors: Armin Biere
• Keywords: Conjunctive Normal Form, Expansion Based Decision, SAT 2004, State-of-the-art Qbf Solvers