WikiDer > Erfüllbarkeit

In dem klassische Logik ist ein Vorschlagerfüllbar wenn es eine Auszeichnung gibt, richtig oder falsch, besteht aus dem Atomformeln in dem Satz, für den der Satz wahr ist. Liegt keine Zuordnung vor, ist der Vorschlag unbefriedigend. Ein unerfüllbarer Satz wird a Widerspruch erwähnt. Die Erfüllbarkeit einer Formel lässt sich mit a Wahrheitstabelle überprüft werden.

Beispiele

Beispiele für ausfüllbare Formeln sind:

${displaystyle Alor zB B}$

${displaystyle Alor zB A}$ (ein Tautologie, diese Formel ist immer wahr)

Beispiele für unerfüllbare Formeln sind:

${displaystyle Pland zB P}$

${displaystyle Pland zB Qland (P o Q)}$

Eine unerfüllbare Formel wird auch als a . bezeichnet Widerspruch.

Erfüllbarkeitsprobleme

sehen Zufriedenheitsproblem für den Hauptartikel zu diesem Thema.

Das Zufriedenheitsproblem, auch bekannt als SAT, aus dem from Komplexitätstheorie besteht darin zu entscheiden, ob eine bestimmte Formel erfüllbar ist oder nicht. Es gibt verschiedene Arten von Lösungen für das Erfüllbarkeitsproblem Algorithmen, wie Auflösung und der DPLL-Algorithmus. Aus bestimmten Darstellungen, wie z binäres Entscheidungsdiagramm, kann auch die Erfüllung eines Satzes gelesen werden. Das Sättigungsproblem ist NP-vollständig und das erste Problem, für das NP-Vollständigkeit demonstriert wurde. Ein weiteres Füllbarkeitsproblem ist die Hornfüllbarkeit (HORNSAT), bei der die Füllbarkeit von a Verbindung von Hornklauseln angesehen wird.

Es gibt viele Varianten des Erfüllbarkeitsproblems, wie zum Beispiel das Erfüllen von Formeln in Konjunktive Normalform (CNF-SAT). Hier kann man auch nach der Anzahl der unterscheiden Literale das passiert in der Klauseln der Formel in normaler Konjunktivform. Gängige Formen sind 2-SAT mit zwei Literalen pro Klausel und 3-SAT mit drei Literalen oder häufiger, k-SAT mit k Literale pro Klausel. Ein verwandtes Problem ist MAX-SAT, das nach der maximalen Anzahl von Klauseln sucht, die erfüllt werden können.^[1] Diese Bedingungen können kombiniert werden; auf diese Weise bekommt man Probleme wie MAX 3-SAT, die nach der maximalen Anzahl von Klauseln suchen, die in einer Formel in normaler Konjunktivform mit drei Literalen pro Klausel erfüllt werden können.