Diskussion:Einheitsresolution

Letzter Kommentar: vor 10 Jahren von 91.32.105.229 in Abschnitt Verlinkung

Einheitsresolution Bearbeiten

Verschoben von Benutzer Diskussion:Quartl. --Quartl (Diskussion) 18:18, 26. Nov. 2012 (CET)Beantworten

Hi,

wieso bist du der Meinung, dass die Klausel, die nur aus einem Literal besteht erhalten bleiben muss? Könntest du das belegen? So wie ich die Regeln kenne, sind sie eigentlich eindeutig und können nicht so interpretiert werden, wie du es gemacht hast...

Edit: Ich kenne es wirklich nur so, dass bei der unit propagation eine Einheitsklausel ausgewählt wird, mit welcher dann die unit propagation durchgeführt wird, um die Klauselmenge zu vereinfachen. Dabei verringert sich immer die Anzahl der Klauseln in der Klauselmenge und insbesondere die Einheitsklausel wird dabei aus der Klauselmenge entfernt. Das muss auch so sein, da sonst z.B. der DPLL-Algorithmus nicht terminieren würde.

Edit2: Hmm ich habe mal hier geschaut: http://en.wikipedia.org/wiki/Talk:Unit_propagation Das scheint wohl nicht immer ganz eindeutig zu sein. Die Erklärung, warum man es auch so interpretieren kann, wie du es gemacht hast, verstehe ich im englischen Artikel nicht so genau. Vor allem Würde aus meiner Sicht der DPLL-Algorithmus so nicht terminieren, weil er das eben nur dann tut, wenn die Klauselmenge schlussendlich leer ist.

Grüße, -- Slllu (Diskussion) 23:35, 25. Nov. 2012 (CET)Beantworten

Ich habe nochmal in ein paar Büchern nachgelesen. Man muss zwischen unit propagation und unit resolution unterscheiden. Tatsächlich wird bei unit resolution das Literal entfernt. Der Artikel en:Unit propagation betrachtet in seinem Beispiel nur unit propagation, bei der eine Klauselmenge vereinfacht werden soll, ohne deren Wahrheitsgehalt zu verändern (this would make the resulting set not equivalent to the original one). Auf unit resolution wird dann im folgenden Abschnitt en:Unit propagation#Unit propagation and resolution eingegangen, allerdings ohne Beispiel. Vielleicht sollte man auf diesen Unterschied in Einheitsresolution auch hinweisen. Oder (evtl. noch besser) einen eigenen Artikel zum DPLL-Algorithmus (vgl. en:DPLL algorithm) schreiben. Grüße, --Quartl (Diskussion) 06:29, 26. Nov. 2012 (CET)Beantworten
Den Artikel zum DPLL-Algorithmus wollte ich schon länger einmal schreiben... Leider habe ich gerade sehr wenig Zeit. Vlt. könnten wir diese Diskussion auf die Diskussionsseite des Artikels verschieben? Wenn ich dann dazu komme, würde ich wieder daran arbeiten und mich den genannten Punkten annehmen. -- Slllu (Diskussion) 15:37, 26. Nov. 2012 (CET)Beantworten

Verlinkung Bearbeiten

Hallo, der Artikel wird als deutsche Version des Artikels "unit propagation" angezeigt. Das ist mehr als Verwirrend, da es sich ja um zwei verschiedene Algorithmen handelt. Gruß --Ashcase (nicht signierter Beitrag von 91.32.105.229 (Diskussion) 18:36, 8. Aug. 2013 (CEST))Beantworten