4511
правок
K-КНФ-алгоритмы на основе поиска с возвратом: различия между версиями
Перейти к навигации
Перейти к поиску
м
K-КНФ-алгоритмы на основе поиска с возвратом (посмотреть исходный код)
Версия от 18:07, 24 февраля 2018
, 24 февраля 2018→Постановка задачи
Irina (обсуждение | вклад) м (→Нотация) |
Irina (обсуждение | вклад) |
||
| Строка 1: | Строка 1: | ||
== Постановка задачи == | == Постановка задачи == | ||
Широко известна задача определения сложности алгоритма выполнимости формул, записанных в форме k-КНФ. Пусть дана булева формула в [[конъюнктивная нормальная форма|конъюнктивной нормальной форме]], имеющая не более 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] и представляющим собой алгоритм поиска с возвратом, который проверяет переменные в случайно выбранном порядке. Анализ алгоритма основывается на следующем наблюдении: до тех пор пока у формулы имеется | Далее будет представлен '''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. Это сравнение охватывает только лучшие границы вне зависимости от типа алгоритма (рандомизированного или детерминированного). | 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. Это сравнение охватывает только лучшие границы вне зависимости от типа алгоритма (рандомизированного или детерминированного). | ||