| dbpprop:abstract
|
- Satisfiability 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. The shorthand "SAT" is also commonly used to denote it, with the implicit understanding that the function and its variables are all binary-valued.
- 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 <math>\mathcal{NP}</math> 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 <math>\mbox{SAT} \in \mathcal{P}</math>? Das Erfüllbarkeitsproblem der Aussagenlogik ist NP-vollständig. Das besagt, dass jedes Problem aus <math>\mathcal{NP}</math> 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 <math>\mbox{SAT} \in \mathcal{P}</math> gilt, dann ist jedes Problem aus <math>\mathcal{NP}</math> auch in <math>\mathcal{P}</math>, das heißt, dann gilt <math>\mathcal{P} = \mathcal{NP}</math>. Auch die umgekehrte Richtung der Implikation gilt. Das P-NP-Problem "gilt <math>\mathcal{P} = \mathcal{NP}</math> 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.
- En teoría de la complejidad computacional, el Problema de satisfacibilidad booleana (SAT) fue el primer problema identificado como perteneciente a la clase de complejidad NP-completo. Se trata de un problema donde interesa saber si una expresión booleana con variables y sin cuantificadores tiene asociada una asignación de valores para sus variables que hace que la expresión sea verdadera. Por ejemplo, una instancia de SAT sería el saber si existen valores para <math>x_1,\, x_2, \, x_3, \, x_4</math> tales que la expresión: <math> (x_1 \or \neg x_3 \or x_4) \and (\neg x_2 \or x_3 \or \neg x_4)</math> es cierta. El SAT es el primer problema NP-completo conocido, y fue demostrado por Stephen Cook en 1971. Hasta entonces, el concepto de un problema NP-completo, no estaba definido. El SAT problema sigue siendo NP-completo, incluso si todas las fórmulas están en forma normal conjuntiva (FNC) con 3 variables por cláusula (3SAT-FNC) creando el problema (3SAT), o aun inclusive, en el caso en que solo se permita un solo valor verdadero en cada clusula (3SAT en 1). El problema sigue perteneciendo a la clase de complejidad NP-completo aunque se restrinja el número de literales por claúsula a un máximo de 3. En este caso se conoce como 3 SAT. Cuando el número máximo de literales por cláusula es dos, el problema tiene complejidad polinómica y se conoce como problema 2 SAT. El Teorema de Cook demuestra que el problema de la satisfatibilidade booleana es NP-completo, y de hecho, este fue el primer problema de decisión que se demostró ser NP-completos. Sin embargo, más allá de este teorema, algoritmos eficientes y resistentes al cambio de tamaño del problema para SAT se han desarrollado desde la última década y han contribuido con poderosos avances en nuestra capacidad para resolver el problema de satisfactibilidad automáticamente. La 3-satisfactibilidad es un caso especial de -satisfactibilidad (-SAT), o simplemente satisfactibilidad (SAT), en la que cada cláusula contiene exactamente = 3 literales. Fue uno de 21 problemas NP-completos de Karp. Partiendo de SAT (el caso general) se reduce a 3-SAT y SAT 3 -en 1 y se puede demostrar que son NP-completos, entonces podemos usarlos para demostrar también otros problemas NP-completos. Esto se hace mostrando cómo una solución a otro problema podría ser utilizado para resolver 3-SAT Un ejemplo de este tipo de reduccion es el problema del Clique. Por lo general, es más fácil de utilizar reducción de 3-SAT que con duando se está tratando de probar que algun otro porblema es NP-completo. El SAT 3-puede ser más limitado a la 3SAT Uno-en-tres, cuando lo que pedimos sea sólo una de las variables verdadera en cada cláusula, en vez de por lo menos una. 3SAT Uno-en-tres sigue siendo NP-completo. Extensiones de SAT Una extensión significativa a la popularidad que ganó desde 2003 es el problema de las teorías satisfactibilidad módulo, que permite enriquecer las fórmulas en la FNC con lineales, vectores, la restricción de que todas las variables sean distintas, y no interpretar funciones, etc. Estas extensiones son típicamente NP-completas, pero resultan bastante eficaces para la resolución que son capaces de hacer frente a muchos tipos de restricciones de género. El problema parece ser más difícil satisfactibilidad (PSPACE-completo) si permitimos que los cuantificadores "para todos" y "existencial", que enlace las variables booleanas. Si se utiliza sólo cuantificadores Este sigue siendo el problema SAT Si permitimos que sólo los cuantificadores Se convierte en el problema de la tautología: Co-NP-completo. Si dejamos que ellos, el problema se llama el problema de la fórmula booleana cuantificados (QBF), que puede se ha demostrado PSPACE completa. Se cree ampliamente que los problemas son PSPACE completa-es son más difíciles que cualquier problema en NP, aunque esto aún no ha sido demostrada. . El problema de la máxima satisfactibilidad, una generalización de SAT, para pedir el número máximo de cláusulas que pueden ser satisfechas por ninguna asignación. Este problema tiene aproximación de con algoritmos eficientes, sino que es NP-difícil de resolver con precisión. Peor aún, el problema es APX-completo, lo que significa que no hay ningún sistema de aproximación polinomial de tiempo a este problema a menos que P = NP. Hay diversas clases de algoritmos de alto rendimiento para la solución de los casos de SAT en la práctica: las variantes modernas de el Algoritmo DPLL, como el algoritmo de paja y los algoritmos estocásticos de búsqueda local, como WalkSAT. Una resolución del tipo SAT Algoritmo DPLL emplea un procedimiento sistemático de rastreo para buscar a explorar el espacio (del tamaño exponencial) los valores de las variables que se ajusten. El procedimiento básico de este sistema de búsqueda fue innovador en dos artículos a principios de los años 60 y es, hoy en día, normalmente se conoce como el algoritmo de Davis-Putnam-Loveland-Logemann Algoritmo DPLL. El solucionador SAT moderno (desarrollado en los últimos diez años), mejora el algoritmo de base para encontrar el tipo de Algoritmo DPLL. eficiente con el análisis de conflictos, la cláusula de aprendizaje, no cronológico de rastreo (alias backjumping) y la propagación de la unidad " vieron dos literales "(Dos vistos literales), brazo ajustable, y reinicios aleatorios. Es empíricamente que tales "añadidos" a la búsqueda sistemática de base son esenciales para resolver el problema de casos SAT extensos que se plantean en la automatización de diseño electrónico. Los modernos solucionadores SAT también están causando un impacto significativo en los ámbitos de la verificación de software, la resolución de las limitaciones en la inteligencia artificial, y la investigación operativa, entre otros. Algunos salocucionadores potente disponibles entan en el dominio público, y son muy fáciles de usar. En particular, el MINISAT, que ganó la competencia de la SAT de 2005, sólo alrededor de 600 líneas de código. Algoritmos Genéticos y otros métodos estocásticos de búsqueda local para el uso general también se utilizan para resolver problemas SAT, especialmente cuando no hay o sólo un conocimiento limitado de la estructura específica de los casos del problema a ser resuelto. Ciertos tipos de casos al azar satisfatíveis largo de la SAT se puede resolver por la propagación de la vio literales. En particular en el diseño y verificación de hardware, la lógica satisfactibilidad y otras propiedades de una fórmula proposicional a veces se decidió sobre la base de una representación de la fórmula como un diagrama de decisión binario (BDD). La satisfactibilidad proposicional tiene varias generalizaciones, incluyendo satisfactibilidad al problema de la fórmula booleana cuantificados para la lógica clásica de primer y segundo orden (LCPO y LCSO, respectivamente), a los problemas de la satisfacción de las limitaciones para la programación de enteros 0 -- 1, y el problema de la satisfactibilidad máximo. Muchos otros problemas de la decisión, como los problemas de coloración de grafos, problemas de planificación y programación de problemas, puede ser codificado en SAT
- 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 simple PC ou de son système d'exploitation.
- 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) にうまく定めることによって全体の値を'真'にできるか、という問題をいう。SATisfabilityの頭3文字を取ってしばしば「SAT」と呼ばれる。
- 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 <math>2^N</math>, gdzie <math>N</math> to ilość 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.
- Задача выполнимости булевых формул (SAT или ВЫП) — задача распознавания, важная для теории вычислительной сложности. Экземпляром задачи SAT является булева формула, состоящая только из имен переменных, скобок и операций <math>\wedge</math> (И), <math>\vee</math> (ИЛИ) и <math>\neg</math> (HE). Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ЛОЖЬ и ИСТИНА так, чтобы формула стала истинной. Согласно теореме Кука, доказанной Стивеном Куком в 1971-м году, задача SAT NP-полна.
- Зада́ча здійсни́мості бу́льових фо́рмул (SAT) — задача розпізнавання образів, важлива для теорії обчислювальної складності. Об'єктом задачи SAT є булева формула, що складається тільки з імен змінних, дужок і операцій <math>\wedge</math> (І), <math>\vee</math> (АБО) і <math>\neg</math> (HІ). Задача полягає в наступному: чи можна призначити всім змінним, що зустрічаються у формулі, значення НЕВІРНО і ВІРНО так, щоб формула стала істинною. Згідно теоремі Кука, доведеною Стивеном Куком в 1971-му році, проблема SAT є NP-повною.
- 可滿足性（英語：Satisfiability）是用來解決給定的布林方程式，是否存在一组变量赋值，使問題为可满足。布林可滿足性問題（Boolean satisfiability problem；SAT)）屬於決定性問題，是第一个被证明NP完全问题。為電腦科學上許多領域的重要問題，包括電腦科學基礎理論、演算法、人工智慧、硬體設計等等。
|
![[RDF Data]](/statics/sw-cube.png)
