Diplomarbeit Backdoors in Sat -Instanzen · 2009. 2. 17. · Diplomarbeit Backdoors in Sat...

Diplomarbeit

Backdoorsin Sat-Instanzen

vorgelegt von

Stephan Kottler

August 2007

Betreuer: Prof. Dr. M. Kaufmann

Arbeitsbereich Paralleles RechnenWilhelm-Schickard-Institut für InformatikFakultät für Informations- und KognitionswissenschaftenEberhard-Karls-Universität Tübingen

Eidesstattliche Erklärung

Hiermit versichere ich, dass ich die vorliegende Arbeit selbständig verfasst und keine an-deren als die angegebenen Hilfsmittel benutzt habe.

Tübingen, 10. August 2007

Inhaltsverzeichnis

1 Einleitung 1

2 Grundlagen 42.1 Das Erfüllbarkeitsproblem . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

2.1.1 Aussagenlogik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42.1.2 Konjunktive Normalform . . . . . . . . . . . . . . . . . . . . . . . . 5

2.2 Definition von Graphen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62.3 Ein populäres Konzept zur Lösung von SAT . . . . . . . . . . . . . . . . . 7

2.3.1 Der reine DPLL-Algorithmus . . . . . . . . . . . . . . . . . . . . . 82.3.2 Branching-Heuristiken . . . . . . . . . . . . . . . . . . . . . . . . . 102.3.3 Aus Konflikten lernen . . . . . . . . . . . . . . . . . . . . . . . . . 132.3.4 Random Restarts . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162.3.5 Implementierungen von SAT-Solvern . . . . . . . . . . . . . . . . . 17

2.4 Lokale Suche - Eine Alternative zu DPLL . . . . . . . . . . . . . . . . . . . 172.5 Handhabbare Unterklassen des SAT-Problems . . . . . . . . . . . . . . . . 18

2.5.1 2-SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 182.5.2 Horn-SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192.5.3 Matched Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

2.6 Backbones und Backdoors . . . . . . . . . . . . . . . . . . . . . . . . . . . 212.7 Parametrisierung von Algorithmen . . . . . . . . . . . . . . . . . . . . . . 22

3 Backdoors 233.1 Bestimmung von DPLL-Backdoors . . . . . . . . . . . . . . . . . . . . . . 24

3.1.1 Berechnung von schwachen DPLL-Backdoors . . . . . . . . . . . . . 243.1.2 Erweiterung für starke DPLL-Backdoors . . . . . . . . . . . . . . . 25

3.2 Eine Vorverarbeitung für industrielle Instanzen . . . . . . . . . . . . . . . 273.2.1 Berechnung eines Propagation-Graphen . . . . . . . . . . . . . . . . 273.2.2 Einschränkung möglicher DPLL-Backdoor-Variablen . . . . . . . . 29

3.3 Deletion Backdoors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 323.3.1 Parametrisierte Berechnung von Horn- & Binär-Backdoors . . . . . 323.3.2 Approximieren von Horn- & Binär-Backdoors . . . . . . . . . . . . 34

3.4 Approximation von starken R-Horn-Backdoors . . . . . . . . . . . . . . . . 393.4.1 Genauere Betrachtung der q-Horn Definition . . . . . . . . . . . . . 40

iii

3.4.2 Generieren eines R-Horn-Abhängigkeitsgraphen . . . . . . . . . . . 413.4.3 Eine Approximation auf dem Abhängigkeitsgraphen . . . . . . . . . 45

3.5 Vergleich verschiedener Backdoor Typen . . . . . . . . . . . . . . . . . . . 543.6 Backdoors in Basis- und Erweiterungs-Instanzen . . . . . . . . . . . . . . . 58

3.6.1 Wiederverwendung von Extended DPLL-Backdoors . . . . . . . . . 593.6.2 Wiederverwendung von schwachen DPLL-Backdoors . . . . . . . . . 623.6.3 Wiederverwendung von Deletion Backdoors . . . . . . . . . . . . . 66

4 Eine obere Schranke für eine Unterklasse von 3-SAT 714.1 Die Klasse 2?-Sat . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 724.2 Ein “Backdoor Driven” Algorithmus . . . . . . . . . . . . . . . . . . . . . 734.3 Komplexität des Algorithmus . . . . . . . . . . . . . . . . . . . . . . . . . 74

4.3.1 Eine Anwendung von FPT-Algorithmen . . . . . . . . . . . . . . . 754.3.2 Bestimmung der oberen Laufzeitschranke . . . . . . . . . . . . . . . 75

5 Visualisierung von SAT-Instanzen - Das Tool SatIn 775.1 Einblicke . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 785.2 Verschiedene Visualisierungen eines SAT-Problems . . . . . . . . . . . . . . 80

5.2.1 Verwendete Layouts . . . . . . . . . . . . . . . . . . . . . . . . . . 815.2.2 Darstellungsmodi . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82

5.3 Interaktives Arbeiten . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 825.4 Visualisierung von Backdoors . . . . . . . . . . . . . . . . . . . . . . . . . 83

6 Zusammenfassung und Ausblick 87

Kapitel 1

Einleitung

Mit Hilfe der Informatik können heutzutage viele komplexe Aufgaben wesentlich schnel-ler und zuverlässiger bewältigt werden, als dies durch Menschenhand möglich ist. Lässtman zum Beispiel von einem Navigationssystem die kürzeste Strecke von Tübingen nachPerugia berechnen, so wird die entsprechende Route schon nach wenigen Sekunden ange-zeigt. Es mag dadurch der Eindruck entstehen, als könnten Computer mittlerweile beliebigeAufgabenstellungen und Berechnungen grundsätzlich in kurzer Zeit lösen. Allerdings gibtes Problemstellungen in der Informatik, für die bisher weder effiziente Lösungsverfahrengefunden werden konnten noch bekannt ist, ob effiziente Verfahren überhaupt existierenkönnen.

Ein solches “schwieriges” Problem stellt das Satisfiability-Problem (kurz: Sat-Problem)dar, welches sich mit der Frage beschäftigt, ob die Werte der Variablen einer boolschen For-mel so gewählt werden können, dass die Formel wahr wird. Viele praktische und industrielleFragestellungen, deren enorme Komplexität von einem Menschen nicht mehr überschaubarist, lassen sich als Sat-Problem formulieren. So können zum Beispiel für das Lösen vonPlanungsproblemen [KS92], für das Symbolic Model Checking [BCCZ99], die Verifikationvon Hardware und für das Überprüfen von Automobilkonfigurationen [SKK00] entspre-chende Sat-Instanzen kodiert werden.Glücklicherweise lässt sich - im Gegensatz zu künstlich oder zufällig erzeugten Sat-In-stanzen - die Lösbarkeit oder Unlösbarkeit solcher Sat-Probleme oft durch systematisches“Durchprobieren” einiger Variablenbelegungen und strukturiertes Suchen beweisen. Dabeibasieren die meisten heutigen Lösungsmethoden auf dem DPLL-Verfahren, das in seinerGrundform schon im Jahr 1960 vorgestellt wurde. Die Tatsache, dass praktische Sat-Instanzen häufig sehr schnell gelöst werden können, wird dadurch begründet, dass solcheInstanzen über eine verborgene Struktur verfügen.

Betrachten wir als kleines Beispiel eine Schule, in der alle Lehrer vor Beginn des Schul-jahres ihre Wünsche bezüglich unterrichtsfreier Stunden angeben können. Diese Wünscheund die Verpflichtungen der Lehrer lassen sich dann als Sat-Problem formulieren, in-dem mindestens für jede Kombination aus Lehrer und Unterrichtsstunde eine Variable

1. EINLEITUNG 2

eingeführt wird, die angibt, ob der entsprechende Lehrer unterrichten muss oder eine Frei-stunde hat. MaierMo1 = true gibt somit an, dass Frau Maier montags in der ersten Stundeeine Unterrichtsverpflichtung wahrzunehmen hat. Ein kleiner Ausschnitt einer entsprechen-den Sat-Instanz, die alle Bedingungen enthält, könnte folgendermaßen aussehen:Da Herr Müller und Herr Neumann eine Fahrgemeinschaft bilden, wollen diese gerade inRandstunden stets gemeinsam eingesetzt werden. Daraus ergibt sich die BedingungB1 = ((H.MüllerMo1 ∧ NeumannMo1) ∨ (H.MüllerMo1 ∧ NeumannMo1)).Da Herr Neumann außerdem Referendar ist, muss dieser aus rechtlichen Gründen immergemeinsam mit seiner Mentorin Frau Müller unterrichten, wodurch die ForderungB2 = ((NeumannMo1 ∧ F.MüllerMo1) ∨ (NeumannMo1 ∧ F.MüllerMo1)) entsteht.Aus privaten Gründen möchten Frau und Herr Müller jedoch in der ersten Stunde nie beidearbeiten müssen, was sich durch B3 = (F.MüllerMo1 ∨ H.MüllerMo1) angeben lässt.Die Unterrichtsverpflichtungen fordern, dass eine bestimmte Klasse montags in der er-sten Stunde entweder von Herrn Müller oder von Frau Maier unterrichtet wird, was durchB4 = (H.MüllerMo1 ∨MaierMo1) ausgedrückt wird. Durch eine weitere Klasse entsteht dieBedingung B5 = (F.MüllerMo1 ∨WeberMo1).Da Frau Maier Rektorin und Herr Weber stellvertretender Rektor sind, sollte immer einervon beiden keine Unterrichtsverpflichtung haben, was sich schließlich durch die BedingungB6 = (MaierMo1 ∨WeberMo1) fordern lässt.

Allgemein gilt, dass die Wünsche und Verpflichtungen aller Lehrer genau dann verein-bar sind, wenn es für die Sat-Instanz eine Lösung gibt, wenn also eine gültige Belegungaller Variablen mit den Wahrheitswerten true oder false existiert, so dass die gesam-te Instanz erfüllt ist. Für den obigen Ausschnitt genügt es allerdings schon, nur HerrnMüller zu betrachten, um zu erkennen, dass das Sat-Problem keine Lösung haben kann:Soll Herr Müller montags in der ersten Stunde unterrichten, so ist H.MüllerMo1 = true.Aus B3 folgt daraus F.MüllerMo1 = false und wegen B1 gilt NeumannMo1 = true. Diesstellt aber einen Widerspruch zu der Bedingung B2 dar. Folglich sollte Herr Müller in derersten Stunde montags nicht unterrichten. Dadurch ergibt sich jedoch wiederum die fol-

gende widersprüchliche Implikationsfolge: H.MüllerMo1B4−→ MaierMo1

B6−→ WeberMo1B5−→

F.MüllerMo1B2−→ NeumannMo1

B1−→ H.MüllerMo1.

Im obigen Beispiel ist es somit ausreichend, eine kleine Menge an Variablen (hier sogarnur eine einzige Variable - H.MüllerMo1) zu betrachten, um die Lösbarkeit der gesamtenInstanz zu bestimmen. Diese Eigenschaft konnte schon in mehreren industriellen Instan-zen festgestellt werden: Oft genügt es, alle Belegungen einer kleinen Untermenge B derVariablen einer Instanz zu überprüfen, um entweder eine gültige Lösung für die gesamteInstanz zu finden oder aber zu zeigen, dass schon jede Belegung der Variablen aus B einenWiderspruch erzeugt. Eine solche Variablenmenge B wird als Backdoor-Menge bezeichnet[WGS03a]. Da das Konzept der Backdoors noch relativ jung ist, ergeben sich in diesemZusammenhang viele interessante Fragestellungen.

1. EINLEITUNG 3

Gliederung der Diplomarbeit

In der vorliegenden Diplomarbeit werden verschiedene Aspekte von Backdoor-Mengen inSat-Instanzen untersucht: Im nachfolgenden Kapitel werden zunächst einige Begriffe undgrundlegende Verfahren vorgestellt, die hauptsächlich aus dem Bereich des Sat-Solvingsstammen und für das weitere Verständnis erforderlich sind.

Das dritte Kapitel bildet den Hauptteil der Arbeit. Zunächst werden zahlreiche Back-doors für Sat-Instanzen aus dem Bereich der Automobilkonfiguration nach dem in [WGS03a]beschriebenen Verfahren berechnet, die hauptsächlich als Grundlage für die Analyse vonminimalen Backdoor-Mengen dienen, da die Berechnungsmethode schon das Lösen der je-weiligen Instanz erfordert. Im weiteren Verlauf des dritten Kapitels werden hingegen solcheAnsätze untersucht, die Backdoors vor dem eigentlichen Lösungsprozess ermitteln. Dabeiwird zunächst ein einfaches Verfahren vorgeschlagen, wodurch sich für einige industrielleSat-Instanzen die Menge der Backdoor-Variablen mit Hilfe einer polynomiellen Vorverar-beitungsroutine einschränken lässt.Anschließend wird das Konzept der Deletion Backdoors anhand der parametrisierten Be-rechnung von Binär- und Horn-Backdoors aus [NRS04] vorgestellt. Darauf basierend wer-den jeweils vier Methoden für die Approximation von Binär- und Horn-Backdoors vorge-schlagen und untersucht. Ferner wird ein Algorithmus zum Approximieren von R-Horn-Backdoors entwickelt und mit Resultaten des einzigen uns bekannten Verfahrens zur Be-rechnung von R-Horn-Backdoors [POSS06] verglichen.Sat-Instanzen, die sich aus industriellen Problemstellungen ergeben, stellen häufig nur eineErweiterung eines bestimmten Basis-Problems dar, das zum Beispiel Rahmenbedingungenoder physikalische Einschränkungen kodiert. Am Ende des dritten Kapitels werden Ideenpräsentiert und empirisch untersucht, wie verschiedene Backdoors eines Basis-Problems fürdie Lösung einer “Erweiterungs-Instanz” verwendet werden können.

Im vierten Kapitel wird eine weitere Anwendung des Backdoor-Konzeptes vorgeschla-gen. Zu diesem Zweck wird zunächst eine spezielle Unterklasse von 3-Sat definiert. Fürdiese Klasse wird dann ein vollständiges Lösungsverfahren vorgestellt, das hauptsächlichauf der Berechnung und Verwendung von verschiedenen Backdoors basiert und eine gerin-gere Komplexität als die aktuell schnellsten 3-Sat-Algorithmen aufweist.

Um die Struktur von Sat-Problemen auch visuell untersuchen zu können, wurde imRahmen dieser Diplomarbeit ein Programm entwickelt, das Sat-Instanzen auf verschiede-ne Arten visualisieren kann. Das fünfte Kapitel stellt die Funktionalität dieses Programmesvor und geht insbesondere auf die speziellen Möglichkeiten zur Visualisierung von Back-doors ein.

Im letzten Kapitel werden schließlich die wesentlichen Punkte und Ergebnisse dieserDiplomarbeit noch einmal zusammengefasst und ein Ausblick für Ansatzpunkte künftigerForschungen und Arbeiten gegeben.

Kapitel 2

Grundlagen

Dieses Kapitel soll einen Überblick über die nahezu 50-jährige Forschung im Bereich desSat-Solvings geben und damit eine Grundlage für das Verständnis der vorliegenden Di-plomarbeit schaffen. Darüber hinaus werden fundamentale Begriffe aus dem Gebiet derGraphentheorie und der parametrisierten Berechenbarkeit definiert und erläutert. Um einendetaillierteren Einblick in das Sat-Problem und dessen Lösungsverfahren zu erhalten, sindvor allem die Artikel [GPFW97] von Gu et al. und [ZM02] von Zhang und Malik empfeh-lenswert.

2.1 Das Erfüllbarkeitsproblem

Das Erfüllbarkeitsproblem der Aussagenlogik (satisfiability, Sat) stellt sowohl eine wichti-ge Problemstellung in der theoretischen Informatik als auch eine gängige Schnittstelle zwi-schen industriellen Anforderungen und computerbasierten Lösungsansätzen dar. Es werdenzunächst einige grundlegende Begriffe definiert (vgl. [Sin06, Leh05]).

2.1.1 Aussagenlogik

Eine Formel der Aussagenlogik besteht aus den folgenden Elementen:

• Variablen (V = {xi, xj, . . .}) sind Stellvertreter für beliebige atomare Aussagen wiez.B: “Die Schuhe sind grün”.

• Mit Hilfe der Junktoren ¬ (Negation), ∧ (Konjunktion) und ∨ (Disjunktion) könnenAussagen verknüpft werden1.

• Konstanten 0 (false) und 1 (true).

• Hilfssymbole wie Klammern.1Die weiteren Junktoren ⊕ (exklusives Oder), ⇒ (Implikation) und ⇔ (Äquivalenz ) werden hier nicht

weiter betrachtet, da sie insbesondere durch die oben genannten ausgedrückt werden können.

2.1. DAS ERFÜLLBARKEITSPROBLEM 5

Eine Abbildung τ : V 7→ {0, 1}, die allen Variablen Wahrheitswerte (boolsche Werte) zu-weist, wird als Variablenbelegung bezeichnet. Ist Φ die Menge aller Formeln über V , sokann die Bewertung einer Variablenbelegung τ0 durch eine Funktion evalτ0 : Φ 7→ {0, 1}rekursiv definiert werden:

evalτ0(x) = τ0(x) für x ∈ Vevalτ0(k) = k für Konstante k ∈ {0, 1}evalτ0(¬F ) = 1− evalτ0(F ) für F ∈ Φevalτ0(F ∨G) = max(evalτ0(F ), evalτ0(G)) für F, G ∈ Φevalτ0(F ∧G) = min(evalτ0(F ), evalτ0(G))

Eine boolsche Formel F ist genau dann erfüllbar, wenn es eine Variablenbelegung τ0 gibt,so dass evalτ0(F ) zu 1 (true) auswertet. Eine erfüllende Variablenbelegung wird auch alsModell bezeichnet.

2.1.2 Konjunktive Normalform

Eine sehr gebräuchliche Darstellung von boolschen Formeln ist die konjunktive Normal-form (KNF bzw. engl. CNF), in die jede Formel der Aussagenlogik transformiert werdenkann [Sin06]. Eine Sat-Instanz in konjunktiver Normalform besteht aus drei Komponenten(vgl. [GPFW97]):

• Eine Menge von n Variablen V = {x1, x2, . . . xn}

• Eine Menge von Literalen, wobei ein Literal mit positiver Polarität eine Variable(l = x) und ein Literal mit negativer Polarität die Negation einer Variablen (l = x)darstellt2.

• Eine Menge von m verschiedenen Klauseln C = {C1, C2 . . . Cm}, die durch denlogischen Operator ∧ verknüpft sind. Jede Klausel stellt eine Disjunktion (∨) vonLiteralen dar.

Durch den übersichtlichen Aufbau einer boolschen Formel F in KNF kann die Aussageüber die Erfüllbarkeit von F vereinfacht formuliert werden:F ist genau dann erfüllbar, wenn es eine Variablenbelegung gibt, so dass in jeder Klauselaus C mindestens ein Literal wahr ist. Weist eine Variablenbelegung τpart nur einer Un-termenge S ⊂ V Wahrheitswerte zu, so stellt τpart eine partielle Belegung für F dar.F [τpart] ist die verbleibende Instanz von F , die nur noch die Variablen V \ S und Klauselnenthält, die durch τpart nicht erfüllt werden.Im Folgenden werden Formeln grundsätzlich in konjunktiver Normalform betrachtet. Klau-seln aus C, die nur aus einem Literal bestehen, werden als Unit Klauseln bezeichnet.

2Die Polarität eines Literals wird häufig auch als (positive/negative) Phase oder Ausprägung bezeichnet.

2.2. DEFINITION VON GRAPHEN 6

Das DIMACS Dateiformat

Im Rahmen der DIMACS Challenge wurde ein Dateiformat (*.cnf ) zur Speicherung vonSat-Instanzen in konjunktiver Normalform entworfen, das in den meisten verfügbarenBenchmarks zum Einsatz kommt [Dim93]: Am Dateianfang können beliebig viele Kom-mentarzeilen stehen, die jeweils mit dem Zeichen c einzuleiten sind. Die gespeicherte In-stanz wird anschließend durch eine Problemzeile der Form ’p ’ grob beschrieben. Der Platzhalter entspricht in unserem Fall stetscnf, gibt die Anzahl der Variablen und die Anzahl der Klau-seln an.Unmittelbar auf die Problemzeile folgt die Beschreibung der Klauseln. Jede Klausel stellteine durch Leer-, Tab- oder Newline-Zeichen separierte Liste von Zahlen dar, die mit’ 0’ abgeschlossen wird. Jede Zahl z 6= 0 bezeichnet dabei ein Literal, wobei der Be-trag |z| die ID der entsprechenden Variablen angibt. Ist z negativ (Vorzeichen ’-’), sohat das Literal negative Polarität, anderenfalls (ohne Vorzeichen) positive Polarität. Diein Abbildung 2.1 gezeigten Beispiele stellen damit gültige Repräsentationen der FormelF = (x1 ∨ x2 ∨ x3) ∧ (x4 ∨ x2) ∧ (x1) dar:

c naheliegende Möglichkeit

p cnf 4 3

1 2 -3 0

-4 2 0

-1 0

c andere Variante

c x1 → 2, x2 → 3, x3 → 4, x4 → 1p cnf 4 3

2 3

-4 0 -1 3 0 -2 0

Abbildung 2.1: Beispiel DIMACS Format

2.2 Definition von Graphen

Im Kontext von Erfüllbarkeitsproblemen und deren Lösungsverfahren kommen Graphen inverschiedenen Bereichen zum Einsatz. Aus diesem Grund werden die notwendigen Begriffeim Folgenden definiert.

Ein Graph G = (VG, EG) ist ein Paar aus einer Menge von Knoten VG (vertices) und einerMenge von Kanten EG (edges), wobei EG ⊆ VG × VG eine Relation zwischen den Knotenbeschreibt3. Man unterscheidet gerichtete und ungerichtete Graphen. Bei ungerich-teten Graphen haben die Kanten keine bestimmte Richtung. Eine Kante (u, v) ∈ EG istnicht von einer Kante (v, u) unterscheidbar. Bei gerichteten Graphen werden solche Kantenhingegen unterschieden. Eine gerichtete Kante (u, v) hat die Quelle u ∈ VG und das Zielv ∈ VG. In der gesamten Arbeit werden durchweg einfache Graphen betrachtet, die keinegleiche Kante mehrfach enthalten.

3Der Index G für Knoten und Kanten wird verwendet, um eine Knotenmenge VG besser von einerVariablenmenge V unterscheiden zu können.

2.3. EIN POPULÄRES KONZEPT ZUR LÖSUNG VON SAT 7

Ein Knoten v ∈ VG ist adjazent zu einem Knoten u ∈ VG, wenn im Graphen eine Kante(u, v) ∈ EG existiert. Eine Kante (u, v) ∈ EG wird als inzident zu Knoten u bezeichnet.

Ein Pfad−−−→(u, v) von Knoten u ∈ VG zu einem Knoten v ∈ VG in einem Graphen G ist

eine Folge von Kanten−−−→(u, v) = [e1 = (u, w1), e2 = (w1, w2), . . . , el = (wl−1, v)] ∈ EG, wobei

wi 6= wj für alle i 6= j. Die Länge eines Pfades ist als die Anzahl der Kanten definiert.Ein Graph G wird als azyklisch bezeichnet, wenn für keinen Knoten v ∈ VG ein Pfad−−−→(v, v) existiert, dessen Länge größer null ist.

Ein Graph G heißt genau dann zusammenhängend (connected), wenn es für jedes belie-

bige Knotenpaar u, v ∈ VG einen Pfad−−−→(u, v) oder einen Pfad

−−−→(v, u) gibt.

Ist G zusammenhängend und azyklisch, so wird G auch Baum genannt. In einem Baum isteiner der Knoten aus VG als Wurzelknoten r (root) ausgezeichnet. Jeder von der Wurzel

verschiedene Knoten v eines Baumes ist durch genau einen Pfad pv =−−−→(r, v) mit der Wurzel

verbunden. Durch die Kante (w, v) ∈ pv wird der zu v adjazente Knoten w als Vorgängeroder Vater des Knotens v definiert. In einem Baum hat somit jeder Knoten aus VG \ {r}einen eindeutigen Vorgänger. Alle Knoten, für die ein Knoten w Vorgänger ist, werdenKinder von w genannt. Hat jeder Knoten eines Baumes maximal zwei Kinder, so handeltes sich um einen binären Baum. Die Tiefe eines Baumes entspricht der maximalen Längealler Pfade pv für alle Knoten v des Graphen.

Ein gerichteter Graph, in dem für jedes beliebige Knotenpaar v, w ∈ VG ein Pfad−−−→(v, w)

existiert, heißt stark zusammenhängend (strongly connected). Eine starke Zusam-menhangskomponente (strongly connected component) ist ein maximaler stark zusam-menhängender Teilgraph eines gerichteten Graphen G.Für jeden gerichteten azyklischen Graphen G gibt es eine topologische Sortierung derKnoten VG. Diese Sortierung beschreibt eine partielle Ordnung, so dass gilt: Liegt Knoten

u vor Knoten v, so gibt es keinen Pfad−−−→(v, u).

Ein beliebiger Graph G wird als k-partit bezeichnet, wenn sich alle Knoten des Graphenin k (0 < k < |VG|) disjunkte Mengen V1, V2, . . . , Vk einteilen lassen, so dass für beliebigeu, v ∈ Vj ∀ 1 ≤ j ≤ k keine Kante (u, v) ∈ EG existiert. Ein bipartiter Graph besteht auszwei (k = 2), ein tripartiter Graph aus drei (k = 3) disjunkten Knotenmengen, innerhalbderer keine Kanten vorhanden sind.

2.3 Ein populäres Konzept zur Lösung von SAT

Das Sat-Problem bildet den Kern der Klasse der NP -vollständigen Probleme [GPFW97].Bis zum heutigen Tag ist unbekannt, ob es Algorithmen geben kann, die solche hartnäckigen(intractable) Problemstellungen in Polynomzeit lösen. Spezialfälle von Sat, die zur KlasseP , der in Polynomzeit berechenbaren Probleme, gehören, werden in Abschnitt 2.5 erläutert.


In diesem Kapitel wird eines der am weitesten verbreiteten Verfahren zur Lösung von Sat-Problemen vorgestellt. Anschließend werden verschiedene Erweiterungen des ursprünglichenVerfahrens beschrieben, deren Verwendung in einigen der aktuell schnellsten Sat-Solvernam Ende des Kapitels geschildert wird.

2.3.1 Der reine DPLL-Algorithmus

Lange bevor Cook im Jahr 1971 die Klasse der NP -vollständigen Probleme einführte, ent-wickelten Davis und Putnam 1960 den ersten Algorithmus zum Lösen von Sat-Instanzenin konjunktiver Normalform [DP60]. Das damals vorgestellte Verfahren basiert auf dreiRegeln, von denen die zwei folgenden auch in den meisten heutigen Sat-Solvern nochimplementiert sind4:

Unit Propagation Enthält eine Formel F eine Unit Klausel C = (l), so ist F nurerfüllbar, wenn l wahr ist. Daher können alle Klauseln, die l enthalten, aus der Mengealler Klauseln C gelöscht werden (Subsumption5). Alle Vorkommen des Literals lkönnen aus den entsprechenden Klauseln gestrichen werden (Unit Resolution).

Pure Literal Rule oder auch Pure Literal Elimination. Ein Literal l einer Formel Fwird als pure bezeichnet, wenn das komplementäre Literal l in F nicht enthalten ist.Da die Variable eines pure Literals in F nur in einer Polarität vorkommt, kann derenWahrheitswert entsprechend dieser Polarität gesetzt werden. Alle Klauseln, die daspure Literal enthalten, werden subsumiert.

Die erläuterten Regeln lassen sich für eine Formel F so lange anwenden bis F weder UnitKlauseln noch Pure Literals enthält. Dieses Vorgehen wird meist als Boolean ConstraintPropagation oder allgemein Propagieren bezeichnet. Die Boolean Constraint Propagationkann in der Laufzeit O(|F |) durchgeführt werden (vgl. z.B. [dV00]), wobei die Größe einerFormel F durch die Summe der Klauselgrößen |F | =

∑C∈F |C| definiert ist.

Bei der Implementierung des ursprünglichen Algorithmus erwiesen sich die Speicheranfor-derungen der dritten, hier nicht beschriebenen Regel, als nicht realisierbar. Infolge des-sen ersetzten Davis, Logemann und Loveland diese Vorschrift durch die folgende, logischäquivalente, jedoch besser implementierbare Regel [DLL62]:

Branching Für eine beliebige Variable x ∈ V kann jede Formel F in die Form (A ∨ x)∧ (B ∨ x) ∧ R gebracht werden, wobei A, B, R boolsche Formeln sind, die x nichtenthalten. Ist x = true, so muss B ∧ R gelten, ist x = false, so muss A ∧ R erfülltsein.

4Die in [DP60] eingeführten Bezeichnungen der Regeln unterscheiden sich von den heute gebräuchlichen,in dieser Arbeit verwendeten Namen.

5Die hier erläuterte Regel stellt nur einen Spezialfall der Subsumption dar. Allgemein gilt, dass eineKlausel Ci eine andere Klausel Cj subsumiert, wenn die Literale von Ci eine Untermenge der Literale vonCj bilden [GPFW97].


Durch die Branching-Regel wird ein sogenannter Entscheidungsbaum aller möglichenVariablenbelegungen durchlaufen. Variablen einer boolschen Formel bilden Knoten imbinären Entscheidungsbaum. Die beiden Kanten (Zweige, engl. branches) zu den Kinderneines Knotens repräsentieren die Belegung einer entsprechenden Variablen mit true oderfalse.Bei der Implementierung des erweiterten Verfahrens wurde die Branching-Regel - damalsals Splitting Rule bezeichnet - dadurch realisiert, dass für eine gewählte Variable x beideSubformeln F ′ = B ∧ R und F ′′ = A ∧ R gebildet wurden, von denen eine zunächstauf Band gespeichert wurde. Konnte beim Lösungsprozess der ersten Subformel keinegültige Variablenbelegung gefunden werden, so wurde die zweite Subformel wieder vomBand geladen und weiter untersucht. Die Subformeln F ′ und F ′′ entsprechen im Entschei-dungsbaum gerade den beiden Teilbäumen von Knoten x. Spätere Implementierungen desDPLL-Algorithmus6 durchlaufen den Entscheidungsbaum wie in Algorithmus 1 geschildert.

Algorithmus 1 Mögliche Formulierung des DPLL-Verfahrens (vgl. [ZM02])

Eingabe: Boolsche Formel FAusgabe: “erfüllbar” oder “unerfüllbar”1: function dpll(F )2: status← preprocess( )3: while status /∈ {erfüllbar,unerfüllbar} do4: applyNextBranch( )5: while true do6: status← propagate( )7: if status 6= unerfüllbar then8: break9: else

10: blevel← analyzeConflict( )11: if(blevel = 0) then return unerfüllbar12: backtrack(blevel)13: end if14: end while15: end while16: return status17: end function

In Zeile zwei des Algorithmus 1 wird zunächst in einer Vorverarbeitung die FormelF mit Hilfe der Boolean Constraint Propagation so weit wie möglich vereinfacht. In deräußeren Schleife von Zeile drei bis fünfzehn wird der Suchraum so lange durchlaufen bisentweder eine Lösung gefunden wurde oder bewiesen ist, dass F nicht erfüllbar ist.

6Der Algorithmus wird in der Literatur sowohl als DP- (Davis-Putnam), DLL-(Davis-Logemann-Loveland) und DPLL-Algorithmus bezeichnet.


Zeile vier untersucht einen Zweig des Entscheidungsbaumes, indem eine noch nicht be-legte Variable x als Entscheidungsvariable (Decision Variable) gewählt und auf einenbestimmten Wahrheitswert b gesetzt wird. Dadurch können alle subsumierten Klauseln (indenen x mit Polarität b vorkommt) aus F entfernt und alle Vorkommen von x mit komple-mentärer Polarität aus F gestrichen werden. In Kapitel 2.3.2 werden einige Verbesserungendes DPLL-Verfahrens geschildert, die Heuristiken verwenden, um sowohl Entscheidungs-variablen als auch deren initialen Wahrheitswert möglichst geschickt zu wählen.In Zeile sechs werden die Konsequenzen der gemachten Variablenbelegung mit Hilfe derBoolean Constraint Propagation mit dem Ziel berechnet, den Suchraum möglichst zu ver-kleinern. Führt die Belegung zu keinem Konflikt (Zeile sieben), so wird die innere Schleifeverlassen (achte Zeile), um entweder eine weitere Entscheidungsvariable zu wählen oder,falls status = erfüllbar, die Suche zu beenden.Führt die Variablenbelegung jedoch zu einem Widerspruch (Zeile neun), so wird durchdie Funktion analyzeConflict untersucht, welche Entscheidung den Konflikt verursacht hatund auf welcher Ebene des Entscheidungsbaumes (blevel) eine andere Verzweigung möglichist. Dabei entspricht die i-te Ebene der i-ten Entscheidung, die Wurzel befindet sich alsoauf der ersten Ebene. Ist blevel = 0, so wurden für die erste Entscheidung beide Zweigedurchsucht, ohne eine gültige Variablenbelegung zu finden. F ist somit nicht erfüllbar (Zei-le elf).Ist blevel > 0, so werden durch das Backtracking in der zwölften Zeile alle Variablenbe-legungen aufgehoben, die seit der Belegung der Entscheidungsvariablen x auf Ebene bleveldes Entscheidungsbaumes gemacht wurden. Anschließend wird für x der komplementäreWahrheitswert gewählt. Das Backtracking entspricht somit dem Laden der zweiten Sub-formel vom Band, wie von Davis et al. beschrieben [DLL62]. Die neue Variablenbelegungwird nun durch die innere Schleife in Zeile sechs erneut propagiert.

Der reine DPLL-Algorithmus bietet mehrere Ansatzpunkte zur Optimierung. In derBeschreibung des DPLL-Verfahrens wurde schon angedeutet, dass die Wahl einer geeigne-ten Entscheidungsvariablen den Suchprozess beschleunigen kann und in manchen Fällendiesen erst realisierbar macht. Diese Möglichkeit der Optimierung wurde schon relativ balderkannt und bis heute gibt es zahlreiche Heuristiken zur Wahl von guten Entscheidungs-variablen. Darüber hinaus wird eine erhebliche Beschleunigung des Verfahrens durch dasKonzept erzielt, aus Fehlentscheidungen zu lernen. In den folgenden Abschnitten werdennun einige Verbesserungen des DPLL-Verfahrens vorgestellt.

2.3.2 Branching-Heuristiken

Um die Wahl einer Entscheidungsvariablen und deren initialen Belegung zu beeinflussen,ist es denkbar, vor der Ausführung des DPLL-Algorithmus die Variablen (oder Literale)nach einem bestimmten Kriterium zu sortieren. Kann eine Formel nicht weiter vereinfachtwerden, so wird bezüglich dieser Ordnung die nächste, noch nicht belegte Entscheidungs-variable gewählt. Ein solches Vorgehen hat den Vorteil, dass zusätzliche Berechnungen nureinmal zu Beginn des Lösungsprozesses anfallen. Die meisten Heuristiken ermitteln jedoch


die nächste Entscheidungsvariable und deren initialen Wert aufgrund der Menge der zudiesem Zeitpunkt unerfüllten Klauseln.

Greedy Heuristiken

Die frühen Branching-Heuristiken wie Bohm’s Heuristik, MOM, die Jeroslow-Wang Heu-ristik und die Literal Count Heuristiken können als Greedy-Verfahren bezeichnet werden,da Entscheidungen so getroffen werden, dass sich eine große Anzahl an Implikationen er-gibt oder möglichst viele Klauseln erfüllt werden [ZM02]. Marques-Silva beschreibt undevaluiert diese Heuristiken ausführlich [MS99].

Bohm’s Heuristik trifft Entscheidungen so, dass viele kleine Klauseln subsumiert werdenund gleichzeitig möglichst viele kleine Klauseln weiter verkleinert werden, um denEffekt der Unit Propagation zu vergrößern.

MOM ist ein Akronym für Maximum Occurrences on clauses of Minimum size. Es werdennur Variablen V ′ ⊆ V betrachtet, die in Klauseln mit minimaler Größe vorkommen.Aus V ′ werden solche Variablen bevorzugt, die in den meisten kleinen Klauseln vor-kommen.

Jeroslow-Wang Diese Methode berechnet für jedes Literal l einen Wert:

J(l) =∑

l∈C∧C∈C

2−|C|

Die one-sided Heuristik (JW-OS) wählt diejenige Zuweisung, die das Literal mit demgrößten Wert J(l) erfüllt. Die two-sided Heuristik (JW-TS) wählt die Variable x mitder größten Summe J(x) + J(x). Der initiale Wahrheitswert für x entspricht derPolarität des Literals mit größerem J-Wert.

Literal Count Heuristiken Für eine Variable x wird die Anzahl der noch unerfülltenKlauseln berechnet, in denen sie als positives (cp(x)) und in denen sie als negativesLiteral (cn(x)) vorkommt. Eine Strategie kann nun entweder beide Werte kombinierenoder getrennt betrachten.

Im kombinierten Fall, wird diejenige Variable xi gewählt, welche die größte Summecp(xi) + cn(xi) erzielt. Der initiale Wahrheitswert für xi entspricht cp(xi) ≥ cn(xi).Da die Werte für cp und cn bei jeder Variablenentscheidung neu berechnet werden,wird dieser Ansatz als dynamic largest combined sum (DLCS) bezeichnet.

Berücksichtigt man die Werte cp und cn getrennt, so wird die Variable xi gewählt,die den größten Wert für max(cp(xi), cn(xi)) erzielt. Wie bei DLCS entspricht dieinitiale Belegung für xi gerade cp(xi) ≥ cn(xi). Diese Strategie nennt man dynamiclargest individual sum (DLIS).

Da die Bestimmung der initialen Belegung für eine Entscheidungsvariable durchcp ≥ cn manchmal zu gierig (greedy) sein kann, stellt die zufällige (random) Wahl desersten Wahrheitswertes oft eine gute Alternative dar (RDLCS, RDLIS) [MS99].


Strukturbasierte Heuristiken

Die vorgestellten greedy Heuristiken zur Berechnung einer Variablenordnung verbessernden ursprünglichen DPLL-Algorithmus erheblich. Die ersten drei Strategien sind vor allemfür das Lösen von Zufallsinstanzen geeignet, erfassen jedoch nur wenige Informationen ausstrukturierten Instanzen [ZM02]. Sat-Instanzen, die aus realen Problemstellungen entste-hen, enthalten oft verborgene Strukturen. Strukturbasierte Heuristiken, die Entscheidungs-variablen aufgrund einer vorangegangenen Strukturanalyse auswählen und belegen, könnenfür solche Instanzen oft größere Geschwindigkeitsvorteile erzielen.

Gute Laufzeitverbesserungen, gerade für harte Instanzen, konnten von Aloul et al. durchdie Heuristiken MINCE [AMS01] und die verbesserte Variante FORCE [AMS03] erzieltwerden. Der Kerngedanke in beiden Ansätzen ist es, die Variablenordnung so zu wählen,dass voneinander abhängige Variablen nahe beieinander liegen.Zunächst wird eine beliebige initiale Variablenordnung gewählt. Ist post(x) die Positioneiner Variablen x in der Variablenordnung zum Zeitpunkt t, so wird für jede Klausel Cideren Schwerpunkt berechnet:

St(Ci) =1

|Ci|∑

x∈Ci∨x∈Ci

post(x)

Sei N(x) ⊆ C die Menge aller Klauseln, in denen entweder das Literal x oder x enthaltenist. Die neue Position einer Variablen ergibt sich dann aus dem gerundeten Wert für:

post+1(x) =1

|N(x)|∑

C∈N(x)

St(C)

Dieser Prozess wird solange wiederholt bis sich entweder keine Veränderungen der Posi-tionen von Variablen mehr ergeben oder eine bestimmte Menge an Umpositionierungen(Größenordnung ≈ log |V|) durchgeführt wurde.

Huang und Darwiche stellen in dem Artikel A Structure-Based Variable Ordering Heu-ristic for SAT ein divide and conquer Verfahren zur Bestimmung einer guten Variablen-ordnung vor [HD03]. Diese Heuristik basiert zunächst auf der Tatsache, dass unabhängigeTeilprobleme einer Sat-Instanz getrennt gelöst werden können (vgl. dazu auch [Leh05]).Die Menge der Klauseln C einer Instanz F wird willkürlich in zwei Mengen CL und CReingeteilt. Seien VL und VR die Mengen der Variablen, die in den Klauseln aus CL bzw.CR vorkommen. Im Lösungsprozess werden Entscheidungsvariablen zunächst nur aus derVariablenmenge VL ∩ VR gewählt. Wird in dieser Phase festgestellt, dass F nicht lösbarist, so terminiert der Algorithmus. Anderenfalls sind alle Variablen aus VL ∩ VR belegt,wodurch die resultierenden Teilprobleme C ′L und C ′R nun aus disjunkten Variablenmengenbestehen und dadurch getrennt gelöst werden können.


Ein weiterer Ansatz zur Verwendung von Strukturinformationen wird von Lehmann7

vorgestellt [Leh06]. Dort werden verschiedene graphische Repräsentationen einer Sat-Instanz betrachtet. Für diese Graphen werden mehrere Zentralitätsmaße aus der Graphen-theorie berechnet, um die Bedeutung von Variablen oder Literalen einzustufen. Basierendauf den ermittelten Zentralitätswerten von Variablen und Literalen werden Entscheidungs-variablen und deren initiale Belegung ausgewählt.

Konfliktgesteuerte Heuristiken

Durch die Implementierung des Sat-Solvers Chaff wurde 2000 eine neuartige Variablen-heuristik vorgestellt, die sich in ähnlicher Form in den meisten aktuellen Sat-Solvern eta-bliert hat [MMZ+01]. Die VSIDS Entscheidungsheuristik (Variable State Independent De-caying Sum) bewertet Literale anhand deren Beteiligung an Konflikten:

1. Jedes Literal hat einen auf null initialisierten Aktivitätszähler.

2. Führt eine Variablenbelegung zu einem Konflikt, so wird der Zähler jedes mitverur-sachenden Literals erhöht (siehe Klausellernen, Kapitel 2.3.3).

3. Die Variable des Literals lmax mit dem höchsten Aktivitätswert wird als Entschei-dungsvariable gewählt und so initialisiert, dass lmax wahr ist. Bei Gleichstand wirdzufällig entschieden.

4. In periodischen Zeitabständen werden alle Zähler durch eine Konstante dividiert.

Eine Variante der VSIDS-Heuristik, die in den Solvern Satzoo und MiniSat implementiertist, unterscheidet nicht zwischen den beiden Literalen einer Variablen und verwendet jeweilsnur einen Zähler pro Variable [ES03]. Durch die VSIDS Strategie werden solche Entschei-dungsvariablen gewählt, die häufig an Konflikten beteiligt sind. Besonders für unerfüllbareInstanzen kann dadurch eine immense Laufzeitersparnis erzielt werden. Die Division durcheine Konstante im vierten Schritt führt dazu, dass neuere Erhöhungen des Aktivitätswertesstärker ins Gewicht fallen als ältere.

2.3.3 Aus Konflikten lernen

Eine der weitreichendsten Verbesserungen des DPLL-Verfahrens wurde 1996 von Marques-Silva und Sakallah durch die Entwicklung eines generischen Sat-Algorithmus - GRASP- erreicht8. Bereits im vorigen Abschnitt wurde die Idee, aus Konflikten zu lernen, imZusammenhang mit Branching-Heuristiken vorgestellt. Dieses Unterkapitel beschreibt zweizentrale Ansätze des GRASP Verfahrens, wie aus Konflikten Informationen extrahiertwerden können, um den verbleibenden Suchprozess zu beschleunigen.

7Mittlerweile Zweig.8Da GRASP durch die Verwendung von Methoden aus der Künstlichen Intelligenz erhebliche

Veränderungen eingeführt hat, ist sich die Fachwelt uneins, ob heutige Sat-Solver tatsächlich noch aufdem DPLL-Verfahren beruhen.


Generieren von Konfliktklauseln

Voraussetzung des Lernens aus Konflikten ist es, zunächst die Ursache eines Konfliktesauszumachen. Nach der Ermittlung der Ursache eines Konfliktes kann Lernen dadurchstattfinden, dass eine zusätzliche Bedingung für die Belegungen der Variablen in Form ei-ner Klausel formuliert und zur ursprünglichen Formel hinzugefügt wird. Eine solche Klau-sel, die auch als Lemma bezeichnet wird, dient der Vermeidung der gleichen fehlerhaftenVariablenbelegung in anderen Bereichen des Suchraumes. Diese Idee soll nun an einemBeispiel verdeutlicht werden, das in vereinfachter Form aus [MSS96] übernommen wurde.

C1

C2

C2

C3

C3

C5

C4

C4

C6

x1@6

x9@1

x3@6

x10@3

x2@6 x6@6

x6@6

x5@6

x4@6

a) b)

C1 = (x1 ∨ x2)C2 = (x1 ∨ x3 ∨ x9)C3 = (x2 ∨ x3 ∨ x4)C4 = (x4 ∨ x5 ∨ x10)C5 = (x4 ∨ x6)C6 = (x5 ∨ x6)

Abbildung 2.2: Beispiel eines Implikationsgraphen für die Generierung einer Konfliktklausel

Betrachten wir die Formel F , welche unter anderem die in Abbildung 2.2 b) aufgeliste-ten Klauseln C1 bis C6 enthält. Wir gehen davon aus, dass im bisherigen Lösungsprozessvon F der Variablen x9 auf der ersten Entscheidungsebene der Wert false zugewiesenwurde (x9@1). Ferner hat Variable x10 den Wert false auf der Entscheidungsebene drei er-halten (x10@3). Die weiteren bisherigen Belegungen können für dieses Beispiel außer Achtgelassen werden.Nun wählt der aktuelle Lösungsprozess - auf Entscheidungsebene sechs - die Variable x1 alsEntscheidungsvariable und initialisiert diese mit dem Wert true (x1@6). Abbildung 2.2 a)zeigt den Implikationsgraphen, der den Effekt dieser Variablenzuweisung repräsentiert.Jeder Knoten entspricht der Zuweisung eines Wahrheitswertes für eine Variable. Die gerich-teten Kanten des Graphen entsprechen Implikationen, die sich daraus ergeben, dass durchdie aktuelle Variablenbelegung in manchen Klauseln jeweils nur noch ein Literal übrig ist,durch den diese erfüllt werden können.Mit der Wahl des Wertes true für Variable x1 muss durch Klausel C1 die Variable x2 eben-falls auf true gesetzt werden. Diese Zuweisung findet auf der gleichen Entscheidungsebenestatt, weshalb der Knoten [x2@6] erzeugt wird. Die Kante von [x1@6] nach [x2@6] wirdmit dem Namen der Klausel beschriftet (C1), die diese Zuweisung fordert. Da die Wertex9 = false und x1 = true feststehen, folgt durch Klausel C2, dass Variable x3 ebenfalls den


Wert true erhält. Dadurch werden die Kanten ([x1@6],[x3@6]) und ([x9@1],[x3@6]) erzeugt.Führt man die Kette an Implikationen fort, so entsteht ein Konflikt für die Belegung derVariablen x6.

Eine Möglichkeit, die Ursache für den entstandenen Konflikt zu bestimmen, bestehtdarin, die Kanten des Graphen, ausgehend vom Konfliktknoten, rückwärts zu durchlaufen.Alle so erreichbaren Knoten, die selbst keine eingehenden Kanten haben, repräsentierendiejenigen Entscheidungen, die für den Konflikt verantwortlich sind. In Abbildung 2.2 a)stellt somit die Wahl von x9 = false, x10 = false und x1 = true eine Ursache für denentstandenen Konflikt dar. Als Bedingung kann dadurch festgehalten werden, dass entwe-der x9 = true oder x10 = true oder x1 = false gelten muss. Diese Feststellung kann mitder Erweiterung der ursprünglichen Formel durch die Klausel K1 = (x9 ∨ x10 ∨ x1) für denverbleibenden Suchprozess gelernt werden.Beame et al. untersuchen die Idee des Lernens von Konfliktklauseln im Detail [BKS03].Dabei wird das soeben beschriebene Verfahren zur Generierung von Konfliktklauseln erwei-tert, wodurch nicht immer Klauseln entstehen, die nur Entscheidungsvariablen enthalten.Diese Erweiterung ist in den meisten aktuellen Sat-Solvern implementiert, ist jedoch fürdas Verständnis der vorliegenden Arbeit nicht weiter relevant.

Backjumping statt Backtracking

Die Analyse des Implikationsgraphen bei der Entstehung eines Konfliktes erlaubt eineweitere entscheidende Verbesserung des Lösungsprozesses. Dadurch ist es in vielen Fällenmöglich, die Untersuchung größerer Teilbäume des Entscheidungsbaumes komplett einzu-sparen. Dies wird deutlich, wenn man das Beispiel des vorigen Abschnitts weiter verfolgt[MSS96].

Da die Entscheidung, die Variable x1 = true zu setzen, zu einem Konflikt geführthat, weist ein DPLL-basierter Solver als direkte Konsequenz der Variablen x1 den Wertfalse zu. Angenommen die Formel F enthält zusätzlich zu den in Abbildung 2.2 b) auf-gelisteten Klauseln noch die in Abbildung 2.3 b) genannten Klauseln C7, C8 und C9. Derzugehörige Implikationsgraph in Abbildung 2.3 a) zeigt, dass mit dieser Belegung ein wei-terer Konflikt entsteht. An dieser Stelle ist es wichtig zu beachten, dass die Belegungx1 = false keine Entscheidung sondern vielmehr eine Folgerung des Konfliktes der Bele-gung x1 = true darstellt (Failure-Driven Assertion). Damit wird die Belegung x1@6 vonden Zuweisungen x9 = false und x10 = false impliziert, weshalb der Implikationsgraph inAbbildung 2.3 a) die Kanten ([x9@1],[x1@6]) und ([x10@3],[x1@6]) enthält.

Mit der oben beschriebenen Methode lassen sich für diesen Konflikt die Entscheidun-gen x9@1 und x10@3 verantwortlich machen, was durch die Konfliktklausel K2 = (x9∨x10)gelernt werden kann. Da die Belegung x9 = false auf der ersten Ebene und die Belegungx10 = false auf der dritten Ebene gewählt wurde, ist klar, dass die Ursache des Kon-fliktes mindestens schon auf Ebene drei (oder früher) zu suchen ist. Es macht demnach


C8

C7

C9

C9

K1

K1

x10@3

x9@1

x1@6

x7@6

x8@6

a) b)

C1 . . . C6K1 = (x9 ∨ x10 ∨ x1)C7 = (x1 ∨ x7)C8 = (x1 ∨ x8)C9 = (x7 ∨ x8 ∨ x9)

Abbildung 2.3: Beispiel eines Implikationsgraphen für non-chronological Backjumping

keinen Sinn, wenn der Lösungsprozess die Entscheidungen für die Belegungen der Varia-blen auf den Ebenen fünf und vier umkehrt, wie dies durch das ursprüngliche Backtrackinggemacht wird. Die Lösungssuche kann beschleunigt werden, indem sofort auf die dritteEntscheidungsebene zurück gesprungen wird (non-chronological Backjumping). Betrachtetman allgemein die Entscheidungsebenen der Literale in der Konfliktklausel, so gibt dergrößte Wert die Entscheidungsebene für das Backjumping an.

2.3.4 Random Restarts

Ein leicht zu implementierendes, aber dennoch sehr mächtiges Konzept bieten Neustarts(restarts) nach einer gewissen Zeit “erfolglosen” Suchens. Trotz guter Variablenheuristi-ken, Lernmechanismen und Backjumping kann es sein, dass der Lösungsprozess in einenungünstigen Bereich des Suchraumes gelangt, in dem Konflikte grundsätzlich erst nachvielen Entscheidungen auftreten und dennoch kein Backjumping möglich ist. Um solcheBereiche nicht komplett durchsuchen zu müssen, wird nach einer bestimmten Zeit, einerbestimmten Anzahl an Entscheidungen oder bei Überschreiten einer maximalen Tiefe desEntscheidungsbaumes ein Neustart durchgeführt.Neustarts bergen prinzipiell die Gefahr, dass die Unlösbarkeit einer Formel nicht festgestelltwerden kann, falls die Suche immer abgebrochen wird, bevor die Unlösbarkeit bewiesen ist.Um ein vollständiges Lösungsverfahren zu gewährleisten, wird das Kriterium, durch wel-ches ein Neustart herbeigeführt wird, bei jedem Neustart abgeschwächt [MSS96, MMZ+01].

Damit ein erneuter Suchprozess erfolgreicher verlaufen kann als die vorangegangeneSuche, wird zufällig ein neuer Ausgangspunkt, z.B. eine neue Variablenordnung, gewählt.Darüber hinaus können gelernte Informationen, wie hinzugefügte Konfliktklauseln oderAktivitätswerte von Variablen, wiederverwendet werden. Die genaue Konfiguration kannbei den meisten Sat-Solvern als optionales Argument angegeben werden und es scheint alsgäbe es keine Konfiguration, die für alle Instanzen optimal ist [MMZ+01].

2.4. LOKALE SUCHE - EINE ALTERNATIVE ZU DPLL 17

2.3.5 Implementierungen von SAT-Solvern

Die meisten der aktuellen effizienten Sat-Solver basieren auf dem DPLL-Verfahren unddem erweiterten GRASP-Algorithmus. Seit der Implementierung von Chaff im Jahr 2000wurden erhebliche Fortschritte auf dem Gebiet des Sat-Solvings erzielt [Bie07]. Sowohldie VSIDS Heuristik als auch das Klausellernen in Verbindung mit dem non-chronologicalBackjumping sind in den Sat-Solvern MiniSat [ES03], PicoSat [Bie07] und RSat reali-siert.Alle drei Programme, die zu den aktuell schnellsten Sat-Solvern zählen [Sat07], berech-nen keine besondere initiale Ordnung der Variablen, da die VSIDS Heuristik schon nachwenigen Konflikten eine gute Variablenordnung ermittelt. Um resistent gegen schlechteinitiale Variablenordnungen zu sein, führt MiniSat standardmäßig relativ schnell einen er-sten Neustart durch (nach 100 Konflikten), behält dabei aber die gelernten Klauseln bei.Die größte Verbesserung von PicoSat gegenüber MiniSat wurde durch die Verwendungvon verschiedenen Datenstrukturen für das Speichern von Binärklauseln und Klauseln mitmindestens drei Literalen erzielt [Bie07]. Dadurch wird die Durchführung der BooleanConstraint Propagation beschleunigt, die in DPLL-basierten Implementierungen ungefähr80% der gesamten Laufzeit beansprucht [MMZ+01].

2.4 Lokale Suche - Eine Alternative zu DPLL

Auch wenn viele der aktuellen Implementierungen als Erweiterung des DPLL-Verfahrensbetrachtet werden können, so gibt es auch völlig andere Ansätze zur Lösung von Sat-Problemen. Im Folgenden wird ein weiteres Konzept erläutert, das in dieser Arbeit jedochnur eine untergeordnete Rolle spielt.

Die lokale Suche stellt ein nicht vollständiges Verfahren zur Lösung von Sat-Instanzendar. Das heißt, dass eine lokale Suche für eine lösbare Probleminstanz F oft schnell eineerfüllende Belegung der Variablen findet. Wird jedoch kein Modell gefunden, so kann dar-aus nicht mit absoluter Sicherheit die Unerfüllbarkeit von F geschlossen werden [SKC93].Der Kerngedanke der lokalen Suche ist es, von einer beliebigen Variablenbelegung aus-zugehen und diese Belegung schrittweise so zu verändern, bis schließlich alle Klauselnder Instanz erfüllt sind oder eine bestimmte maximale Zeitspanne verstrichen ist. Dieseschrittweise Annäherung an eine erfüllende Belegung wird dadurch realisiert, dass die Be-legung einer Variablen, die nach einem bestimmten Kriterium ausgewählt wird, geflipptwird [Sin06].

Durch die Publikation des GSat-Algorithmus von Selman et al. wurden 1992 die dama-ligen DPLL-basierten Solver gerade für harte Zufallsinstanzen oft bei weitem übertroffen[SLM92]. GSat wählt gierig eine solche Variable, die durch das Flippen ihrer Belegung diegrößte Steigerung der Anzahl an erfüllten Klauseln verursacht. 1993 wurde dieses Verfah-ren durch den Algorithmus WalkSat verbessert, der die Idee der Random Walk Strategie

2.5. HANDHABBARE UNTERKLASSEN DES SAT-PROBLEMS 18

aufgreift [SKC93]. Das von Papadimitriou vorgestellte Random Walk Verfahren für 2-Sat-Instanzen startet mit einer zufälligen Variablenbelegung, wählt per Zufall ein Literal auseiner unerfüllten Klausel und flippt die Belegung der entsprechenden Variablen.WalkSat vereint beide Strategien, indem mit konstanter Wahrscheinlichkeit p (für 0 < p < 1)zufällig eine Variable x gewählt wird, die in einer unerfüllten Klausel vorkommt. Der bis-herige Wert von x wird daraufhin geflippt. Mit Wahrscheinlichkeit 1− p wird gemäß demGSat-Verfahren gehandelt.

Ähnliche Vorgehensweisen finden oft Anwendung bei der Berechnung von Max-SatProblemstellungen, bei denen es darum geht, eine möglichst große Menge von Klauseln zuerfüllen. In Kapitel 3.4 wird die Idee von WalkSat in einem anderen Kontext verwendet.

2.5 Handhabbare Unterklassen des SAT-Problems

Wie eingangs erwähnt, gibt es Unterklassen des Sat-Problems, die nicht NP -hart sind undin vielen Fällen sogar in Linearzeit gelöst werden können. Solche Klassen spielen geradeim Zusammenhang mit Backdoors eine zentrale Rolle. Eine detaillierte Darstellung derbekanntesten, in Polynomzeit lösbaren Unterklassen des Sat-Problems wurde von Francound Van Gelder veröffentlicht [FG03].

2.5.1 2-SAT

Im Jahr 1979 publizierten Aspvall et al. einen Algorithmus, der die Erfüllbarkeit von 2-Sat-Instanzen9, in denen jede Klausel aus maximal zwei Literalen besteht, in Linearzeitberechnet [APT79]. Der Algorithmus erzeugt zunächst einen (gerichteten) Implikations-graphen, in dem alle Literale einer Formel F durch Knoten repräsentiert werden. EineKlausel (l1∨l2) ∈ F erzeugt die beiden gerichteten Kanten (l1, l2) und (l2, l1). Damit stellendie Kanten die beiden folgenden Implikationen dar:

• Wenn Literal l1 nicht erfüllt ist, dann muss Literal l2 erfüllt sein.

• Wenn Literal l2 nicht erfüllt ist, dann muss Literal l1 erfüllt sein.

Mit Hilfe des Algorithmus von Tarjan werden nun die starken Zusammenhangskomponen-ten des Graphen berechnet [OW02, Kap. 8]. Wie in Abbildung 2.4 b) dargestellt, wird jedeKomponente zu einem Knoten verschmolzen. Die Formel ist genau dann erfüllbar, wennvon keiner Variablen beide Ausprägungen (positives und negatives Literal) in der gleichenKomponente liegen. Befinden sich keine komplementären Literale in einem verschmolzenenKnoten, dann kann ein Lösungsmodell gefunden werden, indem die Knoten topologischsortiert werden. Beginnend mit dem letzten Knoten der Sortierung, werden alle noch nichtbelegten Variablen so gesetzt, dass die Literale des Knotens wahr werden.

92-Sat wird auch als Binary-Sat oder quadratic-Sat bezeichnet.


�

� - -

- -

6

?

6

?

SS

So��

SS

So ��

~~~ ~~

~ ~ ~~

~

x1

x2

x5

x4 x2

x1x3x4

x5

x3

a)

HHHHHHj

��

HHHHHHj

��

~~

~~

x1, x2

x3, x4, x5

x3, x4, x5

x1, x2

b)

Abbildung 2.4: Implikationsgraph von Aspvall. Quelle [Sin06].F = (x1 ∨ x2) ∧ (x1 ∨ x2) ∧ (x3 ∨ x4) ∧ (x4 ∨ x5) ∧ (x5 ∨ x3) ∧ (x3 ∨ x1) ∧ (x4 ∨ x2). EinModell ist durch die Belegung x3, x4, x5 (letzter Knoten der topologischen Sortierung in b)und x1, x2 (möglicher vorletzter Knoten in b) gegeben.

Ein weiteres Verfahren zum Lösen von 2-Sat-Problemen wurde von del Val entwickelt,welches sich aufgrund der Ähnlichkeit zum oben beschriebenen DPLL-Algorithmus in vie-len Fällen besser für die Integration in aktuelle Sat-Solver eignet [dV00]. Dieses Verfahrenunterscheidet zwischen einer temporären und einer endgültigen Belegung von Variablen.Führt die temporäre Belegung einer Variablen xi zu einem Konflikt, so wird die komple-mentäre Belegung für xi endgültig propagiert, ohne die temporäre Belegung durch Back-tracking explizit rückgängig zu machen.

2.5.2 Horn-SAT

Eine weitere Unterklasse von Sat, die in Linearzeit lösbar ist, stellt die Klasse Horn dar[Bor99]. Eine Klausel wird als Hornklausel bezeichnet, wenn sie höchstens ein positives Li-teral enthält. Eine boolsche Formel in konjunktiver Normalform heißt Horn-Formel, wennsie nur Hornklauseln enthält. Die vorteilhafte Eigenschaft an dieser Problemklasse ist,dass Horn-Instanzen mit Hilfe der Boolean Constraint Propagation gelöst werden können[Sin06]. Horn-Formeln spielen auch auf dem Gebiet der Experten Systeme eine große Rolle.

Die Klauseln einer Formel F ∈ Horn lassen sich in drei Kategorien einteilen:

Fakten sind diejenigen Unit Klauseln mit einem positiven Literal.

Regeln sind solche Klauseln, die aus einem positiven und mindestens einem negativenLiteral bestehen.

Ausschlusskriterien stellen solche Klauseln dar, die kein positives Literal enthalten.


Sei beispielsweise F = (x1) ∧ (x1 ∨ x2) ∧ (x1 ∨ x2 ∨ x3) ∧ (x3 ∨ x1) eine Horn-Formel. DieErfüllbarkeit von F kann nun wie folgt überprüft werden:Zu den Fakten in F zählt nur die Klausel (x1), die angibt, dass die Variable x1 auf true ge-setzt werden muss. Mit der Regel (x1∨x2) folgt, dass auch Variable x2 den Wahrheitswerttrue haben muss. Die weitere Regel (x1 ∨ x2 ∨ x3) fordert Variable x3 auf true zu setzen.Wurden sämtliche Regeln angewandt, so wird überprüft, ob ein Widerspruch zu einem derAusschlusskriterien besteht. In diesem Fall wird die Klausel (x3 ∨ x1) nicht erfüllt, wasbeweist, dass F nicht erfüllbar ist.

Enthält eine Formel keine Unit Klauseln mit positiven Literalen, so ist die Menge derFakten leer, wodurch die Erfüllbarkeit der Formel direkt folgt. Da jede Klausel minde-stens ein Literal mit negativer Polarität enthält, lässt sich in diesem Fall ein erfüllendesModell dadurch erzeugen, indem allen Variablen der Wahrheitswert false zugewiesen wird.

Die Klasse der Horn-Formeln wurde in mehrere Richtungen erweitert (vgl. [FG03]).Die einfachste Erweiterung stellt dabei die Klasse Renamable Horn dar. Eine boolscheFormel F wird als Renamable Horn10 (R-Horn) bezeichnet, wenn eine VariablenmengeV ′ ⊆ V existiert, so dass durch das “Flippen” aller Literale der Variablen v ∈ V ′ eineHorn-Instanz erzeugt werden kann. Flippen der Literale x, x einer Variablen x bedeutet,dass alle Vorkommen von x durch x und alle Vorkommen von x durch x ersetzt werden.Formeln der Klasse R-Horn können somit auch in Linearzeit gelöst und erkannt werden[Bor99, dV00]. In Kapitel 3.4 wird eine noch umfassendere Erweiterung von Horn vorgestelltund angewandt.

2.5.3 Matched Formulas

Diese Klasse von Formeln wird unter Verwendung einer graphischen Repräsentation vonSat-Instanzen definiert (vgl. [FG03]). In Kapitel 5 werden verschiedene graphische Dar-stellungen von Sat-Problemen vorgestellt und erläutert.

Für eine Formel F in konjunktiver Normalform betrachten wir den ungerichteten bi-partiten Graphen CV mit den beiden Knotenmengen VC und VV . Die Knoten in VC re-präsentieren die Klauseln, die Knoten in VV die Variablen der Formel F . Eine Kante zwi-schen einem Knoten vi ∈ VV der Variablen xi ∈ V und einem Knoten cj ∈ VC der KlauselCj ∈ C existiert genau dann, wenn xi in positiver oder negierter Form in Cj enthalten ist.

Ein totales Matching für Klauseln in CV ist eine Untermenge M der Kanten inCV , so dass jeder Knoten in VC inzident zu einer Kante aus M und jeder Knoten aus VVinzident zu höchstens einer Kante aus M ist. Es gilt also |C| ≤ |V|. Die Formel F wirdgenau dann als matched bezeichnet, wenn es ein totales Matching für die Klauseln gibt.

10In manchen Artikeln wird Renamable-Horn auch als Disguised-Horn bezeichnet.

2.6. BACKBONES UND BACKDOORS 21

Ein totales Matching für den bipartiten Graphen CV lässt sich mit Hilfe von Netz-werkflussalgorithmen in Polynomzeit berechnen [OW02, Kap. 8]. Nach Rosenberg ist jede“matched Formula” erfüllbar. Ein gültiges Modell für eine solche Formel ist direkt durchdas Matching M gegeben: Der Wahrheitswert jeder Variablen, die am Matching beteiligtist, wird so gewählt, dass dadurch die mit ihr verbundene Klausel erfüllt ist. Da nach derDefinition des totalen Matchings jede Variable mit maximal einer Klausel verbunden istund jede Klausel von einer Variablen erreicht wird, kann F durch diese Belegung erfülltwerden.

2.6 Backbones und Backdoors

Die Ergebnisse der jüngsten Sat-Competition [Sat07] verdeutlichen ein bekanntes, aberdennoch interessantes Phänomen, das beim Lösen von Sat-Problemen immer wieder zubeobachten ist: Auf der einen Seite schaffen es aktuelle Sat-Solver, industrielle Problemin-stanzen mit mehr als einer Million Klauseln in wenigen Sekunden zu lösen, auf der anderenSeite konnte eine Instanz mit 117 Variablen und 244 Klauseln von keinem Programm in-nerhalb der vorgegebenen Zeit (10000 Sekunden) gelöst werden.Dieser Unterschied wird oft dadurch erklärt, dass praktische Sat-Instanzen verborgeneStrukturen aufweisen, wodurch eine Lösung oft in nahezu linearer Zeit ermittelt werdenkann. In diesem Kapitel werden zwei relativ neue Strukturmaße - Backbones und Back-doors - definiert.

Eine Variable x einer Instanz F wird als Backbone-Variable bezeichnet, wenn diesein jeder erfüllenden Variablenbelegung für F den gleichen Wert annimmt. Solche Varia-blen werden auch “frozen variables” genannt [MZK+99]. Diese Variablen sind vor allemnützlich, um den Lösungsraum eines Erfüllbarkeitsproblems zu untersuchen. Eine MengeS ⊆ V ist ein Backbone, wenn es eine eindeutige Belegung τS der Wahrheitswerte für dieVariablen in S gibt, so dass die verbleibende Instanz F [τS] erfüllbar ist [WGS03a].

Das Konzept der Backdoors wurde 2003 von Williams et al. eingeführt [WGS03a,WGS03b]. Die folgende, etwas vereinfachte Definition stammt jedoch von Nishimura et al.[NRS04]:Backdoor-Mengen (kurz: Backdoors) werden bezüglich einer Basisklasse C definiert, dieeine bestimmte Menge von Sat-Formeln beschreibt. Dabei müssen Instanzen einer KlasseC von einem sogenannten Subsolver in Polynomzeit erkennbar und deren Erfüllbarkeit inPolynomzeit berechenbar sein. Sei F eine boolsche Formel und B ⊆ V eine Menge vonVariablen in F , dann gilt:

• B ist ein schwaches C-Backdoor (Weak C-Backdoor) wenn eine Zuweisung vonWahrheitswerten τ : B 7→ {false, true} existiert, so dass F [τ ] erfüllbar ist und zurKlasse C gehört.

• B ist ein starkes C-Backdoor (Strong C-Backdoor), wenn F [τπ] für jede Zuweisungvon Wahrheitswerten τπ : B 7→ {false, true} zur Klasse C gehört.

2.7. PARAMETRISIERUNG VON ALGORITHMEN 22

2.7 Parametrisierung von Algorithmen

Im Kontext mehrerer Problemstellungen, die mit dem Erfüllbarkeitsproblem einher gehen,spielen parametrisierte Algorithmen eine immer größer werdende Rolle. Daher wollen wirzum Abschluss des Grundlagenkapitels einen knappen Einblick in dieses Konzept geben(vgl. [Nie02]).Fixed Parameter Tractable Algorithmen (FPT) stellen einen der bekannten Ansätze dar,um mit NP -vollständigen Problemstellungen umzugehen. Dabei ist der grundlegende Ge-danke, dass viele dieser Problematiken an einen nicht negativen ganzzahligen Parameterk gebunden sind. In der Praxis gibt es oft Fragestellungen, bei denen eine Lösung nur biszu einer bestimmten Größe von Interesse ist. Formell kann dies folgendermaßen definiertwerden:

Definition Ein parametrisiertes Problem L ist “fixed parameter tractable”, wenn die Fra-ge “(x1, x2) ∈ L?” innerhalb der Laufzeit f(|x2|) ∗ |x1|O(1) entschieden werden kann, wobeif eine beliebige Funktion auf nicht negativen Ganzzahlen ist. Die entsprechende Komple-xitätsklasse nennt sich FPT. 11

Im Rahmen dieser Arbeit treten zwei bestimmte NP -vollständige Problematiken, fürdie effiziente parametrisierte Algorithmen zur Verfügung stehen, mehrfach an verschiedenenStellen und in unterschiedlichen Kontexten auf. Aus diesem Grund werden diese Problemehier vorab definiert. Genauere Angaben bezüglich der Komplexität der FPT-Algorithmenwerden dann in den Anwendungsbeispielen gegeben (u.a. Kapitel 4.3.1).

Das Vertex-Cover Problem ist die am besten untersuchte Fragestellung im Bereich derFPT-Algorithmen [Nie02]:

Eingabe: Ein Graph G = (VG, EG) und eine nicht negative Ganzzahl k.Frage: Gibt es eine Untermenge von Knoten C ⊆ VG mit k oder weniger Elemen-ten, so dass von jeder Kante in EG mindestens einer ihrer beiden Endpunkte in C ist?

Ein ebenfalls bekanntes FPT-Problem, dessen Lösungsverfahren fortlaufend optimiert wer-den, ist das d-Hitting-Set Problem:

Eingabe: Eine Sammlung C von Untermengen der (maximalen) Größe d von einerendlichen Menge S und eine nicht negative Ganzzahl k.Frage: Gibt es eine Untermenge S ′ ⊆ S mit |S ′| ≤ k, so dass S ′ von jeder Menge inC mindestens ein Element enthält?

Aus beiden Definitionen lässt sich erkennen, dass das Vertex-Cover Problem geradedem 2-Hitting-Set Problem entspricht. Das allgemeine Hitting-Set Problem wird aufder anderen Seite auch oft als Vertex-Cover in Hypergraphen interpretiert.

11Aus [Nie02] sinngemäß übersetzt.

Kapitel 3

Backdoors

Backdoors stellen eines der Konzepte dar, die in den vergangenen vier Jahren dazu herange-zogen wurden, die Struktur von Sat-Instanzen zu analysieren und zu klassifizieren. SchonWilliams, Gomes und Selman geben in ihrem wegweisenden Artikel von 2003 Backdoors ToTypical Case Complexity [WGS03a] Beispiele von Sat-Instanzen aus dem Bereich der logi-stischen Planung mit ungefähr 7000 Variablen und nahezu 440000 Klauseln an, bei denenBackdoors mit nur zwölf Variablen gefunden wurden. Ihre Vermutung, dass strukturierteSat-Instanzen, die sich aus realen Problemstellungen der Praxis ergeben, über kleine Back-doors verfügen, konnte bisher empirisch bestätigt werden: So gelang es Ruan, Kautz undHorvitz im folgenden Jahr mit ihrem erweiterten Konzept der Backdoor Keys einen Zu-sammenhang zwischen Backdoors und der Schwierigkeit von Sat-Problemen herzustellen[RKH04]. Darüber hinaus zeigte Interian, dass sich bei randomisierten, also unstrukturier-ten 3-Sat Instanzen die Größe der Backdoors im Bereich von 30% bis 65% der gesamtenVariablenanzahl bewegt [Int03].Auf dem Gebiet der exakten Berechnung von Backdoors und der Komplexität dieser Algo-rithmen haben vor allem Szeider et al. sehr interessante Beiträge geleistet [NRS04, Sze05,NRS06, Sze07b, SS07], worauf in diesem Kapitel mehrfach eingegangen wird. Außerdemwurde von Paris et al. ein randomisierter Algorithmus entwickelt [POSS06], der basie-rend auf lokaler Suche minimale R-Horn-Backdoor-Mengen approximiert und damit sei-ne Anwendung als Vorverarbeitungsroutine in einer Erweiterung des Zchaff Sat-Solvers[MMZ+01] findet.

In diesem Kapitel werden einige der bisher bekannten Ergebnisse zur Ermittlung undVerwendung von Backdoor-Mengen vorgestellt. Darüber hinaus werden neue Ideen, sowohlzur Berechnung als auch zum praktischen Einsatz von Backdoor-Mengen, erörtert. Vie-le unserer experimentellen Analysen wurden anhand von realen Sat-Instanzen aus demBereich der Automobilkonfiguration [Sin03] durchgeführt.

3.1. BESTIMMUNG VON DPLL-BACKDOORS 24

3.1 Bestimmung von DPLL-Backdoors

Das Konzept von speziellen Backdoor-Variablen in Sat-Problemen wurde in Kapitel 2.6definiert und vorgestellt. Es ist offensichtlich, dass mit Hilfe einer kleinen Backdoor-Mengedie entsprechende Sat-Instanz effizient gelöst bzw. auf Erfüllbarkeit überprüft werdenkann. Kennt man z.B. ein Backdoor B ⊆ V mit |B| ≤ log |V|, so kann das entsprechendeSat-Problem in der Laufzeit 2log |V| ∗ Polynom(|V|) = |V| ∗ Polynom(|V|) gelöst werden,indem alle möglichen Variablenbelegungen der Backdoor-Variablen durchprobiert werdenund die logischen Konsequenzen der jeweiligen Belegung für die verbleibende Instanz inPolynomzeit propagiert werden.Leider ist das Auffinden und Erkennen von Backdoor-Mengen in den meisten Fällen nichteinfach. Eine naheliegende Vorgehensweise, um schwache Backdoor-Mengen von erfüllbarenSat-Instanzen zu bestimmen, wird schon von Williams et al. [WGS03a, WGS03b] vorge-schlagen und angewandt:Bei einem auf dem DPLL-Verfahren basierenden Solver wird diejenige Menge an Entschei-dungsvariablen für das Backdoor ausgesucht, die im Laufe des Algorithmus für das Bran-ching gewählt wurden und am Ende zu einer gültigen Variablenbelegung geführt haben.Aufgrund der Vorgehensweise der DPLL-Prozedur kann damit die Belegung der verblei-benden Variablen erschlossen werden. Allerdings erfolgt die Ermittlung eines Backdoorserst während des Lösungsprozesses. Ein so gefundenes Backdoor kann damit nicht für daseffiziente Lösen der Sat-Instanz verwendet werden.Betrachtet man den Entscheidungsbaum des Algorithmus, dann entsprechen die so ermit-telten Backdoor-Variablen gerade denjenigen Variablen, die den Pfad von der Wurzel (ersteEntscheidung) bis zu demjenigen Blatt bilden, das der letzten Entscheidung entspricht. Dieersten schwachen Backdoors wurden von Williams et al. durch die Anpassung des rando-misierten SATZ Solvers [LA97] berechnet.Unglücklicherweise ist das Auffinden von DPLL-Backdoors nicht wesentlich effizienter durch-führbar. Szeider bewies 2005 [Sze05] die NP -Härte der Bestimmung von minimalen schwa-chen und starken DPLL-Backdoors und darüber hinaus, dass selbst durch die Einschrän-kung auf einen Subsolver, der nur Unit Propagation oder die Pure Literal Eliminationverwendet, das Problem NP -hart ist.

3.1.1 Berechnung von schwachen DPLL-Backdoors

Aufgrund der Tatsache, dass moderne Sat-Solving Strategien das ursprüngliche DPLL-Verfahren in vielen Aspekten erweitern und verändern (siehe 2.3.2 - 2.3.4), wurde im Rah-men dieser Arbeit ein DPLL-Sat-Solver in C++ implementiert, der weder auf das Kon-zept des Klausellernens ([MSS96, MSS99]) noch auf irgendwelche Variablenheuristikenzurückgreift. Dies führt selbstverständlich zu immensen Laufzeiteinbußen, hat aber denVorteil und den Zweck, Backdoors möglichst unabhängig von Branching-Heuristiken zuermitteln. Da bei dieser Methode die gefundenen Backdoors der Menge von Branching-Variablen entsprechen, ist es sehr wahrscheinlich, dass Solver, die eine ausgeprägte Varia-blenheuristik benutzen, nur bestimmte Backdoor-Mengen auffinden werden.


Die Schwierigkeit, Backdoors mit Hilfe von Solvern zu ermitteln, die das Konzept desKlausellernens implementieren, besteht darin, dass gelernte Klauseln einen (gewollten)Einfluss auf die Unit Propagation haben. Dies führt dazu, dass die Belegung einer Varia-blen, abhängig von der Menge der gelernten Klauseln, unterschiedliche Auswirkungen aufandere Variablenbelegungen hat. In ersten Versuchen, Backdoors durch die Modifikationdes MiniSat-Solvers ([ES03]) zu berechnen, wurden daher oft “unechte Backdoors” gefun-den, die ohne die spezifische Menge an gelernten Klauseln gar keine Backdoors darstellen.Das Konzept des non-chronological Backjumping ([MSS96]) verkleinert den Suchraum, in-dem bestimmte “unnötige” Zweige des Entscheidungsbaumes identifiziert und übersprungenwerden, und hat damit nur Auswirkungen auf die Laufzeit, nicht aber auf die Menge angefundenen Lösungsmodellen. Daher wurde dieses Konzept in unsere Implementierung auf-genommen. Ebenfalls ist das Konzept der Random Restarts implementiert, da ein Neu-start gerade dann durchgeführt wird, wenn längeres Suchen in einer bestimmten Regiondes Suchbaumes kein Ergebnis erzielen konnte. In einem solchen Fall ist es sehr wahrschein-lich, dass die Anzahl der bisher getroffenen Branching-Entscheidungen sehr groß ist, waswiederum ein großes, für die Praxis irrelevantes Backdoor erzeugen würde.

3.1.2 Erweiterung für starke DPLL-Backdoors

Um auch starke DPLL-Backdoors zu ermitteln, haben wir das oben beschriebene Verfah-ren leicht erweitert: Für nicht erfüllbare Instanzen werden alle Variablen in das Backdooraufgenommen, die während des Suchprozesses irgendwann Branching-Variablen waren. ImUnterschied zum Finden von schwachen Backdoors werden damit auch solche Variablenaufgenommen, die im Entscheidungsbaum des Algorithmus außerhalb des Pfades von derersten bis zur letzten Entscheidung liegen. Kommt der Algorithmus zu dem Schluss, dassdie zugrunde liegende Instanz nicht erfüllbar ist, so wurden alle Variablenbelegungen füralle Entscheidungsvariablen getestet. Daher bildet diese Menge nach Definition gerade einstarkes Backdoor.

Mit Hilfe der beschriebenen Implementierung wurden zahlreiche schwache und starkeBackdoors für Sat-Instanzen aus der Automobilkonfiguration berechnet. Dabei wurden fürerfüllbare Instanzen je bis zu 40000 Berechnungen durchgeführt. Da bei der Implementie-rung auf Klausellernen und Heuristiken verzichtet wurde, musste bei unlösbaren Instanzendie Anzahl der Durchläufe aus zeitlichen Gründen stark reduziert werden. Bei schwierigenunlösbaren Instanzen, bei denen der Suchprozess nach zehn Stunden kein Ergebnis liefernkonnte, wurde die Berechnung der Backdoors abgebrochen. Aus der Menge der berechne-ten Backdoors einer Instanz wurden diejenigen Backdoors eliminiert, die eine Obermengeeines anderen Backdoors bilden.Zusätzlich zu den schwachen Backdoors von erfüllbaren Instanzen wurde die jeweils gültigeVariablenbelegung der Backdoor-Variablen gespeichert, was im Folgenden als “ExtendedBackdoor” bezeichnet wird. Extended Backdoors stellen somit eine Menge von Paaren ausVariablen ∈ V und den zugehörigen Wahrheitswerten ∈ {false, true} dar.Tabelle 3.1 soll einen Überblick über die Größe der gefundenen Backdoors für Instanzen aus


der Automobilkonfiguration geben. In den ersten drei Spalten wird der Name, die Anzahlder Variablen und die Anzahl der Klauseln der jeweiligen Sat-Instanz genannt. In Spaltevier ist die Anzahl der berechneten Backdoors aufgeführt und Spalte fünf gibt an, ob essich bei diesen Backdoors um starke (

√- für unerfüllbare Instanzen) oder schwache (� -

für erfüllbare Instanzen) DPLL-Backdoors handelt. Die Spalten sechs bis acht geben dieminimale, maximale und durchschnittliche Größe der berechneten Backdoors an. Spalteneun und zehn zeigen die Standardabweichung und die Varianz der ermittelten Werte.

Anzahl Typ Backdoor GrößeInstanz Vars. Kls. BDs stark? min. max. � σ σ2

C210 FW 1891 9705 39555 � 6 118 20.65 4.61 21.26C638 FKB 1750 3774 39631 � 8 213 16.57 3.45 11.89C168 FW NC 5 1804 6744 9826 � 6 36 17.56 4.44 19.69C168 FW UT 2465 1804 6744 10000 � 11 43 20.71 3.86 14.94C208 FC UT 3529 1802 7636 10000 � 7 43 17.98 4.20 17.63C210 FW UT 4705 1891 9726 10000 � 8 32 18.40 3.23 10.44C220 FV UC 152 1782 6581 9944 � 4 60 27.17 6.34 40.19C220 FV UC 166 1782 6581 9923 � 4 61 27.21 6.35 40.35C220 FV UT 1177 1782 6606 10000 � 13 68 31.91 6.18 38.20C638 FKA UC 256 1753 7613 10000 � 17 47 27.82 4.15 17.20C638 FKA UT 589 1753 7616 10000 � 7 49 26.40 5.62 31.62C168 FW SZ 128 1583 5425 3

√31 72 53.67 20.84 434.33

C168 FW SZ 41 1583 5387 30√

1 64 19.77 12.93 167.22C168 FW UT 851 1804 7491 45

√2 18 9.76 5.24 27.42

C170 FR RZ 32 1528 4956 24√

36 63 52.50 5.90 34.78C170 FR SZ 92 1528 5082 50

√12 68 35.62 14.35 205.87

C202 FS SZ 95 1556 6184 42√

2 37 15.88 8.91 79.33C202 FW SZ 118 1561 8811 50

√7 64 28.20 13.63 185.84

C208 FA SZ 87 1516 5299 49√

3 44 25.47 10.68 114.09C210 FW SZ 91 1628 7721 50

√12 68 32.10 14.49 209.97

C220 FV SZ 46 1530 4498 24√

1 37 13.00 9.55 91.22C220 FV SZ 55 1530 5753 44

√5 53 24.59 9.73 94.76

aim-50-2 0-no-4 50 100 20√

12 44 28.00 7.68 59.05

Tabelle 3.1: Backdoors in Instanzen der Automobilkonfiguration. Alle Instanzen stammenaus [Sin03]. Die letzte Zeile zeigt zum Vergleich die Backdoor-Größe einer Zufallsinstanz.

Für die Instanzen des ersten Blockes wurden jeweils 40000, für die des zweiten Blockes10000 und für die restlichen Instanzen je 50 Berechnungen durchgeführt. Die minimalenschwachen Backdoors, die für erfüllbare Instanzen ermittelt wurden, sind durchweg sehrklein, gerade im Vergleich zur Variablenanzahl der jeweiligen Instanz. Die jeweils maximaleGröße der gefundenen Backdoors zeigt, dass es durchaus auch sehr schlechte Variablenord-nungen geben kann. Für unerfüllbare Instanzen konnte in der vorhandenen Zeit (mindestenszehn Stunden pro Instanz) nicht immer ein kleines starkes Backdoor gefunden werden. InKapitel 3.6.2 werden zwei Ansätze vorgestellt, die es für einige der unerfüllbaren Instanzenermöglichen, kleinere starke Backdoors zu berechnen.

3.2. EINE VORVERARBEITUNG FÜR INDUSTRIELLE INSTANZEN 27

In diesem Unterkapitel wurden die gefundenen DPLL-Backdoors unter dem Aspekt derGröße von Backdoors betrachtet. Dazu mussten die jeweiligen Sat-Instanzen vollständiggelöst werden. Im Folgenden werden mehrere Methoden vorgestellt, andere Arten von Back-doors zu ermitteln, für die das Lösen der Instanz nicht erforderlich ist. In Kapitel 3.6 wer-den schließlich weitere interessante Aspekte von DPLL-Backdoors gerade für Instanzen derAutomobilkonfiguration aufgezeigt.

3.2 Eine Vorverarbeitung für industrielle Instanzen

Natürlich ist es wünschenswert eine Methode zu kennen, die in Polynomzeit eine möglichstkleine starke Backdoor-Menge ermitteln kann. Wie schon im vorigen Kapitel erläutert wur-de, ist diese Aufgabe im Allgemeinen nicht leicht zu bewältigen. Steckt man die Ziele nichtzu hoch, so kann es auch hilfreich sein, in einer Vorverarbeitung schon diejenigen Varia-blen zu bestimmen, die als Backdoor-Variablen außer Acht gelassen werden können. Gelingtes, mit Hilfe einer Vorverarbeitungsroutine die Menge der möglichen sinnvollen Backdoor-Variablen B einzuschränken, so kann die daraus erhaltene Information eine gute Grundlagefür eine entsprechende Sat-Solving-Heuristik sein, selbst wenn das Durchprobieren aller2|B| Belegungen zu komplex ist. Eine Möglichkeit besteht darin, eine optimale initiale Va-riablenordnung zu wählen, bei der die Backdoor-Variablen an den Anfang gesetzt werden.Gerade bei Sat-Solvern, die eine statische Variablenordnung implementieren, ist dieserAnsatz durchaus sinnvoll. In einem praktischen Beispiel wurde diese Idee als Vorstufe desZchaff-Solvers realisiert und die Variablenordnung für die DPLL-Prozedur entsprechendvorsortiert [POSS06].Der in dieser Arbeit entwickelte und im Folgenden beschriebene Vorverarbeitungsprozesseignet sich für Instanzen, in denen mehrere Klauseln mit weniger als drei Literalen vor-handen sind. Diese Voraussetzung wird oft in Sat-Instanzen erfüllt, die aus industriellenFragestellungen entstanden sind (vgl. z.B. [Sat07]).

3.2.1 Berechnung eines Propagation-Graphen

In Algorithmus 2 wird zunächst ein gerichteter Graph erzeugt, der jeder Variablen einerFormel F einen Knoten zuweist. Die Kanten dieses Propagation-Graphen ergeben sichdurch das hintereinander durchgeführte, testweise Propagieren beider Variablenbelegun-gen (vierte Zeile) für jede Variable ∈ V. Die Menge Lip beinhaltet diejenigen Literale, dieals Konsequenz der Zuweisung xi ← true wahr werden, Lin enthält diejenigen Literale, diedurch die Belegung xi ← false wahr werden.Verursacht sowohl die testweise Belegung des Wahrheitswertes true als auch des Wertesfalse für eine Variable xi ∈ V einen Konflikt (Lip = Lin = null), so ist klar, dass Fnicht erfüllbar sein kann (fünfte Zeile). Führt nur eine der beiden Zuweisungen zu einerungültigen Belegung, so kann daraus gerade die entgegengesetzte Belegung für xi gefolgertwerden (siebte Zeile).Implizieren beide Belegungen einer Variablen xi den gleichen Wahrheitswert b für eine an-dere Variable xj, so kann dieser Wert b für Variable xj fest angenommen werden (neunte


Algorithmus 2 Erzeugen eines Propagation-Graphen

Eingabe: Eine boolsche Formel F mit Variablen VAusgabe: Ein Propagation-Graph1: function createPropagationGraph(F )2: G = (VG, EG)← jeder Variablen xi ∈ V wird ein

Knoten ki ∈ VG zugeordnet, EG = ∅3: for all xi ∈ V do4: Lip ← testPropagate(xi), Lin ← testPropagate(xi)5: if Lip = Lin = null then return ”Unsatisfiable”6: if Lin = null and Lip 6= null then7: applyPropagate(xi) . analoger Fall für xi8: else9: applyPropagate(l) ∀ l ∈ {Lip ∩ Lin}

10: for all xj ∈ {V ariables(Lip) ∩ V ariables(Lin)} do11: EG ← EG ∪ (ki, kj)12: end for13: end if14: end for15: return G16: end function

Zeile). Darüber hinaus ist es nicht notwendig, Variable xj in ein DPLL-Backdoor aufzu-nehmen. Diese Idee ist stark mit dem Konzept der Backbone-Variablen verwandt, welchesdie Menge solcher Variablen beschreibt, die in jedem Lösungsmodell einer Formel stetsden selben Wahrheitswert haben (siehe Kapitel 2.6) [MZK+99]. Allerdings müssen nichtalle in Zeile neun gesetzten Variablen tatsächlich Backbone-Variablen sein. Dies liegt ander Anwendung der Pure Literal Elimination während des Propagierens: Treten von einerVariablen nicht (mehr) beide Literale in F auf, so kann der Wahrheitswert entsprechendgesetzt werden. Dies ist aber für die Erfüllbarkeit der Formel nicht zwingend erforderlich!Eine gerichtete Kante (xi, xj) wird dann erzeugt, wenn beide temporären Belegungen einerVariablen xi auch eine Belegung für Variable xj implizieren (Zeilen zehn und elf). In die-sem Fall ist offensichtlich, dass der Wahrheitswert der Variablen xj immer vom Wert derVariablen xi abhängt. Die Variable xi “dominiert” somit die Variable xj. Für die weitereArgumentation ist es wichtig, dass durch eine Kante (xi, xj) im Propagation-Graphen einebinäre Relation zwischen den Variablen xi und xj dargestellt wird, die insbesondere tran-sitiv ist, denn es gilt: Dominiert eine Variable xi eine andere Variable xj, die wiederumeine weitere Variable xk dominiert, so dominiert xi auch xk.

Man sollte beachten, dass der so erzeugte Propagation-Graph nach einem Durchlauf derFunktion createPropagationGraph nicht eindeutig ist. Der Graph - beziehungsweise dessenKantenmenge - ist von der Ordnung abhängig, in der die Variablen betrachtet werden. DieUrsache hierfür ist, dass sich durch das temporäre Propagieren auch endgültige Variablen-


belegungen ergeben können, wie dies in Zeile sieben und neun von Algorithmus 2 der Fallist. An diesen Stellen wird die Formel F tatsächlich verändert. Entstehen dadurch z. B.neue Binärklauseln, so könnten diese für die temporären Belegungen der bisher betrachte-ten Variablen weitere Konsequenzen verursachen.Prinzipiell ist es natürlich möglich, die Schleife in Algorithmus 2 so lange auszuführen,bis keine endgültigen Zuweisungen mehr möglich sind. In unseren Testfällen konnte jedochschon durch das zweimalige Aufrufen der Funktion createPropagationGraph nur noch ei-ne minimale Verbesserung im Vergleich zur einmaligen Durchführung der Funktion erzieltwerden. Da diese Vorverarbeitung, wie oben erwähnt, eher als eine Möglichkeit zur Opti-mierung der Variablenordnung zu sehen ist, kann eine minimale Verbesserung die erhöhteLaufzeit wahrscheinlich nicht rechtfertigen.Die hier angewandte Idee der temporären Zuweisung beider Wahrheitswerte für eine Varia-ble ist nicht unbekannt und bildet einen der grundlegenden Bestandteile des Satz-Solvers[LA97]. Dort wird auf diese Weise das Branching-Verhalten und somit die Variablenord-nung des Solvers beeinflusst.

3.2.2 Einschränkung möglicher DPLL-Backdoor-Variablen

Anhand des erzeugten Propagation-Graphen und den dadurch beschriebenen Abhängig-keiten der Variablenbelegungen, lassen sich nun bestimmte Variablen bestimmen, die alsBackdoor-Variablen ungeeignet sind und somit vernachlässigt werden können. Der grund-legende Gedanke ist dabei, einige derjenigen Variablen auszuschließen, die von anderenVariablen dominiert werden. In Algorithmus 3 wird die gesamte Vorverarbeitungsroutinevorgestellt.

Algorithmus 3 Eliminieren von Nicht-Backdoor-Variablen

Eingabe: Eine boolsche Formel F mit Variablen VAusgabe: Ein Backdoor B ⊆ V von F1: function eliminateNoBackdoorVariables(F )2: Führe Unit Propagation und Pure Literal Elimination durch3: G = (VG, EG)← createPropagationGraph(F )4: SCCs← computeStronglyConnectedComponents(G)5: for all S ∈ SCCs : |S| ≥ 2 do6: s0 ← beliebiges Element aus S7: for all s ∈ {S \ {s0}} do8: EG ← EG \ (s, v) ∪ (s0, v) ∀ (s, v) ∈ EG9: EG ← EG \ (v, s) ∪ (v, s0) ∀ (v, s) ∈ EG

10: end for11: VG ← VG \ {S \ {s0}}12: end for13: return {xi ∈ V : ki ∈ VG hat keine eingehenden Kanten}14: end function


Nach der Durchführung der Boolean Constraint Propagation und dem anschließendenErzeugen des Propagation-Graphen G werden in Zeile vier die starken Zusammenhangs-komponenten von G mit Hilfe des Algorithmus von Tarjan [OW02, Kap. 8] berechnet.Eine starke Zusammenhangskomponente Z ⊆ VG ist so definiert, dass es innerhalb dieserKomponente von jedem Knoten s ∈ Z einen Pfad zu jedem anderen Knoten t ∈ Z gibt(Kapitel 2.2).Angewandt auf den Propagation-Graphen bedeutet dies, dass jede Variable die Belegungenaller anderen Variablen der selben starken Zusammenhangskomponente beeinflusst. Da das“Dominieren” von Variablen eine transitive Beziehung darstellt, können außerdem folgendeRegeln festgehalten werden:

• Dominiert eine beliebige Variable xi eine andere Variable xj, so dominiert xi auchalle Variablen, die sich in der gleichen SCC wie xj befinden.

• Dominiert eine beliebige Variable xi einer SCC S eine beliebige andere Variable xj,so wird xj auch von allen anderen Variablen aus S dominiert.

Damit kann im Graphen aus jeder starken Zusammenhangskomponente S je ein Knotens0 als “repräsentierende Variable” gewählt werden, der alle eingehenden und ausgehendenKanten der anderen Knoten in S \{s0} übernimmt. Da beide Belegungen (false, true) derrepräsentierenden Variablen eine Belegung aller Variablen in der selben SCC implizieren,können alle Knoten ∈ {S \ {s0}} gelöscht werden. Diese Idee ist in Algorithmus 3 in denZeilen sechs bis elf realisiert.Durch die beschriebene Prozedur entsteht ein sogenannter Blockgraph G′. Dieser ist insbe-sondere azyklisch, da jeder Zykel eine starke Zusammenhangskomponente in G bildet, dieim verbleibenden Graphen G′ nur noch durch einen einzigen Knoten repräsentiert wird.Da in G′ keine Zykel existieren, ist jeder Knoten ki mit Eingangsgrad größer als null vonmindestens einem Knoten kj mit Eingangsgrad null aus erreichbar. Durch diese topologi-sche Sortierung wird jede Variable, deren Knoten einen Eingangsgrad größer null hat, vonmindestens einer anderen Variablen dominiert, deren Knoten keine eingehenden Kantenhat. Für das Backdoor brauchen also nur solche Variablen in Betracht gezogen werden,deren Knoten in G′ keine eingehenden Kanten haben. In Zeile dreizehn des Algorithmuswerden gerade diese Variablen zurückgegeben. Die Größe der zurückgegebenen Variablen-menge stellt eine obere Schranke für ein minimales DPLL-Backdoor dar.Da das Erzeugen des Propagation-Graphen für jede Variable das Propagieren beider Wahr-heitswerte erfordert, was jeweils in der Zeit O(|F |) möglich ist (Kapitel 2.3.1), lässt sichdie Laufzeit von Algorithmus 2 durch O(|V| ∗ |F |) beschränken. In Algorithmus 3 könnendie starken Zusammenhangskomponenten mit Hilfe von Tarjan’s Algorithmus in der ZeitO(|VG| + |EG|) bestimmt werden. Die gleiche obere Laufzeitschranke gilt auch für dieDurchführung der Schleife von Zeile fünf bis zwölf in Algorithmus 3, da jeder Knotenund jede Kante insgesamt einmal betrachtet werden. Somit liegen beide Berechnungen inO(|V|2) ∈ O(|V| ∗ |F |), wodurch der gesamte Vorverarbeitungsprozess die KomplexitätO(|V| ∗ |F |) erfordert.


Kls. mit Größe < 3 Vars. nach VorprozessInstanz sat? Vars. Kls. # % # %C169 FV

√1402 1982 1960 98.89 2 0.14

C171 FR√

1743 4005 3430 85.64 31 1.78C202 FS

√1822 8883 5588 62.91 229 12.57

C203 FCL√

1819 5225 4490 85.93 1763 96.92C638 FKB

√1750 3774 3485 92.34 1398 79.89

C638 FVK√

1727 3162 3001 94.91 59 3.42D1119 M20

√1392 1698 1597 94.05 13 0.93

C168 FW UT 980√

1804 6744 4342 64.38 1642 91.02C208 FC UT 3528

√1802 7636 5618 73.57 1701 94.40

C220 FV UC 116√

1782 6581 4631 70.37 126 7.07C220 FV UT 1762

√1782 6593 4632 70.26 1704 95.62

C220 FV UT 1772√

1782 6589 4639 70.41 164 9.20C168 FW SZ 107 � 1583 6599 4141 62.75 1455 91.91C170 FR SZ 58 � 1528 5001 4171 83.40 1341 87.76C202 FW SZ 96 � 1561 8849 5607 63.36 6 0.38C202 FW SZ 98 � 1561 8689 5607 64.53 1502 96.22barrel5 � 1407 5383 1631 30.30 977 69.44hanoi4

√718 4934 2609 52.88 718 100.00

hole8 � 72 297 288 96.97 72 100.00longmult6 � 2848 8853 6008 67.86 2213 77.70ssa7552-160

√1391 3126 2443 78.15 413 29.69

Tabelle 3.2: Ergebnisse der Prozedur eliminateNoBackdoorVariables für Instanzen aus derAutomobilindustrie [Sin03] und DIMACS-Benchmarks [Ben].

In Tabelle 3.2 werden einige Beispiele für die Anwendung des beschriebenen Vorver-arbeitungsprozesses zum Eliminieren von “Nicht-Backdoor-Variablen” gegeben. Die erstenvier Spalten nennen den Namen, die Erfüllbarkeit und die Anzahl von Variablen und Klau-seln einer Instanz. Die Spalten fünf und sechs zeigen

Diplomarbeit Backdoors in Sat -Instanzen · 2009. 2. 17. · Diplomarbeit Backdoors in Sat...

Documents

Transcript of Diplomarbeit Backdoors in Sat -Instanzen · 2009. 2. 17. · Diplomarbeit Backdoors in Sat...