Трудные выполнимые формулы для DPLL-подобных алгоритмов

Данная статья касается нижних оценок времени работы алгоритмов, решающих задачу пропозициональной выполнимости. Рассмотрены два DPLL-подобных алгоритма, использующих эвристики выбора единичного клоза и чистого литерала. Доказаны экспоненциальные нижние оценки на время работы этих алгоритмов на заведомо выполнимых формулах. Библ. – 11 назв.