Sciweavers

Share
SAT
2004
Springer

Resolve and Expand

10 years 5 months ago
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.
Armin Biere
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where SAT
Authors Armin Biere
Comments (0)
books