| dbo:abstract
|
- Das Erfüllbarkeitsproblem der Aussagenlogik (SAT, von englisch satisfiability ‚Erfüllbarkeit‘) 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 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 ? Das Erfüllbarkeitsproblem der Aussagenlogik ist NP-vollständig. Das besagt, dass jedes Problem aus 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 gilt, dann ist jedes Problem aus auch in , das heißt, dann gilt . Auch die umgekehrte Richtung der Implikation gilt. Das P-NP-Problem „gilt 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. Diese Annahme entspricht der Überzeugung vieler Mathematiker, dass nicht gilt. (de)
- Das Erfüllbarkeitsproblem der Aussagenlogik (SAT, von englisch satisfiability ‚Erfüllbarkeit‘) 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 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 ? Das Erfüllbarkeitsproblem der Aussagenlogik ist NP-vollständig. Das besagt, dass jedes Problem aus 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 gilt, dann ist jedes Problem aus auch in , das heißt, dann gilt . Auch die umgekehrte Richtung der Implikation gilt. Das P-NP-Problem „gilt 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. Diese Annahme entspricht der Überzeugung vieler Mathematiker, dass nicht gilt. (de)
|
| rdfs:comment
|
- Das Erfüllbarkeitsproblem der Aussagenlogik (SAT, von englisch satisfiability ‚Erfüllbarkeit‘) 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. SAT gehört zur Klasse ? Das Erfüllbarkeitsproblem der Aussagenlogik ist NP-vollständig. Das besagt, dass jedes Problem aus Falls also auch in nicht gilt. (de)
- Das Erfüllbarkeitsproblem der Aussagenlogik (SAT, von englisch satisfiability ‚Erfüllbarkeit‘) 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. SAT gehört zur Klasse ? Das Erfüllbarkeitsproblem der Aussagenlogik ist NP-vollständig. Das besagt, dass jedes Problem aus Falls also auch in nicht gilt. (de)
|
