Strukturerkennung mit SAT (STRIDES)

SAT (für satisfiability) ist das klassische Problem der aussagenlogischen Erfüllbarkeit. Es fragt danach, den Variablen einer aussagenlogischen Formel die Wahrheitswerte 0 und 1 zuzuweisen, damit die gesamte Formel wahr wird. SAT gilt allgemein als nicht-handhabbar, aber in den letzten zwanzig Jahren wurden Computerprogramme (SAT-Löser) entwickelt, die das Problem überraschend schnell lösen können. Zahlreiche andere schwere Probleme können nach SAT übersetzt und mittels SAT-Löser gelöst werden. Die Übersetzung nach SAT verursacht jedoch oft eine erhebliche Erhöhung der Eingabegröße, was die Anwendung von SAT-Lösern auf kleine Problem-Eingaben beschränkt. Das Projekt zielt darauf ab, die Verwendung von SAT-Lösern auf große Problem-Eingaben zu skalieren. Das soll durch die Anwendung der kürzlich eingeführten SAT-basierten lokalen Verbesserungsmethode (SAT-based Local Improvement Method, SLIM) erreicht werden. Man beginnt mit einer initialen Lösung und wendet mehrmals einen SAT-Löser auf kleine lokale Teile der Eingabe an, um die Größenbeschränkung zu überwinden. Das Projekt untersucht die Anwendung von SLIM auf Probleme, bei denen es darum geht, eine bestimmte schwer zu findende Struktur in Eingabedaten zu finden. Solche Strukturerkennungsprobleme treten bei Textdaten, großen Graphen und Netzwerken und in logischen Schaltkreisen auf. Das Projekt zielt auf die Effizienzsteigerung des SLIM-Ansatzes und auf die Suche nach allgemeinen Erkenntnissen über seine Funktionsweise ab. Neue theoretische und praktische Ergebnisse werden erwartet.