DepQBF: A Dependency-Aware QBF Solver

We present DepQBF 0.1, a new search-based solver for quantified boolean formulae (QBF). It integrates compact dependency graphs to overcome the restrictions imposed by linear quantifier prefixes of QBFs in prenex conjunctive normal form (PCNF). DepQBF 0.1 was placed first in the main track of QBFEVAL'10 in a score-based ranking. We provide a general system overview and describe selected orthogonal features such as restarts and removal of learnt constraints.

• Type: Journal
• Year: 2010
• Where: JSAT
• Authors: Florian Lonsing, Armin Biere
• Keywords: Compact Dependency Graphs, Conjunctive Normal Form, JSAT 2010, Linear Quantifier Prefixes