Problema booleano de satisfacibilidad
En lógica e informática , el problema de satisfacibilidad booleano (a veces llamado problema de satisfacibilidad proposicional y abreviado SATISFIABILIDAD , SAT o B-SAT ) es el problema de determinar si existe una interpretación que satisfaga una fórmula booleana determinada . En otras palabras, pregunta si las variables de una fórmula booleana determinada pueden reemplazarse consistentemente por los valores VERDADERO o FALSO de tal manera que la fórmula se evalúe como VERDADERO. Si este es el caso, la fórmula se llama satisfacible. Por otro lado, si no existe tal asignación, la función expresada por la fórmula es FALSA para todas las posibles asignaciones de variables y la fórmula es insatisfactoria . Por ejemplo, la fórmula " a Y NO b " es satisfactoria porque uno puede encontrar los valores a = VERDADERO yb = FALSO, que hacen ( a Y NO b ) = VERDADERO. Por el contrario, " a Y NO a " es insatisfactorio.
SAT es el primer problema que demostró ser NP-completo ; véase el teorema de Cook-Levin . Esto significa que todos los problemas de la clase de complejidad NP , que incluye una amplia gama de problemas de optimización y de decisión natural, son como máximo tan difíciles de resolver como SAT. No existe un algoritmo conocido que resuelva de manera eficiente cada problema del SAT y, en general, se cree que dicho algoritmo no existe; sin embargo, esta creencia no se ha probado matemáticamente, y resolver la cuestión de si SAT tiene un algoritmo de tiempo polinomial es equivalente al problema P versus NP , que es un famoso problema abierto en la teoría de la computación.
Sin embargo, a partir de 2007, los algoritmos SAT heurísticos pueden resolver instancias de problemas que involucran decenas de miles de variables y fórmulas que consisten en millones de símbolos, [1] lo cual es suficiente para muchos problemas prácticos de SAT de, por ejemplo, inteligencia artificial , diseño de circuitos , [2] y demostración automática de teoremas .
Una fórmula lógica proposicional , también llamada expresión booleana , se construye a partir de variables , operadores AND ( conjunción , también denotada por ∧), OR ( disyunción , ∨), NOT ( negación , ¬) y paréntesis. Se dice que una fórmula es satisfactoria si puede hacerse VERDADERA asignando valores lógicos apropiados (es decir, VERDADERO, FALSO) a sus variables. El problema booleano de satisfacibilidad (SAT) es, dada una fórmula, para comprobar si es satisfacible. Este problema de decisión es de importancia central en muchas áreas de las ciencias de la computación , incluyendoinformática teórica , teoría de la complejidad , [3] [4] algorítmica , criptografía [5] [6] e inteligencia artificial . [7] [ cita(s) adicional(es) necesaria(s) ]
Un literal es una variable, llamada literal positivo , o la negación de una variable, llamada literal negativo . Una cláusula es una disyunción de literales (o un solo literal). Una cláusula se llama cláusula Horn si contiene como máximo un literal positivo. Una fórmula está en forma normal conjuntiva (CNF) si es una conjunción de cláusulas (o una sola cláusula). Por ejemplo, x 1 es un literal positivo, ¬ x 2 es un literal negativo, x 1 ∨ ¬ x 2 es una cláusula. La fórmula ( x 1 ∨ ¬x 2 ) ∧ (¬ x 1 ∨ x 2 ∨ x 3 ) ∧ ¬ x 1 está en forma conjuntiva normal; sus cláusulas primera y tercera son cláusulas Horn, pero su segunda cláusula no lo es. La fórmula es satisfactoria, eligiendo x 1 = FALSO, x 2 = FALSO y x 3 arbitrariamente, ya que (FALSO ∨ ¬FALSO) ∧ (¬FALSO ∨ FALSO ∨ x 3 ) ∧ ¬FALSO se evalúa como (FALSO ∨ VERDADERO) ∧ (VERDADERO ∨ FALSO ∨ x 3 ) ∧ VERDADERO, ya su vez a VERDADERO ∧ VERDADERO ∧ VERDADERO (es decir, a VERDADERO). Por el contrario, la fórmula CNF a ∧ ¬ a, que consta de dos cláusulas de un literal, es insatisfactoria, ya que =VERDADERO o =FALSO se evalúa como VERDADERO ∧ ¬VERDADERO (es decir, FALSO) o FALSO ∧ ¬FALSO (es decir, nuevamente FALSO), respectivamente.
