K-КНФ-алгоритмы на основе поиска с возвратом

Постановка задачи

Широко известна задача определения сложности алгоритма выполнимости формул, записанных в форме k-КНФ. Пусть дана булева формула в конъюнктивной нормальной форме, имеющая не более k литералов на дизъюнкт. Необходимо найти такое присваивание переменным, которое удовлетворяет всем дизъюнктам, или дать ответ об отсутствии такого присваивания. Хорошо известно, что проблема разрешимости для задачи выполнимости k-КНФ является NP-полной для [math]\displaystyle{ k \ge 3 \; }[/math]. Далее будут рассмотрены алгоритмы, позволяющее значительно улучшить время выполнения в наихудшем случае, ассоциированное с алгоритмом поиска полным перебором и составляющее [math]\displaystyle{ poly(n)2^n \; }[/math] для формулы с n переменными. Мониен и Шпекенмейер [8] впервые улучшили границу, предложив простой алгоритм с временем выполнения [math]\displaystyle{ O(2^{(1 - \varepsilon_k)n}) }[/math], где [math]\displaystyle{ \varepsilon_k \gt 0 \; }[/math] для всех k. В последующих работах [1, 3, 5, 6, 7, 9, 10, 11, 12] были предложены и проанализированы алгоритмы со все более приемлемым временем выполнения (для больших значений [math]\displaystyle{ \varepsilon_k \; }[/math]).

Эти алгоритмы обычно применяют один из двух подходов к поиску удовлетворительного решения. Первый класс составляют алгоритмы поиска с возвратом. Эти алгоритмы, изначально предложенные Дэвисом, Логеманом и Лавлендом [4], иногда называют процедурами Дэвиса-Патнем. Подобные алгоритмы пытаются найти присваивание, удовлетворяющие условиям, присваивая в некотором порядке значения каждой переменной и выполняя возврат в случае, если дизъюнкт оказался ложным. Другой класс алгоритмов построен на использовании локального поиска (первые результаты с гарантированной эффективностью были получены Шонингом [12]). Алгоритм начинает работу со случайно или стратегически выбранного присваивания и выполняет локальный поиск присваиваний, удовлетворяющих условиям, ориентируясь на неудовлетворенные дизъюнкты.

Далее будет представлен ResolveSat, рандомизированный алгоритм проверки выполнимости k-КНФ с одними из лучших известных на данный момент верхних границ. Он основан на более раннем алгоритме, предложенном Патури, Пудлаком и Зейном [10] и представляющим собой алгоритм поиска с возвратом, который проверяет переменные в случайно выбранном порядке. Анализ алгоритма основывается на следующем наблюдении: до тех пор пока у формулы имеется удовлетворяющее условию присваивание, изолированное от других удовлетворяющих условию присваиваний, треть переменных встречается в виде единичных дизъюнктов, поскольку переменные присваиваются в случайном порядке. Таким образом, алгоритму нужно правильно угадать значения не более чем 2/3 переменных. Этот анализ был расширен для общего случая благодаря следующему наблюдению: либо существует изолированное удовлетворяющее условию присваивание, либо существует много решений, так что вероятность угадать подходящее достаточно высока.

ResolveSat объединяет эти идеи и стремление значительно улучшить границы [9]. На данный момент алгоритму ResolveSat удается обеспечить наилучшие известные верхние границы для задачи выполнимости k-КНФ для всех [math]\displaystyle{ k \ge 5 \; }[/math]. Для k = 3 и k = 4 Ивама и Таками [6] получили наилучшую известную верхнюю границу при помощи рандомизированного алгоритма, сочетающего идеи алгоритма локального поиска Шонинга и ResolveSat. Более того, для задачи с предусловием о существовании единственного решения задачи выполнимости k-КНФ, считающейся одной из самых трудных вариаций задачи о выполнимости k-КНФ [2], ResolveSat достигает рекордных значений для всех [math]\displaystyle{ k \ge 3 \; }[/math]. Границы, полученные ResolveSat для задачи с единственным решением и задачи общего вида для значений k = 3, 4, 5, 6, представлены в таблице. Эти границы сравниваются с границами алгоритма Шонинга [12], последовательно улучшенными результатами на базе локального поиска [1, 5, 11] и недавними изменениями, предложенными Ивамой и Таками [6]. Полученные для этих алгоритмов верхние границы выражаются в форме [math]\displaystyle{ 2^{cn - o(n)} \; }[/math], а значения в таблице отражают показатель c. Это сравнение охватывает только лучшие границы вне зависимости от типа алгоритма (рандомизированного или детерминированного).

Нотация

Далее булева формула в КНФ [math]\displaystyle{ F(x_1, x_2, ..., x_n) \; }[/math] будет рассматриваться и как булева функция, и как множество дизъюнктов. Булева формула F является формулой в k-КНФ, если все дизъюнкты имеют величину не более k. Для дизъюнкта C обозначим за var(C) множество переменных, встречающихся в C. Если [math]\displaystyle{ v \in var(C) \; }[/math], то ориентация [math]\displaystyle{ v \; }[/math] является положительной, если литерал v принадлежит к C, и отрицательной, если литерал [math]\displaystyle{ \bar{v} \; }[/math] принадлежит к C. Вспомним, что если F является булевой формулой в КНФ над переменными [math]\displaystyle{ (x_1, x_2, ..., x_n) \; }[/math], а [math]\displaystyle{ a \; }[/math] – частичным присваиванием переменным, то ограничение F согласно [math]\displaystyle{ a \; }[/math] определяется как формула [math]\displaystyle{ F' = F \lceil_a \; }[/math] на множестве переменных, значения которых задаются без использования [math]\displaystyle{ a \; }[/math], полученная в результате обработки каждого дизъюнкта C формулы F следующим образом: если значение C в результате присваивания a становится равным 1, то C следует удалить; в противном случае заменить C дизъюнктом C’, полученным в результате удаления из C любых литералов, значения которых в результате присваивания [math]\displaystyle{ a \; }[/math] становятся равными 0. Единичным дизъюнктом называется дизъюнкт, содержащий ровно один литерал.

Основные результаты

Алгоритм ResolveSat