Horn-Erfüllbarkeit - Horn-satisfiability

In der formalen Logik ist Horn-Erfüllbarkeit oder HORNSAT das Problem der Entscheidung, ob eine gegebene Menge von propositionalen Horn-Klauseln erfüllbar ist oder nicht. Horn-Erfüllbarkeit und Horn-Klauseln sind nach Alfred Horn benannt .

Grundlegende Definitionen und Terminologie

Eine Horn-Klausel ist eine Klausel mit höchstens einem positiven Literal , dem so genannten Kopf der Klausel, und einer beliebigen Anzahl negativer Literale, die den Körper der Klausel bilden. Eine Horn-Formel ist eine propositionale Formel, die durch die Konjunktion von Horn-Klauseln gebildet wird.

Das Problem der Hornerfüllbarkeit ist in linearer Zeit lösbar . Das Problem der Wahrheitsentscheidung quantifizierter Hornformeln kann auch in polynomieller Zeit gelöst werden. Ein Polynomialzeitalgorithmus für die Hornerfüllbarkeit basiert auf der Regel der Einheitsausbreitung : Wenn die Formel eine Klausel enthält, die aus einem einzelnen Literal besteht (eine Einheitsklausel), dann werden alle enthaltenden Klauseln (außer der Einheitsklausel selbst) entfernt, und alle Klauseln, die enthalten, haben dieses Literal entfernt. Das Ergebnis der zweiten Regel kann selbst eine Einheitsklausel sein, die auf dieselbe Weise propagiert wird. Wenn keine Einheitsklauseln vorhanden sind, kann die Formel erfüllt werden, indem einfach alle verbleibenden Variablen negativ gesetzt werden. Die Formel ist nicht erfüllbar, wenn diese Transformation ein Paar entgegengesetzter Einheitsklauseln und erzeugt . Die Hornerfüllbarkeit ist tatsächlich eines der "schwersten" oder "ausdrucksvollsten" Probleme, von dem bekannt ist, dass es in polynomieller Zeit berechenbar ist, in dem Sinne, dass es ein P- vollständiges Problem ist.

Dieser Algorithmus ermöglicht auch das Bestimmen einer Wahrheitszuweisung von erfüllbaren Horn-Formeln: alle Variablen, die in einer Unit-Klausel enthalten sind, werden auf den Wert gesetzt, der diese Unit-Klausel erfüllt; alle anderen Literale werden auf false gesetzt. Die resultierende Zuweisung ist das minimale Modell der Horn-Formel, d. h. die Zuweisung mit einem minimalen Satz von Variablen, die wahr zugewiesen sind, wobei der Vergleich unter Verwendung der Mengenbegrenzung durchgeführt wird.

Bei Verwendung eines linearen Algorithmus für die Einheitspropagation ist der Algorithmus in der Größe der Formel linear.

Eine Verallgemeinerung der Klasse von Horn-Formeln ist die der umbenennbaren Horn-Formeln, die der Satz von Formeln ist, die in Horn-Form platziert werden können, indem einige Variablen durch ihre jeweilige Negation ersetzt werden. Die Überprüfung der Existenz eines solchen Ersatzes kann in linearer Zeit erfolgen; daher liegt die Erfüllbarkeit solcher Formeln in P, da sie gelöst werden kann, indem zuerst diese Ersetzung durchgeführt und dann die Erfüllbarkeit der resultierenden Horn-Formel überprüft wird. Hornerfüllbarkeit und umbenennbare Hornerfüllbarkeit stellen eine von zwei wichtigen Unterklassen der Erfüllbarkeit bereit, die in polynomieller Zeit lösbar sind; die andere solche Unterklasse ist 2-Erfüllbarkeit .

Das Horn-Erfüllbarkeitsproblem kann auch für propositionale vielwertige Logiken gestellt werden . Die Algorithmen sind normalerweise nicht linear, aber einige sind polynomiell; siehe Hähnle (2001 oder 2003) für eine Übersicht.

Dual-Horn-SAT

Eine duale Variante von Horn SAT ist Dual-Horn SAT , bei der jede Klausel höchstens ein negatives Literal hat. Das Negieren aller Variablen wandelt eine Instanz von Dual-Horn SAT in Horn SAT um. 1951 wurde von Horn nachgewiesen, dass Dual-Horn SAT in P steht .

Siehe auch

Verweise

  1. ^ Dowling, William F.; Gallier, Jean H. (1984), "Linear-time algorithms for testing the satisfiability of propositional Horn formulae", Journal of Logic Programming , 1 (3): 267–284, doi : 10.1016/0743-1066(84)90014- 1 , HERR  0770156
  2. ^ Buning, HK; Karpinski, Marek; Flogel, A. (1995). "Auflösung für quantifizierte Boolesche Formeln" . Informationen und Berechnung . Sonst. 117 (1): 12–18. doi : 10.1006/inco.1995.1025 .
  3. ^ Stephen Koch; Phuong Nguyen (2010). Logische Grundlagen der Beweiskomplexität . Cambridge University Press. P. 224. ISBN 978-0-521-51729-4.
  4. ^ Lewis, Harry R. (1978). „Umbenennen eines Satzes von Klauseln als Hornsatz“. Zeitschrift der ACM . 25 (1): 134–135. doi : 10.1145/322047.322059 . MR  0.468.315 ..
  5. ^ Aspvall, Bengt (1980). „Erkennen von getarnten NR(1)-Instanzen des Erfüllbarkeitsproblems“. Zeitschrift für Algorithmen . 1 (1): 97–103. doi : 10.1016/0196-6774(80)90007-3 . MR  0.578.079 .
  6. ^ Hébrard, Jean-Jacques (1994). "Ein linearer Algorithmus zum Umbenennen eines Satzes von Klauseln in einen Hornsatz" . Theoretische Informatik . 124 (2): 343–350. doi : 10.1016/0304-3975(94)90015-9 . MR  1.260.003 ..
  7. ^ Chandru, Vijaya; Collette R. Collard ; Peter L. Hammer; Miguel Montañez; Xiaorong-Sonne (2005). „Über umbenennbare Horn- und verallgemeinerte Hornfunktionen“. Annalen der Mathematik und Künstliche Intelligenz . 1 (1–4): 33–47. doi : 10.1007/BF01531069 .
  8. ^ Reiner Hähnle (2001). „Erweiterte vielwertige Logik“. In Dov M. Gabbay, Franz Günthner (Hrsg.). Handbuch der philosophischen Logik . 2 (2. Aufl.). Springer. P. 373. ISBN 978-0-7923-7126-7.
  9. ^ Reiner Hähnle (2003). „Komplexität der vielwertigen Logik“. In Melvin Fitting, Ewa Orłowska (Hrsg.). Jenseits von zwei: Theorie und Anwendungen der mehrwertigen Logik . Springer. ISBN 978-3-7908-1541-2.

Weiterlesen