Aussagenlogik #18 - Horn-SAT
Vložit
- čas přidán 18. 08. 2024
- iltis.cs.tu-do...
Wir lernen den eine eingeschränkte Art von aussagenlogischen Formeln kennen, die sogenannten Horn-Formeln. Das Erfüllbarkeitsproblem für Horn-Formeln (Horn-SAT) ist effizient lösbar, und zwar durch den sogenannten Markierungsalgorithmus.
Die besten Erklärungen zum Thema!
Hätte dich früher entdeckt!! Perfekt erklärt, vielen dank
ich groove hier viel zu hart zu dieser musik
Rettest mir die Klausur danke:)
Sehr verständlich erklärt.
Thank you very much!
Top, danke.
Wie fange ich denn an, wenn ich kein alleinstehendes Literal was wahr sein muss habe? Oder ist es dann einfach nicht möglich?
Wenn es kein solches Literal gibt, dann ist die Formel immer erfüllbar. Man setzt einfach alle Variablen auf false.
Danke für die schnelle Antwort❤ @@NLogSpace
Nehmen wir mal an, in einer Klausel kommen 2 positive Literale B und C, und ein negatives Literal nA vor (n soll für "nicht" stehen). Also wäre die Klausel dann (nA v B v C). Dies wäre ja keine Horn-Formel mehr. Aber könnten wir nicht eine neue Variable nD=B definieren und dies als Klausel hinzufügen? Dann würde aus (nA v B v C)(nA v nD v C)^(nDB).
Dies könnte man doch rein theoretisch auch bei anderen Formeln machen: Z.B.
(nA v B v C)^(nB v A)^(nA v nC v D) könnte man mit nE:=B umformen zu (nA v nE v C)^(nB v A)^(nA v nC v D) ^ (nEB)
Den ersten Teil könnten wir nun überprüfen. Wenn es keine Lösung gibt, also auch nicht mit der viel allgemeineren Formel mit E, dann gibt es auch keine Lösung für die Grundgleichung.
Wenn aber unser erster Teil (nA v nE v C)^(nB v A)^(nA v nC v D) eine Lösung besitzt, müssten wir nur noch schauen, ob auch die letzte Bedingung (nEB) gilt.
Gibt es einen derartigen Algorithmus?
Sehr schöne Idee, allerdings sehe ich noch ein kleines Problem: Die Formel nDB ist auch keine erlaubte Klausel in einer Horn-Formel, da es keine Disjunktion von Literalen ist. Wenn man es umschreibt, dann wird das zu (nD v nB) ^ (D v B), und da haben wir leider wieder zwei positive Literale in einer Klausel. Man kann die Idee trotzdem benutzen: Anstatt eine zusätzliche Variable einzuführen, negieren wir einfach jedes Vorkommen von B in der gesamten Formel. Das ist eine erfüllbarkeitsäquivalente Umformung.
Ich kenne jedoch keinen Algorithmus, der diesen Trick benutzt.