Tengo problemas para comprender el algoritmo DPLL y me preguntaba si alguien me lo podría explicar porque creo que mi comprensión es incorrecta.

Según tengo entendido, tomo un conjunto de literales y si alguna de las cláusulas es verdadera, el modelo es verdadero, pero si alguna cláusula es falsa, entonces el modelo es falso.

Compruebo el modelo de forma recursiva buscando una cláusula de unidad, si hay una establezco el valor de esa cláusula de unidad para que sea verdadera, luego actualizo el modelo. Eliminar todas las cláusulas que ahora son verdaderas y eliminar todos los literales que ahora son falsos.

Cuando no quedan cláusulas unitarias, elijo cualquier otro literal y asigno valores para ese literal que lo hagan verdadero y lo haga falso, luego elimine nuevamente todas las cláusulas que ahora son verdaderas y todos los literales que ahora son falsos.