testBonus2SpecificationCompliance ist falsch

[GoogleCodeExporter]

Nach der Spezifikation steht da:
"Um ein Pure-Literal zu finden, untersucht man für jede Variable die Klauseln, 
in denen die Variable vorkommt und deren Wahrheitswert noch nicht feststeht. "
Das heißt, dass bei    
Cnf cnf = TestUtilFelix.parseCompactCnfString("a-b"); 
cnf.getVariableForName("a").setTruthValue(TruthValue.TRUE); cnf.getVariableForNa
me("b").setTruthValue(TruthValue.UNDEFINED);

null zurueckgegeben wird, da die klausel schon einen wahrheitswert hat.

Original issue reported on code.google.com by philolog...@gmail.com on 10 Jul 2012 at 6:53

[GoogleCodeExporter]

ok, ich schaue mir das mal im forum an.

Original comment by philolog...@gmail.com on 10 Jul 2012 at 6:58

[GoogleCodeExporter]

mal sehen, was die zu dem Textbeweis antworten.
https://forum.st.cs.uni-saarland.de/boards/viewthread?thread=1535&lastpage=yes#8
560

Original comment by philolog...@gmail.com on 10 Jul 2012 at 7:03

[GoogleCodeExporter]

"Um ein Pure-Literal zu finden, untersucht man für jede Variable die Klauseln, 
in denen die Variable vorkommt und deren Wahrheitswert noch nicht feststeht. 
Kommt eine unbelegte Variable [b ist unbelegt] in diesen Klauseln [es gibt 
keine solchen Klauseln] auschließlich nicht-negiert vor [...] ist die Variable 
ein (positives) Pure-Literal."

Als musst du b zurückgeben.

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

[GoogleCodeExporter]

Nach meiner Logik aber, "Um ein Pure-Literal zu finden, untersucht man für 
jede Variable die Klauseln, in denen die Variable vorkommt und deren 
Wahrheitswert noch nicht feststeht" Es gibt keine, also untersucht man keine. 
Nach deiner Logik ist doch dann aber auch !b ein PureLiteral, fuer mich macht 
das keinen Sinn...

Original comment by philolog...@gmail.com on 10 Jul 2012 at 7:36

[GoogleCodeExporter]

Außerdem ist b nicht element der leeren Menge (denn es gibt ja keine Klauseln, 
wie du selbst sagst).

Original comment by philolog...@gmail.com on 10 Jul 2012 at 7:38

[GoogleCodeExporter]

!b kann kein Pure Literal sein, denn es kommt ja nirgends vor.
Tobias hat diese Auslegung in diesem Thread ja auch explizit bestätigt.

b ist kein Element der leeren Menge, das war aber auch nie gefordert. Es heißt 
nur:

Für alle Variablen:
  Ist nicht unbelegt -> nächste probieren
  Untersuche alle Klauseln mit Variable und Wahrheitswert UNDEFINED
    Wenn die Variable negiert vorkommt -> nächste Variable probieren
  Alle Klauseln untersucht -> gibt als positives Pure Literal zurück

Beachte, dass das Quantifizierungen über die leere Menge sind. Folgende 
Aussage ist mathematisch korrekt:
Für alle x aus der Menge {} gilt: 1 = 2

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

[GoogleCodeExporter]

Was ich noch anmerken wollte:
Der Pseudocode von mir sagt nur, was die Spezifikation hier meint. Du musst das 
natürlich nicht so implementieren, da die vorgegebenen Methode (wie z.B. 
isPure) da natürlich einen anderen Weg nahelegen.

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

[GoogleCodeExporter]

Ich denke schon, dass ich das programmieren kann, ist ja nicht der Aufwand, 
wenn man das beispielsweise mit AlgEng vergleicht. Naja, trotzdem ein bisschen 
unsinnig das alles. I would rather live in a more free world. 
thanks anyway.

Original comment by philolog...@gmail.com on 10 Jul 2012 at 12:28

[GoogleCodeExporter]

...das kannst du machen, da du aber die ganzen isPure(), isPurePositive usw. 
auch implementieren musst, musst du dann doppelt arbeiten. Es empfiehlt sich 
deshalb schon dringend, den vorgesehenen Weg auch zu nutzen.

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

[GoogleCodeExporter]

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

• Changed state: NoReply