Exploiting structure in an AIG based QBF solver

10 years 2 months ago
Exploiting structure in an AIG based QBF solver
—In this paper we present a procedure for solving quantified boolean formulas (QBF), which uses And-Inverter Graphs (AIGs) as the core data-structure. We make extensive use of structural information extracted from the input formula such as functional definitions of variables and non-linear quantifier structures. We show how this information can directly be exploited by the symbolic, AIG based representation. We implemented a prototype QBF solver based on our ideas and performed a number of experiments proving the effectiveness of our approach, and moreover, showing that our method is able to solve QBF instances on which state-of-the-art QBF solvers known from literature fail.
Florian Pigorsch, Christoph Scholl
Added 20 May 2010
Updated 20 May 2010
Type Conference
Year 2009
Where DATE
Authors Florian Pigorsch, Christoph Scholl
Comments (0)