Quantifizierte Boolesche Formeln: Beweiskomplexität und Solving

• Antragsteller: Professor Dr. Olaf Beyersdorff
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 462332910

Die Erfüllbarkeitsprobleme der Aussagenlogik (SAT) und für quantifizierte Boolesche Formeln (QBF) sind zentrale Berechnungsprobleme der Theoretischen Informatik: einem Gebiet im Spannungsfeld zwischen Algorithmen und Komplexität. Aus komplexitätstheoretischer Sicht werden SAT als NP-vollständiges und QBF sogar als PSPACE-vollständiges Problem als schwierige Berechnungsprobleme eingeordnet. Dies steht in starkem Kontrast zu ihrer algorithmischen Behandlung durch moderne SAT- und QBF-Solver, die großen industriellen Instanzen in Millionen von Variablen lösen und zu universellen Werkzeugen zur Lösung schwerer Berechnungsprobleme aus nahezu allen Anwendungsfeldern geworden sind. Dieses Projekt entwickelt eine Theorie des SAT- und QBF-Solving, die diesen Erfolg erklärt. Zentrale Projektziele sind der Entwurf präziser theoretischer Solvermodelle, die einer komplexitätstheoretischen Analyse zugänglich sind. Diese Analyse zeigt sowohl Grenzen derzeitiger Solving-Paradigmen auf als auch Möglichkeiten zur algorithmischer Verbesserung. Im Zentrum unserer Untersuchungen stehen QBF, die im Vergleich zu SAT weitere Anwendungsfelder erschließen. Unser methodisches Hauptwerkzeug ist die Beweiskomplexität. Jeder Solver definiert implizit ein logisches Beweissystem. Die Herausforderung besteht darin, schlanke beweistheoretische Modelle in der Praxis verwendeter Solver zu entwickeln. Um diese Modelle komplexitätstheoretisch zu analysieren, wird das Projekt die QBF-Beweiskomplexität durch neue Techniken für untere Schranken, neue Familien harter Formeln und Heuristiken zur Beweissuche vorantreiben. In der ersten Projektphase modellierten wir die Basisversion von QCDCL, eine der wichtigsten Ansätze im QBF-Solving, auf dem erfolgreichen CDCL-Paradigma für SAT fußend. Wir entwickelten eine maßgeschneiderte Technik für untere Schranken für QCDCL und klärten die Beziehung zu wichtigen QBF-Beweissystemen. Darauf aufbauend wollen wir in der zweiten Projektphase diese Analyse zu modernsten Methoden im QBF-Solving, insbesondere Dependency Learning, signifikant verbessern. Dies erfordert deutlich stärkere Techniken und neue Klassen von QBF. Parallel dazu wollen wir den Transfer unserer theoretischen Resultate in die Praxis durch Entscheidungs- und Reduktionsheuristiken sowie Proof-of-Concept-Implementierungen initiieren. Unser theoretisches Projekt bietet Potential für weitreichende Anwendungen, sowohl im Solving wie auch in der Beweiskomplexität. Der gegenwärtige Zeitpunkt bietet dafür ideale Voraussetzungen: während die wichtigsten algorithmischen Durchbrüche im SAT-Solving bereits Ende der 1990er Jahre stattfanden, ist eine solche Phase algorithmischer Innovation im QBF-Solving jetzt im Gange. Für die Beweiskomplexität bedeutet unser Projekt einen Paradigmenwechsel: von abstrakten logischen Kalkülen zu theoretischen Modellen für praktisches Solving.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Indien, Österreich, Spanien
• Kooperationspartnerinnen / Kooperationspartner: Professor Ilario Bonacina; Professorin Meena Mahajan; Dr. Tomas Peitl