The QBF-Solver AIGSolve

| Beteiligte Mitarbeiter | Projektbeschreibung | Software | Beschreibung | Publikationen |

Here we investigate solving principles for so-called Quantified Boolean Formulas (QBF).
The goal is to decide whether a QBF is satisfiable or not.
Quantified Boolean Formulas are a powerful generalization of satisfiability formulas (SAT).
In contrast to SAT, QBF allows existentially as well as universally quantified variables,
which allows for exponentially more compact representations of many problems compared to SAT,
but comes at the price of raising the decision complexity from NP-complete to PSPACE-complete.

Many real world problems from various application domains, such as formal verification and artificial intelligence, can be compactly formulated as QBF, including the verification of incomplete circuit designs, conditional planning, and nonmonotonic reasoning problems.

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.
The basic method consists of cofactor-based quantifier elimination which is
combined with a multitude of optimization approaches including a SAT- and
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.

Click here for downloading the QBF solver AIGSolve.

This is a gzipped version of the binaries aigsolve which are compiled and statically linked under Ubuntu Linux 14.04.4 (64 bit).

The AIGSolve tool is free for non-commercial applications in academia only.

AIGSolve runs on benchmarks in QDIMACS format.
Benchmarks are available for download at qbflib.org.