Ja, herzlich willkommen. Sie werden sich an das Thema der letzten Sitzung erinnern. Die Aussagen

logische Resolution. Wir hatten gesehen, ein Verfahren zur Bestimmung der Erfüllbarkeit

einer gegebenen konjunktiven Normalform, das heißt, wenn wir jetzt eine Aussagen logische

Formel in voller Allgemeinheit auf Erfüllbarkeit prüfen wollen, müssen wir sie zunächst in

konjunktive Normalform transformieren, dann das Verfahren anwenden. Wir haben das Verfahren selbst

gesehen und wir haben es ausprobiert an zwei Beispielen. Wir haben gesehen, einmal den Fall,

wo das Verfahren negativ terminiert, also mit der Antwort unerfüllbar, wo wir also nach ein paar

Resolutionsschritten die leere Klausel erzeugt hatten und wir haben andererseits gesehen den

Fall, wo das Verfahren positiv terminiert, also mit einer Menge, auf die die Resolutionsregel nicht

mehr anwendbar ist und die die leere Klausel nicht enthält und die der Algorithmus also insofern als

erfüllbar erkennt. Ich erinnere noch mal an die Grundregel, die sogenannte Resolutionsregel,

auf der der gesamte Algorithmus basiert. Die sagt also, wenn ich in irgendeiner Klausel,

in meiner momentanen CNF ein positives Literal in einer Klausel finde und dasselbe Literal negiert

in einer anderen Klausel, womöglich anderen Klausel, dann darf ich die sogenannte bunte Kreide,

die sogenannte Resolventen, also die Klausel, die entsteht, indem ich aus den beiden gegebenen

Klauseln die beiden Vorkommen des betreffenden Literals entferne und die Klauseln ansonsten

zusammenschmeiße, diese Klausel darf ich zu meiner CNF dazu fügen. Das heißt, so ist diese

Regel zu lesen. Ich schreibe den Algorithmus jetzt nicht noch mal an. Der Algorithmus besteht also

darin, dass er immer wieder sich Klauseln in einer aktuellen CNF sucht, die also hier auf

dieses Format dieser Prämissen passen und wenn er die gefunden hat, die Resolvente zur CNF dazu

fügt, so sie denn noch nicht drin ist. Gut, das war als Algorithmus ja ganz schön, aber wir haben

bisher noch keinen Anlass zu glauben, dass dieser Algorithmus tatsächlich funktioniert, außer dass

wir gesehen haben, dass er in zwei Beispielen es tatsächlich korrekt getan hat. So, ich eben

angekündigt, ich schreibe ihn nicht noch mal an, ich schreibe ihn jetzt doch noch mal an, einfach

für die laufende Diskussion. Die Eingabe schreibe ich nicht noch mal an, also die Eingabe ist eine

CNF-Phi, die auf Erfüllbarkeit zu prüfen ist. Im ersten Schritt schauen wir nach, ob die leere

Klausel in Phi enthalten ist und wenn das der Fall ist, dann brechen wir ab mit der Antwort nein,

also unerfüllbar. Zweitens suchen wir jetzt ein Match der Resolutionsregel, sodass die entstehende

Resolvente C vereinigt D, dass die nicht in Phi enthalten ist. Das heißt, wir gucken, finden wir

solche Klauseln, die also zusammenpassen an einem Literal, einer enthält es positiv,

einer negativ, sodass die entstehende Resolvente noch nicht in unserer aktuellen CNF drin ist.

Und dann haben wir hier so eine mächtige Sprache, die uns also Suchalgorithmen einfach per Zauberwort

gibt. Und wenn das also viel schlägt, wenn wir so ein Ding nicht mehr finden,

dann brechen wir ab und geben Ja zurück. Also die Klausel ist erfüllbar, die Klauselmenge ist

erfüllbar, die CNF. So, wenn wir andererseits so einen Match gefunden haben, fügen wir die

Resolvente C vereinigt D tatsächlich zu Phi dazu und fangen wieder von vorne. So,

das ist der Algorithmus. Wir haben jetzt im Wesentlichen drei Dinge zu zeigen. Erstens,

der Algorithmus terminiert. Das ist überhaupt erstmal immer schön für so einen Algorithmus.

Zweitens, er kann ja zwei verschiedene Antworten geben. Wenn er die eine Antwort gibt Nein, dann

hat er recht. Und zweitens, wenn er die andere Antwort gibt Ja, hat er auch recht. Davon sind drei

Fragen sehr leicht zu beantworten und eine nicht ganz. Fangen wir an mit Terminierung. Also,

warum terminiert das Ding? Fast einfacher zu beantworten ist die Frage, wie viel Schritte

läuft es höchstens? Also wie oft wird diese Schleife höchstens durchlaufen?

Ja. Nein, was ich hinzufüge hier ist eventuell größer als das, was vorher da war. Also es ist ja C

vereinigt D, wenn das sehr lange Klauseln sind. Also dieser hier Länge 20, der da Länge 30,

das kann vorkommen. Dann schmeiße ich zwar die A's weg, dann sind das hier nur noch 19 und das

nur noch 29, aber der hier am Ende hat also, verlassen Sie mich 38 oder was? 48. Also die

Klauseln können erstmal größer werden. Also noch anders gefragt, wie viele

Klauseln habe ich denn höchstenfalls am Ende in meiner CNF? Ja. Nee, ein bisschen mehr fürcht ich

weiß schon. Da vorne war noch eine Frage. Ja, das ist im Wesentlichen die Antwort. Also es gibt