WS05/06 Rechnergestütztes Beweisen (Hofmann) 2005-10-27 VL4 DPLL (Davis & Putnam, Logemann & Loveland) ==== verwendet in SAT-Solvern. Unit propagation: Enthält eine Klauselmenge CC eine Einerklausel {A} bzw. {NOT A}, so kann man CC durch CC[A->tt] bzw. C[A->ff] ohne Veränderung der Erfüllbarkeit ersetzen. Der Abschluss einer Klauselmenge CC unter Unit propagation wird gebildet, in dem man diesen Schritt so lange wiederholt, bis keine Einerklauseln mehr vorhanden sind. Beispiel: 3 Tauben (A,B,C), 2 Schläge (1,2) A1 OR A2, B1 OR B2, C1 OR C2, NOT A1 OR NOT B1, NOT B1 OR NOT C1, NOT A1 OR NOT C1, NOT A2 OR NOT B2, NOT B2 OR NOT C2, NOT A2 OR NOT C2, Versuch A1 = tt (1) gelöscht (4) NOT B1 (6) NOT C1 Durch Unit propagation: B1=C1=ff (2) B2 (3) C2 (4-6) gelöscht (7) NOT A2 (8) LEERE KLAUSEL Dann muss man noch A1 = ff durchführen. Jedesmal ist die Klauselmenge unerfüllbar. Algorithmus: Globale Var. CC (Klauselmenge) DPLL (eta) /* eta: partielle Belegung */ /* liefert "erfüllbar" zurück, falls CC durch eine eta erweiternde Belegung erfüllt werden kann, "unerfüllbar" sonst. Ausserdem kann C um solche Klauseln k erweitert werden, die aus CC logisch folgen: Jede Bewertung rho, die C erfüllt, erfüllt auch K */ DD := Abschluss von CC[eta] unter unit propagation eta' := die resultierende Erweiterung von eta Wenn DD leer, dann "erfüllbar". /* durch eta' */ Wenn BOX in DD, dann - finde kleinste Teilbelegung rho <= eta, die zu BOX geführt hat, - bilde Klausel K, die besagt, dass mindestens ein Atom anders als in rho gesetzt wird (Bsp: rho = {A->tt,B->ff,C->tt}, K= NOT A OR B OR NOT C), C := C union { K } /* Klausellernen */ - "unerfüllbar". Ansonsten: Wähle ein Atom nicht in dom(eta'). Wenn DPLL(eta'[A->tt]) "unerfüllbar", dann DPLL(eta'[A->ff]), ansonsten "erfüllbar". Optimierung: DD wird nicht explizit berechnet, sondern nur eta'. Satz von Haken: Es existiert eine Familie von Klauselmengen CC1, CC2, ..., so dass |CCn| = O(n^2) und jeder Resolutionsbeweis, dass CCn unerfüllbar enthällt Omega(c^n) Klauseln für festes c > 1 fest. Bem: CC_n = "n+1 Tauben passen in n Schläge" Bem: Aus DPLL-Lauf kann Resolutionsbeweis (direkt) extrahiert werden. Daher Laufzeit von DPLL auch exponentiell. Kürzerer Beweis des Satzes von WIDGERSON. Logik erster Stufe (Prädikatenlogik) ================== Beispielsätze: 1. Jeder Student hat Matrikel.nr. 2. Wenn eine Studentin sich nicht rückmeldet, wird sie exmatrikuliert. 3. Jeder Mensch ist ein Philosoph. 4. Es gibt einen Studenten, des sich über jede VL beschwert. 5. Es gibt eine Menge ohne Elemente. 6. Für jedes n in N existiert ein d in N, so dass 2^d <= n < 2^{d+1}. 7. Der Knirp jedes Bilgs ist ein Prugl aber belft keinen Quist. Die Prädikatenlogik gibt es typisiert und untypisiert. Untypisiert: ============ Variablen rangieren alle über denselben Bereich. Quantoren: FORALL x, EXISTS x Bsp: 1. FORALL x. student(x) => EXISTS y. nummer(y) AND hat_matr_no(x,y) 2. FORALL x. student(x) => NOT meldet_zurück(c) => wird_exmatr(x) 4. EXISTS x. student(x) AND FORALL v. vorlesung(v) => beschwert_sich(x,y) 7. FORALL b. bilg(x) => prugl(knirp(x)) AND FORALL q. quist(q) => NOT (belft(knirp(x),q)) Sprache erster Stufe L: enthält Prädikat-, Relations-, und Funktionssymbole Interpretation einer Sprache Menge D: Individuen-Bereich Prädikate und Funktionen für alle Symbole. 6. FORALL x. nat(x) => EXISTS d. nat(d) AND le(power2(d),n) AND lt(n,power2(plus(d,one))) Interpretation: D = R nat(x) <==> x in N power2(d) = 2^d plus(x,y) = x + y one = 1 le(x,y) <==> x <= y lt(x,y) <==> x < y In dieser Interpretation ist die Formel 6. wahr. Ändere ich die Interpretation, z.B., power2(d)=0, dann wird die Formel falsch. Typisierte Prädikatenlogik ========================== 6. FORALL x:nat. EXISTS d:nat. le(power2(d),n) AND lt(n,power2(plus(d,one))) 4. EXISTS x:student. FORALL v:vorlesung. beschwert_sich(x,y) Definition: Eine Sprache L der typisierten Prädikatenlogik ist ein Quadrupel (TT, PP, FF, ar) mit - TT ist eine Menge (von Typen) - PP ist eine Menge (von Prädikatsymbolen) - FF ist eine Menge (von Funktionssymbolen) - ar ist eine Funktion die jedem Prädikat- und Funktionssymbol eine Stelligkeit (engl. arity), ein Tupel von Typen, zuordnet. Für Prädikatensymbole P in PP schreiben wir das Tupel (tau_1,...,tau_n) [tau_1,...,tau_n -> boolean], für Funktionssymbole f in FF (n>=1) [tau_1,...,tau_{n-1} -> tau_n]. Beispiel: 7. TT = {bilg, quist, knirp_t} PP = {prugl : [knirp_t -> boolean], belft : [knirp_t,quist -> boolean]} FF = {knirp : [bilg -> knirp_t]} Wir fixieren eine (abzählbare) Menge VV von Variablen. Ein Typisierungskontext K bezüglich einer Sprache L = (TT, PP, FF, ar) ist eine partielle Funktion von VV nach TT, manchmal geschrieben als x_1:tau_1, ..., x_n:tau_n. Wohltypisierte Terme und Formeln sind induktiv durch folgende Regeln definiert. Typisierungsurteil: K >L t : tau (tau darf auch boolean sein) K(x) = tau ------------ K >L x : tau K >L t_1 : tau_1 ... K >L t_n : tau_n f : [tau_1,...,tau_n -> tau] ---------------------------------------------------------------------- K >L f (t_1,...,t_n) : tau (diese Regel nochmal mit P/f, boolean/tau) K >L phi : boolean ---------------------- K >L phi : NOT boolean K >L phi : boolean K >L psi : boolean --------------------------------------- * in { AND, OR, =>, <=> } K >L phi * psi : boolean K, x:tau >L phi : boolean ------------------------- Q in { FORALL, EXISTS } K >L Qx:tau.phi : boolean Spezialfall: ar(f) = [ -> tau ] = tau, d.h. n=0, dann ist f eine Konstante. f : tau ------------ K >L f : tau Es gibt auch nullstellige Relationssymbole (Aussagenkonstanten). Semantik: Sei L eine Sprache L = (TT, PP, FF, ar). Eine Interpretation II von TT ist gegeben durch 1. Eine Menge II(tau) für jedes tau in TT. 2. Eine Teilmenge II(P) <= II(tau1) x ... x II(taun) für jedes P : [tau1,...,taun->boolean] in PP. 3. Eine Funktion II(f) : II(tau1) x ... x II(taun) -> II(tau) für jedes f : [tau1,...,taun -> tau] in FF. Falls 0 >L phi : boolean, so lässt sich phi unter II ein Wahrheitswert [|phi|]_II zuordnen.