WS05/06 Rechnergestütztes Beweisen (Hofmann) 2005-10-27 VL4 2007-10-30 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'. Anwendung: Schulstundenplanung U = Menge der Unterrichte l : U -> Lehrer k : U -> Klasse T = Menge der Timeslots = {1..35} Fuer jeden Unterricht und Timeslot t eine Variable x_u,t (Erfahrung: Nicht mit Var. geizen, lieber viele Variablen und dafuer einfache Klauseln). Fuer je zwei Unterrichte u1,u2 mit l(u1)=l(u2) oder k(u1)=k(u2) und t aus T eine Klausel NOT x_u1,t OR NOT x_u2,t Fuer jeden Unterricht u eine Klausel x_u,1 OR x_u,2 OR ... OR x_u,n Weiche Klauseln: * Falls u Hauptfach und t 6.Stunde oder Nachmittag: NOT x_u,t * Lehrer keine Hohlstunden. Heuristik: Schieberegler, wieviel % der weichen Klauseln verwendet werden (die dann zufaellig ausgesucht werden). Anwendung: Optimale Instruktionswahl, um Prozessorzyklen zu sparen. 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) PVS erlaubt Definition beliebiger Typen z.B. posnat = {x : nat | x > 0} Damit kann man schwierige Probleme in Typen kodieren, so dass Typsierung nicht mehr entscheidbar ist, sondern Beweise bedarf. Gute Praxis ist es, nur entscheidbare Typen zu verwenden. 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. (Auch: wohlgeformte Formeln.) 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 NOT phi : 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). Bemerkung: 1. Terme und Formel sind Baeume, werden aber linear notiert. 2. In Q x:tau. phi ist x eine gebundene Variable und darf jederzeit umbenannt werden (jedoch nicht in eine Variable, die in phi frei vorkommt!). Eigentlich steckt dahinter eine Aequivalenzklasse von Baeumen. Mit diesen Details setzen wir uns aber im Folgenden nicht auseinander. 3. Eine Formel phi ist geschlossen falls 0 >L phi : boolean. 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. Schreibweise: [[tau]]_II. 2. Eine Teilmenge II(P) <= II(tau1) x ... x II(taun) für jedes P : [tau1,...,taun->boolean] in PP. Schreibweise: [[P]]_II. 3. Eine Funktion II(f) : II(tau1) x ... x II(taun) -> II(tau) für jedes f : [tau1,...,taun -> tau] in FF. Schreibweise: [[f]]_II. Falls 0 >L phi : boolean, so lässt sich phi unter II ein Wahrheitswert [|phi|]_II zuordnen. 2005-11-02 Gegeben sei eine Interpretation II. Eine Bewertung rho eines Kontexts K = x1:tau1, ..., xn:taun ist eine partielle Funktion auf Variablen, so dass rho(xi) in [|taui|]_II (das ist dasselbe wie II(taui)). Durch Induktion über Term & Formelaufbau ordnen wir jedem Term K > t : tau und Bewertung rho von K einen Wert [[t]]_II,rho in [|tau|]_II und jeder Formel K > phi : boolean einen Wahrheitswert [|phi|]_II,rho in {tt,ff} zu. (Ich lasse den Subskript II im Folgenden weg.) [|x|]_rho = rho(x) [|f(t1,...,tn)|]_rho = [[f]]_II ([|t1|]_rho, ..., [|tn|]_rho) [|FORALL x:tau.phi|]_rho = tt gdw. [|phi|]_rho[x->v] = tt für alle Werte v in [|tau|] etc. (EXISTS, AND, OR, NOT) Bemerkung: Für Formeln unterscheiden wir * wohlgeformt (K > phi : boolean) [darf auch falsch sein] * wahr ([|phi|]_II,rho) * und beweisbar (G ==> phi) Definition. Eine geschlossene Formel phi (0 > phi : boolean) ist Tautologie (allgemeingueltig), wenn [|phi|]_II = tt (Abkürzung für [|phi|]_II,0) für alle II.