Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Ja, herzlich willkommen. Wir hatten letztes Mal gesehen, dass unser formales Seduktionssystem,

der Kalkül des natürlichen Schließens nach Fitch, korrekt und vollständig ist. Das heißt,

eine logische Folgerung in Aussagenlogik liegt genau dann vor, wenn wir einen entsprechenden

Beweis in unserem formalen System finden. Was aus dem System nicht so unbedingt sofort hervorgeht,

ist, dass man solche Beweise auch automatisch finden kann. Das System verallgemeinert auch zu

System für ausdrucksstärkere Logiken, die wir später noch sehen werden, für die man Beweise

im Allgemeinen nicht automatisch finden kann. Man muss also selber kreativ sein beim Anwenden der

Regel. Wir sind ja Informatiker, das heißt, wir wollen gerne Algorithmen haben, die Aussagenlogik,

die ja nun mal entscheidbar ist, in vernünftiger Zeit entscheiden. Das ist nun alles so ein bisschen

relativ. Wir haben gesehen, wir können die Erfüllbarkeit einer aussagenlogischen Formel

entscheiden und zwar mittels Wahrheitstafeln. Das ist nun ein fürchterlich ineffizientes Verfahren.

Wir müssen in einer Wahrheitstafel für jede Variable praktisch eine Spalte haben und dann

alle möglichen Kombinationen von Wahrheitswerten für alle diese Spalten ausprobieren. Das heißt,

wir haben im Allgemeinen zwei hoch n Spalten, wenn wir n-propositionale Atome haben. Und zwar

haben wir die immer, schon um überhaupt die Tabelle hinzuschreiben, ohne zu wissen, was die

Formel ist, verbringen wir erst mal exponentiell lange Zeit damit auf der linken Seite überhaupt

erst mal diese ganzen Kombinationen von Wahrheitswerten aufzulisten. Gut, kann man natürlich leichte

Effizienzsteigerungen einbauen, indem man statt erst alle Valuationen aufzulisten sofort anfängt,

in der rechten Spalte die tatsächlichen Werte auszurechnen. Das ist auch tatsächlich ein

Verfahren, das ich vielleicht für die Aufgaben, die wir da rechnen, empfiehlt. Aber wenn man auf dem

Wege also zu einer kürzeren Laufzeit kommt in gewissen Fällen, dann ist das reines Glück. Man

ist halt zufällig vorher über zum Beispiel eine Valuation gestolpert, die eine Formel,

von der überprüft werden soll, ob sie zum Beispiel gültig ist, dann falsch macht oder umgekehrt,

die vielleicht eine Formel, von der Erfüllbarkeit geprüft werden soll, wahr macht oder sowas.

Das ist also kein Verfahren, das in irgendeiner Form die Hoffnung auch nur am Horizont erscheinen

lässt, dass man es hier mit einem Problem zu tun hätte, was zwar im schlechten Fall exponentiell

lange für die Lösung braucht, also dann, wenn ich irgendwelche bösartigen Beispiele anfütter,

das aber, sagen wir mal, im Durchschnitt schnell zu lösen ist, in realistischen Fällen. Das wäre

also mit diesem Algorithmus gerade nicht so. Nun ist es aber so, dass das Sattproblem,

obwohl es NP-vollständig ist, ich weiß nicht, ist es in BFS das schon bei NP-Vollständigkeit

angekommen eigentlich? Nein. Also halten wir nur fest, also obwohl es ein auch theoretisch

schweres Problem ist, dass, wenn das zutrifft, was alle glauben, nämlich dass P ungleich NP ist,

für das es also dann keinen Algorithmus gibt, der in Polynomialzeit läuft, dass dieses Problem

trotzdem in einem relativ wohl definierten Sinne meistens relativ schnell lösbar ist. Da gibt es

einen sogenannten Phasenübergang. Das wird jetzt eine Grafik, wo Sie also die senkrechte

Achse streng genommen erst nach dieser Vorlesung verstehen. Stellen Sie sich im Moment mal vor,

als Größe der Formel gewissermaßen oder Anzahl Formeln, die ich erfüllen muss, wenn man

gewissermaßen. So, und hier in der waagerechten Achse tragen wir auf die Anzahl Atome, die die

Formel hat. Ja, wir überlegen uns mal kurz, was haben diese beiden Größen mit der Formel zu tun.

Einmal, wenn ich sehr, sehr viele Formeln habe, die ich alle erfüllen muss, also eine Formel,

entsprechend einer langen Formel, mit sehr, sehr vielen Konjunkten. Nun, es ist ja relativ

unwahrscheinlich, dass so ein Ding erfüllbar ist. Also, wenn ich 5 Millionen Formeln habe,

die ich alle wahrmachen muss, dann ist es also relativ schwierig für das Ding erfüllbar zu sein.

Das heißt also, malen wir das am besten. Also hier bin ich so, ich mal das ja so ein bisschen,

wie macht man das am besten. Ich mach das mal fadig. Also hier, mal ich mal dunkel, ja dunkel ist

unerfüllbar. Ja, so. Dagegen, wenn ich viele Atome habe, dann habe ich viele Möglichkeiten,

da Wahrheitswerte einzustellen. Es gibt also unheimlich viele Valuationen. Ich habe also

unheimlich viele Chancen, meine Formelmenge wahrzumachen. Das heißt, wenn ich hier sehr

viele Formeln habe, insbesondere viele Atome habe, insbesondere viele im Verhältnis zur Anzahl