SAT-солвер на основе метода резолюций

[bocovp]

Это же алгоритм Дэвиса — Патнема (DP; не путать с DPLL), один из первых алгоритмов решения задачи о выполнимости...

[lapkin25]

Спасибо за полезный ответ! Действительно, алгоритм очень похож на DP, но вместо эвристик "Unit-literal rule" и "Pure-literal rule" поддерживается структура данных, сразу исключающая все возможные поглощения клауз. За счет этого количество клауз в множестве становится меньше.