4511
правок
K-КНФ-алгоритмы на основе поиска с возвратом: различия между версиями
Перейти к навигации
Перейти к поиску
м
K-КНФ-алгоритмы на основе поиска с возвратом (посмотреть исходный код)
Версия от 19:11, 25 февраля 2018
, 25 февраля 2018→Основные результаты
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 132: | Строка 132: | ||
<math>\tau(F_s) \ge 2^{-(1 - \frac{\mu_k}{k - 1})n - o(n)}</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) стремится к бесконечности достаточно медленно.''' | ||
'''(ii) Для <math>k \ge 3 \;</math> те же границы действительны для случая, когда формула F является уникально выполнимой.''' | '''(ii) Для <math>k \ge 3 \;</math> те же границы действительны для случая, когда формула F является уникально выполнимой.''' | ||
| Строка 140: | Строка 140: | ||
'''Теорема 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> имеет вероятность | '''Теорема 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> имеет вероятность | '''Теорема 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>.''' | ||
== Применение == | == Применение == | ||