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.

Um also von einem Portfolio an Algorithmen möglichst stark zu profitieren, sollten möglichst viele verschiedene Algorithmen oder Algorithmen mit möglichst verschiedenen oder gegensätzlichen Einstellungen für ihre Heuristiken verwendet werden. Dadurch durchsuchen die Algorithmen mit höherer Wahrscheinlichkeit unterschiedliche Teile des Suchraums gleichzeitig. Die Heuristiken, die unterschiedliche Einstellungen erlauben, ergeben sich in der Regel aus den sequentiellen Versionen der verwendeten Algorithmen, und sind nicht explizit Teil des parallelen Algorithmus. Die parallele Ausführung erlaubt lediglich das Problem zu umgehen, sich für eine feste Konfiguration der Heuristiken entscheiden zu müssen.

Eine weitere Möglichkeit der Diversifikation in Portfolio-Ansätzen ist die Aufteilung des Suchraums, analog zum Teile-und-herrsche-Verfahren. Dabei können den parallelen Instanzen Variablenbelegungen vorgegeben oder empfohlen werden, um sie möglichst in einen separaten Teilbereich des Suchraums zu dirigieren.

Anstatt eine Diversifikation durch manuelle Konfiguration vieler Instanzen zu erreichen, was Vertrautheit mit der Probleminstanz und den Algorithmen erfordert, ist es auch möglich ein Portfolio online zu generieren, das aus automatisch konfigurierten Instanzen desselben Algorithmus besteht. Dieser Ansatz erzielt kompetitive Ergebnisse, wenn man ihn mit manuell erzeugten Portfolios vergleicht.

Massively Parallel Processing

Während der Übergang von sequentiellen zu parallelen Algorithmen in der Regel symmetrische Mehrprozessorsysteme betrachtet, finden sich mit Supercomputern und Grafikkarten auch Beispiele für parallele Architekturen mit asymmetrischer Parallelität. Diese lassen sich in der Regel nicht effizient durch allgemeine parallele Algorithmen des Erfüllbarkeitsproblems ausnutzen, da es wegen unzureichenden Speicherressourcen oder zu hohem Grad der Parallelität zu Engpässen bei Speicherzugriffen oder Kommunikation kommt.

Cloud-Algorithmen

Auf Rechnernetzen skalierbare Algorithmen gibt es sowohl für den auf CDCL basierenden Portfolio-Ansatz, als auch eine für Divide-And-Conquer. Hierbei tun sich jedoch neue Probleme bezüglich der Skalierbarkeit auf: Je nach Netzwerktopologie können die einzelnen Rechner nur mit Aufwand untereinander kommunizieren. Zudem ist die Übertragungsrate begrenzt, und die gleichzeitige Kommunikation mehrerer Teilnehmer kann zur Überlastung des Netzwerks und damit einhergehenden Verzögerungen führen. Einzelne Prozesse, die den Suchraum aufteilen, oder den Austausch erlernter Klauseln regulieren, führen daher zu Verlangsamungen und es müssen dezentrale Lösungen gefunden werden. Das heißt, dass Cloud Algorithmen in der Regel nicht über zentrale Verwaltungsstrukturen verfügen, sondern sich Prozesse einzeln miteinander abstimmen.

Portfolio-Algorithmen verlassen sich weiterhin auf bekannte sequentielle Algorithmen, aber verhindern Leistungseinbußen beim Clause-Sharing durch weitere Innovation. Da die hohe Diversifikation sequentieller Algorithmen und ihrer Konfiguration zu einer breiten Abdeckung des Suchraums führt, sind nicht alle erlernten Klauseln von Nutzen für alle Instanzen. Und weil die Verteilung von Klauseln zwischen hunderten Rechnern erhebliche Netzwerklast verursacht, ist es daher wichtig, durch Heuristiken und Filter das mehrfache Senden gleicher Klauseln, sowie den Import von wahrscheinlich uninteressanten Klauseln zu verhindern, und die Datenmenge möglichst kompakt zu halten. Die Verteilung der Clauses geschieht üblicherweise über eine Middleware wie MPI, sodass eine möglichst effiziente All-to-all-Kommunikation möglich ist.

Da ein sehr hoher Grad an Parallelität besteht, und die einzelnen Rechner in der Regel auch über Hardware Threads verfügen, werden Kommunikation und damit verbundene Heuristiken parallel zum sequentiellen Algorithmus in separaten Threads ausgeführt. Der Import erlernter Klauseln geschieht ebenfalls parallel, sodass die Arbeit der Solver möglichst nie unterbrochen wird. Die Algorithmen können selbst unter hoher Skalierung signifikanten, bis hin zu superlinearem Speedup messen.

Für industrielle Probleme ist es häufig nicht wünschenswert, einen ganzen Superrechner für ein einzelnes Problem zu verwenden. Der in mehreren SAT-Competitions dominante Cloud-Algorithmus HordeSAT wurde aus diesem Grund um einen Lastverteilungsalgorithmus erweitert, der Job-Parallelismus erlaubt. Mit diesem kann die Anzahl an Prozessoren, die für eine einzelne Instanz dezentral und dynamisch während der Ausführung angepasst werden. So kann Problemen, die sich während der Lösung als schwierig erweisen, mehr Rechenleistung zugewiesen werden, und Rechenleistung für neue Jobs im Netzwerk dynamisch freigegeben werden.

Der Cube-And-Conquer Ansatz hat weiterhin einen zentralen Algorithmus, um die Cubes zu wählen. Abgeschnittene Cubes werden einem Slave-Rechner im Netzwerk übergeben. Ein Kommunikationsprotokoll zwischen allen Rechnern tauscht Informationen über Auslastung aus und ermöglicht den einzelnen Algorithmen so, ihren Suchraum weiter zu spalten, wenn andere Rechner keine Arbeit mehr haben.

Grafikkarten

Grafikkarten sind nicht geeignet, um die gängigen parallelen Algorithmen für das Erfüllbarkeitsproblem auszuführen. Diese Algorithmen brauchen viel Speicher, um die notwendigen Datenstrukturen zu speichern. Während Grafikkarten zwar viele Rechenkerne haben, teilen sich alle diese Kerne vergleichsweise wenig Speicher, sodass nur wenige Instanzen der Algorithmen gleichzeitig ausgeführt werden können. Allerdings gibt es durchaus Ansätze, Grafikkarten für die Berechnung auszunutzen.

Beispielsweise lassen sich einfachere Algorithmen, die nicht mit modernen Solvern mithalten können, zu Hybridalgorithmen kombinieren: Die Grafikkarte führt einen einfachen, leicht parallelisierbaren Algorithmus basierend auf lokaler Suche aus, und ein CDCL-Algorithmus auf der CPU nutzt dessen Teilergebnisse für seine Heuristiken. Anstatt einen kompletten Algorithmus auszuführen, lassen sich auch die Heuristiken direkt auf die GPU auslagern. Diese kann von schnellen Vektoroperationen profitieren, um viele Entscheidungen wichtiger Heuristiken gleichzeitig zu treffen.

Noch einen Schritt weiter geht die Ersetzung gängiger Heuristiken durch künstliche neuronale Netzwerke, die ohnehin in der Regel auf Grafikkarten berechnet werden.

Lastverteilung

Das größte Problem, mit dem alle parallelen Ansätze zu kämpfen haben, ist die gleichmäßige Verteilung der Rechenlast auf alle verfügbaren Prozessoren. Der älteste Ansatz der Parallelisierung, das Teile-und-herrsche-Verfahren, veranschaulicht diese Problematik am besten. Das im zugehörigen Abschnitt beschriebene Verfahren führt aber zu einer ungleichmäßigen Aufteilung auf Prozessoren.

Cube-And-Conquer ist ein Ansatz, um dieses Problem dynamisch zu lösen. Anstatt die Arbeit am Anfang der Berechnung auf die Prozessoren zu verteilen, generiert ein Prozess laufend kleine Teilprobleme, von denen sich Prozessoren ohne Arbeit jeweils eines auswählen und abarbeiten. Dadurch kann die Berechnung mit verhältnismäßig wenig zusätzlichem Aufwand auf alle Kerne verteilt werden. Die Arbeit des Prozesses, der das Problem in Cubes aufteilt, ist hierbei größtenteils kein Overhead, sondern ist ebenfalls ein Suchalgorithmus. Die abgespaltenen Subprobleme sind Teil seines eigenen Suchraums. Dadurch sind alle Prozessoren die meiste Zeit mit der Lösung des eigentlichen Problems beschäftigt, und nicht etwa mit der Verwaltung der Lastverteilung.

Algorithmen in großen Rechnernetzwerken setzen hingegen auf eine selbstständige Lastverteilung auszuführender Jobs zwischen den Nodes durch lokale Kommunikation, um Probleme mit Skalierbarkeit zu vermeiden. Auch das dynamische Neuzuweisen von Rechenresourcen an schwierige Jobs sei hier zu erwähnen, welches HordeSAT unterstützt.

Speicherverwaltung

Portfolio-Solver haben hohe Speicheranforderungen, da die einzelnen Instanzen jeweils die Problemstellung und eine eigene Datenbank an erlernten Klauseln im Speicher halten. Das Teilen erlernter Klauseln verstärkt dieses Problem, da die Instanzen zusätzlich zu den eigens erlernten Klauseln auch die ihrer konkurrierenden Instanzen importieren. Diese Herangehensweise ist historisch durch die Weiterverwendung sequentieller Algorithmen in den Portfolios bedingt, die möglichst wenig modifiziert wurden. Da dies jedoch mit erheblichen Speicheranforderungen verbunden ist, gibt es auch Algorithmen, die mit neuen sequentiellen Algorithmen das Teilen von erlernten Klauseln durch Referenzierung erlauben.

Dabei entstehen neue Probleme für die Implementierung des CDCL Algorithmus. So können beispielsweise falsifizierte Literale nicht einfach aus Klauseln entfernt werden, da andere Instanzen parallel darauf zugreifen. Da die zentrale Datenbank der Klauseln nicht modifiziert werden darf, muss ein anderes Verfahren benutzt werden, um das Aussieben von falsifizierten Literalen aus Klauseln zu ermöglichen.

Auch können zentrale Datenstrukturen nicht parallel verkleinert werden. Stattdessen werden Änderungen an den Klauseln zunächst lokal behandelt, und der CDCL Algorithmus regelmäßig unterbrochen, um mit einer Master-Instanz zu kommunizieren, die solche Änderungen exklusiv vornimmt, falls eine Klausel von keiner Instanz mehr referenziert wird. Dies senkt zwar die Effizienz einzelner Instanzen, doch ist dafür eine wesentlich bessere Skalierung der Speicheranforderungen sichtbar.

Deterministische Lösungen

Nicht alle parallelen Algorithmen für das Erfüllbarkeitsproblem verwenden randomisierte Techniken. Dennoch liefern die meisten Algorithmen keine deterministischen Ergebnisse. Das heißt, dass trotz gleicher Eingabe verschiedene Ausgaben möglich sind. Dieses Verhalten liegt hauptsächlich an der Kooperation der Instanzen, und damit verbundenen zufälligen Verzögerungen durch unterschiedliche Systemlast, Cache-Effekte, oder Netzwerk-Congestion. Viele Anwendungen benötigen jedoch reproduzierbare Ergebnisse, was die Verwendung paralleler Algorithmen erschwert.

Aus diesem Grund existieren verschiedene Ansätze, die Algorithmen so zu synchronisieren, dass es keine Änderungen der Reihenfolge bestimmter Ereignisse (wie zum Beispiel Clause-Exchange) gibt, die zufälliges Verhalten nach sich ziehen. Den ersten Ansatz hierzu lieferte bereits ManySAT, einer der ersten Portfolio-Solver. Alle Instanzen führen ihre lokalen Algorithmen aus, bis eine Heuristik entscheidet, dass eine Runde Clause-Exchange stattfinden soll. Dann warten alle Instanzen an einer Barriere, bis alle anderen Instanzen bereit sind. Dadurch findet der Klauselaustausch in fester Reihenfolge statt, und es kann nicht zu Nicht-Determinismus kommen. Nach dem Austausch fahren alle Algorithmen mit einer weiteren Runde der normalen Berechnung fort.

Dieses Verfahren hat den Nachteil, dass die Instanzen Zeit mit Warten verbringen, was die Effizienz des Algorithmus senkt. Stattdessen lässt sich der Clause-Exchange auch um einige wenige Runden verzögern. Wenn die Instanzen ihre Klauseln für Runde erst in Runde austauschen, ist die Wahrscheinlichkeit, dass alle Instanzen die erste Runde bereits abgeschlossen haben, höher.

SAT Competition

Seit 2002 gibt es einen Wettbewerb zwischen verschiedenen SAT-Solvern, welcher jährlich in unterschiedlichen Ausführungen stattfindet. Der Wettbewerb soll die Entwicklung neuer und besserer Algorithmen für das SAT-Problem fördern. Die Veranstalter fordern Industriezweige auf, die auf SAT-Solver angewiesen sind, industrielle Benchmarks für ihre Anwendungsbereiche zur Verfügung zu stellen. Weiterhin gibt es unerfüllbare und zufällig generierte Problemstellungen zu lösen. Die Algorithmen treten meist in unterschiedlichen Kategorien gegeneinander an. Dazu zählen üblicherweise eine sequentielle, eine parallele, eine hoch-parallele (genannt Cloud), sowie einige spezielle Kategorien, die sich teilweise von Jahr zu Jahr unterscheiden.

Die Algorithmen versuchen möglichst viele Probleminstanzen jeweils innerhalb eines Zeitlimits zu lösen. Der Algorithmus, der die meisten Instanzen löst, gewinnt.

Während der SAT Competition 2011 wurde das Konzept der Portfolioalgorithmen für SAT-Solving eingeführt, indem einfach alle Gewinner der verschiedenen Kategorien über ein Script parallel ausgeführt wurden. Um ein solches Vorgehen zu unterbinden, da es für Teilnehmer sehr demotivierend sein kann, wenn ein Teilnehmer mit Algorithmen anderer Einreichungen gewinnt, sind Portfolio-Algorithmen nur noch durch Diversifikation einzelner Algorithmen, aber nicht mehr durch die Kombination unterschiedlicher Algorithmen zugelassen. Dies widerspräche auch dem erklärten Ziel des Wettbewerbs, die Entwicklung neuer Algorithmen zu fördern, da ausschließlich vorhandene Algorithmen verwendet wurden. Seit 2022 werden diese Regeln für die Cloud Kategorie gelockert, weil hier der Fokus der Entwicklung nicht mehr auf den einzelnen Algorithmen liegt, sondern auf effizienter Kommunikation und Lastverteilung.

  • Youssef Hamadi, Lakhdar Sais: Handbook of Parallel Constraint Reasoning. Springer, 2018, ISBN 978-3-319-63515-6
  • Ruben Martins, Vasco Manquinho, Inês Lynce: An overview of parallel SAT solving. In: Constraints. Band 17, Nr. 3, 1. Juli 2012, ISSN 1572-9354
  • Satisfiability: Application and Theory (SAT) e.V.: The International SAT Competition Web Page. Abgerufen am 23. Januar 2023.

Einzelnachweise

  1. ↑ Youssef Hamadi, Lakhdar Sais (Hrsg.): Handbook of Parallel Constraint Reasoning. Springer, 2018, ISBN 978-3-319-63516-3, S. 3, doi:10.1007/978-3-319-63516-3.
  2. 1 2 Nils Merlin Ullman, Tomáš Baylo, Michael Klein: Parallelizing a SAT-Based Product Configurator. In: CP. Dagstuhl Publishing, 2021, doi:10.4230/LIPIcs.CP.2021.55 (dagstuhl.de [PDF]).
  3. ↑ Fabien Corblin, Y. Hamadi, E. Fanchon, Laurent Trilling: A SAT-based approach to decipher Gene Regulatory Networks. 2007, abgerufen am 10. Januar 2023 (englisch).
  4. ↑ Hannah Brown, Lei Zuo, Dan Gusfield: Comparing Integer Linear Programming to SAT-Solving for Hard Problems in Computational and Systems Biology. In: Algorithms for Computational Biology. Springer, 1. Februar 2020, doi:10.1007/978-3-030-42266-0_6, PMC 7197060 (freier Volltext) – (63–76 S.).
  5. ↑ Holger Dambeck: Der längste Mathe-Beweis der Welt umfasst 200 Terabyte. In: Der Spiegel. 30. Mai 2016, ISSN 2195-1349 (spiegel.de [abgerufen am 10. Januar 2023]).
  6. ↑ Carsten Sinz, Tomáš Balyo: Practical SAT Solving. In: Institute for Theoretical Computer Science – Karlsruhe Institute of Technology. Karlsruhe Institute of Technology, 23. April 2019, abgerufen am 10. Januar 2023 (englisch).
  7. ↑ Henry Kautz, Bart Selman: Planning as Satisfiability. In: Bernd Neumann, European Committee for Artificial Intelligence [ECAI] (Hrsg.): Proceedings of the 10th European Conference on Artificial Intelligence (ECAI). Wiley, Wien 1992, ISBN 0-471-93608-1 (359–363 S., psu.edu [PDF]).
  8. 1 2 3 4 5 6 7 8 9 10 11 12 13 Tomáš Balyo, Carsten Sinz: Parallel Satisfiability. In: Youssef Hamadi, Lakhdar Sais (Hrsg.): Handbook of Parallel Constraint Reasoning. Springer, 2018, ISBN 978-3-319-63516-3, doi:10.1007/978-3-319-63516-3.
  9. ↑ Matti Järvisalo, Daniel Le Berre, Olivier Roussel: The SAT 2011 competition - Results of phase 1. In: Centre de Recherche en Informatique de Lens. 18. Juni 2011, abgerufen am 10. Januar 2023 (englisch).
  10. 1 2 3 4 5 6 Youssef Hamadi, Said Jabbour, Lakhdar Sais: ManySAT: a Parallel SAT Solver. In: Journal on Satisfiability, Boolean Modeling and Computation. Band 6, Nr. 4, 1. Januar 2010, S. 245–262, doi:10.3233/SAT190070 (iospress.com [abgerufen am 10. Januar 2023]).
  11. 1 2 3 4 Nicolas Prevot, Mate Soos, Kuldeep S. Meel: Leveraging GPUs for Effective Clause Sharing in Parallel SAT Solving. In: Theory and Applications of Satisfiability Testing – SAT 2021. Springer International Publishing, Cham 2021, ISBN 978-3-03080223-3, S. 471–487, doi:10.1007/978-3-030-80223-3_32 (springer.com [abgerufen am 10. Januar 2023]).
  12. 1 2 3 4 5 6 Dominik Schreiber, Peter Sanders: Scalable SAT Solving in the Cloud. In: Theory and Applications of Satisfiability Testing – SAT 2021. Springer International Publishing, Cham 2021, ISBN 978-3-03080223-3, S. 518–534, doi:10.1007/978-3-030-80223-3_35 (springer.com [abgerufen am 10. Januar 2023]).
  13. ↑ B. Selman, H. Levesque, D. Mitchell: A New Method for Solving Hard Satisfiability Problems. 1992, abgerufen am 10. Januar 2023 (englisch).
  14. 1 2 Alejandro Arbelaez, Youssef Hamadi: Improving Parallel Local Search for SAT. In: Learning and Intelligent Optimization. Springer, Berlin, Heidelberg 2011, ISBN 978-3-642-25566-3, S. 46–60, doi:10.1007/978-3-642-25566-3_4 (springer.com [abgerufen am 10. Januar 2023]).
  15. ↑ Padraigh Jarvis, Alejandro Arbelaez: Cooperative Parallel SAT Local Search with Path Relinking. In: Evolutionary Computation in Combinatorial Optimization. Springer International Publishing, Cham 2020, ISBN 978-3-03043680-3, S. 83–98, doi:10.1007/978-3-030-43680-3_6 (springer.com [abgerufen am 10. Januar 2023]).
  16. 1 2 3 G. Folino, C. Pizzuti, G. Spezzano: Parallel hybrid method for SAT that couples genetic algorithms and local search. In: IEEE Trans. Evol. Comput. 2001 (semanticscholar.org [abgerufen am 10. Januar 2023]).
  17. ↑ I. Borgulya: An evolutionary framework for 3-SAT problems. In: Proceedings of the 25th International Conference on Information Technology Interfaces, 2003. ITI 2003. 2003 (semanticscholar.org [abgerufen am 10. Januar 2023]).
  18. 1 2 Marijn J. H. Heule, Oliver Kullmann, Siert Wieringa, Armin Biere: Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. In: Hardware and Software: Verification and Testing. Springer, Berlin, Heidelberg 2012, ISBN 978-3-642-34188-5, S. 50–65, doi:10.1007/978-3-642-34188-5_8 (springer.com [abgerufen am 11. Januar 2023]).
  19. 1 2 3 4 5 6 7 Tomás Balyo, P. Sanders, C. Sinz: HordeSat: A Massively Parallel Portfolio SAT Solver. In: ArXiv. 2015, arxiv:1505.03340 [abs] (semanticscholar.org [abgerufen am 10. Januar 2023]).
  20. ↑ Lin Xu, H. Hoos, Kevin Leyton-Brown: Hydra: Automatically Configuring Algorithms for Portfolio-Based Selection. In: Proceedings of the AAAI Conference on Artificial Intelligence. 2010 (semanticscholar.org [abgerufen am 10. Januar 2023]).
  21. 1 2 3 Maximilian Levi Heisinger: Paracooba Enters SAT Competition 2022. In: Tomá ̆s Balyo, Marijn J. H. Heule, Markus Iser, Matti Järvisalo, and Martin Suda (Hrsg.): Proceedings of SAT Competition 2022 : Solver and Benchmark Descriptions. University of Helsinki, Helsinki 2022.
  22. ↑ Sander Beckers, Gorik De Samblanx, Floris De Smedt, Toon Goedemé, Lars Struyf, Joost Vennekens, Jos WHM Uiterwijk, Nico Roos, Mark HM Winands: Parallel hybrid SAT solving using OpenCL. In: Proceedings BNAIC 2012. Maastricht University; Maastricht, 1. Oktober 2012 (kuleuven.be [abgerufen am 12. Januar 2023]).
  23. ↑ Wenxi Wang, Yang Hu, Mohit Tiwari, S. Khurshid, K. McMillan, R. Miikkulainen: NeuroComb: Improving SAT Solving with Graph Neural Networks. In: ArXiv. 2021 (semanticscholar.org [abgerufen am 12. Januar 2023]).
  24. 1 2 Mathias Fleury, Armin Biere: Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses. In: arXiv:2207.13577 [cs]. 29. Juli 2022, arxiv:2207.13577 [abs] (arxiv.org [PDF; abgerufen am 13. Januar 2023]).
  25. ↑ Ruben Martins, Vasco Manquinho, Inês Lynce: An overview of parallel SAT solving. In: Constraints. Band 17, Nr. 3, 1. Juli 2012, ISSN 1572-9354, S. 304–347, doi:10.1007/s10601-012-9121-3.
  26. 1 2 3 Hidetomo Nabeshima, Katsumi Inoue: Reproducible Efficient Parallel SAT Solving. In: Theory and Applications of Satisfiability Testing – SAT 2020. Springer International Publishing, Cham 2020, ISBN 978-3-03051825-7, S. 123–138, doi:10.1007/978-3-030-51825-7_10, PMC 7326539 (freier Volltext) – (springer.com [abgerufen am 15. Januar 2023]).
  27. ↑ Satisfiability: Application and Theory (SAT) e.V.: The International SAT Competition Web Page. Abgerufen am 23. Januar 2023 (englisch).
  28. ↑ Marijn Heule, Matti Järvisalo, Martin Suda, Markus Iser, Tomáš Balyo: SAT Competition 2022. In: github.io. Abgerufen am 23. Januar 2023 (englisch).
  29. ↑ Marijn Heule, Markus Iser, Matti Jarvisalo, Martin Suda, Tomáš Balyo: SAT Competition 2022 - Rules. Abgerufen am 16. Februar 2023 (englisch).
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.