Submitter: Florian Pigorsch
Description: Devised by F. Pigorsch and C. Scholl, it uses And-Inverter Graphs (AIGs) as the main data structure, and AIG-based operations to reason about the input formula. The solver includes preliminary phases devoted to simplification, structure extraction and early quantification of the input formula.
Details are available in
Pigorsch, F., Scholl, C.: Exploiting structure in an AIG based QBF solver. In: Design, Automation and Test in Europe (DATE 2009), IEEE (2009) 15961601