StefanUniBonn
commented
1 year ago Ich habe gerade festgestellt, dass es Korrektheitsmäßig mehr Probleme gibt, als ich dachte, konzentriere dich lieber darauf. Das hier ist vielleicht trotzdem interessant, aber wie gesagt echt nicht notwendig, um die Einführungsaufgabe zu bestehen.
Alles, was hier steht, ist nicht nötig, um die Einführungsaufgabe zu bestehen, aber ich dachte, es ist vielleicht trotzdem ganz interessant.
Wenn man möchte, dass der Algorithmus irgendeine habwegs sinnvolle praktische Laufzeit hat, dann ist es unglaublich wichtig, dass man sich gut überlegt, welche Variable man als nächstes auf einen Wert setzt. Variablen in unerfüllten Klausen mit möglichst wenigen unassigned Variablen sind im Normalfall die beste wahl. Selbst wenn man etwas sehr simples macht (z.B. einfach eine unerfüllte Klausel mit den wenigsten nicht assigned Variablen suchen und eine beliebe Variable auf einen beliebigen Wert sezten) ist das schon viel viel besser, als alle Variablen nacheinander durchzugehen. Macht natürlich das backtracking komplizierter.
Ansonsten sollte man versuchen, die Laufzeit für jede Interation des Algorithmus möglichst klein zu halten. Du hast an sehr vielen Stellen lineare Laufzeit pro Iteration, weil du z.B. über alle Klauseln läufst (oder das ganze SAT kopiertst). Man kann das sehr viel schneller machen, wenn man sich ein paar einfacher Tricks überleget. Zum Beispiel kann man sich für jede Variable merken, in welchen Klauseln sie überhaupt vorkommt. Dann muss man, wenn man die Variable assigned, nur diese Klauseln überprüfen. (Das ist natürlich weniger einfach, wenn man es mit der Heuristik aus dem vorherigen Absatz kombinieren möchte! Dann braucht man zusätzlich noch eine Datenstruktur, um schnell unerfüllte Klauseln mit wenigen nicht assigned Variablen zu finden ...)