El mecanismo algorítmico que asigna de forma iterativa los valores implicados por cláusulas unitarias en un conjunto de cláusulas proposicionales para simplificar la instancia y detectar conflictos; comúnmente llamado Propagación de Restricciones Booleanas (BCP).

Principio

Si una cláusula se convierte en unitaria (solo un literal no asignado), ese literal debe fijarse a verdadero para satisfacer la cláusula; propagar esa asignación por el conjunto de cláusulas, simplificar cláusulas y repetir hasta punto fijo o conflicto.

Demostración

Dadas las cláusulas { {p}, {¬p, q}, {¬q} }, propagar p=true desde {p}; esto satisface {¬p, q} que puede eliminarse, quedando {¬q} que fuerza q=false; la secuencia de propagaciones unitarias simplifica la instancia y muestra consistencia o conflicto.

Aplicación incorrecta

Aplicar propagación unitaria a fórmulas que no se han reducido a forma de cláusulas sin tener en cuenta la estructura introducida, o asumir que la propagación preserva otras propiedades como alcance de cuantificadores o restricciones específicas de teoría.

Consecuencia

La propagación unitaria reduce rápidamente el espacio de búsqueda, detecta contradicciones tempranamente y es una inferencia de bajo coste que sustenta la eficiencia de resolución en SAT y el podado en marcos DPLL/CDCL.

Inversión

Omitir la propagación y solo ramificar en variables obliga a una exploración combinatoria de asignaciones que la propagación unitaria habría podado, incrementando típicamente la búsqueda de forma exponencial.

Límite

Definida para conjuntos de cláusulas proposicionales en CNF; las extensiones a teorías más ricas requieren propagación específica de la teoría (por ejemplo congruencia, aritmética lineal) y la implementación debe ser cuidadosa para mantener la corrección.

Tensión semántica

La propagación unitaria se confunde a menudo con la propagación de restricciones general o la simplificación booleana completa; es una inferencia sintáctica estrecha, impulsada por unidades, cuya fuerza depende de la estructura de cláusulas y estructuras de datos del solver (watched literals).

Síntesis

La propagación unitaria es el proceso determinista e iterativo de asignar y propagar literales forzados por cláusulas unitarias para simplificar cláusulas y detectar conflictos, formando la columna vertebral inferencial de los procedimientos SAT modernos.