Problema de satisfacibilidad booleano
En lógica y ciencias de la computación , 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 satisface una fórmula booleana dada . En otras palabras, pregunta si las variables de una fórmula booleana dada pueden ser reemplazadas consistentemente por los valores VERDADERO o FALSO de tal manera que la fórmula se evalúe como VERDADERA . Si este es el caso, la fórmula se llama satisfactoria. Por otro lado, si no existe tal asignación, la función expresada por la fórmula es FALSA para todas las asignaciones de variables posibles 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 AND NOT a " no es satisfactorio.
SAT es el primer problema que demostró ser NP-completo ; consulte el teorema de Cook-Levin . Esto significa que todos los problemas en la clase de complejidad NP , que incluye una amplia gama de problemas de optimización y decisión naturales, son como mucho tan difíciles de resolver como SAT. No existe un algoritmo conocido que resuelva de manera eficiente cada problema SAT, y generalmente se cree que no existe tal algoritmo; sin embargo, esta creencia no ha sido probada 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 casos de problemas que involucran decenas de miles de variables y fórmulas que constan de millones de símbolos, [1] lo cual es suficiente para muchos problemas SAT prácticos 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 Y ( conjunción , también denotada por ∧), OR ( disyunción , ∨), NOT ( negación , ¬) y paréntesis. Se dice que una fórmula es satisfactoria si se puede convertir en VERDADERA asignando valores lógicos apropiados (es decir, VERDADERO, FALSO) a sus variables. El problema de satisfacibilidad booleano (SAT) es, dada una fórmula, para comprobar si es satisfactorio. Este problema de decisión es de importancia central en muchas áreas de la informática , incluida lainformática teórica , teoría de la complejidad , [3] [4] algoritmos , criptografía [5] [6] e inteligencia artificial . [7] [ cita (s) adicional (es) necesarias ]
Hay varios casos especiales del problema de satisfacibilidad booleano en los que se requiere que las fórmulas tengan una estructura particular. Un literal es una variable, llamada literal positiva , o la negación de una variable, llamada literal negativa . Una cláusula es una disyunción de literales (o un solo literal). Una cláusula se denomina cláusula Horn si contiene como máximo un literal positivo. Una fórmula está en forma conjuntiva normal (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 normal conjuntiva; su primera y tercera cláusulas son cláusulas de 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, y a 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, no es satisfactoria, ya que para a = TRUE o a = FALSE se evalúa como TRUE ∧ ¬TRUE (es decir, FALSE) o FALSE ∧ ¬FALSE (es decir , nuevamente FALSO), respectivamente.
