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

Quaig

| Beteiligte Mitarbeiter | Beschreibung | Benchmarks | Publikationen |


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