Hornklauseln sind Klauseln wie {Q,¬A,¬B} mit jeweils maximal einem positiven Bestandteil. Mit dem Markierungsalgorithmus kann man in einfachen Schritten ihre minimale Belegung erhalten.
Schritt 1: Umformen
Dieser Schritt ist nicht unbedingt nötig, vereinfacht die Sache aber. Die Klauseln werden umgeformt in Implikationsform.
Dies funktioniert nach folgenden Regeln:
Bei negativen und positiven Elementen wird das positive gefolgert:
{Q,¬A,¬B} := ((A & B)->Q)
Nur negative Elemente folgern !T (wird ausgewertet zu 0):
{¬Q, ¬A,¬B}:=((A & B & Q)-> !T)
Ein positives Element folgert sich aus T (wird ausgewertet zu 1):
{Q}:=(T->Q)
Ein Beispiel:
Aus
M:= { {a,¬c}, {c}, {¬a, b, ¬c} } {¬b, ¬c, a, ¬d)
wird
(c -> a) & (T -> c) & ((a & c) -> b) & ((b & c & d) -> a)
Schritt 2: Initialmarkierung
Nun werden die Element markiert, die aus einem T gefolgert werden:
M1: (c¹ -> a) & (T -> c¹) & ((a & c¹) -> b) & ((b & c¹ & d) -> a)
Schritt 3: Whilemarkierung
Schritt für Schritt werden alle bisher unmarkierten Elemente markiert, die aus Elementen gefolgert werden, die schon alle(!) markiert sind.
Abbruchbedingungen:
1. Es gibt nichts mehr zu markieren: erfüllbar
2. Es wäre !T zu markieren: unerfüllbar.
Dem Beispiel von oben folgend:
M2: (c¹ -> a²) & (T -> c¹) & ((a² & c¹) -> b) & ((b & c¹ & d) -> a²)
M3: (c¹ -> a²) & (T -> c¹) & ((a² & c¹) -> b³) & ((b³ & c¹ & d) -> a²)
=> erfüllbar.
Schritt 4: Auswertung
Teil der Minimalbelegung sind nun die markierten Elemente. In diesem Fall sind das alle außer d:
Quelle
