Un procedimiento de búsqueda recursiva con retroceso para la satisfacibilidad proposicional que integra división de variables, propagación de unidades (propagación de restricciones booleanas), eliminación de literales puros y retroceso sistemático para decidir si una fórmula en CNF es satisfacible.

Principio

Reducir la búsqueda derivando asignaciones forzadas (propagación de unidades) y eliminando elecciones obvias (literales puros), ramificar sobre variables solo cuando sea necesario y retroceder ante contradicciones para explorar un árbol de búsqueda exponencial pero susceptible de poda.

Demostración

Para decidir la satisfacibilidad de (A ∨ B) ∧ (¬A ∨ C) ∧ (¬B ∨ ¬C), el algoritmo aplica propagación de unidades cuando aparecen cláusulas unitarias, elige un literal de ramificación (por ejemplo A), explora recursivamente A = verdadero y A = falso, y retrocede si se encuentra una contradicción hasta hallar una asignación satisfactoria o probar la insatisfacibilidad.

Aplicación incorrecta

Tratar DPLL como una búsqueda puramente codiciosa sin mantener ni aplicar propagación de unidades o aprendizaje de cláusulas conduce a una exploración redundante y a un empeoramiento severo del rendimiento en muchas instancias SAT.

Consecuencia

Aplicado correctamente, DPLL puede decidir muchas instancias SAT prácticas de forma eficiente podando grandes porciones del espacio de búsqueda; constituye la base de los solucionadores SAT modernos y habilita mejoras basadas en conflictos.

Inversión

Invertir el concepto realizando una enumeración exhaustiva y ciega de todas las asignaciones sin propagación ni heurísticas de retroceso; esto mantiene corrección pero pierde poda escalable y explotación de la estructura.

Límite

Se aplica a la lógica proposicional en CNF y a procedimientos de decisión centrados en la estructura booleana; no maneja por sí solo teorías con funciones interpretadas (SMT) salvo que se combine con razonamiento específico de teoría.

Tensión semántica

Compite con procedimientos puramente resolutivos o algebraicos: la resolución deriva consecuencias globalmente mediante combinación de cláusulas, mientras DPLL enfatiza la búsqueda con propagación local y decisiones de ramificación.

Síntesis

DPLL integra deducción lógica local (propagación de unidades y eliminación de literales puros) con búsqueda sistemática y retroceso para convertir la resolución SAT en una exploración controlable de un árbol de asignaciones podable, constituyendo el andamiaje algorítmico de los procedimientos proposicionales modernos.