Von QBF zu DQBF: Theorie zusammen mit Praxis

Mathematische und rechnerische Optimierung spielt heute sowohl in unserem privaten als auch in unserem beruflichen Alltag eine wesentliche Rolle. Es stellt sich aber leider heraus, dass Optimierung in der Regel schwierig ist, und zwar so schwierig, dass es oft bereits praktisch unmöglich ist, auch nur eine einzige gültige Lösung für ein Problem zu finden (man nennt das die Suchvariante des Problems), ganz zu schweigen von der optimalen Lösung. Ein gutes Beispiel ist das Problem des Handelsreisenden, bei dem nach der kürzesten Rundreise über eine Reihe von vorgegebenen Zwischenstationen gesucht wird. Man kann beweisen, dass schon die Frage, ob eine Rundreise mit einer gewissen Höchstlänge existiert, äußerst schwierig ist. Trotz der inhärenten Komplexität dieser Probleme haben WissenschaftlerInnen Algorithmen und Software entwickelt, die große, praktisch relevante Optimierungs- und Suchprobleme lösen können. Weil es aber unpraktisch und teuer wäre, für jede Anwendung entsprechende Verfahren von Grund auf neu zu entwickeln, existieren einige wenige Algorithmen und Solver für allgemeine Probleme, in die alle anderen Probleme übersetzt werden. Hier stoßen wir auf eine weitere Herausforderung: in manchen Fällen ist nicht nur das Lösen eines Optimierungsproblems schwierig, sondern sogar dessen Übersetzung in ein für allgemeine Verfahren geeignetes Eingabeformat. Für Probleme von derart hoher Komplexität bedarf es ausdruckstärkerer Eingabesprachen. Als Beispiel kann die Suche nach Gewinnstrategien für Schach dienen. Die Existenz einer Strategie (für Weiß) kann mithilfe einer Formel der folgenden Form ausgedrückt werden: es gibt einen Zug für Weiß, sodass es für alle Züge von Schwarz einen Zug für Weiß gibt, , sodass Schwarz matt gesetzt wird. Die Abfolge von universellen (für alle Züge) und existenziellen (es gibt einen Zug...) Aussagen ist hier wesentlich. Solche sogenannten quantifizierten booleschen Formeln (QBF) sind Gegenstand dieses Projekts, zusammen mit Dependency QBF (DQBF), einer Verallgemeinerung, die Spielen mit mehreren Spielern entspricht. Neben Spielen haben QBF und DQBF Anwendungen in der formalen Verifikation und Synthese von Software, künstlicher Intelligenz, und dem automatisierten Design von integrierten Schaltkreisen. Dieses Projekt soll das Verständnis von QBF und DQBF durch zwei innovative Ansätze fördern. Erstens sollen QBF und DQBF gleichzeitig untersucht werden, zweitens wollen wir Theorie und Software im Einklang entwickeln. Im Zuge dessen sollen grundlegende Fragen geklärt werden, die das Verhältnis von QBF und DQBF, theoretischen Konzepten und praktischen Verfahren, und die Auswirkung von cleveren Kodierungsmethoden auf die Leistung von Solvern betreffen. Das Projekt ist an der Schnittstelle von Theorie und Praxis angesiedelt und umfasst sowohl mathematische Arbeit mit Papier und Bleistift als auch umfangreiche Experimente auf Clustern mit Hunderten von Prozessoren.

Das Hauptziel des Projekts bestand darin, unser Verständnis von quantifizierten Booleschen Formeln (QBF) und abhängigkeitsquantifizierten Booleschen Formeln (DQBF) zu vertiefen. Diese Formeln werden zur Modelierung und Lösung von verschiedenen Ausgaben verwendet, wie z.B. die Verifikation und Synthesis von Soft- und Hardware. Das Projekt zielte darauf ab, sowohl theoretisches als auch praktisches Wissen über diese Formeln zu entwickeln. Diese Forschung suchte die Lücke zwischen Theorie und Praxis in diesem Bereich zu schließen, da diese beiden oft getrennt entwickelt wurden, was zu einem Mangel an fundierten theoretischen Grundlagen für praktische Fortschritte führte. Beweissysteme sind eine formale Methode, um mathematische Beweise zu untersuchen und bieten einen strukturierten Rahmen, wodurch man die Eigenschaften und Komplexitäten verschiedener Probleme verstehen kann. Solver für komplexe Probleme erzeugen oft formale Beweise, die mit Beweissystemen analysiert werden können, um Einblicke in den Problemlösungsprozess zu gewinnen. Ein bedeutendes Ergebnis des Projekts war ein besseres Verständnis der Schwierigkeit von mathematischen Formeln. Die Forscher konnten die Schwierigkeitslandschaft für Resolution kartieren, eines der grundlegendsten Beweissysteme in der Informatik, und welches auch für die Praxis wichtig ist. Diese Arbeit führte zu einem Datensatz mit Formeln und Beweisen sowie einem Softwaretool, das kürzeste Beweise von Formeln berechnen kann. Diese Ressourcen können Forschern helfen, die Schwierigkeit verschiedener Probleme weiter zu untersuchen und möglicherweise effizientere Algorithmen für ihre Lösung zu entwickeln. Ein weiteres wichtiges Ergebnis war der Vergleich verschiedener QBF-Lösungsalgorithmen. Die Forscher gaben Solver-Entwicklern Einblicke, indem sie die theoretische Leistungsfähigkeit verschiedener Algorithmen untersuchten, die in modernen QBF-Solvern verwendet werden. Diese Forschung führte zur erfolgreichen Implementierung einer neuen Funktion im QBF-Solver Qute, die jetzt von Praktikern verwendet werden kann, um komplexe Probleme effizienter zu lösen. Darüber hinaus leistete das Projekt bedeutende Beiträge im Bereich der Abhängigkeitsschemata. Abhängigkeitsschemata sind Algorithmen, die Formeln manipulieren, um sie leichter lösbar zu machen, oft durch Umordnung von Variablen in einem Problem oder durch Entdeckung versteckter kausaler Zusammenhänge. Sie bieten wertvolle Einblicke für die Entwicklung von Beweissystemen und Solvern. Die Forscher führten eine große Menge von Abhängigkeitsschemata für QBF und DQBF ein, die eine präzise Struktur aufweisen und wertvolle Einblicke für die Entwicklung von Beweissystemen und Solvern bieten. Einige davon wurden bereits implementiert und zur Verfügung gestellt.