Erfüllbarkeitsproblem der Aussagenlogik

Erfüllbarkeitsproblem der Aussagenlogik

Das Erfüllbarkeitsproblem der Aussagenlogik (SAT, von engl. satisfiability) ist ein Entscheidungsproblem. Es fragt, ob eine aussagenlogische Formel erfüllbar ist. Anwendungen finden sich unter anderem in der Komplexitätstheorie, Verifikation und im Entwurf von logischen Schaltungen. Insbesondere in der Komplexitätstheorie wird mit SAT auch nur der Spezialfall von Formeln bezeichnet, die in konjunktiver Normalform vorliegen.

Das Erfüllbarkeitsproblem der Aussagenlogik ist in exponentieller Zeit in der Anzahl der Variablen entscheidbar, zum Beispiel durch das Aufstellen einer Wahrheitstabelle. Ob es auch einen Algorithmus gibt, der SAT in Polynomialzeit löst, ist nicht bekannt. Die Forschung beschäftigt sich mit der Entwicklung möglichst effizienter Verfahren (sogenannter SAT-Solver). Bekannte SAT-Solver sind Binäre Entscheidungsdiagramme, oder das Davis-Putnam-Verfahren. Manche Solver verwenden stochastische oder systematische Suchverfahren zur Entscheidung der Erfüllbarkeit. Das bekannteste und am meisten verbreitete Verfahren zur systematischen Suche ist (Stand 2008) das DPLL-Verfahren (Davis-Putnam-Logemann-Loveland), welches in den letzten Jahrzehnten mit Hilfe von Heuristiken und Lernverfahren stark verbessert wurde.

SAT gehört zur Klasse \mathcal{NP} der Probleme, die in polynomieller Zeit mit einer nichtdeterministischen Turingmaschine gelöst werden können. Die noch ungelöste Frage, ob SAT auch mit einer deterministischen Turingmaschine (also mit einem herkömmlichen Rechner) in polynomieller Zeit gelöst werden kann, kann man formulieren als: Gilt \mbox{SAT} \in \mathcal{P}?

Das Erfüllbarkeitsproblem der Aussagenlogik ist NP-vollständig. Das besagt, dass jedes Problem aus \mathcal{NP} in polynomieller Zeit auf SAT zurückgeführt werden kann (Polynomialzeitreduktion). Anfang der 1970er Jahre zeigten Stephen A. Cook und Leonid Levin unabhängig voneinander diese Eigenschaft, bekannt als der Satz von Cook. Cook zeigte hierfür einen Algorithmus auf, mit dem die Berechnungsschritte einer nicht-deterministischen Turingmaschine in Aussagenlogik formuliert und damit auf SAT reduziert werden können. Richard M. Karp zeigte 1972 die NP-Vollständigkeit weiterer Probleme. Er prägte damit das heutige Verständnis von NP-Vollständigkeit.

Falls also \mbox{SAT} \in \mathcal{P} gilt, dann ist jedes Problem aus \mathcal{NP} auch in \mathcal{P}, das heißt, dann gilt \mathcal{P} = \mathcal{NP}. Auch die umgekehrte Richtung der Implikation gilt. Das P-NP-Problem „gilt \mathcal{P} = \mathcal{NP} oder nicht?“ ist eine der großen ungelösten Fragen der Komplexitätstheorie. Ist ein Problem NP-vollständig, so darf man annehmen, dass die Suche nach einem Polynomialzeit-Algorithmus dafür aussichtslos ist. Dieser Annahme zu folgen, bedeutet nichts anderes, als die Überzeugung vieler Mathematiker, dass \mathcal{P} = \mathcal{NP} nicht gilt, zu teilen.

Varianten von SAT

SAT kann auf viele Weisen durch Einschränkungen und Verallgemeinerungen variiert werden. Das Problem 3-SAT ist eine Variante, die höchstens drei Literale pro Klausel enthält. Trotz der Einschränkung ist auch 3-SAT NP-vollständig, denn SAT lässt sich in polynomieller Zeit auf 3-SAT reduzieren.

Jedes 3-SAT mit p Variablen und q Klauseln lässt sich auf einen Graphen G mit p+q Knoten abbilden, in dem alle Variablenknoten mit denjenigen Klauselknoten verbunden sind, in denen sie vorkommen. Eine Formel ist in P3SAT, wenn sie in 3-SAT ist, und der Graph planar ist. Auch P3SAT ist NP-vollständig.

Das Problem MAX-SAT besteht darin, die maximale Anzahl erfüllbarer Klauseln einer Formel zu bestimmen. Es ist NP-schwer.

Zu vielen weiteren Komplexitätsklassen gibt es Varianten von SAT, die bezüglich dieser Klassen vollständig sind. Beispielsweise ist die Variante 2-SAT NL-vollständig. Das HORNSAT-Problem ist P-vollständig. Die Erweiterung der aussagenlogischen Formeln durch die Einführung von Quantoren führt zu QBF (auch QSAT genannt), einem PSPACE-vollständigen Problem.

Schließlich kann man SAT auch mit anderen Entscheidungstheorien koppeln. Das sich ergebende Problem wird als ein SMT-Problem (Satisfiability Modulo Theory) bezeichnet und kann z.B. durch Kodierung in ein reines SAT-Problem oder durch eine Kombination von Entscheidungsverfahren gelöst werden.

Siehe auch

Quellen


Wikimedia Foundation.

См. также в других словарях:

  • Erfüllbarkeitsproblem — Das Erfüllbarkeitsproblem der Aussagenlogik (SAT, von engl. satisfiability) ist ein Entscheidungsproblem. Es fragt, ob eine aussagenlogische Formel erfüllbar ist. Anwendungen finden sich unter anderem in der Komplexitätstheorie, Verifikation und… …   Deutsch Wikipedia

  • Aussagenlogik — Die Aussagenlogik ist ein Teilgebiet der Logik, das sich mit Aussagen und deren Verknüpfung durch Junktoren befasst, ausgehend von strukturlosen Elementaraussagen (Atomen), denen ein Wahrheitswert zugeordnet wird. In der klassischen Aussagenlogik …   Deutsch Wikipedia

  • Erfüllbarkeitsproblem für quantifizierte boolesche Formeln — In der Komplexitätstheorie ist das Erfüllbarkeitsproblem für quantifizierte boolesche Formeln (oft nur kurz QBF oder QSAT) eine Verallgemeinerung des Erfüllbarkeitsproblems der Aussagenlogik. Es untersucht, ob eine mit Quantoren versehene… …   Deutsch Wikipedia

  • Problem der exakten Überdeckung — Das Problem der exakten Überdeckung (englisch Exact Cover) ist ein Entscheidungsproblem der Kombinatorik. Es gehört zu den 21 klassischen NP vollständigen Problemen, von denen Richard M. Karp 1972 gezeigt hat, dass sie NP vollständig sind.… …   Deutsch Wikipedia

  • Unterstreichungsalgorithmus — Der Markierungsalgorithmus ist ein Algorithmus zur Überprüfung von Horn Formeln auf Erfüllbarkeit. Im Unterschied zu allgemeinen aussagenlogischen Formeln, für die vermutet wird, dass kein Polynomialzeit Algorithmus existiert (siehe… …   Deutsch Wikipedia

  • NP-Vollständig — Der Begriff NP Vollständigkeit ist ein Begriff aus der Komplexitätstheorie der Theoretischen Informatik, der im Jahre 1971 von Stephen A. Cook durch den Satz von Cook eingeführt wurde. Er zeichnet spezielle formale Sprachen der Komplexitätsklasse …   Deutsch Wikipedia

  • NP-vollständig — Der Begriff NP Vollständigkeit ist ein Begriff aus der Komplexitätstheorie der Theoretischen Informatik, der im Jahre 1971 von Stephen A. Cook durch den Satz von Cook eingeführt wurde. Er zeichnet spezielle formale Sprachen der Komplexitätsklasse …   Deutsch Wikipedia

  • Markierungsalgorithmus — Der Markierungsalgorithmus ist ein Algorithmus zur Überprüfung von Horn Formeln auf Erfüllbarkeit. Im Unterschied zu allgemeinen aussagenlogischen Formeln, für die vermutet wird, dass kein Polynomialzeit Algorithmus existiert (siehe… …   Deutsch Wikipedia

  • Satz von Cook — Der kanadische Wissenschaftler Stephen A. Cook begründete 1971 eine neue Klasse von Problemen in der Komplexitätstheorie. Er zeigte, dass eine Teilmenge der Klasse NP existiert, auf die sich alle Probleme aus NP polynomiell reduzieren lassen.… …   Deutsch Wikipedia

  • Feedback Vertex Set — Der Begriff Feedback Vertex Set bzw. kreiskritische Knotenmenge bezeichnet in der Komplexitätstheorie ein graphentheoretisches Entscheidungsproblem, das NP vollständig ist. Definition Es fragt, ob es zu einem ungerichteten Multigraphen G = (V,E) …   Deutsch Wikipedia


Поделиться ссылкой на выделенное

Прямая ссылка:
Нажмите правой клавишей мыши и выберите «Копировать ссылку»