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.

• Type: Conference
• Year: 2009
• Where: DATE
• Authors: Florian Pigorsch, Christoph Scholl
• Keywords: AIG Based Representation, DATE 2009, Hardware, Non-linear Quantifier Structures, Qbf Solvers