Quaig

Beteiligte Mitarbeiter
Lehrstuhl für Rechnerarchitektur
Sven Reimer, Dipl. Inf.	Entwickler / Kontakt
Lehrstuhl für Betriebssysteme
Florian Pigorsch, Dipl.-Inf.	Entwickler

Beschreibung

Quaig ist ein Tool zur Validierung von quantifizierten booleschen Formeln (QBF). Es kombiniert zwei orthogonale State of the Art Algorithmen - Quantorenelimination (AIGSolve) und suchbasierte Verfahren (QuBE). Dafür wird die Qualität des Restproblems beim laufenden Eliminierungsverfahrens abgeschätzt - das beste aktuelle Teilergebnis wird jeweils abgespeichert. Weiterhin wird die Qualität des Eliminierungsverfahrens an sich abgeschätzt (Laufzeit der Eliminierungsschritte, Größe der zu Grunde liegenden AIG Datenstruktur) und bei Bedarf zum suchbasierten Verfahren gewechselt. Das gelernte Teilergebnisse aus der Eliminierung kann dann im suchbasierten Ansatz weiterverwendet werden.

Benchmarks

Jede beliebige QBF in QDimacs Format. Eine Sammlung von QBF Problemen ist in der QBFLIB zu finden.

Publikationen

Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd Becker
Integration of Orthogonal QBF Solving Techniques
Design, Automation and Test in Europe (DATE), 2011