Algoritmos, estructuras de datos y procedimientos para determinar si una fórmula booleana proposicional (típicamente en CNF) es satisfacible y para producir una asignación satisfactoria cuando existe; la resolución SAT moderna incluye DPLL, CDCL, heurísticas, aprendizaje de cláusulas, reinicios y preprocesado.

Principio

Buscar sistemáticamente una asignación booleana que satisfaga todas las cláusulas mediante búsqueda con backtracking (estilo DPLL), aumentada por aprendizaje de cláusulas dirigido por conflictos (CDCL), propagación de unidades, heurísticas de selección de variables y registro de pruebas o núcleos insatisfactibles para mejorar la eficiencia y aportar evidencia de insatisfactibilidad.

Demostración

Dada una instancia CNF que codifica una restricción de planificación, un solver CDCL realiza propagación de unidades para deducir asignaciones forzadas, ramifica sobre una variable elegida, registra cláusulas aprendidas en los conflictos para evitar repetir asignaciones parciales erróneas y finalmente devuelve una asignación completa que satisface todas las cláusulas o una prueba de insatisfactibilidad.

Aplicación incorrecta

Proporcionar a un solver SAT un problema sin una codificación apropiada (perdiendo la semántica), esperar un comportamiento polinómico en el peor caso sobre instancias NP‑completas, o interpretar erróneamente el resultado 'unknown' o un time‑out como satisfacible o insatisfacible sin un análisis posterior.

Consecuencia

Los solvers SAT ofrecen motores muy eficaces para muchos problemas NP prácticos mediante codificaciones (planificación, verificación, síntesis), generan modelos concretos para instancias satisfacibles y pueden aportar pruebas de resolución o núcleos insat para casos insat; escalan bien en la práctica a pesar de la dureza teórica.

Inversión

Contar soluciones (#SAT) o resolver fórmulas booleanas cuantificadas (QBF) invierte la tarea de SAT abordando la enumeración o alternancias de cuantificadores adicionales; ambos son estrictamente más difíciles y requieren algoritmos y consideraciones de complejidad diferentes.

Límite

Se aplica a la lógica proposicional; los problemas deben codificarse (a menudo en CNF) y la eficacia del solver depende mucho de la calidad de la codificación y de las heurísticas. SAT solving es decidible y completo para la proposicional pero no maneja teorías directamente (usar SMT para razonamiento en teorías).

Tensión semántica

Existe tensión entre SAT y la programación por restricciones o SMT: SAT se apoya en codificaciones booleanas y aprendizaje de cláusulas, mientras CP usa dominios más ricos y propagación; SMT extiende SAT integrando teorías, intercambiando rendimiento booleano por expresividad.

Síntesis

SAT solving es un enfoque maduro y muy orientado a la ingeniería para decidir satisfacibilidad proposicional: combina búsqueda sistemática con potentes mecanismos de inferencia y aprendizaje para producir asignaciones o pruebas, y sirve como motor para muchas tareas de razonamiento de nivel superior mediante codificación.