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ße industrielle Instanzen in Millionen von Variablen lösen und zu universellen Werkzeugen zur Lösung schwerer Berechnungsprobleme aus nahezu allen Anwendungsfeldern geworden sind.Dieses Projekt plant den Aufbau einer Theorie des SAT- und QBF-Solving, welche deren Erfolg erklären sowie deren Grenzen aufzeigen kann. Die zentralen Projektziele sind der Entwurf präziser und abstrakter theoretischer Modelle für SAT und QBF-Solver, welche einer komplexitätstheoretischen Analyse zugänglich sind. Solche Analyse zeigt sowohl Grenzen derzeitiger Solving-Paradigmen auf als auch Möglichkeiten zu deren Verbesserung. Im Zentrum unserer Untersuchungen stehen QBF, deren Erfüllbarkeitstest im Vergleich zu SAT ein algorithmisch noch schwierigeres Problem darstellen und weitere Anwendungsfelder erschliessen.Unser methodisches Hauptwerkzeug ist die Beweiskomplexität. Jeder Solver definiert implizit ein logisches Beweissystem. Die Herausforderung besteht jedoch 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 die automatische Suche nach Beweisen vorantreiben.Unser theoretisches Projekt bietet Potential für weitreichende Anwendungen, sowohl im Solving wie auch in der Beweiskomplexität. Unsere neuen theoretischen Modelle werden helfen, zur Entwicklung besserer Solver beizutragen. 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 momentan im Gange. Für die Beweiskomplexität bedeutet unser Projekt einen Paradigmenwechsel: von abstrakten logischen Kalkülen hin zu theoretischen Modellen für praktisches Solving. Dies wird dazu beitragen, die oft beklagte Diskrepanz zwischen theoretischer Forschung in der Beweiskomplexität und praktischem SAT/QBF-Solving zu verringern.

• DFG-Verfahren: Sachbeihilfen