K-КНФ-алгоритмы на основе поиска с возвратом: различия между версиями

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

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

Далее булева формула в КНФ F(x1, x2, ..., xn) будет рассматриваться и как булева функция, и как множество дизъюнктов. Булева формула F является формулой в k-КНФ, если все дизъюнкты имеют величину не более k. Для дизъюнкта C обозначим за var(C) множество переменных, встречающихся в C. Если v 2 var(C), то ориентация v является положительной, если литерал v принадлежит к C, и отрицательной, если литерал v принадлежит к C. Вспомним, что если F является булевой формулой в КНФ над переменными (x1, x2, ..., xn), а a – частичным присваиванием переменным, то ограничение F согласно a определяется как формула F’ = F da на множестве переменных, значения которых не задаются при помощи a, полученная в результате обработки каждого дизъюнкта C формулы F следующим образом: если значение C в результате присваивания a становится равным 1, то C следует удалить; в противном случае заменить C дизъюнктом C’, полученным в результате удаления из C любых литералов, значения которых результате присваивания a становятся равными 0. Единичным дизъюнктом называется дизъюнкт, содержащий ровно один литерал.