Lösen von abhängigkeitsquantifizierten Booleschen Formeln

| Beteiligte Mitarbeiter | Projektbeschreibung |

Algorithmen für Boolesche Erfüllbarkeitsprobleme (SAT) werden heutzutage in zahlreichen Anwendungsgebieten der Informatik und der elektronischen Entwurfsautomatisierung mit großem Erfolg eingesetzt. Sie sind, um nur einige wenige zu erwähnen, von höchster Relevanz in der formalen Verifikation und im Test von Hard- und Software, z. B. beim Bounded Model Checking (BMC) und bei der automatischen
Testmustergenerierung (ATPG). Sie werden jedoch auch im Bereich der künstlichen Intelligenz, z. B. im Planen, eingesetzt. Obwohl
das Problem NP-vollständig ist, können moderne Algorithmen mit Formeln umgehen, die aus Hunderttausenden von Variablen und Millionen von Klauseln bestehen. Aus diesem Grund haben SAT-Verfahren große industrielle Relevanz erlangt; so verwenden die meisten bedeutenden Chiphersteller  SAT-basierte Techniken, um Fehler in ihren Hardwareentwürfen zu finden.

Neben Arbeiten zur weiteren Verbesserung der SAT-Verfahren konzentriert sich die aktuelle Forschung auf eine Erweiterung des SAT-Problems, sogenannte quantifizierte Boolesche Formeln (QBF). Die Lösung von QBF ist noch komplexer (das Problem ist PSPACE-vollständig); trotzdem haben moderne Lösungsverfahren enorme Fortschritte bei der Lösung praktisch relevanter Probleme gemacht, und hierdurch eine ernsthafte Möglichkeit geschaffen, um viele schwierige Probleme zu lösen.

Eine Reihe von Problemen kann jedoch nicht auf natürliche Art und Weise als QBF codiert werden, sondern benötigt eine Verallgemeinerung davon. Beispiele sind die Realisierbarkeit von unvollständigen digitalen Schaltungen, die Analyse von nicht-kooperativen Spielen mit unvollständiger Information, bestimmte Bitvektor-Logiken und die Synthese sicherer Controller. Für eine natürliche und kompakte Formulierung benötigen sie sogenannte Henkin-Quantoren, die zu abhängigkeitsquantifizierten Booleschen Formeln (DQBF) führen. Mit DQBFs lassen sich beliebige Abhängigkeiten der existentiellen Variablen im Quantorenpräfix ausdrücken, während QBF auf lineare Abhängigkeiten beschränkt ist.

Momentan schränkt der Mangel an effizienten DQBF-Verfahren deren Anwendbarkeit auf praktische Probleme stark ein. In diesem Projekt entwickeln und verbessern wir Lösungstechniken für DQBF. Eine zentrale Aufgabe ist es, deren Effizienz bzgl. Berechnungsaufwand und Speicherbedarf zu verbessern. Darüber hinaus ist es von besonderer Bedeutung, die Lösungsverfahren so zu erweitern, dass sie nicht nur die Erfüllbarkeit einer Formel entscheiden, sondern auch Zertifikate für die Erfüllbarkeit in Form von sogenannten Skolem-Funktionen berechnen. Skolem-Funktionen spielen eine bedeutende Rolle z. B. als Implementierung fehlender Schaltkreisteile in unvollständigen Schaltungen oder als Gewinnstrategien in Spielen. Um die Machbarkeit der entwickelten Techniken zu demonstrieren, wenden wir sie auf
Probleminstanzen aus verschiedenen Anwendungsdomänen an.