Structure-based Algorithm Engineering for SAT-Solving

• Applicant: Professor Michael Kaufmann, Ph.D.
• Subject Area: Theoretical Computer Science
• Term: from 2007 to 2014
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 47775802

In unserem Projekt haben wir die Struktur von praxisrelevanten SAT-Instanzen mit Hilfe von Backdoormengen visualisiert, Algorithmen entwickelt, um diese Backdoormengen effizient zu finden, und eine neue obere Schranke für eine Unterklasse von 3-SAT unter Verwendung dieser Mengen bewiesen. Daneben haben wir einen eigenen SAT-Solver als Basis für zwei neue Hybridverfahren implementiert, die zur SAT-Competition 2009 eingeschickt wurden. Aufbauend auf diesen Erfahrungen und Ansätzen aus dem Algorithm Engineering konnten wir das Laufzeitverhalten des Solvers unseres Industriepartners in einer zeitkritischen Anwendung um über 90 Prozent verbessern. Im Folgeprojekt wollen wir den strukturbasierten Ansatz weiter ausbauen, weitere Lernstrukturen und -muster erforschen und insbesondere Strukturveränderungen während des Lösungsprozesses kartieren und nutzen. Unser neues Visualisierungswerkzeug SatIn wird dahin erweitert, dass wir die entsprechenden dynamischen Strukturen auch graphisch anzeigen und so die Analyse visuell unterstützen. Ein wichtiges Thema wird auch die realistische Einschätzung des Zustands des Lösungsprozesses (progress estimation) sein, die wir mit strukturellen Methoden verbessern wollen. Letztendlich werden wir im Hinblick auf unsere industrielle Anwendung effektive Möglichkeiten entwickeln, einem Nutzer zu erklären, warum eine SAT-Instanz nicht erfüllbar ist.

• DFG Programme: Priority Programmes
• Subproject of: SPP 1307: Algorithm Engineering
• Participating Person: Professor Dr. Wolfgang Küchlin