In computer science, satisfiability (often written in all capitals or abbreviated SAT) is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE. Equally important is to determine whether no such assignments exist, which would imply that the function expressed by the formula is identically FALSE for all possible variable assignments.

PropertyValue
dbpedia-owl:abstract
  • 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 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. 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 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. Dieser Annahme zu folgen, bedeutet nichts anderes, als die Überzeugung vieler Mathematiker, dass nicht gilt, zu teilen.
  • In computer science, satisfiability (often written in all capitals or abbreviated SAT) is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE. Equally important is to determine whether no such assignments exist, which would imply that the function expressed by the formula is identically FALSE for all possible variable assignments. In this latter case, we would say that the function is unsatisfiable; otherwise it is satisfiable. To emphasize the binary nature of this problem, it is frequently referred to as Boolean or propositional satisfiability. SAT was the first known example of an NP-complete problem. That briefly means that there is no known algorithm that efficiently solves all instances of SAT, and it is generally believed that no such algorithm can exist. Further, a wide range of other naturally occurring decision and optimization problems can be transformed into instances of SAT. A class of algorithms called SAT solvers can efficiently solve a large enough subset of SAT instances to be useful in various practical areas such as circuit design and automatic theorem proving, by solving SAT instances made by transforming problems that arise in those areas. Extending the capabilities of SAT solving algorithms is an ongoing area of progress. However, no current such methods can efficiently solve all SAT instances.
  • En teoría de la complejidad computacional, el Problema de satisfacibilidad booleana (tambien llamado SAT) fue el primer problema identificado como perteneciente a la clase de complejidad NP-completo.
  • Quello della Soddisfacibilità è il problema di determinare se le variabili di una data formula booleana possano essere assegnate in modo che la formula sia valutata "TRUE". Ugualmente importante è individuare che tale assegnamento non esiste, arrivando a concludere che la funzione espressa dalla formula è identicamente "FALSE" per tutti i possibili assegnamenti delle sue variabili. In quest'ultimo caso si dice che la funzione è insoddisfacibile; altrimenti, soddisfacibile. Per enfatizzare la natura binaria di tale problema, ad esso ci si riferisce spesso come al problema di soddisfacibilità booleana o soddisfacibilità proposizionale. Il diminuitivo "SAT" è una sigla comunemente utilizzata per denotare tale problema, dove si intende implicitamente che la funzione e le sue variabili sono tutte valutate in modo binario.
  • 充足可能性問題（じゅうそくかのうせいもんだい、satisfiability problem, SAT）は、一つの乗法標準形 (CNF) が与えられたとき、それに含まれるすべての変数の値を偽 (False) あるいは真 (True) にうまく定めることによって全体の値を'真'にできるか、という問題をいう。SATisfiabilityの頭3文字を取ってしばしば「SAT」と呼ばれる。
  • In de complexiteitstheorie verwijst het vervulbaarheidsprobleem (ook bekend als SAT, van het Engelse satisfiability) naar het bepalen of een logische propositie vervuld kan worden; een propositie kan vervuld worden als er een toekenning van waar of onwaar aan de atomaire formules bestaat zodanig dat de gehele propositie waar is.
  • Problem spełnialności to pytanie rachunku zdań - czy dla danej formuły logicznej istnieje takie podstawienie (wartościowanie) zmiennych zdaniowych, żeby formuła była prawdziwa. Jest równoważne negacji pytania czy "negacja tej formuły jest tautologią". Problem spełnialności jest rozstrzygalny - można wypróbować wszystkich podstawień których jest, gdzie to liczba zmiennych w formule. Metoda ta ma więc złożoność wykładniczą. Szczególnie ciekawy jest problem spełnialności formuł w koniunkcyjnej postaci normalnej (ang. CNF - conjunctional normal form), których klauzule mają nie więcej niż k literałów (k-SAT). Literałem nazywamy zmienną lub zmienną zanegowaną, klauzulą nazywamy alternatywę literałów, natomiast formuła to koniunkcja klauzul. 1-SAT i 2-SAT mają rozwiązania w P, czyli w deterministycznym czasie wielomianowym, natomiast już 3-SAT jest NP-zupełny, czyli takim, że każdy problem z klasy NP jest do niego redukowalny przy pomocy redukcji w czasie wielomianowym.
  • Na teoria da complexidade computacional, o problema de satisfazibilidade booleana (SAT) foi o primeiro problema identificado como pertencente à classe de complexidade NP-completo. O Problema de satisfazibilidade Booleana é o problema de determinar se existe uma determinada valoração para as variáveis de uma determinada fórmula booleana tal que esa valoração satisfaça esta fórmula em questão. Por exemplo, tomando como as variáveis booleanas e a expressão, caso exista uma atribuição de valores de verdade para as variáveis da fórmula que torne a fórmula avaliada VERDADEIRA, esta fórmula é considera satisfazível, em contrapartida se nenhuma atribuição levou a uma avaliação da fórmula como verdadeira, ela é considerada insatisfazível. Para salientar a natureza binária deste problema, ele é referenciado freqüentemente como o problema de satisfazibilidade booleana ou proposicional. A sigla SAT também é geralmente utilizada para denotá-lo, com o entendimento implícito de que a função e suas variáveis recebem valores binários.
  • Зада́ча выполни́мости бу́левых фо́рмул (SAT или ВЫП) — важная для теории вычислительной сложности алгоритмическая задача. Экземпляром задачи SAT является булева формула, состоящая только из имен переменных, скобок и операций (И), (ИЛИ) и (HE). Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной. Согласно теореме Кука, доказанной Стивеном Куком в 1971-м году, задача SAT для булевых формул, записанных в конъюнктивной нормальной форме, является NP-полной. Требование о записи в конъюнктивной форме существенно, так как, например, задача SAT для формул, представленных в дизъюнктивной нормальной форме, тривиально решается за линейное время от размера записи формулы.
  • 可滿足性（英語：Satisfiability）是用來解決給定的布林方程式，是否存在一组变量赋值，使問題为可满足。布林可滿足性問題（Boolean satisfiability problem；SAT)）屬於決定性問題，是第一个被证明NP完全问题。為電腦科學上許多領域的重要問題，包括電腦科學基礎理論、演算法、人工智慧、硬體設計等等。
  • On nomme problème SAT un problème de décision visant à savoir s'il existe une solution à une série d'équations logiques données. En termes plus précis : une évaluation sur un ensemble de variables propositionnelles telle qu'une formule propositionnelle donnée soit alors logiquement vraie. Ce problème est très important en théorie de la complexité et a de nombreuses applications en planification classique, model checking, diagnostic, et jusqu'au configurateur d'un PC ou de son système d'exploitation. Le terme SAT est repris de l'anglais : Modèle:Lang.
dbpedia-owl:wikiPageExternalLink
dcterms:subject
rdf:type
rdfs:comment
  • En teoría de la complejidad computacional, el Problema de satisfacibilidad booleana (tambien llamado SAT) fue el primer problema identificado como perteneciente a la clase de complejidad NP-completo.
  • 充足可能性問題（じゅうそくかのうせいもんだい、satisfiability problem, SAT）は、一つの乗法標準形 (CNF) が与えられたとき、それに含まれるすべての変数の値を偽 (False) あるいは真 (True) にうまく定めることによって全体の値を'真'にできるか、という問題をいう。SATisfiabilityの頭3文字を取ってしばしば「SAT」と呼ばれる。
  • In de complexiteitstheorie verwijst het vervulbaarheidsprobleem (ook bekend als SAT, van het Engelse satisfiability) naar het bepalen of een logische propositie vervuld kan worden; een propositie kan vervuld worden als er een toekenning van waar of onwaar aan de atomaire formules bestaat zodanig dat de gehele propositie waar is.
  • 可滿足性（英語：Satisfiability）是用來解決給定的布林方程式，是否存在一组变量赋值，使問題为可满足。布林可滿足性問題（Boolean satisfiability problem；SAT)）屬於決定性問題，是第一个被证明NP完全问题。為電腦科學上許多領域的重要問題，包括電腦科學基礎理論、演算法、人工智慧、硬體設計等等。
  • 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.
  • In computer science, satisfiability (often written in all capitals or abbreviated SAT) is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE. Equally important is to determine whether no such assignments exist, which would imply that the function expressed by the formula is identically FALSE for all possible variable assignments.
  • Quello della Soddisfacibilità è il problema di determinare se le variabili di una data formula booleana possano essere assegnate in modo che la formula sia valutata "TRUE". Ugualmente importante è individuare che tale assegnamento non esiste, arrivando a concludere che la funzione espressa dalla formula è identicamente "FALSE" per tutti i possibili assegnamenti delle sue variabili. In quest'ultimo caso si dice che la funzione è insoddisfacibile; altrimenti, soddisfacibile.
  • Problem spełnialności to pytanie rachunku zdań - czy dla danej formuły logicznej istnieje takie podstawienie (wartościowanie) zmiennych zdaniowych, żeby formuła była prawdziwa. Jest równoważne negacji pytania czy "negacja tej formuły jest tautologią". Problem spełnialności jest rozstrzygalny - można wypróbować wszystkich podstawień których jest, gdzie to liczba zmiennych w formule. Metoda ta ma więc złożoność wykładniczą.
  • Na teoria da complexidade computacional, o problema de satisfazibilidade booleana (SAT) foi o primeiro problema identificado como pertencente à classe de complexidade NP-completo. O Problema de satisfazibilidade Booleana é o problema de determinar se existe uma determinada valoração para as variáveis de uma determinada fórmula booleana tal que esa valoração satisfaça esta fórmula em questão.
  • Зада́ча выполни́мости бу́левых фо́рмул (SAT или ВЫП) — важная для теории вычислительной сложности алгоритмическая задача. Экземпляром задачи SAT является булева формула, состоящая только из имен переменных, скобок и операций (И), (ИЛИ) и (HE). Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной.
  • On nomme problème SAT un problème de décision visant à savoir s'il existe une solution à une série d'équations logiques données. En termes plus précis : une évaluation sur un ensemble de variables propositionnelles telle qu'une formule propositionnelle donnée soit alors logiquement vraie.
rdfs:label
  • Erfüllbarkeitsproblem der Aussagenlogik
  • Boolean satisfiability problem
  • Problema de satisfacibilidad booleana
  • Problème SAT
  • Soddisfacibilità booleana
  • 充足可能性問題
  • Vervulbaarheidsprobleem
  • Problem spełnialności
  • Problema de satisfatibilidade booleana
  • Задача выполнимости булевых формул
  • 布尔可满足性问题
owl:sameAs
foaf:page
is dbpedia-owl:wikiPageDisambiguates of
is dbpedia-owl:wikiPageRedirects of
is owl:sameAs of
is foaf:primaryTopic of