Markierungsalgorithmus

Der Markierungsalgorithmus dient zur Überprüfung von Hornformeln 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).

Idee des Algorithmus

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.

Vorgehensweise des Algorithmus

Kurzübersicht über die Formen einer Hornformel

(genaueres unter Hornformeln) 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):

Typ 1: A <=> (falsch -> A)

Typ 2: (-A1|-A2|...|-An|B) <=> (A1,...,An -> B)

Typ 3 (-A1|-A2|...|-An) <=> (A1,...,An -> wahr)

Hornformeln, die nur Disjunktionsterme vom Typ III enthalten, sind trivialerweise erfüllbar. Durch die Belegung der Variablen mit 0 wird die gesamte Aussage wahr. Horn-Formel, die keinen Term vom Typ III besitzen, sind erfüllbar. Durch Belegung aller Variablen mit 1 wird dieser Sachverhalt leicht nachgewiesen. 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!

Ablauf des Algorithmus im einzelnen

Eingabe: eine Hornformel phi

1. Schritt:
Für jede Formel vom Typ I:
markiere diese atomare Formel und alle anderen Literale die diese Formel enthalten.

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.