Нижние оценки для DPLL алгоритмов с эвристикой отсечения ветвей.
Аннотация
DPLL алгоритмы (названные в честь авторов: Davis, Putnam, Logemann и
Loveland) - это один из самых распространенных подходов к решению
задачи выполнимости пропозициональной формулы. DPLL алгоритм - это
рекурсивный алгоритм, который получает на вход формулу F в КНФ, с
помощью процедуры A выбирает переменную x, а с помощью процедуры B
выбирает значение a (0 или 1), которое будет подставлено первым и
делает два рекурсивных вызова на входах F[x:=a] и F[x:=1-a]. Рекурсия
обрывается, если входная формула содержит заведомо невыполненный
пустой дизъюнкт. Алгоритм немедленно заканчивает работу, если найден
выполняющий набор.
Давно известно, что DPLL алгоритмы работают долго (экспоненциальное
время) на невыполнимых формулах, которые кодируют такой простой факт:
в графе нечетной степени не может быть нечетное число вершин нечетной
степени, на невыполнимых формулах, которые кодируют принцип Дирихле и
др. Однако доказать, что DPLL алгоритмы работают экспоненциальное
время на каком-нибудь семействе выполнимых формул не удается,
поскольку, если P=NP, то процедура B может всегда выбирать значение
для переменной, которое согласуется с каким-нибудь выполняющим
набором. Нижнюю оценку на выполнимых формулах удается доказать, если
ограничить возможности процедур A и B. Процедуры A и B называются
близорукими, если им доступна не вся информация о формуле, а лишь ее
часть, например, из m дизъюнктов доступны только m^{1-\epsilon}. Для
близоруких DPLL алгоритмов можно доказать, что время их работы на
формулах, которые кодируют системы линейных уравнений по модулю 2 с
невырожденной квадратной матрицей, экспоненциально. Схема
доказательств нижних оценок для выполнимых формул такая: показывается,
что близорукий алгоритмы очень быстро сделает неправильную подстановку
и получит трудную невыполнимую формулу.
В докладе мы рассмотрим новую модель вычислений: DPLL алгоритмы с
эвристикой отсечения ветвей. Перед рекурсивными вызовами
дополнительная процедура C решает, продолжать работать алгоритму в
этой ветви или нет. Алгоритмы с эвристикой отсечения всегда выдают
правильный ответ на невыполнимых формулах, однако могут не найти
выполняющий набор для выполнимой формулы. Для близоруких DPLL
алгоритмов с эвристикой отсечения мы докажем теорему о компромиссе
между эффективностью и корректностью: существует такая
последовательность невыполнимых формул F_n и для каждого близорукого
DPLL алгоритма (с полиномиально вычислимыми процедурами A и С)
существует полиномиально моделируемый ансамбль распределений D_n с
носителем на выполнимых формулах, такие, что при каждом n, этот
близорукий DPLL алгоритм либо работает долго на формулах F_n, либо
ошибается с вероятностью 0.99 на формулах из распределения D_n.
Доклад основан на совместной работе с Д. Соколовым.