Lösen von abhängigkeitsquantifizierten Booleschen Formeln

• Antragsteller: Professor Dr. Bernd Becker; Professor Dr.-Ing. Christoph Scholl; Dr. Ralf Wimmer
• Fachliche Zuordnung: Rechnerarchitektur, eingebettete und massiv parallele Systeme ; Theoretische Informatik
• Förderung: Förderung von 2015 bis 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 278046454

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ürfenzu 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ängigkeitsquantifiziertenBooleschen 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. Im beantragten Projekt wollen wir Lösungstechniken für DQBF entwickeln und verbessern. 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, werden wir sie auf Probleminstanzen aus verschiedenen Anwendungsdomänen anwenden.

• DFG-Verfahren: Sachbeihilfen