4511
правок
K-КНФ-алгоритмы на основе поиска с возвратом: различия между версиями
Перейти к навигации
Перейти к поиску
K-КНФ-алгоритмы на основе поиска с возвратом (посмотреть исходный код)
Версия от 11:09, 25 февраля 2018
, 25 февраля 2018→Основные результаты
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 73: | Строка 73: | ||
В случае, если функция F оказывается невыполнимой, алгоритм '''Search'''(F, I) всегда выдает результат «невыполнима». Таким образом, единственной проблемой остается нахождение верхней границы в случае, когда F выполнима. Обозначим за | В случае, если функция F оказывается невыполнимой, алгоритм '''Search'''(F, I) всегда выдает результат «невыполнима». Таким образом, единственной проблемой остается нахождение верхней границы в случае, когда F выполнима. Обозначим за <math>\tau(F) \;</math> вероятность того, что '''Modify'''(<math>F, \pi, y \;</math>) найдет некоторое присваивание, обеспечивающее выполнимость. Тогда для выполнимой функции F вероятность ошибки '''Search'''(F, I) равна <math>(1 - \tau(F))^I \le e^{-I \tau(F)}</math>, что не превышает <math>e^{-n} \;</math> при условии <math>I \ge n / \tau(F)</math>. Следовательно, достаточно получить хорошую верхнюю границу для <math>\tau(F) \;</math>. | ||
Анализ сложности алгоритма ResolveSat требует | Анализ сложности алгоритма '''ResolveSat''' требует введения ряда констант <math>\mu_k \;</math> для <math>k \ge 2 \;</math>: | ||
<math>\mu_k = \sum_{j=1}^{\infty} \frac{1}{j (j + \frac{1}{k - 1})}</math>. | |||
Легко показать, что <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>. | |||
Результаты работы алгоритма ResolveSat можно изложить в следующих трех теоремах. | |||
Результаты работы алгоритма '''ResolveSat''' можно изложить в следующих трех теоремах. | |||