Structure-based Algorithm Engineering for SAT-Solving

点击翻译按钮获取中文摘要

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.