Uni-Logo
English       Login
Professur für Betriebssysteme
        Startseite         |         Institut für Informatik         |         Technische Fakultät
 

The QBF-Solver AIGSolve

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


Beteiligte Mitarbeiter

Lehrstuhl für Betriebssysteme
Christoph Scholl, Prof. Dr.
Florian Pigorsch, Dipl.-Inf.


Projektbeschreibung

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.



Software

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.



Beschreibung

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



Publikationen
Florian Pigorsch, Dipl.-Inf., Christoph Scholl, Prof. Dr.
Exploiting structure in an AIG based QBF solver.
Design, Automation & Test in Europe (DATE) 2009
Florian Pigorsch, Dipl.-Inf., Christoph Scholl, Prof. Dr.
An AIG-based QBF-solver using SAT for preprocessing.
Design Automation Conference (DAC) 2010