imported>Xenein: /* growthexperiments-addlink-summary-summary:3|0|0 */

2024-11-15T03:01:11Z

growthexperiments-addlink-summary-summary:3|0|0

Neue Seite

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

== Horn-Formeln ==
{{Hauptartikel|Horn-Formel}}

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.

{| class="wikitable"
! Typ
! 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.

== Algorithmus ==
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.)

:* Schritt 1:
:** Falls keine Fakten existieren:
:*** Ausgabe "erfüllbar".
:** 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.

== Weblinks ==
* [https://lamboolda.com/logic#5 Online Markierungsalgorithmus auf Formeln anwendet]

[[Kategorie:Mathematische Logik]]

Markierungsalgorithmus - Versionsgeschichte

imported>Xenein: /* growthexperiments-addlink-summary-summary:3|0|0 */