H 3.2

eesti
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 116
Registriert: 6. Okt 2008 20:59
Wohnort: Darmstadt

H 3.2

Beitrag von eesti »

ich bin gerade dabei zu überlegen, wo der widerspruch auftritt, also wo ich sehen kann, dass die Formelmenge nicht erfüllbar ist.
Dabei bedeutet:
F1: Transitivität
F2: wenn eine kante(Relation) von x nach y existiert, wird x gefärbt (P) und y nicht.

P
c -> fc -> ffc -> fffc -> ...
x......y
Jetzt gehe ich einen Schritt weiter und nehme mein voriges y als x
Dann ist aber die Funtkion für c schon nicht mehr gültig, da ja jetzt fc gefärbt ist.

P......P.....
c -> fc -> ffc -> fffc -> ...
........x......y..

aber zwei funktionen müssten doch erfüllbar sein??!!

Benutzeravatar
John
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 167
Registriert: 12. Dez 2008 17:41
Wohnort: E-Pool

Re: H 3.2

Beitrag von John »

eesti hat geschrieben: F2: wenn eine kante(Relation) von x nach y existiert, wird x gefärbt (P) und y nicht.
Nein, dort steht: Wenn eine Kante von x nach y existiert, ist x gefärbt gdw. y nicht gefärbt ist.
Es gilt nämlich: \((a \leftrightarrow b) \neq (a \wedge b)\)
Die Formel soll also heißen: Wenn a gefärbt ist, ist b nicht gefärbt, und wenn a nicht gefärbt ist, ist b gefärbt.

Aber ich muss hier auch noch meinen Senf dazu geben: Nun beschreibt ja \(\varphi_1\) die Reflexivität der Relation \(Rxy\), und \(\varphi_2\) sagt aus, dass wenn \(Rxy\) gilt, dann ist \(x\) gefärbt gdw. \(y\) nicht gefärbt ist.

Sei folgendes gebilde mein konstruierter "Graph":
\(c \rightarrow fc \rightarrow ffc\)
Hier steht \(c\) auch mit \(ffc\) in Relation, aufgrund \(\varphi_1\). Da aber schon \(fc\) mit \(ffc\) in Relation steht, muss \(ffc\) gleichzeitig gefärbt und nicht gefärbt sein (da \(Pc \leftrightarrow \neg Pfc\)), was ein Widerspruch ist. Aber alle Formeln sollen doch paarweise erfüllbar sein?
DON'T PANIC

Benutzeravatar
John
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 167
Registriert: 12. Dez 2008 17:41
Wohnort: E-Pool

Re: H 3.2

Beitrag von John »

Ah, da kommt mir eine Idee. Erst \(\varphi_3\) sagt ja aus, dass jeder Knoten auch mit einem anderen Knoten in Relation steht, was heißt, dass \(\varphi_1\) und \(\varphi_2\) zusammen zwar erfüllbar sind, aber nur mit \(R = \emptyset\).
DON'T PANIC

mister_tt
Kernelcompilierer
Kernelcompilierer
Beiträge: 502
Registriert: 29. Sep 2008 15:54

Re: H 3.2

Beitrag von mister_tt »

Ich hab da noch ein ganz anderes Problem... Was macht ihr denn bei der Resolution aus dem \(\leftrightarrow\) ? Klar kann man \(\phi \leftrightarrow \psi\) auflösen als \((\phi \rightarrow \psi) \land (\psi \rightarrow \phi)\), nur daraus wird dann \((\neg \phi \lor \psi) \land (\neg \psi \lor \phi)\) und mit dem \(\land\) komme ich dann nicht klar... Würde ja wie in Übung 6 dann zwei Klauseln drauß machen, allerdings hat man vor dieser \(\land\)-Beziehung ja auch noch ein \(\lor\) stehen... Wie kriegt man das dann in den Griff?

quanz
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 103
Registriert: 1. Okt 2007 19:32

Re: H 3.2

Beitrag von quanz »

mister_tt hat geschrieben:Ich hab da noch ein ganz anderes Problem... Was macht ihr denn bei der Resolution aus dem \(\leftrightarrow\) ? Klar kann man \(\phi \leftrightarrow \psi\) auflösen als \((\phi \rightarrow \psi) \land (\psi \rightarrow \phi)\), nur daraus wird dann \((\neg \phi \lor \psi) \land (\neg \psi \lor \phi)\) und mit dem \(\land\) komme ich dann nicht klar... Würde ja wie in Übung 6 dann zwei Klauseln drauß machen, allerdings hat man vor dieser \(\land\)-Beziehung ja auch noch ein \(\lor\) stehen... Wie kriegt man das dann in den Griff?
Mal anders gefragt, wie kann man (a+b) * (c+d) noch äquivalent umschreiben.

mister_tt
Kernelcompilierer
Kernelcompilierer
Beiträge: 502
Registriert: 29. Sep 2008 15:54

Re: H 3.2

Beitrag von mister_tt »

Danke für deine Antwort.

(a+b)*(c+d) = a*c + a*d + b*c + b*d
Das löst das Problem aber leider nicht. Bezogen auf mein Problem steht dann da:
\(X \lor (\neg \phi \land \neg \psi) \lor (\phi \land \psi)\) Daraus kriege ich aber immer noch keine Klausel, da in meiner Disjunktion Konjunktionen vorkommen... :?

quanz
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 103
Registriert: 1. Okt 2007 19:32

Re: H 3.2

Beitrag von quanz »

mister_tt hat geschrieben:Danke für deine Antwort.

(a+b)*(c+d) = a*c + a*d + b*c + b*d
Das löst das Problem aber leider nicht. Bezogen auf mein Problem steht dann da:
\(X \lor (\neg \phi \land \neg \psi) \lor (\phi \land \psi)\) Daraus kriege ich aber immer noch keine Klausel, da in meiner Disjunktion Konjunktionen vorkommen... :?
Wenn ich mich nicht irre steht, da ja sowas: \(X \lor ((\neg \phi \lor \neg \psi) \land (\phi \lor \psi))\)
Das kann man doch so umschreiben.

mister_tt
Kernelcompilierer
Kernelcompilierer
Beiträge: 502
Registriert: 29. Sep 2008 15:54

Re: H 3.2

Beitrag von mister_tt »

Und wie soll ich das bitte in eine Klausel packen? Eine Klausel ist nach Definition ja eine endliche Menge von Literalen, wobei Literale atomare oder negiert atomare Formeln sind... \((\neg \phi \lor \neg \psi) \land (\phi \lor \psi)\) ist aber doch keine atomare Formel... :?

quanz
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 103
Registriert: 1. Okt 2007 19:32

Re: H 3.2

Beitrag von quanz »

mister_tt hat geschrieben:Und wie soll ich das bitte in eine Klausel packen? Eine Klausel ist nach Definition ja eine endliche Menge von Literalen, wobei Literale atomare oder negiert atomare Formeln sind... \((\neg \phi \lor \neg \psi) \land (\phi \lor \psi)\) ist aber doch keine atomare Formel... :?
Die Definition ist schon richtig.
Klauseln sehen so aus: \(\{\neg \phi_1, \neg \psi_1, \phi_2 \psi_2\}\)

Ich habe nie behauptet, dass das hier \(X \lor ((\neg \phi \lor \neg \psi) \land (\phi \lor \psi))\) eine Klausel ist.
Ich sage nur, dass man daraus Klauseln erstellen kann. Ich sehe da zwei Stück.

mister_tt
Kernelcompilierer
Kernelcompilierer
Beiträge: 502
Registriert: 29. Sep 2008 15:54

Re: H 3.2

Beitrag von mister_tt »

Ja ok, das oder davor kann man da rein ziehen und dann hat man zwei Klauseln... Danke für deine Hilfe!

Antworten

Zurück zu „Archiv“