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. Это сравнение охватывает только лучшие границы вне зависимости от типа алгоритма (рандомизированного или детерминированного).

Время выполнения ResolveSat(F, s, I) можно ограничить следующим образом. '''Resolve'''(F, s) добавляет не более <math>O(n^s) \;</math> дизъюнктов к F за счет сравнения пар дизъюнктов, так что прямолинейная реализация будет выполняться за время <math>n^{3s}poly(n) \;</math> (эту границу можно улучшить, однако ее улучшение не повлияет на асимптотику основного результата). '''Search'''(<math>F_s, \; I</math>) требует <math>I(|F| + n^s)poly(n) \;</math> времени. Следовательно, полное время выполнения '''ResolveSat'''(F, s, I) можно грубо ограничить сверху значением <math>(n^{3s} + I(|F| + n^s))poly(n) \;</math>. If s = O(n/log n), общее время выполнения можно ограничить значением <math>I|F|2^{O(n)} \;</math>, поскольку <math>n^s = 2^{O(n)} \;</math>. Для этого нужно взять в качестве s некоторую константу достаточно большой величины или ''медленно растущую'' функцию от n. Таким образом, s(n) будет стремиться к бесконечности с n, но будет оставаться в пределах O(log n).

Легко показать, что <math>\mu_3 = 4 - 4 \; ln \; 2 > 1,226</math>, используя разложение функции ln 2 в ряд Тейлора. Используя стандартные способы, также легко показать, что <math>\mu_k \;</math> представляет собой возрастающую функцию от k с пределом <math>\sum_{j=1}^{\infty} (1 / j^2) = (\pi^2 / 6) = 1,644</math>.

<math>\tau(F_s) \ge 2^{-(1 - \frac{mu_k}{k - 1})n - o(n)}</math>.

 

'''Следовательно, '''ResolveSat'''(F, s, I) при <math>I = 2^{(1 - \frac{mu_k}{k - 1})n - O(n)}</math> имеет вероятность ошибок O(1) и время выполнения <math>2^{(1 - \frac{mu_k}{k - 1})n - O(n)}</math> на любой выполнимой формуле в k-КНФ при условии, что s(n) стремится к бесконечности достаточно медленно.'''

'''Теорема 2. Пусть s = s(n) – медленно растущая функция. Для любой выполнимой 3-КНФ-формулы с n переменными верно <math>\tau(F_s) \ge 2^{-0,521^n}</math>, в силу чего '''ResolveSat'''(F, s, I) с <math>I = n \; 2^{0,521n}</math> имеет вероятность ошибок O(1) и время выполнения <math>2^{0,521 n + O(n)} \;</math>.'''

'''Теорема 3. Пусть s = s(n) – медленно растущая функция. Для любой выполнимой 4-КНФ-формулы с n переменными верно <math>\tau(F_s) \ge 2^{-0,5625n}</math>, в силу чего '''ResolveSat'''(F, s, I) с <math>I = n \; 2^{0,5625n} \;</math> имеет вероятность ошибок O(1) и время выполнения <math>2^{0,5625n + O(n)} \;</math>.'''