Erfüllbarkeitsproblem
-
Das Erfüllbarkeitsproblem ist offensichtlich leicht zu lösen, wenn die aussagenlogische Formel in DNF vorliegt. Dann kann man die Lösungen ja direkt ablesen, bzw. jede Formel in DNF ist erfüllbar, wenn da nicht sowas steht wie "x && !x".
Sehe ich es richtig, dass das Problem dann ist, eine Formel in Polynomialzeit von DNF in KNF umzuwandeln?
-
Hab mich verschrieben. Meinte natürlich:
"von KNF in DNF"
-
zum genannten Problem
KNF: SAT (Erfüllbarkeit)
gibt es das entsprechende Problem
DNF: TAUT (entscheide, ob die Formel für alle Belegungen wahr ist)
- dürfte beides NP-vollständig sein, wenn ich mich richtig erinnere.
-
"TAUT" steht für "Tautologie"- klar, ne.
-
Kuwe schrieb:
Das Erfüllbarkeitsproblem ist offensichtlich leicht zu lösen, wenn die aussagenlogische Formel in DNF vorliegt. Dann kann man die Lösungen ja direkt ablesen, bzw. jede Formel in DNF ist erfüllbar, wenn da nicht sowas steht wie "x && !x".
Sehe ich es richtig, dass das Problem dann ist, eine Formel in Polynomialzeit von DNF in KNF umzuwandeln?Es ist nicht schwer zu beweisen, dass manche KNF-Formeln exponentiell aufgeblasen werden müssen, um sie in DNF umzuwandeln. Das heißt, jeder Algorithmus, der KNF nach DNF umwandelt, hat automatisch exponentielle Laufzeit auf bestimmten Formeln.
Das zeigt aber noch lange nicht, dass das Erfüllbarkeitsproblem zwangsläufig exponentielle Laufzeit hat. Nur der Ansatz "KNF -> DNF -> ablesen" hat exponentielle Laufzeit. Vielleicht gibt es ja auch effizientere Methoden, aus der KNF-Form die Erfüllbarkeit abzulesen.