IntegrationFelixTest

[GoogleCodeExporter]

Hallo ich bins schon wieder. 
Beim Test IntegrationFelixTest testIntegrationSat1 faile ich knapp 129000 der 
tests. Was mich dabei nur wundert ist, dass unter anderem als Meldung kommt:

You did not recognize that a ! is satisfiable.

Wenn ich jetzt aber in einem eigenen Test die Formel a ! testen lasse, gibt er 
regulär true zurück. Nach dem Test Code müsste er für true allerdings in 
den else fall der abfrage gehen und die Meldung dürfte es garnicht geben. 
Ich hab per debugging meinen Algorithmus auch schritt für schritt mitverfolgt 
und zumindest für das beispiel läuft alles wie es soll.

Original issue reported on code.google.com by sebastia...@gmail.com on 5 Jul 2012 at 7:56

[GoogleCodeExporter]

Hallo,

wenn du den Test mehrfach laufen lässt, bekommst du dann immer die gleiche 
Zahl fehlschlagender Tests?

Du scheinst generell ziemlich oft "unsatisfiable" als Ergebnis zu bekommen. 
Läuft der testIntegrationUnSat1 bei dir durch?

Ich vermute, dass dein Test bei mehreren Durchläufen irgendwann durcheinander 
kommt.

Kannst du mal den angehängten Test laufen lassen und die Ausgabe hier posten?

--Felix

Original comment by felix@familie-freiberger.net on 5 Jul 2012 at 8:08

Attachments:

• _DebugTest.java

[GoogleCodeExporter]

Ok es schlagen immer verschieden viele fehl.
Der UnSat1 läuft durch. Performance auch.

Die ergebnisse sind im Anhang

Original comment by sebastia...@gmail.com on 5 Jul 2012 at 8:34

Attachments:

• debugtestresult.txt

[GoogleCodeExporter]

Offensichtlich ist irgendetwas an deinem Programm nichtdeterministisch. Leider 
sehe ich nicht, ob es an Tseitin oder an DPLL liegt, da die CNFs nicht 
ausgegeben werden (mein Fehler, ich hab Cnf.toString() implementiert, muss man 
nicht).

Eventuell kannst du den Test (neue Version im Anhang) noch einmal laufen lassen 
und nachschauen, ob die immer die gleiche Formel bekommst. Falls ja (wovon ich 
mal ausgehe), liegt das Problem im DPLL. Du kannst versuchen, mehrfach zu 
debuggen, mit etwas Glück erwischst du mal einen "schlechten" Durchlauf (die 
Chancen stehen laut dem Auszug nicht schlecht, da ja meistens alle 1-3 Tests 
das falsche Ergebnis kommt).

Mein persönlicher Tipp wäre, dass du darauf vertraust, dass eine Collection 
ihre Reihenfolge behält. Das tun Collections, Sets und einige weitere aber 
nicht, sie können sich im Gegenteil selbstständig umsortieren. Hilfreich sind 
da Listen (die behalten ihre Reihenfolge) und der Befehl 
java.util.Collections.sort(List), mit dem du Listen sortieren kannst.

Original comment by felix@familie-freiberger.net on 5 Jul 2012 at 8:45

Attachments:

• _DebugTest.java

[GoogleCodeExporter]

Ok also beim test sind alle formeln gleich.
Ich hab mir zum debuggen immer eine der formeln die angeblich fehlgeschlagen 
sind rausgesucht und einzeln debuggt, weil ichs bischen wahnsinnig fand 130000 
tests auf einmal zu debuggen. 

An der Liste dürfte es nicht liegen. Ich benutze eine ArrayList für die 
lexikalische ordnung und die ändert ihre reihenfolge auch nicht. Hab ich 
getestet.

Original comment by sebastia...@gmail.com on 5 Jul 2012 at 9:05

[GoogleCodeExporter]

OK, dann dürfte das Problem beim DPLL liegen. Du kannst wirklich immer wieder 
die gleiche Formel (z.B. a !) debuggen, da dein Algorithmus ja offensichtlich 
gelegentlich (pseudozufällig) falsch arbeitet.

Solange du nicht bewusst Random benutzt, bleibt als Quelle für Zufall 
allerdings wirklich nicht mehr viel. Du bist dir 100% sicher, dass im 
DPLLAlgorithm nichts nichtdeterministisches geschieht, insbesondere kein 
Arbeiten auf Collections, Sets oder Maps? Denk auch an Aufrufe wie 
Cnf.getClauses()!

Original comment by felix@familie-freiberger.net on 5 Jul 2012 at 9:13

[GoogleCodeExporter]

[deleted comment]

[GoogleCodeExporter]

Ich lese aus den getClauses die Namen der Variablen aus in eine ArrayList die 
ich dann sortiere. In der Map sollte die Reihenfolge auch stimmen und 
eigentlich auch egal sein, da ich ja immer über die keys zugreife. 

Ich hab den Test für a ! jetzt per schleife paarmal ausführen lassen und die 
ergebnisse wechseln sich wirklich einfach ab. Ich werd das morgen mal schritt 
für schritt durchgehen. 
Vielen vielen dank schonmal!

Original comment by sebastia...@gmail.com on 5 Jul 2012 at 9:31

[GoogleCodeExporter]

Kein Problem. Wie gesagt, wenn du es debuggst, solltest du nach 1-5 Versuchen 
einen "schlechten" Lauf sehen. Ich drücke dir die Daumen :)

Original comment by felix@familie-freiberger.net on 5 Jul 2012 at 9:33

[GoogleCodeExporter]

Ein ähnliches Problem hatte ich auch. Hast du schon Bonus2 implementiert? Wenn 
ja kommentiere die entsprechenden Zeilen in DPLL mal aus. Falls nicht 
kommentiere auch mal die  Zeilen zum Pure-Literal in DPLL aus. 
Bei mir lag das Problem daran, dass zwar (~a) ein Pure-Literal war, isPure() 
aber auch bei (a) angesprungen ist. Je nachdem, was im Set vorher kam, kam dann 
ein anderes Ergebnis raus. 
Vielleicht ist dein Problem ja ähnlich. 

Original comment by rothe...@gmx.de on 5 Jul 2012 at 11:59

[GoogleCodeExporter]

> Falls nicht kommentiere auch mal die Zeilen zum Pure-Literal in DPLL aus.
Meinst du damit die Unit-Clause-Eliminierung? Falls nein, schlage ich das 
hiermit vor :)

Original comment by felix@familie-freiberger.net on 6 Jul 2012 at 5:34

[GoogleCodeExporter]

[deleted comment]

[GoogleCodeExporter]

Ich hab die Unit Clause jetzt entfernt und das Nicht-Determinismus Problem 
scheint dort zu liegen. 
Der Test für a ! läuft immer durch, aber von den anderen failen konstant 
132861 der tests.

Mal eine Verständnisfrage zur UnitClause: Soll er pro Iteration nur eine 
UnitClause erfüllen oder alle? Das wird mir nicht ganz klar. Im Pseudo Code 
steht zwar "Wenn" (Zeile 177) aber im Beispiel 3.2 klingt das ganze für mich 
so das ALLE erfüllt werden sollen.

Die Version von gestern abend, besteht bei den Nightlys auch fast alle für 
Sat. Aber das ist wahscheinlich einfach nur Glück gewesen :D

Original comment by sebastia...@gmail.com on 6 Jul 2012 at 10:27

[GoogleCodeExporter]

Pro Schritt wird eine (oder keine) Unit-Clause erfüllt.

Original comment by felix@familie-freiberger.net on 6 Jul 2012 at 10:36

[GoogleCodeExporter]

Okay das Problem ist, dass getUnitClauseLiteral aus Cnf ein beliebiges Literal 
liefert. 
Folgendes Beispiel:
(a \/ ~x1) /\ (b \/ ~x1) /\ (x1 \/ ~a \/ ~b) /\ (x1)

Der Algorithmus wählt x1 und a korrekt als true und legt x1 IMPLIED und a 
CHOSEN auf den stack.

Jetzt ist das Problem ob getUnitClauseLiteral das b aus der zweiten oder 
dritten Klausel liefert. Falls es die zweite ist, setzt chooseSatisfyAssignment 
b korrekt auf true und alles stimmt. Wenn es das b aus der dritten Klausel ist 
wird b auf false gesetzt. Dadurch geht der Algorithmus im nächsten Schritt in 
die Rücksetzung des Stacks und das unglück nimmt seinen Lauf.

Ich könnte b auch einfach nur als Chosen auf den Stack legen, aber das würde 
ja nicht mit der Spezifikation aus der pdf übereinstimmen. 
Kann mir jemand einen Tipp geben? 

Original comment by sebastia...@gmail.com on 6 Jul 2012 at 11:26

[GoogleCodeExporter]

Da zum genannten Zeitpunkt x1 = TRUE gewählt ist, hat die Klausel (x1 \/ ~a \/ 
~b) schon den Wert TRUE und ist damit nach Zeile 147 der Spezifikation keine 
Unit-Klausel.

Original comment by felix@familie-freiberger.net on 6 Jul 2012 at 11:34

[GoogleCodeExporter]

Ich habe den SpecificationComplianceFelixTest geupdated, so dass dieser Fehler 
in Zukunft erkannt wird.

Original comment by felix@familie-freiberger.net on 6 Jul 2012 at 12:08

[GoogleCodeExporter]

Es klappt jetzt! Vielen Dank!

Original comment by sebastia...@gmail.com on 6 Jul 2012 at 12:15

[GoogleCodeExporter]

Wunderbar, ich schließe dann mal das Ticket. Wenn du noch Fragen hast, kannst 
du gerne ein neues Ticket anlegen.

Original comment by felix@familie-freiberger.net on 6 Jul 2012 at 12:22

• Changed state: Added