Parallele Verfahren und Systeme für das SAT-Solving

• Antragsteller: Professor Dr. Wolfgang Blochinger
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2006 bis 2011
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 24060795

Das Ziel des Projektes HighPerfSAT ist die signifikante Beschleunigung der Erfüllbarkeitsprüfung aussagenlogischer Formeln (SAT-Solving) mittels Parallelverarbeitung. Diverse Anwendungsprobleme aus Wissenschaft und Wirtschaft (z.B. aus den Bereichen der Entwicklung mikro-elektronischer Schaltungen, der Konfiguration und Verifikation komplexer Systeme oder der Kryptographie) können mittlerweile als aussagenlogische Formeln dargestellt werden. Das SAT-Solving wird damit zu einem vielseitigen Werkzeug zur Lösung schwerer Probleme. 1 Mit den Resultaten des Projektes wird der Anwendungsradius des SAT-Solving wesentlich erweitert. Es können weitaus größere Probleminstanzen gelöst werden, als dies zurzeit der Fall ist. Zudem soll eine neue Leistungsdimension des SAT-Solving realisiert werden, welche den Weg zur Erschließung völlig neuer Anwendungsgebiete ebnen kann. Damit leistet das Projekt wesentliche Beiträge innerhalb der übergeordneten Problemstellung der Beherrschbarkeit komplexer Systeme. Die angestrebte Leistungssteigerung soll durch die kombinierte Entwicklung von neuen parallelen Verfahren und mächtigen Software-Systemen auf verschiedenen Parallelrechner-Architekturen verwirklicht werden. Ein Schwerpunkt liegt dabei auf dem parallelen SAT-Solving auf Desktop Grids, welche sich praktisch in jeder Institution ohne nennenswerte Mehrkosten betreiben lassen und gleichwohl eine enorme Rechenkapazität liefern. Damit wird sichergestellt, dass die erzielte Leistungssteigerung der breiten Anwenderbasis des SAT-Solving unmittelbar zur Verfügung steht.

• DFG-Verfahren: Sachbeihilfen
• Beteiligte Person: Professor Dr. Wolfgang Küchlin