Aussagenlogische Beweise als Big Data

• Antragsteller: Dr. Dominik Schreiber
• Fachliche Zuordnung: Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme ; Theoretische Informatik
• Förderung: Förderung seit 2025
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 565407588

Das Lösen aussagenlogischer Erfüllbarkeitsprobleme (SAT Solving) ist ein grundlegendes Werkzeug für eine Vielzahl wissenschaftlicher und industrieller Anwendungen. Zuletzt haben massiv parallele SAT-Solver an Bedeutung gewonnen, da sie erheblich schnellere Laufzeiten bieten und bisher unlösbare Probleme bewältigen können. Während sequentielle SAT-Solver schon lange in der Lage sind, effizient überprüfbare Beweise für die Unzufriedenheit einer Instanz auszugeben, bleiben skalierbare parallele und verteilte SAT-Solver jedoch bisher zurück: Bestehende beweisgestützte parallele Ansätze weisen entweder deutliche Bottlenecks auf oder können keine persistenten Beweisartefakte erzeugen. Da Beweise zu einem Kernbestandteil der Theorie, Praxis und empirischen Forschung zu SAT geworden sind, stellt dieser Mangel ein dringendes Problem dar und verhindert die Nutzung verteilter SAT-Solver für kritische Aufgaben rund um logisches Schließen. Mit unserem Projekt möchten wir diese Forschungslücke schließen, indem wir einen formalen, algorithmischen und praktischen Rahmen für Beweisproduktion und -prüfung entwerfen, der für hochgradig parallele Berechnungen konzipiert und somit voll skalierbar ist. Ähnlich zu verteilten Operationen in Big-Data-Frameworks (z.B. MapReduce oder Apache Spark) sollten Beweisdaten parallel und über viele Knoten hinweg produziert, gespeichert und überprüft werden. Das Konzept von verteilten Beweisdateien kann skalierbares Erstellen und Prüfen von Beweisen ermöglichen, da es die inhärenten Bottlenecks bisheriger paralleler Ansätze vermeidet. Zunächst entwerfen, implementieren und evaluieren wir ein paralleles und verteiltes Framework zur skalierbaren Produktion, Verarbeitung und Überprüfung von Beweisen. Wir streben effiziente, zugängliche und gut dokumentierte Softwareartefakte an, die realistische Aussichten auf weit verbreitete Anwendung haben. Im Einklang mit dem Stand der Technik in der Beweisprüfung umfasst der nächste Teil unseres Projekts eine formal verifizierte Implementierung unseres parallelen und verteilten Beweisprüfungsalgorithmus. Zudem müssen wir sicherstellen, dass unser Framework ausreichend mächtig und funktionsreich ist, um umfassend einsetzbar zu sein. Zu diesem Zweck planen wir, unseren Ansatz auf die gängigsten Beweisformate auszuweiten, einige der neuesten und leistungsfähigsten Beweissysteme zu integrieren und Kombinationen von Klauselaustausch mit expliziter Suchraumaufteilung zu unterstützen. Schließlich möchten wir eine Auswahl bedeutender Anwendungen betrachten, einschließlich mathematischer Beweisführung und empirischer Studien zur Beweisstruktur. Dies demonstriert zum einen die Fähigkeiten unseres parallelen Beweis-Frameworks und treibt gleichzeitig konstruktiv die Forschung in der Anwendung voran. Insgesamt erwarten wir, dass unser Projekt die Nutzbarkeit und Zuverlässigkeit skalierbarer Werkzeuge zu logischem Schließen für viele kritische Anwendungen erheblich erhöhen wird.

• DFG-Verfahren: Sachbeihilfen