Satisfiability

Satisfiability

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 polynomieller Zeit 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 polynomialer 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 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.

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.

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.

Siehe auch

Quellen

  • Christos H. Papadimitriou: Computational Complexity. Addison Wesley, ISBN 978-0201530827

Wikimedia Foundation.

Игры ⚽ Нужно решить контрольную?

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Satisfiability Modulo Theories — (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first order logic with equality. Examples of theories typically used in computer science are the theory of real… …   Wikipedia

  • Satisfiability Modulo Theories — В программировании, Satisfiability Modulo Theories (SMT) это задача разрешимости для логических формул с учётом лежащих в их основе теорий. Примерами таких теорий для SMT формул являются: теории целых и вещественных чисел, теории списков,… …   Википедия

  • Satisfiability Modulo Theories (SMT) — Problème SMT (Satisfiability Modulo Theories) est un problème de la décision pour les formules logiques dans le respect d une théorie exprimée dans la logique du premier ordre contenant l égalité. Des exemples de théories sont la théorie des… …   Wikipédia en Français

  • satisfiability — noun Able to be satisfied …   Wiktionary

  • Boolean satisfiability problem — For the concept in mathematical logic, see Satisfiability. 3SAT redirects here. For the Central European television network, see 3sat. In computer science, satisfiability (often written in all capitals or abbreviated SAT) is the problem of… …   Wikipedia

  • 2-satisfiability — In computer science, 2 satisfiability (abbreviated as 2 SAT or just 2SAT) is the problem of determining whether a collection of two valued (Boolean or binary) variables with constraints on pairs of variables can be assigned values satisfying all… …   Wikipedia

  • Maximum satisfiability problem — In computational complexity theory, the Maximum Satisfiability problem (MAX SAT) is the problem of determining the maximum number of clauses, of a given Boolean formula, that can be satisfied by some assignment. It is an FNP generalization of SAT …   Wikipedia

  • Horn-satisfiability — In formal logic, Horn satisfiability, or HORNSAT, is the problem of deciding whether a given set of propositional Horn clauses is satisfiable.A Horn clause is a clause with at most one positive literal, called the head of the clause, and any… …   Wikipedia

  • Local consistency — In constraint satisfaction, local consistency conditions are properties of constraint satisfaction problems related to the consistency of subsets of variables or constraints. Several such conditions exist, the most known being node consistency,… …   Wikipedia

  • Median graph — The median of three vertices in a median graph In mathematics, and more specifically graph theory, a median graph is an undirected graph in which any three vertices a, b, and c have a unique median: a vertex m(a,b,c) that belongs to shortest… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”