4511
правок
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) мНет описания правки |
||
Строка 8: | Строка 8: | ||
Далее будет представлен '''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, представлены в таблице 1. Эти границы сравниваются с границами алгоритма Шонинга [12], последовательно улучшенными результатами на базе локального поиска [1, 5, 11] и недавними изменениями, предложенными Ивамой и Таками [6]. Полученные для этих алгоритмов верхние границы выражаются в форме <math>2^{cn - o(n)} \;</math>, а значения в таблице отражают показатель c. Это сравнение охватывает только лучшие границы вне зависимости от типа алгоритма (рандомизированного или детерминированного). | ||
''Таблица 1'' | |||
{| class="wikitable" | |||
|- | |||
! k | |||
! уник. k-КНФ [9] | |||
! k-КНФ [9] | |||
! k-КНФ [12] | |||
! k-КНФ [1, 5, 11] | |||
! k-КНФ [6] | |||
|- | |||
| 3 | |||
| 0,386... | |||
| 0,521 ... | |||
| 0,415... | |||
| 0,409... | |||
| 0,404... | |||
|- | |||
| 4 | |||
| 0,554... | |||
| 0,562... | |||
| 0,584... | |||
| | |||
| 0,559... | |||
|- | |||
| 5 | |||
| colspan="2" align="center"| 0,650... | |||
| 0,678... | |||
| | |||
| | |||
|- | |||
| 6 | |||
| colspan="2" align="center"| 0,711 ... | |||
| 0,736... | |||
| | |||
| | |||
|} | |||
''В таблице представлен показатель c, используемый в значении границы <math>2^{cn - o(n)} \;</math> для уникального и общего случаев задачи k-КНФ, решаемой при помощи алгоритма ResolveSat, границы для k-КНФ и алгоритма Шонинга [12], его улучшенной версии для 3-КНФ [1, 5, 11] и гибридной версии из работы [6]'' | |||
== Нотация == | == Нотация == | ||
Строка 110: | Строка 150: | ||
== Открытые вопросы == | == Открытые вопросы == | ||
Разрыв между границами для общего случая и для случая уникальной выполнимости при <math>k \in \{ 3, 4 \}</math> связан со слабостью анализа; было высказано предположение, что асимптотические границы для случая уникальной выполнимости выполняются в общем случае для всех k. Если это предположение верно, из него следует, что '''ResolveSat''' оказывается быстрее любого существующего алгоритма и в случае k = 3. | Разрыв между границами для общего случая и для случая уникальной выполнимости при <math>k \in \{ 3, 4 \}</math> связан со слабостью анализа; было высказано предположение, что асимптотические границы для случая уникальной выполнимости выполняются в общем случае для всех k. Если это предположение верно, из него следует, что '''ResolveSat''' оказывается быстрее любого существующего алгоритма и в случае k = 3. | ||
правок