Gut, dann kommen wir zur Vorlesung, Algorithmen 1, heute zum letzten
Mal.
Und wie üblich schauen wir mal wieder zurück, was haben wir diese
Woche am Montag gemacht.
Wir hatten uns noch beschäftigt mit diesen generischen
Optimierungsansätzen, ein weiteres Mal.
Und ein bisschen nochmal dynamische Programmierung.
Dann hatten wir uns dieses Branch-and-Bound-Verfahren angeschaut, wo
man typischerweise eine regressive Suche hat und versucht, über
irgendwelche schon bereits gefundenen optimalen Lösungen andere Teile
des Suchbaums abzuschneiden.
Dann hatten wir uns die lokale Suche angeschaut und eine Variante
davon, die evolutionären Algorithmen.
Gut, und heute werden wir dieses Kapitel noch abschließen.
Also eigentlich kommt jetzt gar nichts mehr Großneues dazu, sondern
nur nochmal ein Vergleich der Verfahren, die wir uns zur Optimierung
angeschaut hatten.
Dann werde ich noch ein bisschen was zum Aussagenlogischen
Erfüllbarkeitsproblem, wird auch SAT genannt für Satisfiability
erzählen.
Das ist auch eines der Forschungsthemen bei uns in der Gruppe.
Also das wird auch jetzt nicht in der Klausur eine Rolle spielen.
Also das, was wir uns heute da zu SAT anschauen, das ist ein bisschen
schon darüber hinausgehend.
Aber es hat schon auch einen engen Bezug zu den Algorithmen, die wir
uns in der Vergangenheit in diesem Semester angeschaut hatten.
Und dann zum Ende der Vorlösung möchte ich noch ein bisschen was zur
Klausur sagen, die ja am 4.
September stattfindet und wie das Ganze abläuft und was wir dazu
beachten haben.
Dazu am Ende der Vorlösung dann noch ein paar Informationen.
Optimierungsverfahren hatten wir uns ja einige Methoden angeschaut,
wie das funktionieren kann.
Zum Beispiel dieses Greedy-Verfahren, was eben versucht, lokal den
nächsten besten Schritt zu machen und praktisch hofft, dass es damit
auch zu einer insgesamt global optimalen Lösung kommt.
In manchen Fällen kann man das beweisen.
In anderen Fällen ist es nicht der Fall, dass man zu einer optimalen
Lösung kommt.
Aber es ist ein Verfahren, das sehr häufig relativ einfach zu
implementieren ist und auch von der Laufzeit her gute Worst-Case
-Garantien abgibt.
Also optimal nur, wenn Sie da in speziellen Fällen einen Beweis dafür
finden, was etwas häufiger schon der Fall ist, dass Sie nicht beweisen
können, dass es optimal ist, aber immerhin, dass sich die Lösung, die
so ein Greedy-Verfahren findet, nicht zu sehr entfernt ist von einer
optimalen Lösung.
Also dass Sie sogenannte Approximationsgarantien angeben können.
Also dass zum Beispiel die gefundene Lösung maximal um einen Faktor
zwei oder um einen Faktor N schlechter ist als Ihre optimale Lösung.
Also Greedy-Verfahren, einfach, aber häufig nicht optimale, dass Sie
optimale Lösungen garantieren.
Dann im Gegensatz dazu die systematische Suche, die schaut sich eben
wirklich alle Möglichkeiten an und findet deshalb auch immer optimale
Lösungen, hat dadurch aber auch schlechtere Laufzeiten und die
Algorithmen, um das zu implementieren, sind häufig auch sehr komplex.
Was sich da anbietet, ist dann, dass man einfach die bereits
bestehenden Werkzeuge hernimmt und die in einer Art oder so als
Blackbox -Solver einsetzt.
Zum Beispiel die Werkzeuge zur linearen Programmierung oder Integer
-Linear -Programming oder Satz-Solver oder allgemein Constraint
-Programming -Tools.
Also die systematische Suche, dann lineare Programmierung.
Je nachdem, mit was man da zu tun hat, kann das auch einfacher oder
schwieriger sein.
Wir hatten gesehen, wenn man zum Beispiel an rationalen Lösungen
interessiert ist, wenn wir an rationalen Lösungen interessiert sind,
dass es dann einfache oder von der Laufzeit her bessere Algorithmen
gibt, das heißt polynomielle Algorithmen.
Wenn wir an Integer-Linear-Programming interessiert sind, also an
ganzzeitigen Lösungen nur, dann erfordert es exponentielle Laufzeit in
fast allen Fällen.
Und eine Optimalität ist eigentlich fast immer zu erreichen mit den
Verfahren, wenn Sie die Modellierung passend gemacht haben.
Und das Modellieren selber, das kann zum Teil nicht ganz so einfach
sein.
Und Sie müssen da eben aufpassen, dass Sie wirklich das richtige
Problem codiert haben, auch für Ihren Solver.
Dann haben wir uns angeschaut, die dynamische Programmierung anhand
von dem Rucksackproblem.
Das Rucksackproblem hat uns ja bei einigen dieser Lösungsverfahren als
Beispiel gedient.
Und die dynamische Programmierung war die Idee, dass wir für Teile des
Problems eine optimale Lösung finden und die dann versuchen zu
erweitern, schrittweise auf das Gesamtproblem.
Und dann haben wir auch festgestellt, das geht, wenn die Probleme
austauschbar sind und noch weitere Kriterien gelten.
Hat unter Umständen hohen Platzbedarf, Sie erinnern sich daran, wir
hatten bei dem Rucksackproblem diese Tabelle aufgebaut, die eben
quadratisch Platz benötigt.
Das hatte ich eigentlich schon gesagt, zur ganzteiligen linearen
Programmierung ist eben sehr rechenintensiv.
Man hat auch wieder das Codierungsproblem wie eben generell bei diesen
linearen Programmierungs- oder Constraint Programming Aufgaben.
Aber dann gibt es eben da auch die Blackbox, wo wir diese einsetzen
können.
Lokale Suche war ein weiteres Verfahren und daneben die Variante
Evolutionäre Algorithmen.
Lokale Suche sind häufig sehr einfache Algorithmen.
Es gibt da eine ganze Reihe von Varianten davon oder Stellschrauben,
wie Sie das machen können.
Also die generelle Idee ist ja, dass man versucht, erstmal eine Lösung
irgendwie zu raten oder eine, die nicht beliebig weit vom Optimum sein
kann, einfach irgendwie zu erstellen und dann diese Lösung
schrittweise zu optimieren, indem man sich die Nachbarschaft dieser
Lösung anschaut.
Ob es eben durch kleine Änderungen der Lösung möglich ist, das Optimum
zu verbessern.
Dann gab es eben solche Varianten wie das Hill Climbing oder das
Simulated Annealing, was an diesem physikalischen Modell orientiert
war.
Bei Simulated Annealing ist es so, dass das häufig sehr lange dauert,
weil man simuliert ja diesen physikalischen Prozess eines Materials,
das in flüssigen, festen Zustand übergeht oder in kristallinen Zustand
und da eben durch Absenken der Temperatur das erreicht wird.
Und das Absenken der Temperatur hängt dann mit zusammen, mit welcher
Wahrscheinlichkeit man welche Wechsel in der Lösung zulässt.
Und da ist es häufig so, dass man eben diese Simulierte Temperatur in
sehr kleinen Schritten absenken muss und deshalb die Laufzeit sehr
groß sein kann.
Gut, evolutionäre Algorithmen haben ähnliche Eigenschaften.
Da ist eben dann noch die Idee dabei, außer dieser lokalen
Modifikation einer bereits bestehenden Lösung, typischerweise zwei
Lösungen herzunehmen und die zu kombinieren, indem man Teile der einen
Lösung mit Teilen der anderen Lösung zusammennimmt und diese
kombinierte Lösung dann als Ausgangspunkt für weitere Optimierung
verwendet.
Also das sind die verschiedenen Varianten, die wir uns angeschaut
hatten in der Vorlesung, um Optimierungsprobleme zu lösen und in der
Praxis sieht es einfach so aus, dass Sie sich anschauen müssen, wenn
Sie ein bestimmtes Problem gegeben haben, welche Charakteristika das
aufweist, also haben wir zum Beispiel mit Ganzzahlen zu tun als Lösung
oder sind es rationale Zahlen, dann eben auch je nachdem, ob Sie
wirklich an einem Optimum interessiert sind oder ob auch eine
Nährungslösung ausreicht, je nachdem werden Sie dann eben das
entsprechende Lösungsverfahren hier auswählen.
Gut, okay, also soweit zur Optimierung und damit schließen wir auch
dieses Thema dann ab und ich möchte jetzt dann so die nächste halbe,
dreiviertel Stunde mich noch mit einem Problem beschäftigen, nämlich
mit diesem aussagenlogischen Erfüllbarkeitsproblem.
Da sind die Vorlinien jetzt zu auf Englisch, aber ich denke, das
stellt auch kein Problem dar.
Also worum geht es bei dem Satzproblem, bei dem aussagenlogischen
Erfüllbarkeitsproblem?
Es geht um Aussagenlogik und im Englischen heißt es Propositional
Logic und da geht es dabei darum, eben bei Formeln festzustellen, ob
die Lösungen haben oder nicht.
Also müssen wir uns zuerst mal anschauen, was sind denn überhaupt die
Formeln, mit denen wir zu tun haben.
Die sind eben rekursiv aufgebaut, als Grundbausteine haben sie
Variablen, Bool'sche Variablen, das heißt, das sind Variablen, die
einfach nur die Werte True oder False oder häufig auch 0 oder 1
bezeichnet annehmen können.
Also einfach aussagenlogische Werte und aus denen können sie dann
eben, das sind die Grundbausteine, aus denen sie größere Formeln
aufbauen können, indem sie die eben mit den logischen Konnektiven
verknüpfen.
Nicht und oder eventuell noch Implikationen oder Äquivalenz, aber im
Normalfall, und es ist auch ausreichend, um beliebige Formen
darzustellen, beschränken sie sich auf Negation oder und nicht.
Und was man in dem Bereich der Erfüllbarkeitsprüfung auch sehr häufig
macht, ist, dass man nicht jetzt beliebige Formen zulässt.
Also man darf nicht mit beliebig strukturierte Formen aufbauen,
sondern die müssen eine etwas eingeschränktere Form haben.
Und zwar ist es so, dass man sich hier im Normalfall mit Formen
beschäftigt, die in konjunktiver Normalform sind.
Und das, haben Sie vielleicht schon gehört, in anderen Formen ist es
eine konjunktive Normalform.
Also die ganze Formel ist eine Konjunktion, also auf der obersten
Ebene, eine Unverknüpfung von Teilbausteinen.
Die Teilbausteine sind dann Oder-Verknüpfungen und diese Oder
-Verknüpfungen sind Verknüpfungen eben von sogenannten Literalen, also
Variablen oder negierten Variablen.
Okay, also wir haben dann, wenn wir nochmal von unten nach oben gehen,
wir haben erstmal die Variablen, die können dann unter Umständen
negiert sein.
Das nennen wir auch Literal eine Variable oder negierte Variable.
Dann haben wir auch als nächstes die Oder-Verknüpfung von solchen
Literalen.
Und auch dafür gibt es wieder einen Namen, das nennt sich eine Clausal
oder Clause im Englischen.
Also eine Clausal ist die Oder-Verknüpfung von Literalen und unsere
Gesamtformel ist dann eine Unverknüpfung von solchen Clauseln.
Und das ist dann eine Formel in konjunktiver Normalform oder eben im
Englischen in conjunctive Normalform, also CNF.
Und wenn wir uns mal ein Beispiel anschauen, also hier unten hat man
die Formel F, die ist eben nach diesem Prinzip gebildet, das heißt sie
ist in konjunktiver Normalform.
Die besteht aus drei Clauseln, das heißt wir haben eine Unverknüpfung
von drei solchen Bausteinen, die mit Oder verknüpft sind.
Dann haben wir am Anfang eben eine Clausal, die enthält zwei Literale,
einmal dieses Nicht-X1 und das X2.
Die Literale müssen ja mit Oder verknüpft sein in der Clausal, also
haben wir diese Form hier.
Die Variablen von der Formel sind eben die Variablen, die hier
auftreten.
Das ist X1, X2, X3.
Die Literale, die in der Formel auftreten, haben wir eben dann in
manchen Fällen noch die negierte Variante davon.
Also bei X1 und X2 haben wir noch die negierte Variante der Variable.
Und wenn wir uns die Clauseln anschauen, das soll mit Clause von F,
PLS von F bezeichnet sein, dann ist das eben die Menge von diesen drei
Bestandteilen, die mit Unverknüpft werden.
Gut, und was ich jetzt einfach so dazu sage, ohne Beweis, also wenn
Sie eine beliebige aussagenlogische Formel haben, die eben eine ganz
andere Struktur hat, also zum Beispiel eine verschachtelte
Unverknüpfung oder Verknüpfung und vielleicht auch eine Negation mal
zwischendrin, die lassen sich alle in diese CNF-Form, also in
konjunktive Normalform bringen.
Und für den Zweck, den wir hier benötigen, also für das Finden einer
Lösung, lässt sich das sogar in polynomialer Zeit erreichen.
Also es gibt Transformationen, die eine beliebige Formel hernehmen und
die in konjunktive Normalform bringen und diese Transformation
benötigt polynomiale Zeit und produziert damit eben auch Ausgaben, die
höchstens polynomiell größer als die Eingabe sind.
Das ist nicht ganz so trivial, wie das funktioniert, aber dazu können
Sie auch in anderen Vorlesungen dann noch mehr hören, wie man solche
Transformationen macht.
Okay, also der Gegenstand, mit dem wir uns beschäftigen, sind Formeln
dieser Art hier.
Und was ist jetzt dann das Erfüllbarkeitsproblem?
Bei dem Erfüllbarkeitsproblem geht es darum eben festzustellen, gibt
es eine Möglichkeit, den Variablen in der Formel Wahrheitswerte
zuzuweisen, also true und false, sodass die Gesamtformel wahr wird.
Gut.
Und dazu benötigen wir eben den Begriff dieses Truth Assignment oder
einfach einer Variablenbelegung, wie es im Deutschen meistens genannt
wird.
Und diese Variablenbelegung, mit phi hier bezeichnet, die weist eben
jeder Variable entweder wahr oder falsch zu.
Und wir sagen dann, dass eine Variablenbelegung phi, die erfüllt
erstmal ein Literal, ein positives Literal, also wenn es nicht negiert
ist, wenn eben die Variablenbelegung für die Variable wahr ist, also
wenn die Funktion dieser Variable den Wert true zuweist.
Wenn wir etwas negiertes haben, so etwas wie nicht x, wann wird das zu
wahr oder wann ist diese Formel erfüllt, sagt man dann auch.
Das ist dann der Fall, wenn diese Variablenbelegung x eben falsch
zuweist.
Wenn man es dann wieder negiert, kommt ja wieder true raus.
Ähnlich dann, wenn wir eine Klausel haben, also so eine Oder
-Verknüpfung, wann ist die erfüllt, also wann wird die wahr.
Das ist dann der Fall, wenn mindestens eines der Literale wahr wird.
Und dann in der cnf eben, die ist dann erfüllt, wenn sämtliche
Klauseln erfüllt sind.
Dann gibt es auch noch ein paar Begriffe hier, wenn so eine
Variablenbelegung phi eine Formel f erfüllt, dann nennt man die auch
erfüllende Belegung oder satisfying assignment.
Und eine Formel nennt man erfüllbar, wenn es eine solche Belegung
gibt, die eben f erfüllt, also f zu wahr macht.
Genau, und das Erfüllbarkeitsproblem geht es jetzt eben darum,
festzustellen, zu einer gegebenen Formel, ob die erfüllbar ist oder
nicht.
Das ist erstmal einfach nur eine Ja-Nein-Antwort, also ein
Entscheidungsproblem, aber häufig ist man auch noch an einer Lösung
interessiert.
Das heißt im besten Fall, das ist auch bei fast allen Algorithmen so,
dass die einem so eine Lösung, also ein satisfying assignment oder
eine erfüllende Belegung noch mit zurückliefern, dass man auch weiß,
wie muss ich die Variablen in den setzen, um die Formel wahrzumachen.
Schauen wir uns ein paar Beispiele an.
Also hier oben haben wir jetzt Formeln, erstmal drei, die erfüllbar
sind.
Also die Formel, die nur aus x1 besteht, als einziger Klausel, klar,
die ist erfüllbar, wenn wir x1 den Wert 1 zuweisen oder true, dann ist
auch die Gesamtformel true.
Dann ähnlich die nächste Formel, x2 oder x8 oder nicht x3, die ist
natürlich auch erfüllbar, wenn wir zum Beispiel x2 den Wert 1
zuweisen, dann ist auch schon die ganze Oder-Verknüpfung wahr und
damit auch die gesamte Formel.
Und dann bei der dritten Formel hier, da muss man jetzt ein bisschen
sich etwas mehr überlegen.
Also um die wahrzumachen, wenn wir von rechts anfangen, muss auf jeden
Fall diese Variable x1 mit wahr belegt werden, weil sonst eben diese
eine Klausel nicht erfüllt ist und damit auch die Gesamtformel nicht
mehr erfüllt werden kann.
Also x1 muss wahr sein, wenn wir uns dann links die erste Klausel
anschauen.
Wenn x1 wahr ist, dann ist auf jeden Fall das Nicht-x1 falsch, also
ist auch wieder erzwungen, dass x2 wahr sein muss.
Und wenn x1 und x2 wahr sind, dann kommen wir über die mittlere Formel
heraus, dass dann auch x3 wahr sein muss.
Und das heißt, wenn wir alle drei Variablen auf wahr setzen, dann ist
das eine erfüllende Belegung dieser Formel wieder und es ist in dem
Fall auch die einzige erfüllende Belegung, da gibt es dann keine
weiteren.
Nicht -erfüllbare Formeln, also für die es keine Lösung gibt, wie man
so eine Variablenzuweisung machen kann, wäre x1 und Nicht-x1, klar,
das ist ein Widerspruch einfach, wenn es egal was ist, ob es wahr oder
falsch ist.
x1 zuweisen wird die Formel immer falsch sein.
Im nächsten Fall ist es auch relativ offensichtlich, wenn sie x1 und
Nicht -x1 und nochmal was haben, dann reicht es schon aus, wenn der
vordere Teil, also die ersten beiden Klauseln nicht erfüllt werden
können, dann gibt es auch keine Lösung mehr für das Gesamtproblem.
Und in dem letzten Fall müssen Sie sich auch wieder ein bisschen mehr
überlegen, um herauszufinden, dass es keine Lösung gibt.
Also dann könnte man entweder versuchen, die Formel irgendwie
umzuformen, indem man irgendwelche Dinge vielleicht ausklammert oder
einfach versucht, alle Möglichkeiten, wie man x1 und x2 belegen kann,
also diese vier Möglichkeiten, einfach Reihen nach durchzuprobieren
und ausrechnen, was kommt denn an Wahrheitswert hier raus.
Okay, also das Problem, das ist relativ einfach, sieht relativ einfach
aus, lässt sich auch einfach beschreiben.
Die Formeln haben eine einfache Struktur, einfach eben immer diese
Unverknüpfung oder Verknüpfung von Klauseln.
Trotzdem ist das Problem überraschend schwer zu lösen.
Also wir hatten bei dem letzten Beispiel hier unten schon gesehen,
dass es da nicht so ganz klar ist, wie man da jetzt für einen
systematischen Algorithmus schreiben kann, der besser ist, als einfach
alles durchzuprobieren.
Wie gesagt, vielleicht kann man irgendwelche Umwandlungen machen oder
versuchen, irgendwelche Schlussfolgerungen daraus zu ziehen, dass eben
zum Beispiel, vorne könnte man bei den ersten beiden Klauseln x2
ausklammern und das wären Pricks, die halt hier gut funktionieren,
aber möglicherweise nicht bei anderen Formeln.
Also das einfach zu beschreiben das Problem, aber zu lösen
überraschend hart.
Und hier mal jetzt ein kleines Beispiel, was sich damit kodieren lässt
mit Aussagenlogik.
Das ist häufig auch nicht so einfach, also für die Kodierungen muss
man sich ein bisschen überlegen, was sind denn die Eigenschaften, die
man wirklich benötigt in der Problembeschreibung und welche nicht.
Und in dem Beispiel soll es darum gehen, dass man einen Termin finden
möchte für eine Besprechung oder für ein Meeting.
Und dann gibt es eben vier Personen, die an diesem Meeting teilnehmen
sollen und die haben jeweils Einschränkungen, wann sie eben nicht
können oder wann sie können.
Zum Beispiel Adam kann nur montags oder mittwochs, dann Bridget kann
nur mittwochs, Charles kann nur freitags oder kann nicht freitags,
Bridget kann auch nicht mittwochs und der Darren kann nur donnerstags
oder freitags.
Und das ist jetzt was, was sich eben auch als Aussagenlogisches
Problem kodieren lässt.
Und was man dann typischerweise machen muss, man muss sich erst mal
überlegen, wie möchte ich meine Variablen, mit welcher Bedeutung
möchte ich die haben.
Und dann als zweites überlegt man sich dann, wie man die
entsprechenden Einschränkungen kodiert.
Und wenn man sich die Variablen jetzt anschaut, dann könnte man sagen,
ja man macht jetzt irgendwie für jede Person, versucht mal irgendwie
eine Variable anzulegen, ob diese Person Montagszeit hat, ob diese
Person Dienstagszeit hat, die jeweils eben wahr oder falsch sein kann.
Aber man steht auch relativ schnell fest, dass das eigentlich gar
nicht von der Person abhängt, sondern dass es unabhängig davon ist,
wer jetzt eben so eine Einschränkung hat.
Das heißt, man kann diese Person eigentlich direkt weglassen und nur
kodieren, eben ob jetzt eine Person an einem bestimmten Wochentag Zeit
hat, egal welche.
Also ob ein bestimmter Tag für das Meeting in Frage kommt.
Und damit kommt man dann zu so einer Kodierung von dem Problem, wie es
hier unten dann eben dran steht.
Also wir nehmen dann eben die Variable x1 dafür, dass montags für
diese Besprechung in Frage kommt, dann x2 für Dienstag, x3 für
Mittwoch und bis x5 dann für Freitag.
Und dann können wir diese Einschränkungen relativ einfach kodieren.
Also dass Adam jetzt nur montags oder mittwochs Zeit hat, werden eben
diese Einschränkungen, dass das Meeting entweder montags oder
mittwochs stattfinden muss.
Und die Variablen dafür sind eben dieses x1 und x3.
Also kriegen wir die Bedingung x1 oder x3 für einen Tag, an dem diese
Besprechung stattfinden kann.
Dann die zweite Einschränkung, dass Bridget nicht mittwochs kann, wäre
dann eben das nicht x3 hier.
Also mittwochs fällt damit praktisch raus als Termin.
Schwarz kann nicht Freitag, also das ist das x5, da kriegen wir nicht
x5 raus.
Und dann, dass Donnerstag oder Freitag für das Meeting sein muss, ist
x4 oder x5.
Und damit haben wir dann eigentlich das Problem dann fast schon
kodiert.
Dann möchten wir unter Umständen, aber vielleicht noch nicht ganz
vollständig, also man kann sagen, man möchte zum Beispiel noch sagen,
das soll eben wirklich nur ein Tag für ein Meeting ausgewählt werden.
Also es soll nicht jetzt irgendwie das aufgeteilt sein, dass irgendwie
jetzt zum Beispiel montags und mittwochs ein Teil von den Personen
eben dabei sein können, sondern es muss wirklich an einem Tag
stattfinden.
Und das lässt sich ausdrücken.
Ich habe jetzt hier, das ist jetzt natürlich nicht in CNF, aber wir
haben mal was hingeschrieben, was wir ausdrücken wollen.
Und das ist einfach die Eigenschaft, dass eben höchste, höchstens eine
oder letztendlich eigentlich sogar genau eine von diesen Variablen
wahr sein soll von x1, 2, 3, 4, 5.
Das heißt, das Meeting soll nicht an zwei Tagen mit unterschiedlichen
Personen stattfinden, sondern soll an genau einem Tag stattfinden.
Und das ist jetzt erstmal die Idee, was wir gerne noch dazunehmen
würden.
Und diese Eigenschaft, die können wir natürlich auch jetzt in
konjunktiver Normalform wieder ausdrücken.
Also dieses at most one, das höchstens eine der Variablen x1 bis x5
wahr sein dürfen.
Haben Sie eine Idee, wie man das in einer Aussagenlogik oder am besten
vielleicht noch als CNF ausdrücken könnte, dass von diesen fünf
Variablen höchstens eine wahr ist?
Man könnte sich mal für einen einfacheren Fall überlegen, wenn Sie
zwei Variablen hätten nur und Sie wollen irgendwie ausdrücken, dass
von diesen zwei Variablen, sagen wir x1 und x2, höchstens eine wahr
ist.
Ja, ein XOR, aber genau was... ja genau, das trifft in dem Fall sogar
schon.
Also das XOR wird zulassen, dass entweder eben die eine Variable auf
wahr gesetzt ist oder die andere Variable auf wahr gesetzt ist.
Aber es geht eben nicht, dass beide nicht gesetzt sind oder dass beide
auf eins gesetzt sind.
Also man hat damit sogar ein bisschen was anderes kodiert.
Man hat damit sogar nicht dieses at most one, sondern man hat exactly
one kodiert.
Also es muss dann immer genau eine Variable von x1 oder x2 wahr sein.
Und wenn man jetzt aber noch wirklich den Fall zulassen oder auch noch
zulassen möchte, dass auch keine der Variablen wahr sein darf, wie
würden Sie das dann kodieren?
Was häufig hilft, ist, wenn man sich überlegt, was möchte man denn
ausschließen, in welchem Fall.
Und in welchem Fall möchte man ausschließen, wenn man jetzt von zwei
Variablen sagt, höchstens eine soll auf wahr gesetzt sein.
Man möchte ausschließen, dass beide Variablen gleichzeitig auf eins
gesetzt sind.
Also ich möchte irgendetwas haben, das nicht x1 und x2 soll gelten.
Also nicht in Klammer x1 und x2.
Der Fall wäre natürlich mal so x1 und x2, dass beide wahr sein müssen
und nicht x1 und x2, dass das gerade nicht sein darf.
Und wenn Sie das in CNF wieder bringen, das heißt dann haben Sie das
nicht, was Sie heute Morgen nach innen ziehen können über die
Unverknüpfung, dann wird ein oder draus, dann haben Sie nicht x1 oder
nicht x2.
Und diese Formel würde dann angeben, dass die beiden Variablen nicht
gleichzeitig wahr sein dürfen.
Und das lässt sich dann auch verallgemeinern, das können Sie einfach
in Paarweise für alle Variablenpaare machen.
Also wenn Sie ausdrücken wollen, dass jetzt von den Variablen x1 bis
x5 höchstens eine auf wahr gesetzt werden kann, dann können Sie eben
diese Einschränkung hernehmen wie nicht x1 oder nicht x2.
Das schließt aus, dass x1 und x2 gleichzeitig wahr sind.
Und wenn Sie das für alle Paare machen, also für x1, x2, x3 und so
weiter bis zum Schluss x4, x5, haben Sie eben ausgeschlossen für
beliebige Paare, dass die gleichzeitig auf 1 sind.
Und daraus folgt dann eben, dass jetzt maximal eine der Variablen von
x1 bis x5 wahr sein kann in der Lösung von dieser Formel.
Okay, also das wäre jetzt eine Codierung von unserem Meetingproblem
hier oben in Aussagenlogik und auch in CNF eben.
Das heißt, wenn wir da jetzt ein Lösungsverfahren haben für dieses
Satzproblem, dann könnte man auch diese Fragestellung beantworten nach
dem Meeting.
Also man kann jetzt natürlich versuchen, diese Formel von Hand zu
lösen, indem man mit irgendwelchen Tricks oder vielleicht auch oben
einfach mit andererartiger Überlegung versucht heranzugehen.
Aber was man feststellt, ist, dass diese Formel nicht erfüllbar ist.
Das heißt, mit diesen Einschränkungen, die von den vier Personen
benannt wurden, gibt es keine Möglichkeit, einen Tag für ein Meeting
zu finden.
Okay, und das kann man eben, wie gerade gesehen, als ein
aussagenlogisches Problem codieren und dann mit den entsprechenden
Lösungsverfahren versuchen zu lösen.
Okay, dann schauen wir uns ein bisschen an, wie schwierig es ist,
dieses Problem zu lösen.
Also wie gesagt, einfach formulierbar, aber es stellt sich heraus, es
ist eben sehr schwer zu lösen.
Also das Erfüllbarkeitsproblem, hatten wir auch schon in der Vorlesung
schon gesagt, ist NP-vollständig.
Und das heißt, was bedeutet NP-vollständig?
Es bedeutet erstmal, dass es diese Eigenschaft hat, dass ein nicht
deterministischer Algorithmus in polynomialer Zeit das entscheiden
kann und wie man das auch formulieren kann, ist, dass es möglich ist,
eine Lösung für ein Problem in polynomialer Zeit zu finden, zu prüfen.
Also wenn Sie eine Lösung gegeben haben zu so einer Formel und jemand
behauptet, ja, das ist jetzt eine Lösung, die die Formel wahr macht,
und Sie wollen das nachprüfen, dann ist das etwas, was in polynomialer
Zeit geht.
Also das ist im Grunde so ein bisschen eine andere Sichtweise auf
dieses NP.
Und es geht sogar in lineare Zeit, also es ist sehr einfach möglich.
Und genau, dieser Beweis, warum SatNP vollständig ist, ist vielleicht
auch noch ganz interessant.
Der ist in den 70er-Jahren von einem kanadischen Mathematiker, Cook
heißt der, geführt worden.
Und das ist das erste Problem, von dem gezeigt wurde, dass es NP
-vollständig ist.
Und das ist vielleicht ganz interessant, weil NP-vollständig bedeutet
ja, dass sich alle anderen NP-Probleme auf dieses Problem zurückführen
lassen.
Und das heißt, man muss dann irgendwie jetzt ein Verfahren angeben,
wie man beliebige Probleme, die in der Klasse NP liegen, auf dieses
Sat -Problem abbilden kann.
Und das war eben das, was Cook damals gemacht hat und hat damit
gezeigt, dass eben Sat diese NP-vollständig, zu dieser Klasse der NP
-vollständigen Probleme gehört.
Und das ist dann fürs Beweisen auch recht praktisch.
Also was man normalerweise macht, um eine NP-Vollständigkeit von einem
Problem zu beweisen, ist, dass man das eben auch wieder auf ein
bestehendes Problem, von dem man die NP-Vollständigkeit bereits
gezeigt hat, wieder zurückführt.
Aber dazu braucht man natürlich, um dieses Verfahren einbinden zu
können, erstmal ein Problem, für das man das bewiesen hat.
Sonst redet man über eine leere Menge.
Und das war eben dieses erste Problem, für das man das zeigen konnte,
direkt ohne Zurückführung auf ein anderes Problem, dass das in der
Klasse der NP-Vollständigen liegt.
Okay, das ist eher so die theoretische Seite.
Dann, wenn man sich es von der praktischen Seite her anschaut, was
bedeutet das?
Das bedeutet, dass wir keinen polynomialen Algorithmus für Sat-Problem
haben.
Das heißt, in dem schlechtesten Fall brauchen die alle exponentielle
Laufzeit, um die Algorithmus zu lösen.
Und es ist auch so, dass unter Umständen gar niemals auf so einen
Algorithmus gefunden werden kann.
Wenn sich das PNP-Problem oder P versus NP-Problem, wenn es sich
herausstellt, dass die Klassen wirklich unterschiedlich sind, dass die
Klassen polynomial lösbar haben von einer deterministischen,
polynomial lösbar von einer nicht deterministischen Turing-Maschine,
wenn die sich unterscheiden, dann gibt es keinen polynomialen
Algorithmus für Sat-Problem und damit eben auch keinen polynomialen
Algorithmus für alle anderen NP-vorständigen Probleme.
Genau.
Und die Frage ist, wie gesagt, ja noch offen.
Also man weiß heutzutage nicht, ob P gleich NP ist oder ob es ungleich
ist.
Die meisten gehen davon aus, dass es ungleich ist.
Es gibt aber auch eine Reihe von bedeutenden Personen, die sich da
nicht so festlegen, sondern die auch sich vorstellen können, dass P
gleich NP ist.
Also Donald Knuth zum Beispiel ist jemand, der eher dazu tendiert,
dass es auch gleich sein könnte.
Aber es gibt viele Theoretiker, die eben, oder die meisten sogar, die
vom Gegenteil ausgehen.
Okay, und das bedeutet dann, dass diese Algorithmen eben exponentielle
Laufzeit haben, aber eben nur im schlimmsten Fall, also nur im worst
case.
Und in der Praxis ist es so, dass die eben häufig eine deutlich
bessere Laufzeit haben.
Und in der Vergangenheit hat es dazu geführt, dass man ursprünglich,
als es eben als BNP vollständig festgestellt worden war, dass man sich
dann gar nicht mehr so stark um die Algorithmen dafür interessiert
hat.
Eben unter der Annahme, das ist sowieso für praktische Probleme, wie
sie in der Praxis auftreten, nicht geeignet, weil die einfach zu groß
sind.
Aber später hat sich gezeigt, dass das gar nicht immer der Fall ist,
sondern dass viele Probleme eben sehr weit entfernt sind von der worst
case Laufzeit.
Gut, dann hier habe ich noch einen kleinen Link, wenn Sie mal
ausprobieren wollen, so ein SAT-Problem zu lösen.
Schauen wir mal ganz kurz drauf.
Also die Folien gibt es ja online, das heißt, Sie können auch da nach
dem Link hier schauen.
Und da auf dieser Seite ist ein SAT-Problem, das Sie mal versuchen
können von Hand zu lösen.
Also was man hier sieht, das ist das SAT-Game von Olivier Roussel.
Und Sie haben hier eben eine Formel.
Das, was hier mit diesen Blöcken hier zueinander steht, ist jeweils in
einer Zelle eine Klausel.
Also Sie haben 4, das steht dann für x4, x4 oder nicht x9 oder x6.
Also das Minus steht für Negation dann.
Das heißt, das wäre jeweils ein Dreierblock für eine Klausel, die Sie
wahrmachen müssen.
Und Sie sollen eben versuchen, die gesamte Formel wahrzumachen.
Und diese Hände, die da dran sind, zeigen Ihnen an, dass da noch was
zu tun ist.
Das heißt, jetzt wäre noch gar keine Variable irgendwie belegt mit
wahr oder falsch.
Und wenn wir jetzt mal irgendwo drauf gehen, zum Beispiel auf diese 4
hier oben, dann sehen Sie, ja, die ist jetzt zu wahr geworden und die
Hand da auch verschwunden.
Also die Klausel ist jetzt auch schon erfüllt.
Und an anderen Stellen, das Rot zeigt nur an, ja, dieses Literal ist
jetzt erstmal falsch.
Und jetzt können wir versuchen, zu dieser Formel hier eben eine Lösung
zu finden von Hand.
Also genau, ich mache es jetzt hier nicht, aber das können Sie gerne
mal von Hand ausprobieren.
Genau, das gibt dann auch noch zwischendrin, wenn ich ein bisschen
weiter mache, gibt es, ja, nehmen wir einfach hier die 7 noch zu.
Das sieht jetzt ganz gut aus.
Und jetzt sehen wir hier noch solche blauen Pfeile.
Und diese blauen Pfeile zeigen uns an, dass jetzt hier an dieser
Stelle irgendwas erzwungen wird.
Und zwar, wenn wir mal rechts oben schauen, da haben wir diese Klausel
nicht X6 oder X8 oder X1.
Und wir haben jetzt schon die Variable, oder das Literal nicht X6, das
ist schon zu falsch.
Das heißt also X6 ist mit wahr belegt, X1 ist mit falsch belegt.
Um das jetzt noch wahr machen zu können, müssen wir auf jeden Fall die
Variable X8 zum Beispiel auf True setzen.
Alles andere gibt keine Lösung mehr.
Also das zeigt uns an, hier ist jetzt wirklich was Wichtiges.
Dass was erzwungen wird an der Stelle eine bestimmte Belegung.
Und dann genauso die Minus 5.
Das heißt, wenn wir die jetzt mal hier auswählen, zum Beispiel die
Minus 5, hier oben die 8, dann wird hier wieder was erzwungen, hier
was erzwungen.
Ja, jetzt haben wir fast geschafft eine Lösung zu finden, bis auf
diese letzte Klausel, die ist jetzt leider falsch.
Und wenn Sie jetzt versuchen, das irgendwie zum Beispiel durch
Abändern, indem wir sagen, die 9 machen wir zum Beispiel wahr, dann
geht meistens irgendwas anderes schief.
Aber Sie können es gerne mal ausprobieren zu Hause, ob Sie da von Hand
eine Lösung finden.
Also wenn man diese blauen Pfeile mit berücksichtigt, dann dauert es
sogar gar nicht so lange.
Dann kommt man da ganz gut schon hin damit.
Gut.
Aber Sie sehen auch, wenn Sie das von Hand ausprobieren, dass es nicht
ganz so einfach ist, für so eine formelle Lösung zu finden.
Und was man in der Praxis eben hat, wenn man realistische Probleme
codiert, dass die eben nicht nur aus 9 Variablen bestehen, sondern
dass die 10.000 oder auch 100.000 Variablen enthalten können.
Und die Anzahl der Klauseln, mit denen man zu tun hat, die können auch
im Bereich von einer Million mal liegen.
Und das sind Probleme, wenn man jetzt von der NP-Vollständigkeit
ausgeht, wo man erstmal vermuten würde, da besteht überhaupt keine
Chance, ein Problem mit 100.000 Variablen zu lösen.
In der Praxis funktioniert das aber wirklich überraschend häufig, dass
die eben doch von modernen Verfahren gelöst werden können.
Okay, wenn man sich mal ein bisschen geschichtlich anschaut, wie sich
das Problem entwickelt hat.
Also die ersten Algorithmen, um dieses SAT-Problem, Aussagenlogische
Erfüllungsproblem, zu lösen, die stammen so aus den 60er Jahren.
Also 1960 ist ein Verfahren von Davies und Putnam vorgeschlagen
worden.
Das ist auch interessant, weil in der damaligen Zeit, da hat man
natürlich von Rechenressourcen ganz andere Limitierungen gehabt, als
es heute der Fall ist.
Also wenn man da einen Rechner hatte mit einigen Kilobyte
Hauptspeicher, dann war das schon relativ viel.
Und entsprechend muss man sich dann auch vorstellen, was dann eben die
Grenzen von den Problemen, die damit behandelt werden konnten, waren.
Und eben auch, was es für Herausforderungen an die Programmierung gab.
Dann 1962 gab es eine verbesserte Variante von diesem DP-Algorithmus,
den sogenannten DPLL-Algorithmus.
Da sind noch zwei Autoren dazugekommen.
Also Davies, Putnam und Lockman und Loveland hießen die beiden
weiteren Autoren.
Dann ist erst danach gezeigt worden, also fast zehn Jahre nach diesen
Algorithmen, das Problem selber ist natürlich noch viel älter.
Also geht eigentlich auf Buhl, also Ende 19.
Jahrhundert, auf die Logiker damals zurück, die das ein bisschen
formaler dargestellt haben.
Aber eben erst 1971 hat KUK dann gezeigt, dass es sich um ein NP
-vollständiges Problem handelt.
Dann nochmal fast 20 Jahre später ist die Idee von dieser lokalen
Suche, die wir ja auch uns in der Forschung schon ein bisschen
angeschaut hatten, aufgetaucht im Bereich von Sat-Solving.
Und dann gab es um diese Zeit herum auch die ersten Ideen, dass man
versucht, verstärkt Algorithmen für das Sat-Problem zu entwickeln oder
sich darauf mehr zu konzentrieren.
Es gab dann die erste internationale Sat-Competition, wo eben
verschiedene Algorithmen oder Implementierungen von Algorithmen
gegeneinander antreten konnten und man sehen wollte, was sind denn
wirklich die erfolgreichsten Verfahren in der Praxis.
Und es gab dann weitere solche Vergleichsmitkämpfe im Jahre 1993 und
1996 und seit 2002 finden die jedes Jahr statt.
Jetzt erst vor letzter Woche war die letzte Sat-Competition, von der
die Ergebnisse in Oxford präsentiert wurden.
Also wenn Sie sich dafür interessieren, können Sie mal schauen, was da
die aktuellen Beweiser oder die aktuellen Sat-Solvers so sind und
welche Techniken die einsetzen.
Da gibt es viele Unterlagen dazu auf der Webseite.
Gut, dann 1996 kam ein Verfahren dazu, das nochmal einen ziemlich
großen Sprung nach vorne gebracht hat in den Algorithmen.
Das war ein Verfahren, das nennt sich Conflict Driven Clause Learning.
Also man versucht, bestimmte Eigenschaften vom Lösungsraum aufzufinden
und sich zu merken.
Das war was, was 1996 aufgekommen ist.
Und seit 1996 gibt es auch eine spezialisierte Konferenz nur zu dem
Thema Sat-Solving und leicht verwandte Probleme, die auch seit 2000
jedes Jahr stattfindet.
Und entsprechend, wenn man sich mal anschaut, wie sich die Algorithmen
entwickelt haben, also in den 90er Jahren war es noch so oder Anfang
der 90er Jahre, dass Probleme mit 100 Variablen und 200 Clausen schon
als hart angesehen wurden.
Heutzutage sind das eigentlich Probleme, die auch noch gelöst werden
können, bis in die Größenordnung von einer Million Variablen.
Gut, dann hier, das war die Sat-Konferenz 2015, die war in Austin,
Texas.
Das sind die Teilnehmer von dieser Konferenz.
Dann, wozu wird es wirklich jetzt in der Praxis eingesetzt?
Also es ist etwas, was von Firmen wie IBM oder Intel und auch
Microsoft wirklich eingesetzt wird im täglichen Leben von den
Hardwarefirmen, um Hardware-Designs zu prüfen.
Da gibt es dann eben Techniken wie das Hardware-Model-Checking, das
letztendlich eben auch Sat-Solver dann intern verwendet.
Also damit wird zum Beispiel von diesen funktionalen Einheiten in die
Sicht, die in einem Chip bestehen, die zum Beispiel eine Addition
ausführen können oder eine Ladeoperation ausführen, von denen wird da
die Korrektheit gezeigt.
In der Software-Verifikation werden die Verfahren eingesetzt.
Also sehr viel nochmal mit einer Ebene drüber mit den sogenannten SMT
-Solvern, die erlauben dann eben auch arithmetische Aussagen zu
machen.
Und Microsoft war da sehr früh an diesen Techniken beteiligt, um Sat
-Solver einzusetzen.
Und das Interesse war damals Ende der 90er-Jahre, dass Microsoft
ziemlich große Probleme hat, Gerätetreiber korrekt zu bekommen.
Und Microsoft galt damals auch als nicht sonderlich stabil, kam
relativ häufig zu diesen Blue-Screens.
Und die Behauptung von Microsoft war damals zumindest, dass das nicht
die Schuld von Microsoft ist, sondern von irgendwelchen anderen
Firmen, die Gerätetreiber entwickeln, z.B.
für eine Grafikkarte oder für sonstige Geräte.
Und dass die eben fehlerhaft wären und dann haben sie eben darauf
reagiert, dass an Schnittstellen zu den Gerätetreibern eben bestimmte
Garantien gemacht werden mussten von dieser zugelieferten Software,
die eben automatisiert überprüft wurden.
Oder im Bereich Embedded Systems sind auch diese Verfahren verbreitet.
Also bei Software, die im Fahrzeug oder in Flugzeugen oder auch in
anderen Geräten, z.B.
in der Waschmaschine oder im Kühlschrank laufen.
Auch da ist es unter Umständen so, dass die Software dafür mit dem Sat
-Solver geprüft wurde.
Also Kühlschrank ist vielleicht nicht ganz so sicherheitskritisch,
dass Sie da wirklich wissen müssen, dass der immer genau das Richtige
macht.
Aber wenn Sie dann denken, es gibt auch medizinische Geräte, die auch
Software gesteuert sind, z.B.
Herzschrittmacher.
Und da ist es vielleicht schon wichtiger, dass Sie da eben keine
Fehler in Ihrer Software haben, sondern dass die immer funktioniert.
Gut, dann Planungsprobleme sind etwas, was mit Sat-Solvern behandelt
werden kann.
Sehr gut sogar.
Also wie bekommen Sie als Spedition z.B.
bestimmte Gegenstände von einem Startzustand zu Ihrem Kunden, also zu
einem Endzustand.
Es gibt sehr viele zahlentheoretische Probleme, die mit Sat-Solver
behandelt werden können.
Oder andere NP-vollständige Probleme eben, für die man mit einer Sat
-Codierung auch ein Lösungsverfahren oder ein Sat-Solver einsetzen
kann.
Oh, jetzt haben wir sogar noch musikalische Unterhaltung hier dazu.
Eines von diesen Problemen hier, zwar dieses Pythagoreische-Trippel
-Problem, das wir uns jetzt auch nochmal kurz anschauen, weil das ist
wirklich eines, das es sogar bis in den Spiegel geschafft hat und in
eine Reihe von anderen nicht fachwissenschaftlichen Zeitungen oder
Zeitschriften.
Und zwar liegt es auch erst ein paar Jahre zurück.
Ich weiß nicht, ob wir hier ein Datum draufstehen.
Ich habe es nicht mehr genau im Kopf.
Also vor circa zwei Jahren war das, dass eben mit
Computerunterstützung, das heißt in dem Fall jetzt mit Hilfe von einem
Sat -Solver, ein Beweis gefunden wurde für ein bis dahin noch offenes
zahlentheoretisches Problem.
Und das war eine Kollaboration zwischen der Universität Austin in
Texas und einem Forscher, der da an Sat-Solvern geforscht hat und
einer weiteren Gruppe in Großbritannien.
Und die haben das eben als größten Beweis der Welt dann dargestellt,
weil der Beweis für diese Zahlentheoretische Eigenschaft eben 200
Terabyte benötigt.
200 Terabyte, was wirklich fast nicht auf Ihre Festplatte, die Sie zu
Hause haben wahrscheinlich, drauf, sondern das ist etwas, was wirklich
einen sehr, sehr großen Beweis erfordert, der natürlich auch dann
nicht mehr von Menschen geprüft werden kann, sondern den man dann auch
wieder maschinell prüfen muss, ob der Beweis dann auch in sich stimmig
ist.
Okay, also das ist ein Problem, das mit Sat-Solvern gelöst werden
konnte und schauen wir uns mal an, worum es bei diesem Problem hier
geht.
Also das ist dieses sogenannte Pythagoreische Triple Problem,
zahlentheoretisches Problem.
Lässt sich relativ einfach formulieren, es wirkt vielleicht ein
bisschen exotisch, aber es ist eben eines der offenen Probleme auf
diesem Gebiet.
Worum geht es?
Wir schauen uns die natürlichen Zahlen an und darum steht jetzt auch
erstmal nur ein Ausschnitt, also das heißt die Zahlen von 1 bis N.
Und wir wollen jetzt den Zahlen jeweils eine von zwei Farben zuweisen,
also sagen wir mal Rot und Blau zum Beispiel.
Also jede Zahl bekommt, 1 ist Rot zum Beispiel, 2 ist Blau und so
weiter.
Und das wäre jetzt noch nicht so schwierig, wir haben aber jetzt noch
zusätzlich eine Bedingung.
Und zwar soll noch gelten, wenn wir so ein Zahlentrippel haben, a, b,
c oder es gilt a² plus b² gleich c², dann ist es nicht erlaubt, dass
a, b und c dieselbe Farbe haben.
Also dann darf nicht a, b und c gleichzeitig Rot sein oder
gleichzeitig Blau sein, sondern mindestens eines von diesen drei
Zahlen muss eine unterschiedliche Farbe haben.
Also was wäre so ein Trippel jetzt?
3, 4, 5 ist ja eines der bekanntesten pädagogischen Trippel, also 3²
plus 4², 9 plus 16 ist 25, also 5².
Also das würde bedeuten, 3, 4 und 5 dürfen nicht dieselbe Farbe haben.
Und dann gibt es natürlich jetzt nicht nur die 3, 4 und 5, die diese
Eigenschaft erfüllt, hier drin stehen noch viele andere Zahlen.
Und die Frage ist, ist es möglich, dass man eben diesen Ausschnitt der
Zahlen von 1 bis n so mit Rot und Blau einfärbt, jede Zahl, dass für
alle pädagogischen Trippel unterschiedliche Farben verwendet werden.
Also relativ einfaches Problem, aber es ist auch die Frage, wie man
das jetzt irgendwie lösen könnte.
Und letztendlich kann man da auch schon vermuten, das ist etwas, was
sich vielleicht einfach nur durch Ausprobieren oder durch wirklich
systematisches Durchprobieren von allen Zahlen bewerkstelligen lässt.
Es sei denn, man hat eben wirklich eine ganz geniale Idee oder
irgendeine Eigenschaft über diese pädagogischen Trippel, wie sich die
verhalten, dass man eben so eine Eigenschaft zeigen kann.
Aber das ist eben zahlentheoretisch so, dass es da eben nichts
Offensichtliches gibt, was einem da jetzt weiterhelfen könnte.
Deshalb eben dieser andere Ansatz, einfach als aussagenlogisches
Problem kodieren und dann versuchen zu zeigen, ob das geht oder nicht.
Genau.
Und wenn es jetzt möglich wäre, für alle n diese Färbung vorzunehmen,
dann würde unser Satzhäufer nicht so viel helfen, weil der Satzhäufer
kann ja eben nicht die ganzen natürlichen Zahlen kodieren, sondern
immer nur ein gewisses Anfangsstück.
In der Aussagenlogik ist ja alles immer ähnlich.
Das heißt, hier ist dann auch noch der glückliche Umstand
dazugekommen, dass sich dieses Problem eben nicht lösen lässt oder
dass es keine solche Färbung gibt von den natürlichen Zahlen.
Und das heißt, wenn es keine gibt, dann muss es auch ein Anfangsstück
der natürlichen Zahlen geben, wo diese Eigenschaft dann zum ersten Mal
verletzt ist.
Und dann wurde mit Hilfe von Satzhäuern, der hat einfach
durchprobiert, ja für zunehmend größere n mit dem Satzhäuer hat er
versucht, diese Probleme zu lösen.
Und hat dann festgestellt, bei 7825 ist es zum ersten Mal so, dass
wenn man versucht, diese Zahlen einzufärben mit dieser Einschränkung
für pädagogische Trippel, dass es dann nicht mehr möglich ist.
Also bei bis 7824 war es noch möglich, da konnte man noch so eine
Färbung finden, aber da ist dann eben die Grenze, wo es nicht mehr
geht.
Und dieser Beweis wurde mit einem Satzhäuer durchgeführt und der war
eben dann so groß, wie es hier dran steht, eben diese 3200 Terabyte
groß.
In dem Lösungsverfahren sage ich gleich noch was, was der da an Tricks
angewandt hatte.
Also es ist nicht so ganz so trivial, dass man einfach nur so einen
Blackbox -Satzhäuer hernimmt und dann das direkt gelöst bekommt.
Aber schauen wir uns erst mal an, wie man das Problem codieren kann.
Und das ist eigentlich auch wieder relativ einfach.
Also beim Codieren ist es eigentlich immer so, als erstes überlegen
wir uns, was sind unsere Variablen, was sollen die ausdrücken.
Und es ist hier eigentlich ganz naheliegend, dass man sagt, ja für
jede natürliche Zahl habe ich eben dann eine budge Variable.
Und wenn die auf 1 gesetzt ist, dann ist es eben die Farbe 1.
Und wenn sie, oder sagen wir Rot zum Beispiel, und wenn sie auf 0
gesetzt ist, dann soll das die Farbe Blau sein.
Das heißt, die budge Variable zeigt uns eben an, welche der zwei
Farben die entsprechende Zahl bekommen hat.
Das heißt, wir haben eben dann für jede natürliche Zahl eine
auslogische Variable.
Und dann müssen wir eben diese Lösungen ausschließen, die allen
pythagoreischen Zahlentrippeln, allen Zahlen dieselbe Farbe zuweisen
würde.
Und das können wir eben mit entsprechenden Klausen machen, die wir zu
unserem Problem zunehmen.
Also wenn wir ein bestimmtes pythagoreisches Trippel haben, also zum
Beispiel 3, 4 und 5, dann darf es eben nicht sein, dass die die
gleiche Farbe haben.
Und das heißt, wir müssen ausschließen, dass diese drei Variablen, xa,
xb, xc, dass die gleichzeitig wahr sind und wir müssen ausschließen,
dass die alle gleichzeitig falsch sind.
Und das Ausschließen, dass sie alle gleichzeitig falsch sind, können
wir mit dieser ersten Klausel hier machen.
Also wenn alle jetzt hier Bars oder 0 wären, dann wäre die Klausel
natürlich nicht erfüllt.
Wenn alle 1 wären, wäre diese zweite Klausel nicht erfüllt.
Also das heißt, was macht man?
Man umführt die Codierung, man berechnet alle pythagoreischen Trippel
bis zu dieser Grenze.
Also das muss man halt mit einem externen Algorithmus machen.
Wir suchen eben alle Zahlen a, b, c, für die diese Eigenschaft a² plus
b² gleich c² gilt, wobei die a, b, c eben im Bereich von 1 bis unserem
n liegen.
Und für jedes solche Trippel, das ich gefunden habe, nehme ich diese
zwei Klauseln zum Problem dazu.
Und dann habe ich das Problem codiert und kann versuchen, mit Hilfe
von einem Satzsolver das zu lösen.
Das hat er auch gemacht, das war ein paralleler Satzsolver.
Der Algorithmus hat auch bestimmte Tricks verwendet, wie man die
Teilprobleme für die einzelnen parallel laufenden Solver besonders
geschickt aufteilen kann.
Dann gab es noch ein paar Vereinfachungen an der Formel.
Und der Solver lief dann auf einem Großrechner drei, vier Wochen und
hat dann eben diesen Beweis ausgespuckt, dass es hier eben keine
Lösung gibt.
Und da haben wir dann eben zum ersten Mal den Beweis gefunden für
dieses Pythagorische Trippelproblem.
Also das wäre eine Einwendung von Satzsolver in diesem eher
mathematischen Bereich, Zahlentheoretischen, was jetzt vielleicht in
der Praxis nicht die großen Auswirkungen hat.
Also ob diese Eigenschaft jetzt gilt oder nicht, lässt sich
wahrscheinlich jetzt auch nicht so groß weiter daraus ableiten.
Ein weiteres Problem, was auch häufig von Mathematikern an dieser Art
von Beweisen kritisiert wird, ist eben, dass man durch Lösen oder
durch Beweisen von Eigenschaften sich in der Mathematik eigentlich
erhofft, ein besseres Verständnis von dem Problemgebiet zu bekommen,
auf dem man arbeitet.
Also hier zum Beispiel, dass man ein besseres Verständnis erhalten
könnte zu Eigenschaften von natürlichen Zahlen oder zu Verhältnissen
zwischen Addition und Multiplikation, wie es ja hier auch auftritt.
Wenn man jetzt natürlich so einen computergenerierten Beweis hat, der
verrät einem natürlich relativ wenig darüber, was jetzt eine
menschlich verständliche Eigenschaft wäre oder irgendein
tiefergehender Zusammenhang zwischen natürlichen Zahlen oder zwischen
Addition und Multiplikation, wie man durch einen Beweis jetzt eben
erkennt.
Und genau, das ist ein bisschen ein Nachteil, dafür kann man damit
eben automatisiert solche Dinge entscheiden.
Okay.
Es ist auch ein bisschen eher das, sagen wir mal, das exotischere,
solche Arten von Problemen zu lösen, wo die viel häufiger eingesetzt
worden sind, eben wirklich für die Korrektheit von Hardware oder
Software zum Beispiel.
Okay.
Jetzt habe ich noch ein zweites, etwas zahlentheoretisches Problem,
was wir uns noch schnell anschauen wollen, das sich auch sehr einfach
als aussagenlogisches Problem kodieren lässt.
Und hier geht es um eine Sequenz, um binäre Zahlen.
Also wir haben eine Sequenz von Einsen und Nullen, in dem Fall einfach
jetzt von X1 bis X8 erstmal.
Und die Frage ist, gibt es in dieser Sequenz oder kann man eine
Sequenz von Zahlen oder von solchen Nullen und Einsen angeben, sodass
keine drei Nullen im gleichen Abstand in dieser Sequenz vorkommen und
auch keine drei Einsen mit dem gleichen Abstand in der Sequenz.
Also wenn wir uns das jetzt mal anschauen, was das auch bedeutet.
Also hier wäre die Frage, gibt es hier in dieser Sequenz 01011011,
gibt es da zum Beispiel drei Einsen, die den gleichen Abstand haben.
Und was bedeutet Abstand?
Einfach wie viele Positionen, die praktisch voneinander entfernt sind.
Also wenn wir jetzt von vorne durchsehen, Position 1, dann hätten wir
die erste Eins in Position 2, dann in Position 5 eine und dann in
Position 8 wieder eine.
Und zwischen 2 und 5 und 5 und 8 ist der Abstand natürlich gleich.
Also da liegen jeweils eben zwei Plätze dazwischen.
Und das heißt, hier hätten wir eben drei solche, ja, gleiche Zahlen
mit gleichem Abstand.
Wenn wir bei der Null schauen, wie sieht das hier aus, haben wir bei
der Null drei Nullen mit gleichem Abstand in dieser Sequenz.
Da können wir von vorne probieren, die 1,3 müsste 5 sein, das ist
nicht der Fall, 1,4 passt auch nicht.
Also drei Nullen mit gleichem Abstand haben wir hier nicht in dieser
Sequenz, nur drei Einsen.
Und die Frage ist jetzt eben, wie sieht das aus, wenn wir jetzt
größere Sequenzen wählen?
Gibt es dann immer diese Triple mit gleichem Abstand oder gehen die
irgendwann mal praktisch aus?
Aber schauen wir uns das mal hier noch an, also in dem Fall, wenn wir
nur Sequenzen der Länge 8 haben, ist es so, dass es da sogar sechs
Lösungen gibt.
Können Sie zu Hause überprüfen, dass da wirklich solche Drehzahlen mit
gleichem Abstand gibt oder Drehziffern.
Wenn man jetzt aber von 8 auf 9 Ziffern geht, dann ist es so, dass es
schon keine Lösung mehr gibt.
Also bei 9 Ziffern ist es so, dass es eben, genau, da gibt es dann
nicht mehr.
Also wie können wir das machen?
Wir können uns diese wieder kodieren als ein aussagenlogisches
Problem, was verboten ist.
Also zum Beispiel hier x2, x5 und x8 dürfen nicht gleichzeitig alle 1
sein, weil die eben den gleichen Abstand hätten.
Es gibt dann diese Klausel und genau die können wir...
Und wenn wir jetzt diese Klausel in einer abgekürzten Weise hier
aufschreiben, zum Beispiel mit diesem... also nicht 2, nicht 5, nicht
6, nicht 8 mit diesem Strich drüber, dann kommen wir eben hier
letztendlich dazu zu 32 Klauseln für die Sequenz, wenn wir uns auf 9
Ziffern jetzt anschauen, die so irgendwie aussehen.
Und wenn man prüft, ob die erfüllbar sind, dann stellt man eben fest,
dass das nicht mehr erfüllbar ist.
Okay, und das ist auch wieder was, also diese Sequenzen selber, die
wirken jetzt vielleicht noch nicht so interessant, aber das ist eine
etwas...
also mit einer Verallgemeinerung kommt man da zu einem Begriff, auch
wieder der Zahlentheorie, der doch von einigen Mathematikern
betrachtet wird.
Und zwar geht es da um die sogenannten Van der Werden-Zahlen.
Und die Behauptung ist erstmal, oder das Theorem von dem Van der
Werden, dass wenn man ein groß genuges n wählt, dann gibt es immer
eine Sequenz von Zahlen x1 bis xn.
Die dürfen jetzt nicht nur 0 und 1 sein, sondern dürfen von 0 bis r-1
gehen.
Das heißt, wir haben jetzt praktisch kein Binärsystem mehr, sondern
ein r-zifferiges System.
Und jede Sequenz, wenn man die lang genug wählt, enthält eine Ziffer,
die mindestens k-mal mit gleichen Abschnitten auftritt.
Also das ist jetzt die Behauptung, dass es, wenn wir nur das n groß
genug wählen, irgendwann mal so eine Sequenz gibt.
Also wie dieses Problem von 2, 5 und 8, was wir vorher hatten.
Und die Van der Werden-Zahl ist jetzt das kleinste n für das Bezug
gegebenen r und k, das zum ersten Mal der Fall ist, dass man diese
gleich abständigen k-Ziffern hat.
Und was wir gesehen hatten, ist, dass zum Beispiel die Van der Werden
-Zahl von 2 und 3, dass die 9 ist und für größere Werte von r und k
ist da aber schon ganz wenig bekannt.
Also da kommt man schnell in Bereiche, wo man nicht mehr weiterkommt.
Also die Zahl W2 6, die ist zum Beispiel bestimmt worden als 1132.
Also das ist jetzt auch wieder 2, das bedeutet immer, dass wir im
Binärsystem arbeiten, also wie wir es gerade gemacht hatten.
Und dass es jetzt darum geht, um Sequenzen, wo eine Ziffer eben
sechsmal hintereinander mit selbem Abstand vorkommt.
Und da ist es so, dass es zum ersten Mal der Fall ist, eben bei 1132.
Das wurde auch mithilfe von einem Satz drüber gezeigt.
Aber schon die Zahl W2 7 ist bis heute nicht bekannt, ab welchem Wert
das für n diese Eigenschaft erfüllt ist.
Also das ist vielleicht auch wieder überraschend, weil das eigentlich
wieder alles relativ einfach formulierbare Probleme sind.
Die Zahlen eigentlich auch nicht so groß sind und man trotzdem eben
durch die Kombinatorik so viele Möglichkeiten erhält, dass es eben
nicht mehr wirklich einfach bewiesen werden kann.
Was es an theoretischen Ergebnissen noch gibt, ist diese obere
Schranke für W r k.
Aber die ist natürlich sehr, sehr grobe Abschätzung, aber immerhin
erst mal eine, die auch erst 2001 gefunden worden ist.
Das heißt, diese Zahl W r k ist höchstens 2 hoch 2 hoch r hoch 2 hoch
2 hoch k plus 9.
Also extrem große Zahl, die man einfach erst mal weisen konnte, dass
es zumindest da drunter liegen muss.
Aber die ist natürlich ziemlich sicher sehr weit von der wirklichen
Zahl W r k entfernt.
Okay, also auch solche Dinge lassen sich eben mit Zahlzonen lösen und
wurden wie gesagt auch mit Zahlzonen gelöst, dass das auch
mathematisch publizierbare Ergebnisse sind.
Andere Dinge wären, die man mit Zahlzonen auch noch betrachtet, zum
Beispiel diese Graph-Farbung.
Und da gab es auch eine interessante Sache, wir hatten ja auch ganz
kurz schon uns mit Graph-Farbung oder mit diesem Phänomen beschäftigt,
dass es in der Ebene eben jeder Graph mit vier Farben gefärbt werden
konnte.
Also diese Vier-Farben-Vermutung, die wurde auch erst in den 70er
Jahren bewiesen.
Und in dem selben Jahr gab es dann in so einer mathematischen
Zeitschrift, ein bisschen so eine Rätselzeitschrift, in Scientific
American gab es eine Kolumne von diesem Martin Gardner Mathematical
Games und da hat er behauptet, ja dieser Beweis stimmt vielleicht doch
nicht für die Vier-Farben-Vermutung und er hätte jetzt hier ein
Beispiel, das er von diesem McGregor bekommen hätte, der eben nur mit
fünf Farben gefärbt werden könnte.
Was auch interessant ist, diese Ausgabe der Zeitschrift, wo er das
behauptet hat, die ist am ersten April rausgekommen und das war dann
letztendlich auch die Auflösung, also es war dann eigentlich nur ein
April -Schatz von ihm und dieser Graph, der lässt sich halt eben auch
mit vier Farben färben.
Aber das war der Graph, den er damals angegeben hatte, den man
versuchen sollte mit vier Farben zu färben.
Das kann man natürlich jetzt von Hand mal probieren, indem man einfach
mal schaut, also jedes Kästchen bekommt eine Farbe, zwei benachbarte
Kästchen, die eine gemeinsame Linie haben, dürfen nicht dieselbe Farbe
haben, ob das jetzt eben mit vier Farben wirklich nicht mehr geht.
Und man findet dann raus, ja das geht eben doch mit vier Farben, hier
wäre zum Beispiel so eine Lösung.
Aber das ist was, was sich eben auch mit dem Satzhäufer zum Beispiel
überprüfen lässt.
Also wenn mir jetzt so ein Problem gegeben hätte, lässt sich dieser
Graph mit wirklich, wie die Behauptung eben sagt, nur mit fünf Farben
färben, könnte man das eben mit einem Satzhäufer versuchen, das für
den zu kodieren und dann mit vier Farben versuchen, eine Lösung zu
finden.
Okay, also hier nochmal das Graph-Färbungsproblem, aber das hat man ja
eigentlich schon gesagt, wie das funktioniert.
Und für eine Satzkodierung, wie gesagt, immer der erste Schritt, man
schaut sich an, was sollen die Variablen ausdrücken und was sich hier
anbietet, ist, dass man jeweils eine bulsche Variable angibt oder
verwendet, die angibt, dass unser Knotenbau im Graph die Farbe C hat.
Also für jedes Paar aus Knoten und Farbe wählen wir eine Variable, die
uns ausdrückt, wenn sie wahr ist, ja, dieser Knoten hat diese gegebene
Farbe.
Und damit kommen wir dann zu einer Kodierung, die für K-Farben eben K
mal die Anzahl der Knoten, viele bulsche Variablen benötigt.
Genau, und die wollen wir auch einfach so dann durchnummerieren zum
Beispiel, dass wir sagen, also für jeden Knoten bekommt halt die
Variable, für jeden Knoten V haben wir diese K-Variablen, V1 bis Vk
für jede der K-Farben.
Und dann können wir ausdrücken, dass jeder Knoten mindestens eine
Farbe benötigt, eben mit so einer Klausel V1 oder Vk.
Also jeder Knoten bekommt mindestens eine Farbe.
Und dann schließen wir aus, dass benachbarte Knoten dieselbe Farbe
haben, indem wir eben für jede Kante von U nach V und für jede Farbe
so eine Klausel dazufügen, dass nicht gleichzeitig UJ und VJ sein
darf.
Also dass nicht gleichzeitig Knoten U die Farbe J haben kann und V die
Farbe J haben kann.
Und das müssen wir eben für jede Farbe machen.
Das heißt, solche Klausel V in der zweiten Zeile bekommen wir dann für
jedes K und für jede Kante.
Und damit haben wir dann auch unser Problem schon als Satzproblem
kodiert.
Okay, und dann kann man wieder einen Satz drauf loslaufen lassen.
Hier noch ein Beispiel, das möchte ich einfach mal überspringen hier.
Das können Sie sich noch zu Hause anschauen.
Vielleicht ganz kurz zum Abschluss bloß.
Wenn Sie wirklich jetzt mal selber so einen Satzsolver einsetzen
wollen, dann ist es so, dass man die in vielen Fällen einfach als
Blackbox -Solver verwendet und man muss dann eben das passende
Eingabeformat von diesen Solvern kennen.
Das ist in der Zwischenzeit quasi standardisiert.
Das heißt, da gibt es dieses sogenannte Dimex-Format dafür.
Hat die Erinnerung DNF.
Und das sind Textdateien, die eben so eine Formel kodieren.
Und es sieht so aus, dass man erst mal Kommentarzeilen haben darf.
Dann gibt es eine Zeile, die mit einem P beginnen muss.
P für Problem, CNF.
Sagt uns eben, dass es sich um eine Formel CNF handelt.
Sieben Variablen, 22 Klauseln.
Gibt uns an, wie groß das Problem ist.
Und dann folgen die Klauseln einfach mit den Variablen-Nummern.
Wenn es negiert, ist die Variable ein Minus davor.
Die Variablen sind dann natürlich ab 1 durchnummert.
Und das Ende einer Klausel wird mit der Null angezeigt.
Also hier hat man zum Beispiel in der ersten Zeile dann die Klausel X1
oder nicht X2 oder X7.
Und in dem Format schreiben Sie dann Ihre Probleme auf, lassen den
Satz nochmal drauflaufen.
Und der gibt Ihnen dann eine Lösung zurück.
Auch wieder in einem standardisierten Format.
Auch wieder Kommentare.
Dann so eine Zeile, die mit S beginnt.
Die uns die Lösung angibt.
Also Satisfiable oder Unsatisfiable.
Eben ob es eine Lösung gab oder nicht.
Darf auch an und drin stehen, wenn der Solver eben keine Lösung finden
konnte oder die Zeit ausgegangen ist.
Und dann danach folgt in diesen V-Zeilen die Belegung der Variablen.
Wobei jetzt hier ausgedrückt, zum Beispiel 1 bedeutet, die Variable 1
wird mit True belegt.
Minus 3 würde bedeuten, die Variable 3 wird mit False belegt.
Gut, und damit können Sie dann, wenn Sie so ein kombinatorisches
Problem haben, versuchen das eben für einen Satz zu kodieren.
Und wie jetzt die Algorithmen dann genau aussehen, die eben auch mit
extrem großen Problemen arbeiten können.
Mit einer Million Variablen zum Beispiel.
Und welche Tricks da so in den Solvern eingebaut sind.
Das ist was, was Sie dann zum Beispiel später in der Vorlesung, wie
der Satz-Hooding-Vorlesung oder auch in anderen formalen Methoden
-Vorlesungen dann noch lernen können.
Okay, gut.
Damit sind wir durch mit dem Stoff der Vorlesung.
Also Algorithmen 1 ist damit abgeschlossen.
Algorithmen 2 steht dann ja noch vor Ihnen.
Aber vor Algorithmen 2 eben auch noch die Klausur.
Und deshalb möchte ich da noch ganz kurz was dazu sagen.
Also die Klausur findet statt Anfang September, am 4.
September.
Und zwar 8 Uhr bis 11 Uhr ist als Zeitraum vorgesehen.
Die Bearbeitungszeit ist etwas kürzer, also wir brauchen am Anfang
noch ein bisschen Zeit, bis alle Klausuren ausgeteilt sind, bis jeder
richtig sitzt.
Aber 8 Uhr pünktlich da sein, da geht's los dann.
Es gibt 60 Punkte, die man bei der Klausur erreichen kann.
Und es ist auch, ähnlich wie bei der Probeklausur, erlaubt, dass Sie
als Hilfsmittel ein handschriftlich beschriebenes DIN A4-Blatt
mitbringen dürfen.
Also es darf beidseitig beschrieben sein, aber nicht irgendwie
ausgedruckt mit 5-Punkt-Schrift oder sowas, sondern muss
handschriftlich sein.
Und da können Sie bestimmte Dinge, die Sie eben sich nicht auswendig
merken wollen, darauf hinterlegen.
Ich sage gleich noch ein bisschen mehr dazu, aber jetzt erst noch mal
zu dem formalen Prozess.
Sie müssen sich anmelden für die Klausur.
Wenn Sie nicht angemeldet sind, können Sie nicht an der Klausur
teilnehmen.
Und die Anmeldung ist bereits freigeschaltet.
Ich habe gesehen, es sind auch schon sehr viele, ich glaube über 300
haben sich schon angemeldet von Ihnen.
Wer sich bisher noch nicht eingetragen hat, muss das bis spätestens
zum 28.
August gemacht haben.
Danach wird die Anmeldung geschlossen und es ist dann eben nicht mehr
möglich, die Klausur anzutreten, sondern Sie müssen dann ein Semester
warten bis nach dem Wintersemester und können erst dann wieder die
Klausur antreten.
Also denken Sie dran, rechtzeitig anmelden.
Dann für die Anmeldung, wenn Sie sich nach der 2015 Prüfungsordnung
prüfen lassen, geht es über das Campus-System, das Sie ja alle kennen.
Wenn Sie sich nach der alten Prüfungsordnung von 2080 noch prüfen
lassen, dann müssen Sie sich über das HisPos-System anmelden.
Betrifft das überhaupt noch jemand?
Darf ich mal kurz fragen, ist jemand noch nach der alten
Prüfungsordnung?
Nee, zumindest von den Anwesenden wohl niemand.
Also das heißt bei Ihnen dann alle das Campus-System.
Was auch noch wichtig ist zu der Klausur, müssen Sie Ihren
Personalausweis oder Pass und Studentenausweis mitbringen.
Wir werden das dann kontrollieren zu Beginn der Klausur, dass niemand
anderes für Sie jetzt die Klausur schreibt und dass es wirklich auch
Sie sind.
Also deshalb dran denken, diese beiden Sachen bitte mitbringen.
Gut, dann ist es so, da wir ja sehr viele Teilnehmer haben, wird die
Klausur nicht in einem Hörsaal, sondern verteilt über verschiedene
Hörsäle stattfinden.
Und das heißt, Sie müssen dann vor der Klausur herausfinden, in
welchen Hörsaal Sie gehen müssen und wo Sie die Klausur mitschreiben.
Und die Einteilung, die werden wir anhand von Matrikelnummer-Bereichen
vornehmen.
Das heißt, wir werden irgendwann mal veröffentlichen über das Ilias
-System, welche Matrikelnummer-Bereiche in welchem Hörsaal sind.
Und da würde ich Sie auch bitten, einfach rechtzeitig vor der Klausur,
also vielleicht zwei, drei Tage vorher mal zu schauen, wo sind Sie
denn jetzt eingeteilt.
Und dazu einfach im Ilias-System auf den Seiten, wo Sie das Forum oder
auch die Übungsblätter und die Vorlesungsfolien runterladen können.
Da wird das auch veröffentlicht werden.
Okay, also wichtig, erst mal sich anmelden bis zum 28.08.
für alle, die es noch nicht gemacht haben.
Sonst können Sie nicht an der Klausur teilnehmen und dann rechtzeitig
schauen, in welchem Hörsaal Sie sitzen.
Also Sie können nur in dem Hörsaal sitzen oder die Klausur schreiben,
in den Sie eingetragen sind.
Gut, dann ist es so, es gibt ja auch schon gesagt, es gibt diesen
Wiederholungstermin dann erst wieder ein Semester später.
Das heißt, wenn Sie zu der Klausur nicht anbreten oder wenn Sie die
Klausur nicht bestehen, dann gibt es eben ein Semester später nach dem
Wintersemester nochmal die Möglichkeit, wieder die Klausur zu
Algorithmen 1 zu schreiben.
Es gibt auch nach der Klausur, ich weiß noch nicht genau wann jetzt,
voraussichtlich ca.
zwei bis drei Wochen später, gibt es die Möglichkeit, die Klausur
einzusehen.
Das heißt, da können Sie, wenn Sie nochmal schauen wollen zu Ihren
Punkten, ob das auch Ihrer Meinung nach so passt, gibt es die
Möglichkeit, eben zu der Klausureinsicht zu kommen.
Den Termin wird man auch noch rechtzeitig bekannt geben.
Okay, dann hatten wir über die Übungsblätter einen Klausurbonus.
Das heißt, wenn Sie die entsprechende Punktzahl während der Übungen
erreicht haben, bekommen Sie einen Bonuspunkt oder ein bis drei
Bonuspunkte.
Und jetzt haben wir insgesamt 130 Punkte für die Übungen gehabt.
Das heißt, die Grenzen für ein, zwei und drei Bonuspunkte sind jetzt
eben entsprechend wie hier angegeben.
Also ab 65 Punkte z.B.
bekommen Sie dann zwei Bonuspunkte für die Klausur.
Es gibt jetzt noch ein paar Regelungen dazu.
Die Bonuspunkte werden nur angerechnet, wenn Sie die Klausur bestanden
haben, auch ohne Bonuspunkte.
Also das heißt, wenn Sie sonst ohne Bonuspunkte durchgefallen wären,
dann helfen Ihnen auch die Bonuspunkte nichts in dem Fall, sondern
nur, wenn Sie sie bestanden haben.
Falls jemand die Klausur schon mal ein Jahr vorher gemacht hat oder
die Übungen zumindest ein Jahr vorher schon mal, dann kann er diese
Bonuspunkte von damals sich auch noch heute anrechnen lassen und dazu
einfach eine E-Mail an Markus Iser schreiben, dass der die Information
zu ihren bisherigen früheren Bonuspunkten hat.
Und dann zu den Inhalten, die in der Klausur drankommen, wird der
gesamte Stoff der Vorlesung sein.
Bis auf das, was wir heute zu Satzformeln gemacht haben, das ist nicht
mit dabei.
Auch das, was in den Übungen, also in den Saalübungen behandelt worden
ist, ist auch was, was in der Klausur mit drankommen kann.
Und ich werde jetzt im Laufe der Woche auch nochmal eine Datei nochmal
hochladen, wo Sie nochmal etwas detaillierter sehen, was denn der
Stoff ist und in welcher Form wir das behandeln werden.
Das ist etwas, was in den letzten Semestern auch häufig in der
Saalübung dann nochmal angekündigt wurde, etwas detaillierter, welche
Themen denn für die Klausur wichtig sind.
Und wenn wir jetzt eben keine Übung mehr haben, würde ich das einfach
in Ilias hochladen.
Dann können Sie da reinschauen, was eben der relevante Stoff ist.
Gut, ansonsten bei Fragen, entweder über das Ilias-System oder wenn es
sehr spezielle Dinge sind, die vielleicht Ihre Kommilitonen nicht
interessieren, können Sie auch direkt eine E-Mail an Markus Iser am
besten wieder schreiben.
Oder jetzt direkt noch, wenn es gerade ganz konkret noch Fragen gibt,
einfach hier eine Frage stellen.
Okay, also scheint gerade nicht der Fall zu sein.
Also falls Ihnen bis zur Klausur noch etwas einfällt, was Sie noch
wissen müssen, dann wie gesagt entweder das Forum verwenden, wenn es
von breitem Interesse ist, oder eben eine E-Mail schicken.
Ansonsten sind wir jetzt damit am Ende der Vorlesung angekommen.
Ich hoffe, es hat Ihnen auch ein bisschen Spaß gemacht, die
Algorithmen zu hören, dass Sie etwas dabei gelernt haben.
Ich wünsche Ihnen dann erholsame Semesterferien, zumindest zum Teil,
solange Sie sich nicht auf die Klausuren vorbereiten müssen, dass Sie
sich da auch ein bisschen entspannen können.
Und hoffe, dass wir uns vielleicht mal in einer weiterführenden
Vorlesung dann wiedersehen.