Skalenfreie Erfüllbarkeit

• Antragsteller: Professor Tobias Friedrich, Ph.D.
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2018 bis 2024
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 416061626

Boolesche Logik ist die Standard-Beschreibungssprache für industrielle Entscheidungsprobleme aus unterschiedlichen Bereichen wie Logistik und Optimierung. Industrielle Software-Werkzeug lösen heutzutage effizient ein solches Problem, d. h. sie finden eine erfüllenden Belegung der Booleschen Variablen - selbst für Instanzen mit Millionen von Variablen.Diese praktische Effizienz steht in scheinbarem Widerspruch zum klassischsten Resultat der theoretischen Informatik: der bewiesenen Schwere des aussagenlogischen Erfüllbarkeitsproblems (SAT). Da praktisch auftretende Probleminstanzen eine andere Struktur aufweisen als "Worst-case" Instanzen, ging man in den letzten beiden Jahrzehnten dazu über, das "Average-case" Verhalten eingehend zu untersuchen. Typischerweise wird hierbei als Wahrscheinlichkeitsverteilung die gleichmäßige Verteilung aller Variablen zugrunde gelegt. Empirisch ist dies jedoch ebenfalls sehr weit entfernt von industriellen SAT Instanzen, da die Häufigkeit einer Variable in der Praxis nicht gleichmäßig ist sondern großen Schwankungen unterliegt.Es ist eine der "großen Herausforderungen der SAT-Forschung", realistische Probleminstanzen künstlich zu erzeugen. Ziel dieses Projekts ist eine verbesserte Beschreibung von industriellen SAT-Instanzen durch nicht-gleichmäßige und skalenfreie Verteilungen. Wir analysieren hierzu die statistischen Eigenschaften von realen SAT-Instanzen, welche für eine effiziente Lösbarkeit sorgen. Basierend auf den verfügbaren stochastischen Werkzeugen zur Analyse von großen skalenfreien Netzwerken werden wir die dazu notwendigen mathematischen Methoden entwickeln. Ein besseres Verständnis der entscheidenen Parameter ermöglicht die Entwicklung von darauf abgestimmten und effizienteren SAT-Solvern für industrielle Anwendungen.

• DFG-Verfahren: Sachbeihilfen
• Mitverantwortlich: Professor Dr. Thomas Bläsius