Markierungsalgorithmus

aus Wikipedia, der freien Enzyklopädie

Du hast neue Nachrichten auf deiner Diskussionsseite.

Der Markierungsalgorithmus 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 dem 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).

[Bearbeiten] 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. 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. Durch Belegung aller Variablen mit 1 wird dieser Sachverhalt leicht nachgewiesen.

[Bearbeiten] Algorithmus

Sei $φ$ eine beliebige Horn-Formel. Folgender Algorithmus erkennt, ob $φ$ erfüllbar ist, oder nicht.

Für alle Klauseln der Form

ψ = x 1

Markiere

x 1

Solange

φ

Klauseln $\psi=\neg x_1 \vee \ldots \vee \neg x_n$ vom Typ 1 oder $\psi=\neg x_1 \vee \ldots \vee \neg x_n \vee y$ vom Typ 2 enthält, so dass $x_1, \ldots, x_n$ markiert sind und

y

im Falle von Klauseln von Typ 2 noch nicht markiert ist:

Falls

φ

eine entsprechende Klausel

ψ

vom Typ 1 enthält:

Beende den Algorithmus mit der Ausgabe unerfüllbar.

Andernfalls:

Wähle eine entsprechende Klausel

ψ

vom Typ 2 beliebig und

markiere

y

überall in

φ

Beende den Algorithmus mit der Ausgabe erfüllbar. Wenn man alle markierten Variablen mit wahr belegt und die restlichen Variablen mit falsch, so erhält man eine Belegung, die