[ Inhalt ] [ Index ]

Das Erfüllbarkeitsproblem

 

Dieses Problem läßt sich sehr einfach beschreiben:

Gegeben ist ein Boolescher Ausdruck mit n Variablen. Gesucht ist eine Belegung dieser Variablen, so daß der Ausdruck den Wert true erhält.

Beispiel:

A =

(A bezeichnet man als Summenproduktausdruck.)

erfüllt die Bedingung.

Eine naheliegende Lösungsmöglichkeit ist, einfach alle Möglichkeiten durchzuprobieren. Ist das Problem nicht erfüllbar, so merkt man das allerdings erst nach Schritten.

In den 60er Jahren haben Davis   und Putnam   einen Algorithmus gefunden, der in vielen Fällen schneller zum Ziel führt, falls der Ausdruck erfüllbar ist:

procedure Aufteilen(A)

1. wenn A eine leere Klausel enthält return
2. wenn A keine Klausel mehr enthält exit mit aktueller Zuordnung
3. Wähle nächste, nicht belegte Variable aus A.
4. Aufteilen( )
5. Aufteilen( )

Im Ausdruck werden die Klauseln entfernt, die enthalten. Aus allen Klauseln wird entfernt.

Im Ausdruck werden ganz analog die Klauseln entfernt, die enthalten. Aus allen Klauseln wird entfernt.

Entstehen dabei leere Klauseln, so führt die aktuelle Teilbelegung nicht zum Ziel.

Beispiel:

*

**

...

* liefert also bereits ein Ergebnis, während ** eine unzulässige Belegung darstellt.

In vielen Fällen findet der Algorithmus eine Lösung in wesentlich kürzerer Zeit als die erschöpfende Suche. Aber es kann nicht garantiert werden, daß das Problem in weniger als exponentieller Zeit gelöst wird.

Eine einfacher aussehende Version des Problems scheint aber genauso schwierig zu sein: gesucht ist ein polynomialer Algorithmus, der für jeden Summenproduktausdruck, der erfüllbar ist, eine 1, sonst eine 0 ausgibt.

Hier möchte man also nur wissen, ob eine erfüllende Zuordnung existiert.

Es wird sich zeigen, daß dieses Erfüllbarkeits-Entscheidungsproblem   von zentraler Bedeutung ist, da sich viele Probleme darauf zurückführen lassen.