(c) W. Conen, Version 0.951 Aussagenlogik -- Verfahren zum Finden von Modellen Prof. Dr. Wolfram...

(c) W. Conen, Version 0.95 1

Aussagenlogik -- Verfahren zum Finden von Modellen

Prof. Dr. Wolfram Conen, INTA, FH GE


Formeln als Constraints

Wie kann man „gut“ Modelle finden? Gegeben sei eine Formel F in KNF. F besteht aus k Klauseln, die aus insgesamt n Aussagenvariablen

aufgebaut sind. Aufgabe: Belegen Sie jede Variable so mit einem Wert aus {0,1},

daß jede Klausel (und damit F) wahr wird.



Jede einzelne Klausel Fi ist endlich und hat die Form {L1,...,Lni}, steht

also für L1 Ç... Ç Lni.

Eine Klausel wird genau dann wahr, wenn mindestens eines der Literale in ihr wahr ist

Die ganze Formel F wird wahr, wenn alle Klauseln wahr werden. Was macht die Situation nun kompliziert?

Jede einzelne Klausel können wir immer erfüllen! z.B. {A} Aber die Klauseln sind natürlich nicht unabhängig von

einander... {A},{:A}... unerfüllbar!



Wir können uns jede aussagenlogische Formel(menge) als Constraintnetzwerk vorstellen:

Die Variablen sind die Aussagenvariablen

Die Domains sind alle {0,1}

Die Constraints sind die Klauseln, d.h. die Disjunktionen (kann auch unär sein, also nur ein Literal enthalten)

Alle Constraints (und damit die „große“ Konjunktion) müssen erfüllt werden!



F = (: A Ç : B Ç C) Æ (A Ç : B Ç : C) Klauselform: { {: A, : B, C}, {A,: B,: C}}

A B C

Beobachtung: Wenn es eine Variable gibt (hier B), die nur von Kanten einer Farbe getroffen wird und mit jedem Constraint verbunden ist, dann ist die Formel erfüllbar!



F = ... Æ A Æ : B ...

B

Beobachtung: Unäre Constraints (also solche mit nur einer Kante) legen den Wert der beteiligten Variable fest!

A



F = ... Æ A Æ : B ...

B

Beobachtung: Unäre Constraints (also solche mit nur einer Kante) legen den Wert der beteiligten Variable fest!

A = 1 = 0



F = ... Æ A Æ : B Æ (B Ç C)...

B

Beobachtung: Nach einer Fixierung kann man nicht mehr erfüllbare Kanten löschen (es sei denn, sie gingen zu anderen unären Constraints, s. nächste Beobachtung)

A = 1 = 0 C



F = ... Æ A Æ : B Æ (B Ç C)...

B

Beobachtung: Nach einer Fixierung kann man erfüllte Constraints und nicht mehr erfüllbare Kanten löschen (es sei denn, sie gingen zu anderen unären Constraints, s. nächste Beobachtung)

A = 1 = 0 C



F = ... :A Æ A ...

A

Beobachtung: Wenn eine Variable von zwei Kanten unterschiedlicher Farbe getroffen wird, die zu unären Constraints führen, dann ist die gesamte Formel unerfüllbar!



F = (:A Ç A) Klauselform: { {: A,A} }

A

Beobachtung: Wenn eine Variable mit einem Constraint über zwei Kanten unterschiedlicher Farbe verbunden ist, dann ist dieser Constraint immer erfüllt! (und kann entfernt werden). Übrigens haben wir genau dann eine Tautologie, wenn der reduzierte Graph nur noch aus Kreisen besteht...

wird zu A



F = (B Ç C) Æ (A Ç : B Ç : C) Klauselform: { {B, C}, {A,: B,: C}}

A B C

Beobachtung: Variablen mit Kanten nur einer Farbe kann (manchmal: muß) man in ihrem Wert fixieren und ...




A B C

Beobachtung: Variablen mit Kanten nur einer Farbe kann (manchmal: muß) man in ihrem Wert fixieren ...

= 1




A B C

... und sicher erfüllte Constraints kann man löschen!

= 1




A B C

= 1

Jetzt gilt Beobachtung 1! Der Constraint ist erfüllbar! (durchC=1 und B=1, oder C=1 und B=0, oder C=0 und B=1)



F = (: A Ç B Ç C) Æ (A Ç : B Ç : C) Klauselform: { {: A, : B, C}, {A,: B,: C}}

A B C

Beobachtung: Der Constraintgraph ist erfüllbar, wenn es ein Matching gibt, dass jedem Quadrat einen Kreis zuordnet, so dass jeder Kreis nur von Kanten einer Farbe getroffen wird.



F = (: A Ç B Ç C) Æ (A Ç : B Ç : C) Klauselform: { {: A, : B, C}, {A,: B,: C}}

A B C

Ein Modell ergibt sich aus den Farben der Kanten (schwarz = 1, rot = 0) oder kann frei gewählt werden (keine Kante).



F = (: A Ç : B Ç C) Æ (A Ç : B Ç : C) Æ (B Ç : C) Æ (: A) Æ (C)

A B C

Wenden wir die Beobachtungen an:1) Unäre Constraints führen zu fixierten Variablenwerten2) Sicher erfüllte Constraints werden entfernt




A B C

Wenden wir die Beobachtungen an:3) Unerfüllbare Kanten werden entfernt

0 = = 1




A B C

Wenden wir die Beobachtungen an:4) Widerspruch wird erkanntDas ging hier übrigens auch so schön, weil die Formel obeneine Hornformel ist...

0 = = 1



F = (: A Ç : B Ç C) Æ (A Ç : B Ç : C) Æ (B Ç : C) Æ (: A Ç B) Æ (C Ç : B)

A B C

Und hier? Probieren wir folgende Heuristik:1) Wähle die Variable mit den meisten Kanten einer Farbe

(und den zugehörigen Wert)Und wende dann die Reduktionsregeln an...




A B C

...und nochmals!

0 =




A B C0 == 0 = 0

Also ist F erfüllbar. Wären übrigens noch andere Modelle möglich? Probieren wir es:




A B C

Diesmal wählen wir den anderen „Fall“ B=1 zu Beginn(mit B=0 kann es keine weiteren Modelle geben, alleübrigen Wertzuweisungen waren erzwungen!)

1=




A B C

Jetzt können wir die „normalen“ Reduktionsregeln anwenden.

1=




A B C

... und nochmal.

1= = 1




A B C

Also ist auch A=1, B=1, C=1 ein Modell (sonst aber nichts!)

1= = 1= 1




A B C

Man könnte auch „lokaler“ denken:1. Welche Constraints sind „am schwersten“ zu erfüllen – diemit den wenigsten Kanten. Wählen wir einen solchen!2. Von den beteiligten Variablen wählen wir dann diejenigemit den meisten Kanten der Farbe der jeweiligen KANTE von der Variable ZUM GEWÄHLTEN CONSTRAINT




A

C2

B C

C3

C5

C4C1

Hier würden wir also C1, C4 oder C5 wählen. Bei Wahl von C1 würde B=1 oder A=0 bestimmt, bei Wahl von C4 wäre es B=0, bei C5 wäre es eine gleichberechtigte Wahl zwischen B und C.

Bei diesem Tiebreaking könnte es sinnvoll sein, die Variable zu wählen, von der weniger Kanten der „falschen“ Farbe wegführen. Hier wäre das C (2xschwarz statt 3xrot)




A

C2

B C

C3

C5

C4C1

Führen wir die letzte Variante durch: also C=0 wählen

= 0




A

C2

B C

C4C1

Das führt zu B=0

= 0




A B C

C1

Das führt zu B=0

= 0= 0




A B C

Und dann zu A=0, und damit zum gleichen Ergebnis, wie dievorige Heuristik

= 0= 0= 0


Formeln als Constraints: Gesamtablauf

Eingabe: Formel F Ausgabe: ein Modell oder „UNERFÜLLBAR“while (TRUE) do Falls keine Constraints mehr vorhanden, gib das gefundene

Modell aus: alle Wertfixierungen und eine beliebige Wahl für unfixierte Variablen, STOPP

Falls eine Variable mit mindestens zwei (verschiedenen!) unären Constraints über Kanten unterschiedlicher Farbe verbunden sind, gib „UNERFÜLLBAR“ aus, STOPP

Wende die Reduktionsregeln solange an, bis keine Änderung mehr erfolgt

Falls gar keine Änderung stattfand, fixiere heuristisch einen Variablenwert (hier wäre auch eine zufällige Wahl möglich)


Formeln als Constraints: Ein Problem

A B C

Wir wenden nochmal die erste Heuristik an: Die Wahl fällt auf B, also B=0.

D

F = (A Ç :B Ç C Ç D) Æ (:A Ç :C) Æ (:B Ç :C) Æ (C Ç B) Æ (:A Ç :B) Æ (A Ç B) Æ (D Ç :B) Æ (:C Ç :D)



A B C

Jetzt müssen C und A jeweils 1 werden, das führt natürlich zu ...

D

= 0




A B C

...einem Widerspruch!

D

= 0

= 1= 1




A B C

Wenn wir stattdessen B = 1 setzen...

D




A B C

Wenn wir stattdessen B = 1 setzen...

D

= 1




A B C

Jetzt wird reduziert...

D

= 1


= 0

= 0



A B C

... und fertig! A = C = 0, B = D = 1 ist ein Modell für F (das einzige Modell, denn nach der Wahl von B = 1 waren alle anderen Werte erzwungen)

D

= 1


= 0

= 0

= 1



Zu welchen Problemen kann dieser Ablauf also führen? Klar: Es kann sein, dass wir „UNERFÜLLBAR“ ausgeben, obwohl es

ein Modell gibt! ...aber wir wissen immerhin: wenn wir ein Modell ausgeben,

dann ist das auch korrekt! Wir müßten hierzu noch formal beweisen, dass unsere

Reduktionsregeln den semantischen Gehalt des Netzwerks bzw. der repräsentierten Formeln nicht verändern

Wie können wir dieses Problem lösen?



Klar – wir müssen das Verfahren in einen Tiefensuche-Algorithmus einbetten!

Eingabe, Ausgabe wie gehabt Solve(Constraintnetz F)

Prüfe Abbruchbedingung wie vorhin, falls eine zutrifft, gib das bestimmte Resultat

zurückWähle heuristisch eine Variable v und einen Wert w für v ausFixiere v auf w; reduziere F zu F‘Rufe Erg Ã Solve(F‘) aufFalls Erg = „UNERFÜLLBAR“, dann fixiere v auf :w;

reduziere F zu F‘ und rufe Erg Ã Solve(F‘) aufGib Erg zurück



Insgesamt könnte der Ablauf so aussehen: Gegeben ist ein Constraintnetz F Reduziere F zu F‘ Gib das Ergebnis von Solve(Constraintnetz F‘) zurück

Hier wird zunächst die Reduktion verwendet, um offensichtlich im Graphen enthaltene Konsequenzen sichtbar zu machen Zur Erinnerung: Solve beginnt mit einer Überprüfung der

Abbruchbedingungen



A

C4

B C

C6

C2

C3

Hätte übrigens die zweite Heuristik ohne Backtracking funktioniert?Kandidaten: C3, C8, C1, C2, C5, C7 (alle mit zwei Kanten)

C1

C5

D


C7C8



A

C4

B C

C6

C2

C3

Weniger falsche Farben? C5/D=1, C8/D=C=2, C2/C=3, C7/C=2, C3/A=2, C1/A=2. Also wählen wir C5 mit 1 für D.

C1

C5

D


C7C8



A

C4

B C

C2

C3

Weitere Reduktion: C = 0

C1

D


C7C8

= 1



A B C

C2

C3

Weitere Reduktion: B = 1

C1

D


= 1

= 0



A B C

C3

Weitere Reduktion wäre A = 0, damit ist das Modell gefunden!

D


= 1

= 0

= 1



Warum müssen wir nur über die Wertauswahl „backtracken“, nicht aber über die Variablenwahl? Weil die Reihenfolge der Variablenwahl für die Erfüllbarkeit

keine Rolle spielt! Wohl aber für die Laufzeit der Suche...

Was kann jetzt noch Übles passieren? Eine Entscheidung „weit oben“ kann schlecht sein und erfordert

sehr viel Backtracking, bevor sie letztlich zurückgenommen wird (Lösung: Backjumping oder „Vorausschauen“)

Beim Backtracking kann es zu „doppelter“ Arbeit kommen: Teilbelegungen werden mehrfach ausprobiert! (Lösung: erfolgreiche Teilbelegungen merken)

Das haben wir uns schon im Constraint-Teil angeschaut!


Modelle finden...

Wir haben versucht, „sinnvoll“ die nächste Variable zu wählen ...und bei den Reduktionen unser Wissen über Notwendigkeiten

konsequent anzuwenden (und dadurch die Wertzuweisungen zu propagieren)

Diese Idee des „rationalen“ Verbesserns von zunächst naive algorithmischen Ideen liegt auch den folgenden Verfahren zur Erfüllbarkeits-Analyse zu Grunde.

Ürbigens entspricht das erste Verfahren ziemlich genau unseren eben dargestellten Ideen...


Modelle finden...

Martin Davis und Hillary Putnam schlugen 1960 die Grundlage für das folgende Verfahren (62 als Verfeinerung publiziert von Davis, Logemann, Loveland)

Ich gebe hier das Skelett des Algo an (diverse Verfeinerung sind möglich zur Effizienzsteigerung)

So finden sie den Algo auch in Russell/Norvig function DPLL-SATISFIABLE?(F) returns true or false

inputs: F, eine aussagenlogische Formel

clauses Ã die Klauseln der Klauselform einer KNF von F symbols Ã eine Liste der Aussagenvariablen in F return DPLL(clauses,symbols,[ ]).


Modelle finden...

function DPLL(clauses,symbols,model) returns true or false

if jede Klausel in clauses wahr ist unter model then return true if eine Klausel in clauses falsch ist unter model then return false P, value Ã FIND-PURE-SYMBOL(symbols,clauses,model)

// Ein Symbol, das nur als positives oder negatives Literal vorkommt if P is non-null then return

DPLL(clauses, symbols-P, EXTEND(P,value,model)) P, value Ã FIND-UNIT-CLAUSE(symbols,clauses,model)

// Eine Klausel, die nur ein Literal enthält (bzw. eines ohne Wert) if P is non-null then return

DPLL(clauses, symbols-P, EXTEND(P,value,model)) P Ã FIRST(symbols); rest Ã REST(symbols); return DPLL(clauses,rest,EXTEND(P,true,model)) or

DPLL(clauses,rest,EXTEND(P,false,model))


Modelle finden...

Laut Russell/Norvig löst die moderne CHAFF-Implementierung des Davis/Puttnam-Verfahrens Hardware-Verifikationsprobleme mit bis zu einer Million Variablen

Wie gesehen wird hier eine Lösung Schritt für Schritt konstruiert Man kann aber auch von einer Belegung ausgehen und diese nach und

nach verbessern. Das versucht das folgende Verfahren:


Modelle finden...

function WALKSAT(clauses,p,max_flips) returns a satisfying model or failure

inputs: clauses (wie vorhin), p (die Wahrscheinlichkeit für die Wahl des „Random Walk“), max_flips (Anzahl der Flips, die höchstens erlaubt sind, um eine Lösung zu finden)

model Ã eine zufällige Belegung for i Ã 1 to max_flips do

if model erfüllt clauses then return model clause Ã zufällig gewählte Klausel, die unter model falsch ist Mit Wahrscheinlichkeit p setze Ai auf : Ai für ein zufällig

gewähltes Symbol Ai aus clause Sonst setze Ak auf : Ak für eines der Symbole aus clause, die die

Anzahl erfüllter Klauseln maximiert return failure


Modelle finden...

WALKSAT und ähnliche Varianten sind sehr populäre Methoden, um nach erfüllenden Modellen zu suchen

WALKSAT ist häufig sehr effizient! Es wählt mit einer Min-Conflicts-Strategie Kandidaten aus (aber auch

zufällig) Es findet natürlich nicht immer eine Lösung...

man könnte max_flips auf unendlich setzen... ...aber auch das gibt keine Garantie: denn ev. gibt es kein Modell! Allerdings könnte man (vorsichtig...) annehmen, dass nach einer

vergleichsweise langen Laufzeit keine Lösung mehr zu erwarten ist (das kann aber natürlich falsch sein...)

Dennoch sind die „zufälligen“ Verfahren häufig eine gute Wahl, s. Bild im Mitschrieb


Modelle finden...

Mit Modellen für Aussagenlogik kann man überraschend viel anfangen: z.B. planen oder Hardware verifizieren

Außerdem kann/könnte man jedes NP-harte Problem mit polynomialem Aufwand auf SAT (also das Erfüllbarkeits- bzw. Satisfiability Problem der Aussagenlogik) abbilden...

...wenn man also eine effiziente Lösung für SAT finden würde, dann wäre auch die NP=P-Frage gelöst!

Übrigens stammt die (oder eine der) beste(n) „zufälligen“ Lösungen (mit einem Worst-Case-Verhalten von 4/3n) von Uwe Schöning (zur Anwendung auf das sogenannte 3-KNFSAT-Problem. Hier bestehen die Klauseln nur aus höchstens 3 Literalen. Jede Formel kann man in eine Formel in 3-KNF transformieren, die

eine äquivalente Menge von Modellen hat (Aufwand!) [seltsame Formulierung aus Russell/Norvig]

Das 3-KNFSAT-Problem ist aber auch NP-vollständig


Modelle finden...

Schöning(clauses,symbols) returns ein Modell Wähle zufällig eine Belegung for i Ã 1 to n do

Falls die aktuelle Belegung die Formel erfüllt, gib sie zurück und stoppe

Wähle zufällig eine nicht-erfüllte Klausel aus Wähle zufällig ein Literal dieser Klausel aus Ändere („flip“) den Wahrheitswert dieser Variable

Das ist noch einfacher als WALKSAT... Wenn man den Algo jetzt c*(4/3)n mal aufruft (er terminiert sicher: for-

Schleife!) mit jeweils anderen „zufälligen“ Anfangsbelegungen ...dann beträgt die Fehlerwahrscheinlichkeit nur noch e-c

Der Algo findet also „fast sicher“ eine Belegung (wenn es eine gibt) Und hat einen asymptotischen Aufwand von „nur“ 1.3334n

Ob er auch „praktisch“ guten Aufwand hat, ist eine zweite Frage.


Literatur...

Auch spannend: Analytische Tableaux‘s, die auf disjunktiven Normalformen arbeiten (s. z.B. Smullyan)

Die Ausführungen zu Davis/Putnam und WALKSAT stammen aus Russell/Norvig (wie gehabt)

Einige Erläuterungen zu und von Schöning finden sich in Uwe Schöning, Ideen der Informatik, 2. Auflage, Oldenbourg

Date post:	05-Apr-2015
Category:	Documents
Upload:	rosalind-neier
View:	107 times
Download:	0 times

(c) W. Conen, Version 0.951 Aussagenlogik -- Verfahren zum Finden von Modellen Prof. Dr. Wolfram...

Documents