DNF vs KNF



  • Hallo zusammen,

    kann mir jemand sagen, warum in der Praxis die DNF wichtiger als die KNF ist? Ich glaube es hat etwas mit den meist weniger vorkommenden ODER - Verknüpfungen, die aus irgendeinem Grund nicht so beliebt sind.

    Weiß da jemand Näheres?

    Vielen Dank
    lg, freakC++



  • Weil du relativ leicht überprüfen kannst, ob eine gegebene Variablen-Belegung die Formel erfüllt. Also du kannst die Wahrheitstabelle einfach ablesen.



  • Und für das Resolutions-Kalkül brauchst Du eine KNF.

    Von welcher Praxis ist die Rede?



  • freakC++ schrieb:

    kann mir jemand sagen, warum in der Praxis die DNF wichtiger als die KNF ist?

    Wer behauptet das den?



  • icarus2 schrieb:

    freakC++ schrieb:

    kann mir jemand sagen, warum in der Praxis die DNF wichtiger als die KNF ist?

    Wer behauptet das den?

    Mein Professor!

    Mit Praxis meine ich den Bau einen Chips...

    Viele Grüße



  • Vielleicht sieht man don't care Stellen leichter ...



  • Nun gut, beim Chipbau wuerden mir noch Karnaugh Maps in den Sinn kommen. Diese funktionieren mit KNF Formeln.

    Ausserdem sind die Horn-Formeln, ein Spezialfall der KNF, in gewissen Bereichen nuetzlich.
    Schau dir auch einmal logische Resolution an. Da braucht es auch KNF Formeln.

    *Edit
    Frag doch sonst mal beim Prof oder bei einem Assistenten nach.



  • DNF und KNF sind dual zueinander, alles was mit der einen geht, geht also im Prinzip auch mit der anderen. Beispiel Karnaugh-Maps (die natürlich nicht in der Praxis angewendet werden): Für die DNF fasst man Blöcke aus Einsen zusammen, für die KNF Blöcke aus Nullen.



  • je nach Aufgabenstellung macht es in der Praxis aber einen erheblichen Unterschied.

    KNF => TAUT trivial, aber SAT NP-c
    DNF => SAT trivial, aber TAUT NP-c

    hat man nun in der Praxis ein paar hundert tausend logische Bedingungen gegeben, und soll berechnen, ob es dafür eine Lösung gibt (bspw Zeitpläne aller Art oder Zuweisung von Resourcen), wäre man mit einer DNF fein raus - man hat aber die KNF, und da ist SAT NP-vollständig



  • SAT trivial? Also da DNF und KNF nur Teile der Wahrheitstabelle sind und die moeglichen Belegungen mit der Anzahl der Variablen exponentiell steigen, hat man mit DNF gegenueber KNF bei SAT nichts gewonnen.



  • knivil schrieb:

    SAT trivial?

    Aber ja doch. Selbst das Argument dafür ist trivial, da denkst du besser nochmal kurz drüber nach.



  • Und wie komme ich zu meinem ersten Term? Wenn ich die Loesung kenne, ja, dann ist die Loesung trivial.



  • knivil: Für SAT in DNF reicht es, sich die Monome einzeln anzuschauen, denn wenn eines erfüllbar ist, ist der Gesamtausdruck erfüllbar. Jetzt schaust du dir die Literale eines Monoms der Reihe nach an und gibst deinen Variablen genau die Belegung, die nötig ist, um das Monom zu erfüllen. Kommt es dabei zu Widersprüchen, gehst du zum nächsten Monom.



  • Entsprechend arbeiten SAT-solver auch eher mit KNF Formeln, da man jede beliebige Formel in polynomieller Zeit in eine erfüllbarkeitsäquivalente KNF Formel umwandeln kann (im Gegensatz zu DNF).



  • knivil, kann es sein, dass du den Aufwand zur Aufstellung der DNF mitrechnest? Die Behauptung war nur: Wenn man die DNF hat, ist das Erfüllbarkeitsproblem trivial. Und das ist es in der Tat, die einzige nicht erfüllbare DNF ist false.



  • Bashar schrieb:

    Und das ist es in der Tat, die einzige nicht erfüllbare DNF ist false.

    "(a \land \neg a) \lor (b \land \neg b)" ist auch nicht erfüllbar und in DNF.

    Natürlich ist jede nicht erfüllbare DNF Formel äquivalent zu "false", aber das gilt (per Definition) auch für jede andere nicht erfüllbare Formel. 😉



  • life schrieb:

    Bashar schrieb:

    Und das ist es in der Tat, die einzige nicht erfüllbare DNF ist false.

    "(a \land \neg a) \vee (b \land \neg b)" ist auch nicht erfüllbar und in DNF.

    Natürlich ist jede nicht erfüllbare DNF Formel äquivalent zu "false", aber das gilt (per Definition) auch für jede andere nicht erfüllbare Formel. 😉

    Je nach Definition... Wenn man sagt, dass eine Variable in einer Klausel nur einmal vorkommen darf geht das nicht mehr.



  • Ausschnitt aus wikipedia

    ... A DNF formula is in full disjunctive normal form if each of its variables appears exactly once in every clause. ...



  • full disjunctive normal form != disjunctive normal form



  • SG1 schrieb:

    full disjunctive normal form != disjunctive normal form

    Wohl war... Aber trotzdem witzlos bei der DNF zwei Literale in einer Klausel zuzulassen.



  • zwei gleiche meine ich.


Anmelden zum Antworten