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>).

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

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