Archiv: onli blogging

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:

a	b	c	d
1	1	1	0

Quelle