Variablenabhängigkeiten Quantifizierter Boolescher Formeln

Kurzfassung. Zahlreiche schwere algorithmische Probleme, die im Bereich der formalen Verifikation von Hard- und Software oder bei der automatischen Lösung von Planungsaufgaben auftreten, können effizient in das Erfüllbarkeitsproblem Quantifizierter Boolscher Formeln (QBF) übersetzt werden. Dieses Projekt erforscht neue Methoden zur Nutzung von Unabhängigkeit zwischen Variablen für QBF. Durch die Verschachtelung von Existenz- und Allquantoren in quantifizerten Boolschen Formeln können Abhängigkeiten zwischen Variablen entstehen, die das Übertragen erfolgreicher Technikenzur LösungdesErfüllbarkeitsproblems aussagenlogischer Formeln (SAT) auf QBF erschweren. In manchen Fällen kann sich eine vermeintliche Abhängigkeit als rein syntaktisch entpuppen und festgestellt werden, dass die entsprechenden Variablen in Wirklichkeit voneinander unabhängig sind. Diese Information kann wiederum dazu genutzt werden, Entscheidungsprozeduren für QBF zu beschleunigen. Im Allgemeinen kann allerdings nicht effizient entschieden werden, ob Variablen einer quantifizierten Boolschen Formel voneinander unabhängig sind oder nicht. Dieses Forschungsprojekt verfolgt drei Ziele: (A) die Weiterentwicklung existierender Techniken zur Ermittlung von Unabhängigkeit zwischen Variablen durch das Erforschen deren theoretischer Grundlagen sowie durch die Entwicklung verbesserter Algorithmen; (B) die Entdeckung neuer Verfahren zur Ermittlung und Nutzung von Unabhängigkeit zwischen Variablen; (C) die Verallgemeinerung dieser Methoden auf Probleme jenseits von QBF.

Die Kombination einer allgemeinen logischen Sprache zur Modellierung kombinatorischer Problememiteffizienten Lösungsverfahren bietet Vorteile gegenüberder problemspezifischen Entwicklung von Algorithmen. Nutzer können ihr Problem mit geringem Aufwand in einer geeigneten Sprache ausdrücken und profitieren automatisch von Fortschritten bei den Lösungsverfahren. Umgekehrt erhalten deren Entwickler durch neue Anwendungen Impulse zur Verbesserung ihrer Algorithmen. Ein Beispiel für derartige Synergien bietet das Erfüllbarkeitsproblem der Aussagenlogik (SAT). SAT-Solver sind im Laufe der vergangenen Jahre so effizient geworden, dass zahlreiche Probleme in der Praxis durch Übersetzung in SAT gelöst werden können. In manchen Fallen wächst der Speicherbedarf exponentiell mit der Problemgröße, sodass eine effiziente Übersetzung nur für kleine Eingaben möglich ist. Die quantifizierte Aussagenlogik (engl. Quantified Boolean Formulas, kurz QBF) ist eine Erweiterung der Aussagenlogik, in der solche Probleme immer noch prägnant ausgedrückt werden können. Ziel des Projekts war die Entwicklung effizienterer Lösungsverfahren für das Erfüllbarkeitsproblem von QBFs.Durch die Schachtelung von All- und Existenzquantoren in einer QBF entstehen Abhängigkeiten zwischen Variablen: der Wert einer Variablen muss abhängig vom Wert einer anderen Variablen gewählt werden. Bei der Lösung von Formeln müssen solche Abhängigkeiten berücksichtigt werden, was allerdings die Effizienz von Algorithmen reduziert. Der Begriff Abhängigkeitsanalyse bezeichnet eine Reihe von Verfahren, die die Vereinfachung bzw. Vermeidung von Abhängigkeiten zum Ziel hat. Im Rahmen des Projekts wurden neue Techniken zur Abhängigkeitsanalyse entwickelt. Eine davon ist das Dependency Learning, bei dem potentielle Abhängigkeiten von einem QBF-Solver während der Laufzeit aufgespürt werden. Dadurch lassen sich viele Abhängigkeiten auflösen, die durch rein syntaktische Inspektion einer QBF als problematisch eingestuft würden. Gleichzeitig bleiben viele wünschenswerte Eigenschaften des Lösungsverfahrens erhalten, die durch den Einsatz von Standardtechniken verlorengehen. Dependency Learning wurde in einem System mit dem Namen QUTE implementiert, das sich im Rahmen eines jährlich stattfindenden Wettbewerbs mittlerweile als einer der besten QBF-Solver etabliert hat.