4430
правок
K-КНФ-алгоритмы на основе поиска с возвратом: различия между версиями
Материал из WEGA
K-КНФ-алгоритмы на основе поиска с возвратом (посмотреть исходный код)
Версия от 11:57, 20 февраля 2018
, 20 февраля 2018нет описания правки
Irina (обсуждение | вклад) мНет описания правки |
Irina (обсуждение | вклад) мНет описания правки |
||
| Строка 6: | Строка 6: | ||
Далее будет представлен ResolveSat, рандомизированный алгоритм проверки выполнимости k-КНФ с одними из лучших известных на данный момент верхних границ. Он основан на более раннем алгоритме, предложенном Патури, Пудлаком и Зейном [10] и представляющим собой алгоритм поиска с возвратом, который проверяет переменные в случайно выбранном порядке. Анализ алгоритма основывается на следующем наблюдении: до тех пор пока у формулы имеется удовлетворяющее условию присваивание, изолированное от других удовлетворяющих условию присваиваний, треть переменных встречается в виде единичных дизъюнктов, поскольку переменные присваиваются в случайном порядке. Таким образом, алгоритму нужно правильно угадать значения не более чем 2/3 переменных. Этот анализ был расширен для общего случая благодаря следующему наблюдению: либо существует изолированное удовлетворяющее условию присваивание, либо существует много решений, так что вероятность угадать подходящее достаточно высока. | Далее будет представлен '''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. Это сравнение охватывает только лучшие границы вне зависимости от типа алгоритма (рандомизированного или детерминированного). | ||
== Нотация == | == Нотация == | ||
Далее булева формула в КНФ <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(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 в результате присваивания a становится равным 1, то C следует удалить; в противном случае заменить C дизъюнктом C’, полученным в результате удаления из C любых литералов, значения которых в результате присваивания <math>a \;</math> становятся равными 0. Единичным дизъюнктом называется дизъюнкт, содержащий ровно один литерал. | ||
== Основные результаты == | == Основные результаты == | ||
Алгоритм ResolveSat | Алгоритм ResolveSat | ||
