Markierungsalgorithmus

Markierungsalgorithmus

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 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

Hauptartikel: Horn-Formel

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.

Algorithmus

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

Für alle Klauseln der Form ψ = x1:
Markiere x1
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 ϕ erfüllt.

Motivation des Algorithmus: Der Algorithmus markiert alle Variablen, die zwangsläufigerweise mit wahr belegt werden müssen (nämlich zuerst die Variablen in den Klauseln, die nur aus einem positiven Literal bestehen, 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, die Variable auf der rechten Seite.). Wenn sich dabei kein Widerspruch ergibt, ist die Formel erfüllbar.

Weblinks


Wikimedia Foundation.

Игры ⚽ Нужна курсовая?

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Leerheitsproblem — Als Leerheitsproblem bezeichnet man in der Theoretischen Informatik das Problem, zu entscheiden, ob eine in Form einer formalen Grammatik gegebene formale Sprache L leer ist, also , oder nicht. Das Problem ist es also herauszufinden, ob es Wörter …   Deutsch Wikipedia

  • Unterstreichungsalgorithmus — 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… …   Deutsch Wikipedia

  • Horn-Klausel — Horn Formeln sind eine spezielle Teilmenge der aussagenlogischen Formeln. Benannt wurden sie nach dem US amerikanischen Logiker Alfred Horn. Inhaltsverzeichnis 1 Definition mit Horn Klauseln 1.1 Beispiele 1.2 Darstellungsformen von Horn Klauseln… …   Deutsch Wikipedia

  • Horn-Klauseln — Horn Formeln sind eine spezielle Teilmenge der aussagenlogischen Formeln. Benannt wurden sie nach dem US amerikanischen Logiker Alfred Horn. Inhaltsverzeichnis 1 Definition mit Horn Klauseln 1.1 Beispiele 1.2 Darstellungsformen von Horn Klauseln… …   Deutsch Wikipedia

  • Hornformel — Horn Formeln sind eine spezielle Teilmenge der aussagenlogischen Formeln. Benannt wurden sie nach dem US amerikanischen Logiker Alfred Horn. Inhaltsverzeichnis 1 Definition mit Horn Klauseln 1.1 Beispiele 1.2 Darstellungsformen von Horn Klauseln… …   Deutsch Wikipedia

  • Hornklausel — Horn Formeln sind eine spezielle Teilmenge der aussagenlogischen Formeln. Benannt wurden sie nach dem US amerikanischen Logiker Alfred Horn. Inhaltsverzeichnis 1 Definition mit Horn Klauseln 1.1 Beispiele 1.2 Darstellungsformen von Horn Klauseln… …   Deutsch Wikipedia

  • Horn-Formel — Horn Formeln sind eine wichtige Teilmenge der prädikatenlogischen Formeln. Sie spielen eine zentrale Rolle in der Logischen Programmierung und sind von Bedeutung für die konstruktive Logik. Benannt wurden sie nach dem US amerikanischen Logiker… …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”