Resolution und die Ganzzahligkeit von SAT-Polytopen

Thomas Friedrich 26. Mai 1997

Seminar über Optimierungsalgorithmen Universität zu Köln

1 Einleitung

Das SAT-Problem besteht darin, ob eine Menge von Klauseln gleichzeitig erfüllt werden kann. Häufig interessiert man sich aber nicht nur für die Existenz einer Lösung, sondern will über alle zulässigen Lösungen optimieren. Hierfür ist es interessant, ob das zugehörige Polytop ganzzahlig ist, weil dann mit Linearer Programmierung eine optimale Ecklösung des Polytops gefunden werden kann, die ja dann auch noch zulässig für das SAT-Problem ist.

Das Hauptergebnis wird sein, daß ein SAT-Polytop genau dann ganzzahlig ist, wenn es alle maximalen Set-Cover-Teilproblem-Polytope sind. Die Ganzzahligkeit von Set-Cover-Polytopen ist einfacher zu bestimmen, z. B. über balancierte Matrizen, für deren Nachweis es einen in polynomieller Zeit arbeitenden Algorithmus gibt; für SAT ist hingegen kein solcher bekannt.

Außerdem wird Resolution vorgestellt, eine Methode, die auch beim automatischen Beweisen, einem Teilgebiet der Künstlichen Intelligenz, eingesetzt wird.

2 Logik-Grundlagen

2.1 Das SAT-Problem

Definition: (logische Variable, Literal, Klausel, Erfüllbarkeit, Leerklausel) Eine logische Variable ist eine Variable, die nur die Werte wahr und falsch annehmen kann. Ein Literal ist entweder eine logische Variable oder ihre Negation. Eine Klausel ist eine Disjunktion (ODER-Verknüpfung) von Literalen, in der keine Variable mehr als einmal vorkommt. Eine Menge S von Klauseln heißt erfüllbar, wenn es eine Belegung der Variablen mit wahr oder falsch gibt, so daß jede Klausel aus S wahr wird. Die Leerklausel enthält keinerlei Literale und ist daher nicht erfüllbar, also stets falsch.

Beispiele: Logische Variablen: x_{1}, x_{2}, x_{3} Literale: x_{1}, ¬x_{1}, x_{2}, ¬x_{2} kein Literal: ¬¬x_{1} Klauseln: x_{1}, x_{1} ∨ x_{2}, ¬x_{1} ∨ x_{2}, x_{1} ∨ ¬x_{2} ∨ x_{3} ∨ x_{4} keine Klausel: x_{1} ∨ ¬x_{1} ∨ x_{2} Leerklausel: □

Definition: (Absorbierung, Implikation, Primimplikant) Eine Menge S von Klauseln impliziert (logisch) eine Klausel C, wenn jede Belegung, die alle Klauseln in S erfüllt, auch C wahr macht. Eine Klausel C absorbiert eine andere Klausel D, wenn alle Literale aus C auch in D sind. Ein Primimplikant einer Menge S von Klauseln ist eine Klausel, die von S impliziert und von keiner anderen Klausel von S absorbiert wird.

Bemerkung: C impliziert D ⟺ C absorbiert D.

Definition: (SAT, KNF, MAXSAT, k-SAT) Das Erfüllbarkeitsproblem (satisfiability problem, SAT) der Aussagenlogik besteht darin, zu entscheiden, ob es eine Belegung der Variablen gibt, so daß alle Klauseln in einer gegebenen Menge wahr werden, ob also die Konjunktion (UND-Verknüpfung) der Klauseln erfüllbar ist. Die Schreibweise als Konjunktion von Disjunktionen heißt Konjunktive Normalform (KNF, auch: conjunctive normal form, CNF). Das SAT-Problem mit höchstens k Literalen in jeder Klausel heißt k-SAT. Beim maximum satisfiability problem (MAXSAT) versucht man, bei gegebener positiver Bewertung jeder Klausel wenigstens eine Teilmenge so zu erfüllen, daß die Summe der Werte der erfüllten Klauseln einen möglichst großen Wert ergibt.

Bemerkungen:

(i) SAT und MAXSAT sind i. a. NP-vollständig. (Satz von Cook, 1971)

(ii) Für k ≥ 3 ist auch k-SAT NP-vollständig.

2.2 Resolution

Definition: (Resolution, Resolvent, Elternklauseln) Wenn bei zwei Klauseln C und D exakt ein Literal in der einen Klausel positiv (x_{j}) und in der anderen negativ (¬x_{j}) vorkommt, entsteht der Resolvent von C und D durch Disjunktion aller Literale aus C und D mit Ausnahme von x_{j} und ¬x_{j}. Das Anwenden dieser Regel heißt Resolution, man resolviert C und D nach x_{j}. C und D nennt man dabei die Elternklauseln.

Bemerkung: Für zwei resolvierbare Klauseln C_{1} und C_{2} mit Resolvent D gilt: {C_{1}, C_{2}} impliziert D.

Beispiel:

(1) x_{1} ∨ ¬x_{2} ∨ x_{4}

(2) x_{1} ∨ x_{3} ∨ ¬x_{4}

(3) x_{1} ∨ ¬x_{3} ∨ x_{4}

(1) und (2) lassen sich nach x_{4} resolvieren, und der Resolvent ist:

(4) x_{1} ∨ ¬x_{2} ∨ x_{3}.

(1) und (3) können nicht resolviert werden, weil es kein Literal gibt, das in der einen Klausel positiv und in der anderen negativ vorkommt.

(2) und (3) können nicht resolviert werden, weil mit x_{3} und x_{4} gleich zwei Literale in der einen Klausel positiv und in der anderen negativ vorkommen.

2.3 Der Algorithmus von Quine

Der folgende Resolutions-Algorithmus von Quine erzeugt alle Primimplikanten einer Klauselmenge S. Ist S nicht erfüllbar, erzeugt der Algorithmus die Leerklausel, die dann einziger Primimplikant ist (weil sie jede andere Klausel absorbiert).

Algorithmus: Resolution S′ := {C ∈ S | ∄D ∈ S, |D| < |C| : D absorbiert C} while (A, B ∈ S′ Klauseln mit Resolvent C,

und ∄D ∈ S′ : D absorbiert C) {

if (C = □) stop: ”S unerfüllbar, □ einziger Primimplikant.“ S′ := S′ \ {D ∈ S′ | C absorbiert D} S′ := S′ ∪ {C}

}

stop: ”S ist erfüllbar; alle Primimplikanten erzeugt.“

Der Algorithmus geht dabei wie folgt vor: S′ besteht zunächst aus allen Klauseln von S, die nicht von kürzeren Klauseln absorbiert werden. Dann werden zwei Klauseln aus S′ resolviert zur Klausel C. Gibt es in S′ keine zwei solchen Klauseln, besteht S′ bereits aus allen Primimplikanten von S. Ist C die Leerklausel, ist S unerfüllbar. Anschließend werden alle Klauseln aus S′ entfernt, die C absorbiert, und C in S′ aufgenommen. Die worst-case-Laufzeit dieses Algorithmus ist exponentiell.

3 Polytop-Grundlagen

3.1 SAT als Polytop

Definition: (Polyeder, Polytop, ganzzahliges Polytop, Ecke) Eine Teilmenge P ⊆ IR^{n} heißt Polyeder, wenn es ein m ∈ IN, eine Matrix A ∈ IR^{m×n} und a ∈ IR^{m} gibt mit P = {x ∈ IR^{n} | Ax ≥ a}. Ein beschränktes Polyeder heißt Polytop. Die eindeutige Lösung eines aus n linear unabhängigen Zeilen bestehenden Teilsystems Bx = b von Ax ≥ a heißt Ecke des Polyeders bzw. Polytops. Ein Polytop heißt ganzzahlig, wenn alle seine Ecken ausschließlich ganzzahlige Koordinaten haben.

Definition: (Lineares Optimierungsproblem, LP) Für gegebene A ∈ IR^{m×n}, b ∈ IR^{m}, c ∈ IR^{n} ist (z. B.) die Aufgabe

(LP) minimiere c^{T}x so daß Ax ≥ b

und x ≥ 0

ein lineares Optimierungsproblem oder lineares Programm (LP).

Bemerkungen:

(i) Ein Polytop ist die konvexe Hülle seiner Ecken.

(ii) Für ein lineares Optimierungsproblem über einem Polytop gilt: Es gibt eine Optimallösung ⟺ es gibt eine optimale Ecklösung.

Identifiziert man bei SAT die logischen Variablen als 0-1-Variablen, wobei ”wahr“ dem Wert 1 und ”falsch“ dem Wert 0 entspricht, und ersetzt man ferner Negationen ¬x_{j} durch (1−x_{j}), so kann man die einzelnen Klauseln als Ungleichungen schreiben, wobei die 0-1-Lösungen der Ungleichungen genau den Erfüllbarkeitsbelegungen von SAT entsprechen. So wird z. B. aus

x_{1} ∨ ¬x_{2} ∨ x_{4}

dann

x_{1} + (1 − x_{2}) + x_{4} ≥ 1.

Dabei ist ”≥ 1“ so zu verstehen, daß mindestens ein Literal 1 wird, also die entsprechende Klausel erfüllt ist.

Durch Umformen erhält man schließlich:

x_{1} − x_{2} + x_{4} ≥ 0.

Auf diese Art wird aus obigen Beispielklauseln (1)-(3):

(5) x_{1} − x_{2} + x_{4} ≥ 0

(6) x_{1} + x_{3} − x_{4} ≥ 0

(7) x_{1} − x_{3} + x_{4} ≥ 0.

Also kann man ein SAT-Problem in ein System Ax ≥ a umschreiben und dieses als Beschreibung für ein Polytop P = {x ∈ IR^{n} | Ax ≥ a, 0 ≤ x ≤ 1} betrachten. Dieses Polytop ist genau dann ganzzahlig, wenn es die konvexe Hülle der zulässigen Lösungen des SAT-Problems ist.

3.2 Maximale Set-Cover-Teilprobleme

Definition: (SC) Für eine 0-1-Matrix B definiert das System Bx ≥ 1, x ∈ {0, 1}^{n} ein Mengenüberdeckungs-Problem (set cover problem, SC).

Das set cover problem besteht im wesentlichen darin, einige wenige Elemente einer Obermenge so auszuwählen, daß für eine gegebene Familie von Teilmengen aus jeder mindestens ein gewähltes Element stammt. Die Matrix B beschreibt dabei zeilenweise die Charakteristiken der einzelnen Teilmengen.

Definition: (Monotonie, Balance) Eine Matrix A heißt monoton, wenn in keiner Spalte sowohl positive als auch negative Elemente vorkommen. A heißt balanciert, wenn für jede Teilmatrix, die in jeder Zeile und jeder Spalte genau zwei Nichtnull-Einträge hat, gilt, daß sich alle ihre Elemente zu 0 modulo 4 aufsummieren.

Bemerkungen: Ist die Matrix B im SC-Problem Bx ≥ 1, x ∈ {0, 1}^{n} balanciert, dann ist das Polytop P = {x ∈ IR^{n} | Bx ≥ 1, 0 ≤ x ≤ 1} ganzzahlig. Dasselbe gilt für die Matrix A und das entsprechende Polytop im SAT-Problem.

Die Balance der Matrix A ist lediglich hinreichend für die Ganzzahligkeit des SAT-Polytops, jedoch nicht notwendig.

Beispiel: Betrachte das (in Ungleichungen geschriebene) SAT-Problem

x_{1} + x_{2} + x_{3} ≥ 1
x_{1} − x_{2} − x_{3} ≥ −1.

Die zugehörige Matrix ist nicht balanciert, weil die Summe der Einträge der ersten beiden Spalten 2 beträgt. Trotzdem definieren die beiden Ungleichungen (zusammengenommen mit 0 ≤ x ≤ 1) ein ganzzahliges Polytop.

Definition: (maximales SC-Teilproblem) Bx ≥ b ist ein Set-Cover-Teilproblem von Ax ≥ a, falls (B, b) eine Teilmenge der Zeilen von (A, a) darstellt, und B eine monotone Matrix ist. Ein Set-Cover-Teilproblem Bx ≥ b heißt maximal, wenn durch Hinzunahme einer beliebigen weiteren Zeile aus Ax ≥ a die Monotonie von B zerstört wird.

In Set-Cover-Teilproblemen kommt also jede Variable entweder nur positiv oder nur negativ vor. Durch Ersetzung der negativen Literale durch Variablen kann man sich o. B. d. A. auf nur positive Literale beschränken. Da das SC-Teilproblem aus einer Teilmenge der SAT-Klauseln besteht, bedeutet hier eine Überdeckung, daß aus jeder Klausel mindestens ein Literal gesetzt ist, also wahr wird.

Die maximalen SC-Teilprobleme des SAT-Problems Ax ≥ a müssen nicht unbedingt disjunkt sein. Man erhält sie durch Erzeugung eines Graphen, in dem die Klauseln die Knoten sind, und eine Kante genau dann zwei Knoten verbindet, wenn in den entsprechenden Klauseln mindestens eine Variable mit unterschiedlichem Signum vorkommt. Die maximalen SC-Teilprobleme sind dann genau die maximalen independent sets, also maximale Knotenmengen, deren induzierte Teilgraphen keine Kanten enthalten.

Bemerkung: Enthält die SAT-Instanz die Leerklausel □, so ist diese auch in allen SC-Teilproblemen enthalten. Sowohl das SAT-Polytop als auch alle SC-Polytope sind dann leer. Dieser Fall ist also uninteressant.

Nach diesen Vorbereitungen folgt nun der zentrale Satz dieses Vortrages.

4 Über die Ganzzahligkeit von SAT-Polytopen

4.1 Der Satz

Hauptsatz: Sei Ax ≥ a die Repräsentation einer SAT-Instanz, die alle ihre Primimplikanten enthält (z. B. durch Resolution gewonnen). Dann beschreiben die Ungleichungen

Ax ≥ a
0 ≤ x ≤ 1

genau dann ein ganzzahliges Polytop P, wenn für jedes maximale Set-Cover-Teilproblem A′x ≥ a′ von Ax ≥ a die Ungleichungen

A′x ≥ a′
0 ≤ x ≤ 1

ein ganzzahliges Polytop beschreiben.

4.2 Der Beweis

4.2.1 ”⇒“

Für eine SAT-Instanz Ax ≥ a, die alle ihre Primimplikanten enthält, definiere Ax ≥ a, 0 ≤ x ≤ 1 ein ganzzahliges Polytop P.

zu zeigen: auch die Polytope aller maximalen SC-Teilprobleme sind ganzzahlig.

Annahme: Es gibt ein SC-Teilproblem A′x ≥ a′ von Ax ≥ a, dessen Polytop P′ eine nicht-ganzzahlige Ecke x^{∗} besitzt, und Ax ≥ a sei ein Gegenbeispiel, das minimal in der Anzahl der Variablen ist.

Da A′ monoton ist, kann man o. B. d. A. annehmen, daß alle Einträge nichtnegativ sind (evtl. Spalten von A mit Negationen substituieren). Wegen der Maximalität enthält A′ alle nicht-negativen Zeilen von A. x^{∗} ist als Ecke von P′ die eindeutige Lösung eines Gleichungssystems Bx = b, bestehend aus n linear unabhängigen Gleichungen aus A′x = a′, x = 0, x = 1.

Behauptung: Wegen der Minimalität des Gegenbeispieles stammen alle Gleichungen von Bx = b aus A′x = a′.

Beweis hiervon: Angenommen, dies sei nicht der Fall, und Bx = b enthalte noch Gleichungen der Form x = 0 bzw. x = 1; o. B. d. A. sei eine solche Gleichung x_{1} = δ, wobei δ = 0 oder 1.

Betrachte nun das Problem Āx̄ ≥ ā, das aus Ax ≥ a dadurch entsteht, daß jedes Auftreten von x_{1} durch δ ersetzt und entsprechend aufgelöst wird. Analog seien Ā′x̄ ≥ ā′ und B̄x̄ = b̄ erklärt. Dann definiert Āx̄ ≥ ā ein ganzzahliges Polytop P̄, denn wenn x̄ nicht-ganzzahlige Ecke von P̄ wäre, dann wäre (δ, x̄) nicht-ganzzahlige Ecke von P; Widerspruch zur Ganzzahligkeit von P. Also ist x̄^{∗} = (x_{2}^{∗}, …, x_{x}^{∗}) eindeutige Lösung von B̄x̄ = b̄ und deshalb nichtganzzahlige Ecke von Ā′x̄ ≥ ā′. Damit wäre dies ein Gegenbeispiel mit einer Variablen weniger als Ax ≥ a; Widerspruch zur Minimalität des Gegenbeispieles. Damit ist die Behauptung bewiesen.

Um jetzt zu zeigen, daß x^{∗} Ecke von P ist, reicht es, zu zeigen, daß x^{∗} ∈ P, da P ⊆ P′. Hierfür genügt es, zu zeigen, daß x^{∗} alle Primimplikanten erfüllt, da jede Ungleichung aus Ax ≥ a von irgendeinem Primimplikanten absorbiert wird.

Annahme: Es gibt einen Primimplikanten cx ≥ γ, der von x^{∗} nicht erfüllt wird. Dann gilt c_{t} = −1 für mindestens ein t, da cx ≥ γ bei c ≥ 0 bereits zu A′x ≥ a′ gehört und somit von x^{∗} erfüllt wird.

1. Fall: Es gibt ein c_{t} = −1, so daß in Bx = b keine Gleichung eine Klausel repräsentiert, die mit cx ≥ γ nach x_{t} resolviert werden kann. Wegen der Regularität von B gibt es aber mindestens eine Gleichung in Bx = b, die x_{t} enthält (sonst Nullspalte in B). Da Bx = b nach obiger Behauptung Teilsystem von A′x = a′ ist, repräsentiert diese Gleichung eine Klausel, die nicht mit cx ≥ γ nach x_{t} resolviert werden kann. Diese Gleichung und die Klausel cx ≥ γ können geschrieben werden als

x_{t} + x_{t′}  + ∑_{j∉{t,t′}} b_{j}x_{j} = 1  (1)
(1 − x_{t}) + (1 − x_{t′})  + ∑_{j∉{t,t′}} f_{j}(x_{j}) ≥ 1,  (2)

für ein t′ ≠ t, wobei b_{j} ≥ 0 für alle j, und f_{j}(x_{j}) ist x_{j}, 1 − x_{j} oder 0.

Da x^{∗} aber Gleichung (1) erfüllt, gilt x_{t}^{∗} + x_{t′}^{∗} ≤ 1, und damit (1 − x_{t}^{∗}) + (1 − x_{t′}^{∗}) ≥ 1, also erfüllt x^{∗} auch (2); dies entsprach der Klausel cx ≥ γ, die von x^{∗} nicht erfüllt wurde. Widerspruch !

2. Fall: Für jedes c_{t} = −1 kann cx ≥ γ mit einer durch eine Gleichung in Bx = b repräsentierten Klausel nach x_{t} resolviert werden. Die Klausel cx ≥ γ kann geschrieben werden als

∑_{j=1}^{u}(1 − x_{j}) + ∑_{j=u+1}^{n} c_{j}x_{j} ≥ 1,  (3)

wobei c_{j} ≥ 0 für j = u+1, …, n. Die Gleichungen, die die Klauseln repräsentieren, mit denen cx ≥ γ nach x_{1}, …, x_{u} resolviert werden kann, lassen sich schreiben als

x_{t} + ∑_{j=u+1}^{n} b_{tj}x_{j} = 1  (4)

für t = 1, …, u, wobei alle b_{tj} ≥ 0. Resolviert man jetzt die der Ungleichung (3) entsprechende Klausel nacheinander mit den entsprechenden der Gleichungen (4), so erhält man die Ungleichung

∑_{j=u+1}^{n} d_{j}x_{j} ≥ 1,  (5)

wobei d_{j} = max {c_{j}, max_{t∈{1,...,u}} b_{tj}}. Gleichung (4) wird von x^{∗} erfüllt; löst man (4) für jedes t nach x_{t} auf und setzt dies in die linke Seite von (3) ein, ergibt sich

∑_{j=u+1}^{n} (c_{j} + ∑_{t=1}^{u} b_{tj}) x_{j}^{∗}.  (6)

Ungleichung (5) muß aber von einem Primimplikanten aus Ax ≥ a absorbiert werden; weil sie jedoch nur positive Literale enthält, muß dieser Primimplikant bereits in A′x ≥ a′ enthalten sein und wird demnach von x^{∗} erfüllt. Deshalb erfüllt x^{∗} auch (5). Da jetzt in (5) bereits die Summe über die Maxima der c_{j} und b_{j} größer als 1 ist, ist erst recht (6), was die rechte Seite von (3) war, größer als 1. Also erfüllt x^{∗} auch (3), was die von x^{∗} nicht erfüllte Klausel repräsentierte; Widerspruch !

Also ist x^{∗} ∈ P und damit auch nicht-ganzzahlige Ecke von P; Widerspruch zur Voraussetzung, daß P ganzzahlig ist.

4.2.2 ”⇐“

Sei für jedes maximale Set-Cover-Teilproblem A′ ≥ a′ von Ax ≥ a das durch A′x ≥ a′, 0 ≤ x ≤ 1 beschriebene Polytop ganzzahlig.

Annahme: Das durch Ax ≥ a, 0 ≤ x ≤ 1 definierte SAT-Polytop habe eine nicht-ganzzahlige Ecke x^{∗}.

Wir konstruieren jetzt, ausgehend von dem Ecken-definierenden System E von n linear unabhängigen Gleichungen aus Ax = a, x = 0, x = 1, dessen eindeutige Lösung x^{∗} ist, ein monotones System M aus n dieser Gleichungen, dessen eindeutige Lösung auch x^{∗} sein soll. Dies würde bedeuten, daß es ein maximales SC-Teilproblem gibt, dessen Polytop x^{∗} als nicht-ganzzahlige Ecke hätte.

Für jedes j füge die Gleichung x_{j} = 1 zu E hinzu, falls x_{j}^{∗} = 1, und x_{j} = 0, falls x_{j}^{∗} = 0. Da E den Rang n hat und die Gleichungen der Form x_{j} = 1 und x_{j} = 0 linear unabhängig sind, sind letztere auch in einem n Gleichungen umfassenden Teilsystem E′ von E enthalten, das immernoch x^{∗} als eindeutige Lösung hat.

Die Gleichungen in E′, die Teil des Systems Ax = a sind, seien die Klausel-Gleichungen, die anderen die Schranken-Gleichungen. Die i-te Klausel-Glei-chung habe die Form ∑_{j} f_{ij}(x_{j}) = 1, wobei jedes f_{ij}(x_{j}) = x_{j}, 1 − x_{j} oder 0 ist. Außerdem sei x^{∗} gebrochen für j ∈ N_{1} und ganzzahlig für j ∈ N_{2}.

Konstruiere nun M wie folgt: Setze M zunächst gleich E′. Wähle ein beliebiges x_{t}, das in den Klausel-Gleichungen mit unterschiedlichem Vorzeichen vorkommt, also f_{it}(x_{t}) = x_{t} und f_{i′t}(x_{t}) = 1−x_{t} für zwei Gleichungen i und i′.

Wir zeigen nun zuerst, daß x_{t}^{∗} gebrochen sein muß. Wenn die Klauseln zu den Gleichungen i und i′ dann resolviert werden können, ist es möglich, bei Beibehaltung der eindeutigen Lösung x^{∗} und ohne Zerstörung bereits bestehender Monotonie, den Vorzeichenkonflikt zu entfernen.

Behauptung: x_{t}^{∗} ist gebrochen.

Die Koeffizientenmatrix B der Gleichungen aus M hat die Struktur: (\begin{matrix}C_{1} & C_{2} \\ D_{1} & D_{2} \\ 0 & 1 \end{matrix}).

Die linke Hälfte enthält die Spalten aus N_{1}, die rechte Hälfte die aus N_{2}.

(C_{1}, C_{2}) besteht aus den zwei Zeilen i und i′. I enthält die Koeffizienten der Schranken-Gleichungen.

Angenommen, x_{t}^{∗} = 1. Weil x_{j}^{∗} für alle j ∈ N_{1} gebrochen ist und ∑_{j∈N_{1}∪N_{2}} f_{ij}(x_{j}^{∗}) = 1, muß f_{ij}(x_{j}) = 0 für alle j ∈ N_{1} sein. Das bedeutet, daß Zeile i Linearkombination der Zeilen in (0, I) ist. Dies widerspricht aber der Regularität von B. Analog hat x_{t}^{∗} = 0 zur Folge, daß die Zeile i′ Linearkombination der Zeilen in (0, I) und somit die Nichtsingularität von B verletzt ist. Damit Behauptung gezeigt.

Behauptung: Die Klauseln i und i′ sind resolvierbar.

Angenommen, sie wären nicht resolvierbar. Dann haben die Gleichungen i und i′ die Form

x_{t} + x_{t′}  + ∑_{j∉{t,t′}} f_{ij}(x_{j}) = 1
(1 − x_{t}) + (1 − x_{t′})  + ∑_{j∉{t,t′}} f_{i′j}(x_{j}) = 1,

oder sie haben die Form

x_{t} + (1 − x_{t′})  + ∑_{j∉{t,t′}} f_{ij}(x_{j}) = 1
(1 − x_{t}) + x_{t′}  + ∑_{j∉{t,t′}} f_{i′j}(x_{j}) = 1.

Im oberen Fall erfüllt x^{∗} beide Gleichungen; ihre Addition und die Tatsache, daß alle f_{ij}(x^{∗}) ≥ 0, ergibt:

∑_{j∉{t,t′}} f_{ij}(x_{j}^{∗}) = ∑_{j∉{t,t′}} f_{i′j}(x_{j}^{∗}) = 0.

Nach der ersten Gleichung folgt also x_{t}^{∗} + x_{t′}^{∗} = 1. Da x_{t}^{∗} gebrochen ist, ist auch x_{t′} gebrochen und t′ ∈ N_{1}. Weil x_{j}^{∗} gebrochen ist für alle j ∈ N_{1}, sind f_{ij} und f_{i′j} Nullfunktionen für alle j ∈ N_{1}\{t, t′}. Daher sind die beiden Zeilen von C_{1} Negationen voneinander. Analoges gilt für den unteren Fall: die Addition der beiden Gleichungen ergibt x_{t}^{∗} = x_{t′}^{∗}, also wieder t′ ∈ N_{1}, und f_{ij} sowie f_{i′j} sind Nullfunktionen für alle j ∈ N_{1}\{t, t′}. Die zwei Zeilen von C_{1} sind auch hier Negationen voneinander.

In beiden Fällen hat C_{1} also nicht vollen Rang. Nun ist aber

det(B) = det (\begin{matrix}C_{1} \\ D_{1} \end{matrix})

nur dann nicht Null, wenn C_{1} vollen Rang hat. Dies ist ein Widerspruch zur Regularität von B. Daher sind die beiden Klauseln i und i′ resolvierbar.

Die zu den beiden Klauseln gehörenden Klauselgleichungen können also geschrieben werden als

x_{t} + ∑_{j∈J_{1}} f_{ij}(x_{j})  + ∑_{j∈J_{3}} f_{ij}(x_{j})  = 1
(1 − x_{t})  + ∑_{j∈J_{2}} f_{i′j}(x_{j}) + ∑_{j∈J_{3}} f_{ij}(x_{j})  = 1,

wobei f_{ij} für jedes j ∈ J_{3} nicht die Nullfunktion sei. Der Resolvent

∑_{j∈J_{1}} f_{ij}(x_{j}) + ∑_{j∈J_{2}} f_{i′j}(x_{j}) + ∑_{j∈J_{3}} f_{ij}(x_{j}) ≥ 1  (7)

wird von einer Klausel i′′ aus Ax ≥ a absorbiert, weil Ax ≥ a nach Voraussetzung alle Primimplikanten enthält. x^{∗} erfüllt sowohl die beiden Klauselgleichungen i und i′ als auch deren Resolventen. Zieht man nun die Summe von i und i′ vom Resolventen ab, erhält man

∑_{j∈J_{3}} f_{ij}(x_{j}^{∗}) = 0.

Dies in die Summe der beiden Klauselgleichungen eingesetzt ergibt, daß x^{∗} die Resolventen-Ungleichung (7) mit Gleichheit erfüllt. Da für j ∈ J_{3} gilt: f_{ij}(x_{j}^{∗}) = 0, aber hier kein f_{ij} die Nullfunktion ist, enthält M die Schranken-Gleichung x_{j} = 0 oder x_{j} = 1.

Konstruiere nun ein System von Gleichungen M′ aus M wie folgt: ersetze eine der beiden Gleichungen i oder i′ durch den als Gleichung geschriebenen Primimplikanten i′′, der den Resolventen von i und i′ absorbiert, also

∑_{j∈J′_{1}} f_{ij}(x_{j}) + ∑_{j∈J′_{2}} f_{i′j}(x_{j}) + ∑_{j∈J′_{3}} f_{ij}(x_{j}) = 1,

wobei J′_{k} ⊂ J_{k} für k = 1, 2, 3. Da x^{∗} sowohl die Summe von i und i′ (mit Gleichheit) als auch den Primimplikanten i′′ erfüllt, erfüllt x^{∗} auch diese letzte Gleichung, da die Mengen J′_{k} ja höchstens kleiner sind. Also erfüllt x^{∗} alle Gleichungen aus M′.

Bleibt noch zu zeigen, daß x^{∗} einzige Lösung von M′ ist. Weil f_{ij}(x^{∗}) = 0 ist für j ∈ J_{3}, und x^{∗} die letzte Gleichung und (7) mit Gleichheit erfüllt, müssen f_{ij}(x_{j}^{∗}) = 0 für j ∈ (J_{1}\J′_{1}) und f_{i′j}(x_{j}^{∗}) = 0 für j ∈ (J_{2}\J′_{2}) sein. Durch die Schranken-Gleichungen x_{j} = 0 bzw. x_{j} = 1, die ja zu M′ gehören, sind f_{ij}(x_{j}) = 0 für j ∈ (J_{1}\J′_{1}) und f_{i′j}(x_{j}) = 0 für j ∈ (J_{2}\J′_{2}). Also erfüllt jedes x, das die Gleichungen aus M′ erfüllt, auch alle Gleichungen von M. Einzige Lösung von M war aber das x^{∗}; also ist x^{∗} auch einzige Lösung von M′.

Wenn jetzt M′ das neue M darstellt, ist x^{∗} nach wie vor eindeutige Lösung von M. Da aber die Gleichung i′′ (der Primimplikant, der den Resolventen von i und i′ absorbiert) x_{t} nicht mehr enthält, ist ein Vorzeichenkonflikt aus M entfernt.

Durch wiederholte Anwendung dieser Prozedur entsteht so das gewünschte monotone System M.

Dann gibt es auch ein maximales SC-Teilproblem, das die zu M gehörenden Klauseln umfaßt, und dessen Polytop das nicht-ganzzahlige x^{∗} als Ecke enthält. Dies ist ein Widerspruch zur Voraussetzung. Also muß auch das SAT-Polytop ganzzahlig sein.

q. e. d.

Inhaltsverzeichnis

1 Einleitung 1

2 Logik-Grundlagen 1 2.1 Das SAT-Problem . . . . . . . . . . . . . . . . . . . . . . . . . 1 2.2 Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.3 Der Algorithmus von Quine . . . . . . . . . . . . . . . . . . . 3

3 Polytop-Grundlagen 4 3.1 SAT als Polytop . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3.2 Maximale Set-Cover-Teilprobleme . . . . . . . . . . . . . . . . 5

4 Über die Ganzzahligkeit von SAT-Polytopen 7 4.1 Der Satz . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 4.2 Der Beweis . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

4.2.1 ”⇒“ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 4.2.2 ”⇐“ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10