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

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

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

ResolveSat объединяет эти идеи и стремление значительно улучшить границы [ ]. На данный момент алгоритму ResolveSat удается обеспечить наилучшие известные верхние границы для задачи выполнимости k-КНФ для всех k > 5. Для 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. Это сравнение охватывает только лучшие границы вне зависимости от типа алгоритма (рандомизированного или детерминированного).