4446
правок
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида: различия между версиями
Перейти к навигации
Перейти к поиску
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида (посмотреть исходный код)
Версия от 14:07, 9 июля 2020
, 9 июля 2020→Основные результаты
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 42: | Строка 42: | ||
давало желаемую верхнюю границу по количеству листьев в дереве рекуррентности и, следовательно, по времени работы алгоритма. В частности, для получения границы <math>|F|^{O(1)} \cdot 2^{0,30897m};</math> необходимо решить либо две подзадачи F[x], F[<math>\lnot</math>x] с рекуррентным неравенством | давало желаемую верхнюю границу по количеству листьев в дереве рекуррентности и, следовательно, по времени работы алгоритма. В частности, для получения границы <math>|F|^{O(1)} \cdot 2^{0,30897m};</math> необходимо решить либо две подзадачи F[x], F[<math>\lnot</math>x] с рекуррентным неравенством | ||
<math>t_m \le t_{m - 3} + t_{m - 4}</math> | |||
либо четыре подзадачи F[x, y], F[x, <math>\lnot</math>y], F[<math>\lnot</math>x, y], F[<math>\lnot</math>x, <math>\lnot</math>y] с рекуррентным неравенством | |||
где | |||
<math>t_m \le 2t_{m - 6} + 2t_{m - 7},</math> | |||
где <math>t_i = max_{m(G)\le i} T(G)</math>. Правила упрощения, используемые в алгоритмах со временем выполнения <math>|F|^{O(1)} \cdot 2^{0,30897m};</math> и <math>|F|^{O(1)} \cdot 2^{0,10299l}.</math>, выглядят следующим образом. | |||
'''Правила упрощения''' | '''Правила упрощения''' | ||