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

Der Quicksort ist vom Prinzip schon sehr effektiv. Trotzdem kann er in natürlich optimiert werden, um den Wort-Case seltener eintreten zu lassen und die reale Performance zu erhöhen - nur wie? Welche Verfahren sind praktikabel, welche Kleinigkeiten kann man beachten?

Ich muss da selbst noch einiges lernen. Was mir aber bei meinen Versuchen bisher aufgefallen ist:

1. Kleinigkeiten nützen schon etwas. Wenn man nicht das mittlere Element als Pivot, sondern das linke oder das rechte wählt, dann kann man den jeweiligen Cursor auch links bzw. rechts vom Pivot ansetzen.

2. Noch eine Kleinigkeit: Beim Tauschen darauf achten, dass die zu tauschenden Elemente nicht sowieso schon gleich sind (evtl. ist das auch schlecht: kostet die Abfrage mehr Leistung als das unnötige Tauschen?)

3. Es gibt eine (relativ) naive Implementierung, bei der das linke, das mittlere und das rechte Element verglichen werden und der Mittelwert als Pivot gewählt wird. Wenn man die sowieso manuell betrachtet, kann man sie auch sortiert zurückschreiben: das kleinste nach links, das größte nach rechts, das Pivot in die Mitte.
Meinen bisherigen Tests nach hilft das enorm bei halbwegs geordneten Listen, schadet aber ein kleines bißchen bei komplett ungeordneten Zahlenabfolgen.

4. Wenn nur noch zwei Elemente in der zu sortierenden Liste sind, sollte das linke zum Pivot werden. Das kann aber natürlich auch eine Macke in meiner Implementation sein.

Noch testen will ich, wie es sich auswirkt, wenn man mehrere Threads nutzt und wie man das am besten anstellt.

Und sowieso: Ist es in der Realität nicht eher besser, auf die Kleinigkeiten zu verzichten und sich auf die Wahl eines guten Pivots zu beschränken, weil so Abfragen gespart werden - oder wiegen die gesparten Arrayzugriffe das wieder auf?

Auch wenn es mindestens die Hälfte meiner Leserschaft nicht wirklich interessieren wird, zeige ich hier mal wie man einen DFA per Hand (auch) minimieren kann. Das ist nämlich eigentlich recht einfach, solange der DFA simpel genug ist, wird aber oft genug kompliziert erklärt.
Nehmen wir folgenden DFA als zu minimierenden:

Minimieren kann nur funktionieren, wenn man überflüssige Zustände entfernt bzw. zusammenfasst. Am Anfang haben wir kein weiteres Unterscheidungsmerkmal als die Frage, ob die Zustände final sind (im Bild oben dargestellt durch die Doppelkreise) oder nicht. Grafisch betrachtet sieht das dann so aus (die Linien stellen die Übergänge dar, a ist blau, b braun, ab türkis)

Der Doppelpunkt markiert das nächste Unterscheidungskriterium: Zustand 1 und 2 gehen über a bzw. b in die linke Gruppe, Zustand 5 geht jeweils in sich selbst, also in die rechte Gruppe: Hier kann innerhalb der Gruppe "125" nochmal unterschieden werden zwischen "12" (gehen beide in die linke Gruppe) und "5" (geht in die rechte Gruppe).
Nun sieht der nächste Schritt so aus:

Da 3 und 4 nun auf eine andere Gruppe als 0 zeigen, kann jetzt auch in der linken Gruppe unterschieden werden.
Führt man das Verfahren nun nochmal aus, zeigt jedes Gruppenmitglied auf die gleiche Gruppe, ein weiteres Unterscheiden ist also nicht möglich.
Der fertig minimiert DFA sieht also wie folgt aus:


PS: Die DFAs wurden mit dem Automaton Simulator gezeichnet.