Lösen von Abhängigkeitsquantifizierten Booleschen Formeln (DQBF)

| Beteiligte Mitarbeiter | Kooperationspartner | Projektbeschreibung | Publikationen |

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.