Guten Morgen allerseits. Je nachdem wie wir zählt haben wir den zweistelligen Bereich

geknackt, so gerade. Ich weiß nicht ob man dich mitzählen darf. Wir sind mitten in der

Logik, das heißt im wahrscheinlich theoretischsten Bereich dieser Vorlesung und haben uns Inferenzverfahren

angeguckt, insbesondere diesmal für die Aussagenlogik, diese DPLL-Prozedur. Und die ist in ihrem

Basisfall relativ einfach. Das guckt man sich am besten mit einem Beispiel an. Wir haben

eine Klauselmenge, wir wollen eine Belegung finden oder eine externe Belegung erweitern

und wir folgen ganz stark der Intuition, dass man solange man kann, die Dinge tun sollte,

die einem die Klauselmenge vorschreibt. Das Ganze nennen wir Unit Propagation, denn wir

haben keine andere Wahl hier, wenn wir diese Klauselmenge erfüllen wollen, als R wahr

zu machen. Das heißt, das tun wir und dann vereinfachen wir mit dieser zusätzlichen

Information. Das ist genau wie Bad Constraints Satisfaction Problemen, wir propagieren Information.

Und wenn wir Glück haben, löst uns Unit Propagation das gesamte Problem. Oft tut es das. Und manchmal

tut es das nicht, in diesem Fall tut es das nicht, wir haben hier nur Zweierklausel. Und

dann muss man irgendwie letztlich raten. Oder, ein bisschen vornehmlich ausdrückt, systematisch

suchen. Wir suchen jetzt hier einfach über beide Möglichkeiten, was wir mit P machen können.

Und das Schöne ist, dass wenn wir P in diesem Fall belegen, dann können wir wieder simplifizieren

und dann macht Unit Propagation der Rest. Wir propagieren immer alle Informationen, die

wir haben, dann bleibt uns nichts anderes übrig, als zu distribuieren, zu suchen und

dann machen wir wieder Fortschritte, weil wir neue Informationen haben. Das ist die ganze

Idee in dieser Prozedur. Und das haben wir uns genauer angeguckt. Wir haben uns verschiedenste

Beispiele angeguckt. Und wir haben auch gesehen, dass diese Prozedur extrem anfällig ist gegenüber

solchen Situationen, wo man die gleichen Fehler immer wieder und immer wieder machen

kann. Dieses Beispiel ist genau so gewählt, dass wir uns hier lange Zeit mit diesen XNs

beschäftigen, die letztlich für den Widerspruch überhaupt keinen Belang haben. Das ist typischerweise

die Art von Beispielen, die man seinen Kollegen gibt, wenn die sagen, ich habe eine tolle

neue Prozedur, die kann fast alles und dann setzt man sich hin und macht ein fieses Beispiel.

Dies hier ist ein fieses Beispiel, denn dieses hier ist gerade so gemacht, dass DPLL auf

die Nase fällt. Und dann sagt man Edge. Und der Kollege, der dann DPLL hat, der überlegt

sich dann, Mensch, was kann ich machen, damit ich diese fiesen Beispiele auch lösen kann.

Und genau das haben wir im Prinzip auch gemacht. Wir haben uns ein fieses Beispiel angeguckt.

Und was hinterher rauskam, war eine Technik, die wir Klausellernen und DPLL mit Klausellernen

haben, ist im wesentlichen Stand der Kunst bei den Satzverwaltungen. Das heißt, wir

haben uns zwei Dinge angeguckt. Die eine Sache war, dass wir Klausellernen gemacht haben.

Die andere Sache ist, dass wir im Wesentlichen DPLL analysiert haben, indem wir DPLL übersetzt

haben in Resolutionsbeweise. Resolutionsbeweise hatten wir vorher uns schon angeguckt. Und

es ist immer eine gute Technik, neue Sachen zurückzuführen auf Zeugs, was man schon

versteht. Und die Idee hierbei war einfach, dass wir uns einen solchen Lauf bis zu einem

Widerspruch von DPLL angucken und dass wir den Dekorieren mit den Klauseln, die leer

werden. Und wenn man dann so einen Baum bekommt, dann kann man diesen Baum hier relativ einfach

übersetzen in einen Resolutionsbeweis, indem wir hier auf eine leere Klausel stoßen. Das

hat zwei Vorteile. Das eine ist, dass wir DPLL besser verstehen als eine spezielle Variante

der Resolution. Man könnte auch einfach einen Resolutionsbeweis auf diese Art und Weise

ansteuern, dann wäre das auch eine DPLL Prozedur. Und wir sehen, dass es sich hierbei um Baumresolution

handelt. Resolution, die keine Klausel mehrfach benutzt. Und das hat Vorteile und Nachteile.

Und wenn wir Baumresolution machen, das heißt wir schließen gewisse Resolutionsbeweise,

nämlich Resolutionsbeweise, die gewisse Klauseln mehrfach benutzen aus, dann ist es klar, dass

die Beweise höchstens länger werden. Und man kann sich überlegen, dass sie exponentiell

länger werden und das sehen wir auch schon bei unserem fiesen Beispiel. Hier ist es,

da haben wir eine Exponentialität drin. Dieser Baum hier unten ist tatsächlich 2 hoch 100

groß. Und wenn uns das nicht reicht, dann machen wir all die Klauseln länger bis zu