The QBF solver AIGSolve. AIGSolve is a rewriting-based solver based on And-Inverter Graphs (AIGs). In this approach, quantifiers are eliminated, starting with the inner-most quantifiers. Intermediate results are represented symbolically using AIGs [22, 23]. The basic method consists of cofactorbased quantifier elimination which is combined with a multitude of optimization approaches including a SATand BDD-based compaction of the representations, methods for preprocessing QBF-formulas based on incremental SAT, heuristics that exchange quantifiers of the same level, heuristics that use BDD-based quantifier elimination as an alternative, as well as structure extraction and structure exploitation for the processed instances
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Pulina, Luca; Seidl, Martina: The 2016 and 2017 QBF solvers evaluations (QBFEVAL’16 and QBFEVAL’17) (2019)
- Peitl, Tomáš; Slivovsky, Friedrich; Szeider, Stefan: Dependency learning for QBF (2017)