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

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, представлены в таблице. Эти границы сравниваются с границами алгоритма Шонинга [12], последовательно улучшенными результатами на базе локального поиска [1, 5, 11] и недавними изменениями, предложенными Ивамой и Таками [6]. Полученные для этих алгоритмов верхние границы выражаются в форме <math>2^{cn - o(n)} \;</math>, а значения в таблице отражают показатель c. Это сравнение охватывает только лучшие границы вне зависимости от типа алгоритма (рандомизированного или детерминированного).

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

Алгоритм ResolveSat

Алгоритм ResolveSat по сути очень прост. Получив на вход формулу в k-КНФ, он вначале генерирует дизъюнкты, которые могут быть получены путем разложения, длина которых не превышает некоторой величины. Затем он устанавливает некоторый случайный порядок переменных и последовательно присваивает им значения согласно этому порядку. Если рассматриваемая в текущий момент переменная встречается в виде единичного дизъюнкта, ей присваивается единственное значение, при котором этот дизъюнкт выполним. Если она встречается в двух противоречащих друг другу единичных дизъюнктах, алгоритм начинает работу заново. На каждом этапе алгоритм также проверяет, выполнима ли формула. Если выполнима, то входной набор принимается. Процедура повторяется до тех пор, пока не будет найдено присваивание, приводящее к выполнимости формулы, либо пока не истечет выделенное время.

Алгоритм ResolveSat использует следующую процедуру, которая принимает на вход произвольное присваивание y, КНФ-формулу F и перестановку <math>\pi \;</math> и выполняет присваивание u. Присваивание u получается путем рассмотрения переменных y в порядке, заданном <math>\pi \;</math>, и изменении их значений в попытке обеспечить выполнимость формулы F.

Функция '''Modify'''(КНФ-формула <math>G(x_1, x_2, ..., x_n) \;</math>, перестановка <math>\pi \;</math> = ({1, 2, ..., n}, присваивание y) <math>\to</math> (присваивание u)

Алгоритм '''Search''' получается в результате выполнения алгоритма '''Modify'''<math>(G, \pi, y) \;</math> на нескольких парах <math>(\pi, y) \;</math>, где <math>\pi \;</math> – случайная перестановка, а y – случайное присваивание.

       u = '''Modify'''<math>(F, \pi, у)</math>;

   <math>F_s</math> = Resolve(F, s).

Время выполнения 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>.'''

Различные эвристики применялись для создания алгоритмов выполнимости формул в 3-КНФ, значительно превосходящих эффективностью алгоритмы перебора. Алгоритм ResolveSat и его анализ представляют строгое объяснение этой эффективности и обозначают структурные параметры (к примеру, длину дизъюнктов и количество решений), влияющие на сложность.

Разрыв между границами для общего случая и для случая уникальной выполнимости при k 2 {3, 4} связан со слабостью анализа; было высказано предположение, что асимптотические границы для случая уникальной выполнимости выполняются в общем случае для всех k. Если это предположение верно, из него следует, что ResolveSat оказывается быстрее любого существующего алгоритма и в случае k = 3.