KNF lösbar wenn Variablen-2-Tupel bekannt?

Servus Freunde!

Ich habe eine KNF (konjunktive Normalform), also eine Verundung von veroderten Variablen.

Beispiel:

(x1 | x2 | x3) & (x4 | x5 | x6) & (x7 | x8 | x9)

Ich habe außerdem die Möglichkeit der Kombinationen
aller Variablen aus verschiedenen UND-Termen gegeben
(siehe Beispiel das folgt):

x1 & x4 = false
x1 & x5 = true
x1 & x6 = true

x1 & x7 = true
x1 & x8 = true
x1 & x9 = false

x4 & x7 = true
x4 & x8 = false
x4 & x9 = true

x5 & x7 = true

… (das gleiche noch weiter und dann mit x2, x3 am Anfang)

Ich habe also Folgendes gegeben:

FOR quelle = UND-Term_1 TO UND_Term_n-1
FOR ziel = UND-Term_quelle+1 TO UND-Term_n
KombinationMöglich(quelle, ziel) = … (das ist jeweils gegeben)

FRAGE:
Kann ich nur mit dem 2-dimensionalen Datenfeld (oder der Menge mit 2 Indices, wenn man es mathematisch ausdrücken will)

„KombinationMöglich(quell_UND-Term, ziel_UND-Term)“

sagen, ob die KNF lösbar ist, oder nicht?

Beispiel:

x1 & x4 = false
x1 & x5 = true

Hallo,

du hast ja somit jede Mögliche 2er-Kombination. Damit kannst du die Lösbarkeit der KNF natürlich bestimmen. Du kannst wahrscheinlich direkt sagen, welche Variablen welche Werte haben - da bin ich mir aber nicht ganz sicher.
Betrachten wir einmal zwei gegebene Formeln mit ihren Werten:
xn & xm = y1
xm & xo = y2
Daraus können wir ja durch &-Verknüpfung zu folgender Formel kommen:
xn & xm & xo = y1 & y2
Nun können mir n, m und o so wählen, dass xn im ersten Konjunkt, xm im zweiten und xo im dritten liegt.
Die Konjunktion ist nur dann erfüllt, wenn alle Konjunkte wahr sind. Eine Disjunktion (also die Konjunkte) ist dann erfüllt, wenn mindestens eines der Disjunkte wahr ist.
Also suchen wir Formeln mit y1 & y2 = wahr, also y1 = wahr und y2 = wahr.
Gibt es unter diesen Formeln einige, für die die oben genannte Einschränkung für n, m und o gilt, so ist die Formel in KNF erfüllbar, andernfalls nicht.

Nico

Vielen Dank Nico, das ist eigentlich ein schöner Beweis, dass man das Problem lösen KANN.

Ich habe aber leider vergessen zu sagen, dass ich das Problem SCHNELL lösen muss.

Also wenn ich z.B. die folgende KNF habe:

(x1|x2|x3|x4|x5|x6)&(x7|x8|x9|x10|x11|x12)&(x13|x14|x15|x16|x17|x18)&…

Nehemen wir an, die Kombinationen in den ersten 99 UND-Terme sind
alle Möglich (wahr), und im sagen wir 100. Term (oder 65. oder 78. …) ‚fällt die Entscheidung‘.

Muss ich dann nicht im ungünstigsten Fall 99^7 oder so ähnlich Möglichkeiten durchprobieren?

Das ist praktisch nicht durchführbar.

Ich hoffe du verstehst, was ich meine. Ist es SCHNELL (nicht x^[Anzahl der UND-Terme] sondern [Anzahl der UND-Terme]^x) überprüfbar, ob die KNF lösbar ist, wenn ich alle 2-er Tupel habe?

Danke nochmal und Gruß,

Rainer

(x1|x2|x3|x4|x5|x6)&(x7|x8|x9|x10|x11|x12)&(x13|x14|x15|x16|x17
|x18)&…

Muss ich dann nicht im ungünstigsten Fall 99^7 oder so ähnlich
Möglichkeiten durchprobieren?

Ich meinte natürlich 99^6, Entschuldigung!
99 Terme, in denen ich alle 6 Variablen ‚gegeneinander‘ testen muss, in allen Kombinationen.

Eventuell wird es ja vielleicht gar nicht so viel.
Du musst ja letztendlich nur die Formeln überprüfen, die wahr sind. Dann könntest du dich auch baumartig von Konjunkt zu Konjunkt hangeln und prüfen, ob du bis zum Schluss kommst. Wenn es nicht mehr weiter geht eben einen Schritt zurück (-> Backtracking).
Allerdings musst du dann im Falle der Nicht-Erfüllbarkeit wirklich jede mögliche Kombination überprüfen. Aber je mehr wahre Formeln du hast, desto höher ist die Wahrscheinlichkeit, dass die Gesamtformel wahr wird und das möglichst früh erkannt wird. Wenn du nur wenige wahre Formeln hast, musst du auch nicht so viel überprüfen. Das ganze kann auch sehr schön parallel ausgeführt werden (sofern man einen Rechner hat und das nicht per Hand berechnen will).
Eine andere Möglichkeit wäre, vorher die Gesamtformel zu modifizieren und Resolventen abzuleiten (->Resolutionsverfahren). Dann findest du vielleicht schon eine Resolvente, die deinen gegebenen Formeln widerspricht. Das ist aber wohl eher Glück und das Verfahren hat auch eine ziemlich hohe Komplexität.
Ich würde es erst mal ausprobieren. Vielleicht dauert es ja gar nicht so lange wie du befürchtest.

Nico

Hi

Ist es SCHNELL (nicht
x^[Anzahl der UND-Terme] sondern [Anzahl der UND-Terme]^x)
überprüfbar, ob die KNF lösbar ist, wenn ich alle 2-er Tupel
habe?

Wenn Du wirklich alle Paare hast, dann ja.

Alle ‚Wahren‘ Paare zusammen liefern genau die und nur die Variablen, die mit ‚Wahr‘ belegt sind. Alle anderen Variablen sind ‚Falsch‘. Anschließend sukzessives Abhaken der einzelnen Glieder der Konjunktion.

Aber, wie gesagt, es müssen alle Paare gegeben sein.

Gruß,
KHK

Danke für alle Antworten.

Ich muss sicher sein, dass es in polynomialer Zeit geht. Also alles durchprobieren bei Nichterfüllbarkeit ist nicht möglich.

Aber, ich HABE ALLE (!) Paare. Wirklich alle.

Kannst Du mir bitte einen Algorithmus beschreiben (Pseudo-Code, und/oder mit einfachem Beispiel bitte), der das macht, was Du meinst?

Ich verstehe bis jetzt nicht, wie das gehen soll.

Wie gesagt, ich habe alle Paare.

Danke und Gruß an alle,

Rainer

Hallo Rainer,

ich kann mich mittlerweile auch ruhigen Gewissens der Meinung von KHK anschließen. Also dass man aus den Tupeln auf die Belegung jeder Variablen schließen kann. Außer wenn alle wahren Variablen nur in einem Konjunkt vorkommen. Aber dann ist die Formel in KNF sowieso nicht wahr.
Nun zum Vorgehen:
Lege eine Menge an, in der alle Variablen sind, die wahr sein müssen:

  • Für jede Formel xn & xm = wahr füge xn und xm der Menge hinzu
    Jetzt könntest du schon einfach durch Einsetzen der Belegung prüfen, ob die KNF-Formel wahr wird. Oder du prüfst das noch separat. Dabei entsteht aber schnell wieder eine hohe Komplexität:
  • für jedes Konkunkt xn | xm | … | xo prüfe ob sich eines der Disjunkte in der erstellten Menge befindet.
    Das sollte es eigentlich gewesen sein. Es sei denn, es gibt noch eine weitere Ausnahme, die ich übersehen habe.

Nico

Also zum Beispiel so?

Gegebene KNF:

(1|2|3)&(4|5|6)&(7|8|9)

Tupel, die wahre Belegungen anzeigen:

1-4
1-5
1-6

2-4
2-6
2-7
2-8

3-4

1-7
1-8

5-9

Ich füge alle vorkommenden Variablen hinzu:

1,2,3,4,5,6,7,8,9

Super, lösbar!

Oder doch nicht?

Es gibt zwar 5-9, aber nicht 1-5 UND 1-9. Mit 2 am Anfang geht’s auch nicht.

Das heißt, dieser Algorithmus, den ich gerade angewandt habe (einfach alle vorkommenden Variablen aus wahren Konjungten der Lösungsmenge hinzufügen, und sehen, ob aus jedem UND-Term mindesten eine Variable vorkommt), funktioniert NICHT.

Hast du das so gemeint?

Kannst du mir bitte ein Beispiel geben (am besten deinen gemeinten Algorithmus auf das Beispiel oben anwenden).

Übrigens, die KNF oben ist NICHT lösbar mit diesen Konjungten.

Danke und Gruß,

Rainer

Tupel, die wahre Belegungen anzeigen:

1-4
1-5
1-6

2-4
2-6
2-7
2-8

3-4

1-7
1-8

5-9

Diese Aufzählung ist NICHT vollständig. Die UND-Verknüpfung ist Kommutativ, Assoziativ und Transitiv. Wenn die Paare 1-5 und 5-9 ‚Wahr‘ sind, muss auch 1-9 ‚Wahr‘ sein.

Mit den von Dir genannten Paaren sind tatsächlich alle 9 Variablen ‚Wahr‘, und die KNF ist erfüllt.

Gruß,
KHK

Tupel, die wahre Belegungen anzeigen:

1-4
1-5
1-6

2-4
2-6
2-7
2-8

3-4

1-7
1-8

5-9

Diese Aufzählung ist NICHT vollständig. Die UND-Verknüpfung
ist Kommutativ, Assoziativ und Transitiv. Wenn die Paare 1-5
und 5-9 ‚Wahr‘ sind, muss auch 1-9 ‚Wahr‘ sein.

Genau DAS ist mein Problem!

Ich muss feststellen, ob die „Aufzählung vollständig“ ist oder nicht.

Es können solche AUfzählungen wie das Beispiel oben auftauchen.

Dann soll der gesuchte Algorithmus „nicht lösbar“ (o.ä.) ausgeben.

Wie kann ich feststellen, dass diese Aufzählung die KNF nicht löst?

Wichtig: geht das in Polynomzeit oder ist es wieder einmal ein NP-vollständiges Problem, wie so viele Probleme, bei denen man mit der dummen Methode alle Kombinationen durchprobieren muss???

Any ideas?

Danke schon mal !!!

Euer Rainer