Lösen von Abhängigkeitsquantifizierten Booleschen Formeln (DQBF)
| Beteiligte Mitarbeiter | Kooperationspartner | Projektbeschreibung | Publikationen
|
Lehrstuhl für Betriebssysteme | |
Aile Ge-Ernst, M.Sc. | |
Christoph Scholl, Prof. Dr. | |
| |
Concept Engineering | |
PD Dr. Ralf Wimmer |
Solver für Erfüllbarkeitsproblem der Aussagenlogik (SAT) werden heute mit großem Erfolg in zahlreichen Bereichen der Informatik und Entwurfsautomatisierung elektronischer Systeme eingesetzt. Beispielsweise haben sie höchste Bedeutung im Bereich der (formalen) Verifikation und den Test von Hard- und Software erlangt. Auch für das Bounded Model Checking (BMC), die automatische Testmustergenerierung (ATPG) und auf dem Gebiet der künstlichen Intelligenz, z. B. für das Planning, werden sie erfolgreich eingesetzt. Obwohl das SAT-Problem NP-vollständig ist, können moderne Solver Formeln mit hunderttausenden von Variablen und Millionen von Klauseln verarbeiten. Daher haben SAT-Solver eine hohe industrielle Relevanz erlangt. Die meisten großen Chiphersteller wenden SAT-basierte Techniken an um Fehler in ihren Hardware-Designs zu finden.
Neben den laufenden Arbeiten zur weiteren Verbesserung der Leistungsfähigkeit von SAT-Solvern, liegt der Fokus der Forschung derzeit auf der Lösung einer Erweiterung des SAT-Problems, den sogenannten quantifizierten booleschen Formeln (QBF). Das QBF-Problem ist härter (PSPACE-vollständig) und dennoch haben moderne Solver enorme Fortschritte bei der Lösung praxisrelevanter Probleme gemacht. Damit eröffnete sich die Möglichkeit viele rechenintensive Probleme anzugehen. Eine Reihe von Problemen kann jedoch nicht auf natürliche Weise in QBFs kodiert werden, sondern erfordert eine weitere Verallgemeinerung. Beispiele sind die Realisierbarkeit unvollständiger digitaler Schaltungen, die Analyse nicht kooperativer Spiele mit unvollständigen Informationen, bestimmte Bitvektorlogiken und die Synthese sicherer Steuerungen. Für eine natürliche und kompakte Formulierung benötigen sie sogenannte Henkin-Quantoren. Dies führt zu den sogenannten dependency quantified Boolean formulas (DQBF). DQBFs ermöglichen es, beliebige Abhängigkeiten von existentiellen Variablen im Quantorenpräfix auszudrücken, während QBF auf lineare Abhängigkeiten beschränkt ist.
Derzeit limitert der Mangel an effizienten DQBF-Solvern die Anwendbarkeit auf praktische Probleme. In diesem Projekt planen wir die Entwicklung und Verbesserung von Lösungstechniken für DQBF. Eine entscheidende Aufgabe ist die Verbesserung der Effizienz mit Hinblick auf Rechenzeit und Speicherverbrauch. Ein weiteres wesentliches Ziel ist es, Solver in die Lage zu versetzen, nicht nur die Erfüllbarkeit einer Formel zu entscheiden, sondern auch Zertifikate für die Erfüllbarkeit in Form von sogenannten Skolem-Funktionen zu berechnen. Diese spielen für viele Anwendungen eine wichtige Rolle, z. B. als Implementierung von Blackboxen in unvollständigen Designs oder als Gewinnstrategie in Spielen. Um die Realisierbarkeit der entwickelten Techniken nachzuweisen, werden wir sie auf Problemfälle aus den verschiedenen Anwendungsbereichen anwenden.
Im Rahmen des Projektes wurde der DQBF-Solver HQS entwickelt. Zum Tool geht es hier.
Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker Equivalence checking of partial designs using dependency quantified Boolean formulae Proceedings of the 31st IEEE International Conference on Computer Design, pages 396–403, IEEE Computer Society Press |
Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, Bernd Becker Solving DQBF Through Quantifier Elimination 2015 Conf. on Design, Automation and Test in Europe |
Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd Becker Preprocessing for DQBF 2015 Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT), Springer-Verlag, issue: 9340, pages: 173 - 190 |
Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker Skolem Functions for DQBF Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA) |
Ralf Wimmer, Sven Reimer, Paolo Marin, Bernd Becker HQSpre – An Effective Preprocessor for QBF and DQBF Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) |
Ralf Wimmer, Karina Wimmer, Christoph Scholl, Bernd Becker Analysis of Incomplete Circuits using Dependency Quantified Boolean Formulas Advanced Logic Synthesis |
Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd Becker From DQBF to QBF by Dependency Elimination Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT) |
Christoph Scholl, Ralf Wimmer Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications Proceedings of 21th International Conference on Theory and Applications of Satisfiability Testing (SAT 2018) |
Christoph Scholl, Jie-Hong Roland Jiang, Ralf Wimmer, Aile Ge-Ernst A PSPACE Subclass of Dependency Quantified Boolean Formulas and Its Effective Solving Proceedings of 33th AAAI Conference on Artificial Intelligence (AAAI-19) |
Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd Becker Dependency Schemes for DQBF 2016 Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT) |