„Markierungsalgorithmus“ – Versionsunterschied

Versionsgeschichte interaktiv durchsuchen

[ungesichtete Version]

[gesichtete Version]

Inhalt gelöscht Inhalt hinzugefügt

Inline

Aktuelle Version vom 15. November 2024, 05:01 Uhr

Der Markierungsalgorithmus (auch Unterstreichungsalgorithmus) ist ein Algorithmus zur Überprüfung von Horn-Formeln auf Erfüllbarkeit. Im Unterschied zu allgemeinen aussagenlogischen Formeln, für die vermutet wird, dass kein Polynomialzeit-Algorithmus existiert (siehe Erfüllbarkeitsproblem der Aussagenlogik), ist mit diesem Markierungsalgorithmus auf der Menge der Horn-Formeln, die eine Teilmenge der aussagenlogischen Formeln darstellen, ein Polynomialzeit-Algorithmus bekannt (eine Implementierung in linearer Zeit ist möglich).

Horn-Formeln

Horn-Formeln sind eine Konjunktion von Horn-Klauseln. Horn-Klauseln sind dabei spezielle Klauseln, die höchstens ein positives Literal besitzen. Horn-Klauseln lassen sich nach den Regeln der Aussagenlogik auch als Implikation darstellen. Die folgende Tabelle gibt einen Überblick über die zwei möglichen Typen einer Horn-Klausel und ein Beispiel in Form der Disjunktion und der Implikation.

Typ	Disjunktion	Implikation
1	$\neg x_{1}\vee \neg x_{2}\vee \ldots \vee \neg x_{n}$	$x_{1}\wedge x_{2}\wedge \ldots \wedge x_{n}\rightarrow 0$
2	$\neg x_{1}\vee \neg x_{2}\vee \ldots \vee \neg x_{n}\vee y$	$x_{1}\wedge x_{2}\wedge \ldots \wedge x_{n}\rightarrow y$

Die Variable $n$ kann für Klauseln vom Typ 2 auch 0 sein. In diesem Fall nennt man die Klausel auch einen Fakt. Horn-Formeln, die nur Klauseln vom Typ 1 enthalten, sind trivialerweise erfüllbar. Durch die Belegung der Variablen mit 0 wird die gesamte Aussage wahr. Horn-Formeln, die nur Klauseln vom Typ 2 besitzen, sind erfüllbar, indem man alle Variablen mit 1 belegt.

Algorithmus

Sei $\phi$ eine beliebige Horn-Formel. Folgender Algorithmus gibt aus, ob $\phi$ erfüllbar ist oder nicht. (Markieren bedeutet dabei, jedes Vorkommen einer Variable in $\phi$ zu markieren.)

Schritt 1:
- Falls keine Fakten existieren:
  - Ausgabe "erfüllbar".
- Sonst:
  - Markiere alle Fakten.
Schritt 2:
- Falls eine Klausel $\psi$ $\psi$ aus $\phi$ $\phi$ von Typ 1 existiert, so dass alle $x_{i}$ $x_{i}$ markiert sind:
  - Ausgabe "unerfüllbar".
- Falls keine Klausel $\psi$ $\psi$ aus $\phi$ $\phi$ von Typ 2 existiert, so dass alle $x_{i}$ $x_{i}$ markiert sind:
  - Ausgabe "erfüllbar".
- Falls eine Klausel $\psi$ $\psi$ aus $\phi$ $\phi$ von Typ 2 existiert, so dass alle $x_{i}$ $x_{i}$ markiert sind aber y nicht:
  - Markiere y.
  - Gehe zu Schritt 2.
- Sonst:
  - Ausgabe "erfüllbar".

Endet der Algorithmus mit der Ausgabe erfüllbar, so erhält man eine Belegung, die

\phi

erfüllt, indem man alle markierten Variablen mit wahr belegt und die restlichen Variablen mit falsch.

Motivation des Algorithmus: Der Algorithmus markiert alle Variablen, die zwangsläufigerweise mit wahr belegt werden müssen (nämlich zuerst die Variablen in den Fakten, und danach in den Klauseln, die eine Implikation darstellen und bei denen die Variablen auf der linken Seite der Implikation schon alle mit wahr belegt sind). Wenn sich dabei kein Widerspruch ergibt, ist die Formel erfüllbar.

Weblinks

Online Markierungsalgorithmus auf Formeln anwendet

@@ Zeile 1: / Zeile 1: @@
-Der '''Markierungsalgorithmus''' dient zur Überprüfung von [[Hornformel]]n auf Erfüllbarkeit oder Unerfüllbarkeit. Das Verfahren, eine allgemeine Formel auf Erfüllbarkeit bzw. Unerfüllbarkeit zu überprüfen, gelingt grundsätzlich mit einer [[Wahrheitstafel]]. Jedoch ist dies verbunden mit einem exponentiellen Aufwand. Die Markierungsalgorithmus ist nur für Hornformeln zugelassen umgeht jedoch das Problem des exponentiellen Aufwandes (In Abhängigkeit von der Eingabelänge. Hier: Länge der Hornformel bzw. Anzahl der Aussagevariablen in der eingegebenen Hornformel).
+Der '''Markierungsalgorithmus''' (auch '''Unterstreichungsalgorithmus''') ist ein [[Algorithmus]] zur Überprüfung von [[Horn-Formel]]n auf [[Erfüllbarkeit]]. Im Unterschied zu allgemeinen [[Aussagenlogik|aussagenlogischen]] Formeln, für die vermutet wird, dass kein [[Polynomialzeit]]-Algorithmus existiert (siehe [[Erfüllbarkeitsproblem der Aussagenlogik]]), ist mit diesem Markierungsalgorithmus auf der Menge der Horn-Formeln, die eine [[Teilmenge]] der aussagenlogischen Formeln darstellen, ein Polynomialzeit-Algorithmus bekannt (eine [[Implementierung]] in linearer Zeit ist möglich).
-== Idee des Algorithmus ==
+== Horn-Formeln ==
+{{Hauptartikel|Horn-Formel}}
-Ziel ist es, eine Hornformel auf Erfüllbarkeit bzw. Unerfüllbarkeit zu überprüfen. Hierzu soll nun eine Vorgehensweise gefunden werden, die es ermöglicht, jede beliebige logische Formel in dieser spezifischen Form zu überprüfen. Hierbei wird die grundlegende Eigenschaft eines [[Algorithmus]] in Betracht gezogen, die besagt, dass ein Algorithmus eine Art "Rezept" zur Lösung eines Problems bereitstellt. Dabei soll dieses "Rezept" die Vollständigkeit und die Korrektheit dieser Lösung garantieren. Vollständigkeit heißt hier, dass von diesem Algorithums alle möglichen Lösungswege getestet werden, so das ein richtiges Ergebniss resultiert.
+Horn-Formeln sind eine [[Konjunktion (Logik)|Konjunktion]] von Horn-Klauseln. Horn-Klauseln sind dabei spezielle [[Disjunktionsterm|Klausel]]n, die höchstens ein positives [[Literal]] besitzen. Horn-Klauseln lassen sich nach den Regeln der Aussagenlogik auch als [[Implikation]] darstellen. Die folgende Tabelle gibt einen Überblick über die zwei möglichen Typen einer Horn-Klausel und ein Beispiel in Form der [[Disjunktion]] und der Implikation.
-== Vorgehensweise des Algorithmus ==
-=== Kurzübersicht über die Formen einer Hornformel ===
-(genaueres unter [[Hornformel]]n)
-Eine Hornformel hat die Eigenschaft, dass sie maximal ein positives [[Literal]] besitzt. Daraus folgen drei verschiedene Disjunkionsterme, die als Elemente einer Hornformel möglich sind (im Rahmen der Definition von Horn-Formeln):
+{| class="wikitable"
-'''Typ 1''':
+! Typ
-A                    <=>  (falsch -> A)
+! Disjunktion
+! Implikation
+|-
+| 1
+| <math>\neg x_1 \vee \neg x_2 \vee \ldots \vee \neg x_n</math>
+| <math>x_1 \wedge x_2 \wedge \ldots \wedge x_n \rightarrow 0</math>
+|-
+| 2
+| <math>\neg x_1 \vee \neg x_2 \vee \ldots \vee \neg x_n \vee y</math>
+| <math>x_1 \wedge x_2 \wedge \ldots \wedge x_n \rightarrow y</math>
+|}
+Die Variable <math>n</math> kann für Klauseln vom Typ 2 auch 0 sein. In diesem Fall nennt man die Klausel auch einen Fakt. Horn-Formeln, die nur Klauseln vom Typ 1 enthalten, sind trivialerweise erfüllbar. Durch die Belegung der Variablen mit 0 wird die gesamte Aussage wahr. Horn-Formeln, die nur Klauseln vom Typ 2 besitzen, sind erfüllbar, indem man alle Variablen mit 1 belegt.
-'''Typ 2''':
-(-A1|-A2|...|-An|B)  <=>  (A1,...,An -> B)
+== Algorithmus ==
-'''Typ 3'''
+Sei <math>\phi</math> eine beliebige Horn-Formel. Folgender Algorithmus gibt aus, ob <math>\phi</math> erfüllbar ist oder nicht. (''Markieren'' bedeutet dabei, jedes Vorkommen einer Variable in <math>\phi</math> zu markieren.)
-(-A1|-A2|...|-An)    <=>  (A1,...,An -> wahr)
+:* Schritt 1:
-Hornformeln, die nur Disjunktionsterme vom Typ III enthalten, sind trivialerweise erfüllbar. Durch die Belegung der Variablen mit 0 wird die gesamte Aussage wahr.
+:** Falls keine Fakten existieren:
-Horn-Formel, die keinen Term vom Typ III besitzen, sind erfüllbar. Durch Belegung aller Variablen mit 1 wird dieser Sachverhalt leicht nachgewiesen.
+:*** Ausgabe "erfüllbar".
-Achtung: Diesem Algorithmus obliegt es NICHT die Formel dahingehend zu überprüfen ob sie eine Hornformel ist. Bei Eingabe einer Formel die nicht der Definition einer Horn-Formel entspricht kann die Korrektheit und Vollständigkeit diese Algorithmuses nicht gewährleistet werden!
+:** Sonst:
+:*** Markiere alle Fakten.
+:* Schritt 2:
+:** Falls eine Klausel <math>\psi</math> aus <math>\phi</math> von Typ 1 existiert, so dass alle <math>x_i
+</math> markiert sind:
+:*** Ausgabe "unerfüllbar".
+:** Falls keine Klausel <math>\psi</math> aus <math>\phi</math> von Typ 2 existiert, so dass alle <math>x_i
+</math> markiert sind:
+:*** Ausgabe "erfüllbar".
+:** Falls eine Klausel <math>\psi</math> aus <math>\phi</math> von Typ 2 existiert, so dass alle <math>x_i
+</math> markiert sind aber y nicht:
+:*** Markiere y.
+:*** Gehe zu Schritt 2.
+:** Sonst:
+:*** Ausgabe "erfüllbar".
+: Endet der Algorithmus mit der Ausgabe ''erfüllbar'', so erhält man eine Belegung, die <math>\phi</math> erfüllt, indem man alle markierten Variablen mit ''wahr'' belegt und die restlichen Variablen mit ''falsch''.
+Motivation des Algorithmus: Der Algorithmus markiert alle Variablen, die zwangsläufigerweise mit ''wahr'' belegt werden müssen (nämlich zuerst die Variablen in den Fakten, und danach in den Klauseln, die eine Implikation darstellen und bei denen die Variablen auf der linken Seite der Implikation schon alle mit ''wahr'' belegt sind). Wenn sich dabei kein Widerspruch ergibt, ist die Formel erfüllbar.
-=== Ablauf des Algorithmus im einzelnen ===
-Eingabe: eine Hornformel phi
+== Weblinks ==
- '''1. Schritt:'''
+* [https://lamboolda.com/logic#5 Online Markierungsalgorithmus auf Formeln anwendet]
- Für jede Formel vom Typ I:
- markiere diese atomare Formel und alle anderen Literale die diese Formel enthalten.
+[[Kategorie:Mathematische Logik]]
- '''2. Schritt:'''
- Solange folgende Bedingungen gelten:
- a) es gibt in phi eine Disjuntionsterm psi=(-A1,-A2,-A3,...,B) vom Typ II derart,
-    dass zwar A1,...,An schon markiert sind, aber B nicht
-                                 '''ODER'''
- b) es gibt in phi einen Disjunktionsterm psi=(-A1,-A2,-A3,...,-An) vom Typ II derart,
-    dass zwar A1,...,An sind markiert sind
- soll folgendes gemacht werden:
- wenn psi vom Typ II ist makiere B.
- wenn aber psi vom Typ II ist, gib "unerfüllbar" aus und halte an.
- '''3. Schritt:'''
- (Wenn die Bedingungen in 2. nicht mehr zutreffen)
- Gib "erfüllbar" aus und halte an.