Welchen Status hat das SAT zu welchem Zeitpunkt - Korrektheit und Laufzeit

[StefanUniBonn]

Es ist an manchen Stellen unklar, was Funktionen eigentlich genau tun sollen, und dadurch auch, ob sie das richtige tun.

Die Funktion Clause::biggesterror verwendet gerade die Belegung überhaupt nicht. Wahrscheinlich soll sie die größte Variable zurückgeben, deren aktuelle Belegung 0 ist, damit dann bis zu der gebacktracked werden und die Variable auf eine 1 gesetzt werden kann?

Die Funktion SAT::biggesterror sollte dann vermutlich durch eine Funktion SAT::backtrack_until ersetzt werden? Wenn zwei Klauseln nicht erfüllt sind, und in der eine ist die größte modifizierbare Variable 13, und in der anderen 11, dann kannst du ja bis 11 backtracken, weil die zweite Klausel immer noch unerfüllbar ist, wenn du nur bis 13 backtrackst?

In next bzw. nextimp findest du erst mal sinnvoll die Variable die du auf 1 ändern möchtest. Aber die Variablen dazwischen setzt du interessanterweise auf 0 statt auf unassigned. Das macht laufzeitmäßig wenig Sinn, weil du nicht mehr weist, welches die erste der Variablen war, durch deren Wahl das assignment unsatisfiable wurde.

Die Aufteilung in backtracking und backtrackingnaive wirkt auch etwas unituitiv. Wenn du in backtrackingnaive schon gezeigt hast, dass die Instanz UNSAT ist, geht du danach zurück nach backtracking, fügst eine Variable hinzu, und gehst zurck nach backtrack. Die neue Variable ist möglicherweise gar nicht in einer nicht satisfied Klausel, also wird in nextimp im Prinzip wieder alles auf 0 gesetzt und du fängst von Forne an, oder? Ich würde versuchen, die beiden Funktionen zu einer Funktion zu vereinigen, die tatsächlich in allen Fällen das richtig tut.

[StefanUniBonn]

Die kleinste Instanz, die ich finden konnte, wo das Verhalten, dass ich im letzten Absatz beschreibe, auftritt:

p cnf 2 3
1 0
-1 0
2 0

Hier bist du dann sogar sehr schnell in einer Endlosschleife. Wie gesagt würde ich nochmal versuchen, mir genau zu überlegen, welche Funktion eigentlich was überhaupt tun soll, und sie dann so anzupassen, dass sie das auch tatsächlich tun.

[Florenzo87]

Kommentare (für mich vor allem) :

Die Funktion Clause::biggesterror verwendet gerade die Belegung überhaupt nicht. Wahrscheinlich soll sie die größte Variable zurückgeben, deren aktuelle Belegung 0 ist, damit dann bis zu der gebacktracked werden und die Variable auf eine 1 gesetzt werden kann?

Dies wird an der SAT::biggesterror verwendet, da die Clause verified wird bevor man deren größte Variable sucht

Die Funktion SAT::biggesterror sollte dann vermutlich durch eine Funktion SAT::backtrack_until ersetzt werden? Wenn zwei Klauseln nicht erfüllt sind, und in der eine ist die größte modifizierbare Variable 13, und in der anderen 11, dann kannst du ja bis 11 backtracken, weil die zweite Klausel immer noch unerfüllbar ist, wenn du nur bis 13 backtrackst?

Das ist eine gute Idee, mir war das so nicht eingefallen

In next bzw. nextimp findest du erst mal sinnvoll die Variable die du auf 1 ändern möchtest. Aber die Variablen dazwischen setzt du interessanterweise auf 0 statt auf unassigned. Das macht laufzeitmäßig wenig Sinn, weil du nicht mehr weist, welches die erste der Variablen war, durch deren Wahl das assignment unsatisfiable wurde.

Dafür musste Ich aber mein backtracking ändern damit man den depth zurück ändern kann, kommt eventuell noch

Die Aufteilung in backtracking und backtrackingnaive wirkt auch etwas unituitiv. Wenn du in backtrackingnaive schon gezeigt hast, dass die Instanz UNSAT ist, geht du danach zurück nach backtracking, fügst eine Variable hinzu, und gehst zurck nach backtrack. Die neue Variable ist möglicherweise gar nicht in einer nicht satisfied Klausel, also wird in nextimp im Prinzip wieder alles auf 0 gesetzt und du fängst von Forne an, oder? Ich würde versuchen, die beiden Funktionen zu einer Funktion zu vereinigen, die tatsächlich in allen Fällen das richtig tut.

Dies passiert tatsächlick für Unsatisfiable SATs, Ich habe diese Fälle nicht so sehr debugged, es wird aber eigentlich schon der no solution found geprintet wo man schon den Program abrechen kann. Ich werde versuchen die beiden zusammenzufügen da sie eigentlich derselbe Funktion sind, die Ich aber der Sauberkeit halber getrennt hatte.