Visión general

El problema de satisfacibilidad booleana, normalmente llamado SAT, pregunta si existe una asignación de valores de verdad (verdadero o falso) para las variables de una fórmula de lógica proposicional que haga que toda la fórmula evalúe como verdadera. Si existe tal asignación, la fórmula se llama satisfacible; si ninguna asignación la hace verdadera, la fórmula es insatisfacible. SAT es un problema de decisión: para cada fórmula de entrada devuelve sí o no.

Formulación y conceptos básicos

Las fórmulas suelen escribirse en forma normal conjuntiva (FNC): una conjunción (AND lógico) de cláusulas, donde cada cláusula es una disyunción (OR lógico) de literales, y un literal es una variable (x) o su negación (¬x). Un ejemplo de FNC es: (x O ¬y O z) Y (¬x O y) Y (z O w O ¬y). Una asignación satisfactoria elige valores verdadero/falso para cada variable de modo que cada cláusula contenga al menos un literal verdadero.

Variantes y casos especiales

  • k-SAT: Cada cláusula tiene como máximo k literales. 3-SAT, donde las cláusulas tienen tres literales, es una variante canónica NP-completa.
  • 2-SAT: Cada cláusula tiene como máximo dos literales. 2-SAT se puede resolver en tiempo polinómico; existen algoritmos lineales.
  • Horn-SAT: Fórmulas en FNC en las que cada cláusula tiene como máximo un literal positivo; Horn-SAT también se resuelve en tiempo lineal y es importante en programación lógica.
  • Max-SAT: Una versión de optimización que busca una asignación que satisfaga el mayor número posible de cláusulas.

Complejidad e historia

SAT fue el primer problema demostrado NP-completo: el teorema de Cook-Levin (hacia 1971) mostró que cualquier problema de NP puede transformarse en SAT en tiempo polinómico. Esto estableció SAT como el problema de decisión NP-completo canónico. Poco después, muchos otros problemas combinatorios naturales se demostraron NP-completos, y 3-SAT se convirtió en una instancia difícil estándar usada en reducciones y pruebas de complejidad.

Algoritmos y resolución práctica

A pesar de su complejidad exponencial en el peor caso, los solucionadores SAT modernos manejan instancias muy grandes surgidas en la práctica. Los métodos completos clásicos se basan en el marco de retroceso DPLL (Davis-Putnam-Logemann-Loveland), mejorado con propagación unitaria y eliminación de literales puros. Los solucionadores contemporáneos usan aprendizaje de cláusulas guiado por conflictos (CDCL), heurísticas sofisticadas de ramificación, reinicios y preprocesamiento. También existen heurísticas incompletas y métodos de búsqueda local que funcionan bien en muchos conjuntos de prueba.

Aplicaciones y datos destacados

SAT se usa ampliamente para codificar problemas de verificación de hardware y software, planificación, programación, diseño combinatorio y razonamiento automatizado. Muchas tareas de verificación se traducen a SAT para aprovechar solucionadores eficientes. Entre las áreas de investigación están la construcción de conjuntos de prueba, las competiciones SAT y el estudio de instancias aleatorias de SAT, que muestran transiciones de fase entre regímenes satisfacibles e insatisfacibles. El éxito práctico de los solucionadores SAT hace del problema tanto una base teórica como una poderosa herramienta de ingeniería.

Distinciones y conceptos relacionados

SAT pertenece a la lógica proposicional; su extensión a las fórmulas booleanas cuantificadas (QBF) eleva la complejidad a clases superiores dentro de la jerarquía polinómica. La satisfacibilidad debe distinguirse de la consecuencia lógica: SAT pregunta por la existencia de un modelo que satisfaga una fórmula, mientras que la consecuencia lógica pregunta si todo modelo de una fórmula también satisface otra. Comprender estas relaciones es fundamental en lógica, teoría de la complejidad y deducción automatizada.