Определение алгоритма DPLL

У меня проблемы с пониманием алгоритма DPLL, и мне было интересно, может ли кто-нибудь объяснить его мне, потому что я думаю, что мое понимание неверно.

То, как я понимаю, что это так, я беру некоторый набор литералов, и если некоторые из предложений истинны, модель истинна, но если какое-то предложение ложно, тогда модель ложна.

Я рекурсивно проверяю модель, ища предложение единицы, если есть это один Я устанавливаю значение для этого предложения unit, чтобы оно стало истинным, а затем обновляю модель. Удаление всех предложений, которые теперь истинны, и всех литералов, которые теперь ложны.

Когда не осталось предложений единиц, я выбрал любой другой литерал и присвоил ему значения, которые делают его истинным и ложным, затем снова удаляют все предложения, которые теперь истинны, и все литералы, которые теперь ложны.