Das Erfüllbarkeitsproblem der Aussagenlogik (SAT, von englisch satisfiability) ist eines der grundlegendsten, schweren Probleme der Informatik. Obwohl die Problemdefinition denkbar einfach und abstrakt ist, finden sich unzählige Anwendungsgebiete in Industrie und Forschung, weshalb effiziente Lösungsansätze schon lange Gegenstand der Forschung sind. Die Anwendungsbereiche des Erfüllbarkeitsproblems erstrecken sich von simplen Konfigurationsaufgaben bis hin zu Lösungsansätzen von schwierigen Problemen der Naturwissenschaften.
Weil viele der Anwendungen für das Erfüllbarkeitsproblem riesige Problemstellungen lösen müssen, und Prozessoren inzwischen an physikalische Grenzen stoßen, was Geschwindigkeit und Größe betrifft, schwenken Prozessorhersteller und in Folge auch die Algorithmentechnik seit Jahren auf Mehrprozessorsysteme um. Dies erfordert allerdings spezielle Algorithmen für das Erfüllbarkeitsproblem, welche die zusätzliche Hardware auch effizient nutzen können.
Anwendungsgebiete Die Anwendungsgebiete für das Erfüllbarkeitsproblem reichen von einfacheren technische Anwendungen wie Produktkonfiguratoren bis hin zu Medizin und Biologie. Wichtige Probleme wie die Analyse von Genregulationsnetzwerken, sowie das Problem der Proteinfaltung lassen sich durch SAT lösen. Gerade letztere gelten wegen der extrem großen Suchräume als schwierig bis unlösbar. Auch außerhalb der Biologie bildet das Erfüllbarkeitsproblem die Grundlage für viele schwierige Probleme, wie der automatisierten Beweisführung in der Mathematik, der formalen Verifikation in der Informatik, sowie der Überprüfung von Prozessordesigns während der Entwicklung. Das Problem hat auch schon lange Einsatzgebiete in Robotik und künstlicher Intelligenz. Da SAT ein NP-vollständiges Problem ist, lässt sich auch jedes andere NP-vollständige Problem durch eine SAT-Instanz darstellen und mit den entsprechenden Algorithmen lösen. Dies bietet sich vor allem für NP-vollständige Probleme an, die weniger gut erforscht sind. Die Erfahrung zeigt, dass die meisten dieser Problemstellungen nicht in sinnvoller Zeit von einem einzelnen Prozessor und einem sequentiellen Algorithmus lösen lassen, und parallele Algorithmen signifikanten Speedup erreichen können.
Ansätze Grundsätzlich unterscheidet man zwischen drei verschiedenen Ansätzen zur parallelen Lösung des Erfüllbarkeitsproblems: Parallele lokale Suche, Teile-und-herrsche-Verfahren und Portfolio-Ansätze. Alle drei basieren dabei auf sequentiellen Ansätzen, verfolgen jedoch unterschiedliche Strategien, um von der Parallelität zu profitieren.
Portfolioansätze Naiv betrachtet ist dies ein sehr einfacher Ansatz für die parallele Berechnung: Man führt verschiedene SAT-Solver unabhängig voneinander auf jeweils einem Prozessor aus. Sobald ein Algorithmus eine Lösung gefunden hat, bricht man die Ausführung aller anderen ab. Dass dieser Ansatz überhaupt zu einer Verbesserung der Performance führt, liegt an einer simplen Beobachtung: Verschiedene Algorithmen für das Erfüllbarkeitsproblem sind in der Regel für verschiedene Problemstellungen geeignet. Es gibt jedoch keine verlässliche Vorhersage, welcher Algorithmus für welche Problemstellung geeignet ist, daher führt man mehrere aus und lässt sie gegeneinander antreten. Der Erfolg dieses Ansatzes wurde von Olivier Roussel während der SAT Competition 2011 präsentiert. Er kombinierte die Gewinner verschiedener Kategorien und führte sie parallel aus, womit er in mehreren Kategorien die jeweils besten Algorithmen schlug.
Kooperation durch Clause-Sharing Die meisten modernen Solver basieren auf dem CDCL-Algorithmus. Dieser erlernt während der Ausführung neue Klauseln, die sich durch Implikationen bei Konflikten ergeben und im weiteren Verlauf des Algorithmus benutzt werden, um ungültige Variablenbelegungen schneller auszuschließen. Diese Klauseln sind unter einer gegebenen Probleminstanz immer gültig, das heißt, dass eine Probleminstanz mit einer gültigen Lösung durch das Hinzufügen der erlernten Klausel nicht unlösbar wird, und umgekehrt. Daraus folgt, dass parallel ausgeführte Algorithmen vom Erlernen der Klauseln der jeweils anderen Algorithmen profitieren können. Dieser Ansatz wurde von Youssef Hamadi vorgeschlagen, und ist seitdem fester Bestandteil aller kompetitiver CDCL-basierten Portfolio-Algorithmen. Die Menge der erlernten Klauseln ist im Allgemeinen sehr hoch, die Nützlichkeit hingegen nur dann gegeben, wenn die Klausel einen Teil des Suchraums betrifft, in dem eine Instanz gerade nach Lösungen sucht. Das heißt, einfach alle Klauseln zu importieren ist durch Speicherlimitierungen nicht möglich, und auch nicht sinnvoll, da viele Klauseln keinen Mehrwert für eine spezifische Instanz bieten. Dieser Effekt wird durch starke Diversifikation weiter verstärkt. Stattdessen sind Heuristiken, die Entscheidungen bezüglich der Nützlichkeit einer Klausel für eine gegebene Instanz treffen, ein wichtiger Teil jedes Portfolio-Algorithmus und Gegenstand aktueller Forschung.
Zwar ist der Portfolioansatz durch simple Verwendung bestehender Algorithmen entstanden, doch lohnt es sich, die Algorithmen speziell für diesen Zweck zu modifizieren: So ist das Exportieren und Importieren von erlernten Klauseln mit zusätzlichem Synchronisationsaufwand verbunden, doch dieser kann durch spezielle Datenstrukturen und Anpassen der sequentiellen Algorithmen mitigiert werden.
Parallele Lokale Suche Lokale Suche ist der denkbar einfachste Ansatz zur Lösung des Erfüllbarkeitsproblems. Man rät eine Belegung aller booleschen Variablen, und modifiziert diese Belegung, bis man eine erfüllende Belegung gefunden hat. Verschiedene Heuristiken geben vor, welche Variablenbelegungen modifiziert werden, und ab wann eine vollständig neue Belegung gewählt wird, um einem lokalen Suchraum zu entkommen. Dieser Ansatz wird auch unvollständige Suche genannt, da der Algorithmus sich nicht merkt welche Teile des Suchraums schon durchsucht wurden, und deshalb zum Beispiel nicht feststellen kann, ob eine Eingabe unlösbar ist.
Portfolioansatz Die einfachste Methode dieses Vorgehen zu parallelisieren, ist wie bei Portfolio-Solvern die Problemstellung auf jeden weiteren Prozessor zu kopieren, und dort eine neue Variablenbelegung zu raten. Dann führen alle Prozessoren den Algorithmus unabhängig voneinander parallel aus. Sobald ein Prozessor eine Lösung findet, werden alle anderen Instanzen abgebrochen.
Bucket Flips Ein weiterer Ansatz, die Arbeit einer lokalen Suche zu parallelisieren, ist das Teilen der Variablen in mehrere Teilmengen (engl. buckets), woraufhin je einer Menge ein Prozessor zugeteilt wird. Dann modifizieren alle Prozessoren die Lösung nur anhand der ihnen zugeteilten Variablen. Es hat sich allerdings gezeigt, dass dieser Ansatz nur bis zu einer bestimmten Anzahl von Prozessoren bessere Ergebnisse liefert als ein sequentieller Algorithmus.
Kooperation Lokale Suche generiert keine neuen Klauseln während der Ausführung, daher ist es nicht offensichtlich, wie die parallelen Instanzen eines Portfolios kooperieren sollten. Da die Einführung von Clause-Sharing jedoch extreme Vorteile für CDCL-basierte Portfolios erbracht hat, ist es wünschenswert, dass auch für parallele lokale Suchen Ansätze für kooperative Lösungsfindung gefunden werden. Eine Möglichkeit ist, die besten bisherigen Variablenbelegungen zwischen den Instanzen zu teilen. Wenn eine Instanz einen Neustart plant, wird aus den geteilten partiellen Lösungen eine neue Startkonfiguration generiert. Für die Generierung gibt es verschiedene Verfahren, die von einer Mehrheitsentscheidung, über Rekombination, bis hin zu einer probabilistischen Auswahl pro Variable reichen.
Diese Verfahren führen zwar zu einer Leistungsverbesserung gegenüber einfacheren Portfolio-Ansätzen lokaler Suche, schlagen jedoch bisher nicht die auf CDCL basierenden Algorithmen.
Evolutionäre Algorithmen Die Rekombination bisheriger Lösungen lässt sich auf evolutionäre Algorithmen verallgemeinern. Anstatt einzelne lokale Suchen auszuführen und gegebenenfalls neu zu starten, werden viele zufällige Variablenbelegungen nach einer beliebigen Strategie (z. B. Random Walk, oder im Hybridverfahren mit lokaler Suche) modifiziert, regelmäßig nach einer Bewertungsfunktion sortiert, und gute Lösungen untereinander rekombiniert, während schlechte Lösungen verworfen werden. Dieses Verfahren läuft wie alle evolutionären Algorithmen Gefahr, gegen lokale Optima zu konvergieren. Aus diesem Grund ist besondere Vorsicht bei der Rekombination anzuwenden, um die auch von anderen Algorithmen angestrebte Diversifikation zu gewährleisten.
Teile und Herrsche Die älteste Methode, das Erfüllbarkeitsproblem auf mehreren Prozessoren zu bearbeiten ist, den Suchraum zwischen den Prozessoren aufzuteilen. Das ist anhand der Variablenbelegung sehr einfach: Wählt man für Prozessor A eine Variable aus und belegt sie mit dem Wahrheitswert wahr, und für Prozessor B mit falsch, dann bearbeiten beide Prozessoren disjunkte Teile des Suchraums, die jedoch den gesamten Suchraum abdecken. Durch die Belegung weiterer Variablen lassen sich die Teilräume erneut aufteilen. Obwohl es viel Forschung bezüglich einer gleichmäßigen Aufteilung gegeben hat, ist bis heute keine Methode bekannt, wie die Last der Berechnung dabei statisch gleichmäßig verteilt werden kann. Führt nämlich eine der gewählten Belegungen sofort zu einem Konflikt, hat einer der Prozessoren keine Arbeit mehr, und die Effizienz des Algorithmus sinkt. Moderne Algorithmen dieser Art spalten den Suchraum daher nicht statisch, sondern bei Bedarf während der Ausführung, wann immer ein Prozessor seine Teilaufgabe beendet. Dieser Ansatz führt zwar zu effizienterer Nutzung der Prozessoren, allerdings auch zu starken Schwankungen in der Laufzeit, selbst bei gleichbleibenden Problemstellungen.
Cube-And-Conquer Algorithmus Das Problem der ungleichmäßigen Aufteilung des Suchraums durch eine ungünstige Variablenbelegung lässt sich auch anders umgehen. Sogenannte Look-Ahead-Solver sind gut geeignet, um kleine, schwierige SAT-Probleme durch aufwändige Look-Ahead-Heuristiken zu lösen. Diese Heuristiken sind im Gegensatz zu den Heuristiken gängiger CDCL-Algorithmen zu teuer für große Probleme, aber dafür geeignet, günstige Variablen für eine Aufteilung des Suchraums zu wählen. Der Cube-And-Conquer Algorithmus führt daher zunächst einen Look-Ahead-Solver aus, der nach und nach Variablenbelegungen in einem Suchbaum auswählt. Dabei wird der Suchraum nicht notwendigerweise anhand einer Variable in zwei Teilräume gespalten, wie herkömmliche Teile-und-herrsche-Algorithmen es tun. Stattdessen wird eine gewählte partielle Variablenbelegung (sogenannte Cubes) vom Suchbaum des Look-Ahead-Solvers abgeschnitten (englisch cutoff), und an einen CDCL-Algorithmus übergeben. Die komplementäre Belegung wird jedoch nicht unbedingt auch abgeschnitten, sofern die Heuristik dies nicht für sinnvoll erachtet, sondern bleibt zunächst Teil des Look-Ahead-Algorithmus. Auf diese Weise generiert der Algorithmus hunderte Teilräume von etwa gleicher Größe, die von verfügbaren Prozessoren mit herkömmlichen CDCL-Algorithmen nacheinander abgearbeitet werden.
Diversifikation Es sind keine Algorithmen für SAT bekannt, die für alle Probleminstanzen schnell (oder überhaupt) eine Lösung finden. So sind beispielsweise Algorithmen, die sich der lokalen Suche bedienen, viel besser für zufällig generierte Probleminstanzen geeignet, während CDCL-basierte Algorithmen in der Regel besser für industrielle Probleminstanzen geeignet sind. Aber auch Algorithmen derselben Klasse verhalten sich sehr unterschiedlich bei Änderungen in den Parametern ihrer Heuristiken.