Ist es überhaupt effizient möglich, eine größere KNF in eine DNF umzuwandeln? Wenn ich eine Formel umforme und dann ein Konstrukt wie das hier

[(A ^ ¬B) v (C ^ ¬D) v (E ^ ¬F) v (G ^ ¬F) v (I ^ ¬F) v (A ^ ¬C) v (¬G ^ ¬A) v (¬J ^ F) v (¬D ^ ¬C)] ^ (¬A v B v ¬C)

bekomme, ich also eine DNF will, und eine (lange DNF)^(kurze KNF) habe, was muss ich dann machen? Wahrheitstafeln kann ich bei 4 und mehr atomaren Formeln ja leider vergessen.

So wie ich das verstanden habe, muss ich alle Formeln der Form ((F v G) ^ H) zu ((F ^ H) v (G ^ H)) umwandeln.

Wenn ich das richtig verstanden habe, dann wird also

[(A ^ ¬B) v (C ^ ¬D) v …] ^ (¬A v B v ¬C)

zu

((A ^ ¬B) ^ (¬A v B v ¬C)) v
((C ^ ¬D) ^ (¬A v B v ¬C)) v …

und daraus wiederum wird

((A ^ ¬B ^ ¬A) v (A ^ ¬B ^ B) v (A ^ ¬B ^ ¬C)) v
((C ^ ¬D ^ ¬A) v (C ^ ¬D ^ B) v (C ^ ¬D ^ ¬C)) v …

, wobei sich manches wegkürzt und

(A ^ ¬B ^ ¬C) v
(C ^ ¬D ^ ¬A) v (C ^ ¬D ^ B) v …

übrig bleibt.

Das alles zu rechnen ist allerdings ewig aufwendig und wenn man Schritte abkürzt, macht man Rechenfehler.

Gibt es da noch irgendeine unglaublich einfache Methode mit der ich das lösen kann und die ich bisher einfach übersehen habe? Oder bin ich dazu verdammt das alles per Hand auszurechnen?

Meines Wissens gibt es keine.

MfG
Xoc