4446
правок
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида: различия между версиями
Материал из WEGA
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида (посмотреть исходный код)
Версия от 13:58, 9 июля 2020
, 9 июля 2020→Основные результаты
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 36: | Строка 36: | ||
Типичный алгоритм «разделяй и властвуй» для задачи SAT состоит из двух этапов: ''разбиение'' исходной задачи на несколько подзадач (например, редукция SAT(F) до SAT(F[x]) и SAT(F[<math>\lnot</math>x])) и упрощение полученных подзадач при помощи правил преобразования с полиномиальным временем работы, не влияющих на выполнимость подзадач (т.е. заменяющих формулу другой формулой, в равной мере выполнимой). Подзадачи | Типичный алгоритм «разделяй и властвуй» для задачи SAT состоит из двух этапов: ''разбиение'' исходной задачи на несколько подзадач (например, редукция SAT(F) до SAT(F[x]) и SAT(F[<math>\lnot</math>x])) и ''упрощение'' полученных подзадач при помощи правил преобразования с полиномиальным временем работы, не влияющих на выполнимость подзадач (т.е. заменяющих формулу другой формулой, ''в равной мере выполнимой''). Подзадачи <math>F_1, ..., F_k</math> для разбиения выбираются таким образом, чтобы соответствующее рекуррентное неравенство с упрощенными задачами <math>F'_1, ..., F'_k</math>, | ||
давало желаемую верхнюю границу по количеству листьев в дереве рекуррентности и, следовательно, по времени работы алгоритма. В частности, для получения границы | |||
<math>T(F) \le \sum_{i=1}^k T(F'_i) + const,</math> | |||
давало желаемую верхнюю границу по количеству листьев в дереве рекуррентности и, следовательно, по времени работы алгоритма. В частности, для получения границы <math>|F|^{O(1)} \cdot 2^{0,30897m};</math> необходимо решить либо две подзадачи F[x], F[<math>\lnot</math>x] с рекуррентным неравенством | |||
tm < tm-3 + fm-4 ]; F[:x; | tm < tm-3 + fm-4 ]; F[:x; | ||
либо четыре подзадачи F[x;y]; F[x; :y] с рекуррентным неравенством | либо четыре подзадачи F[x;y]; F[x; :y] с рекуррентным неравенством | ||
tm < 2fm_6 + 2fm_7 | tm < 2fm_6 + 2fm_7 | ||
где ti = maxm(G)<; T(G). Правила упрощения, используемые в алгоритмах со временем выполнения |F|°«.20-30897m и |F|o«.20-10299/, выглядят следующим образом. | где ti = maxm(G)<; T(G). Правила упрощения, используемые в алгоритмах со временем выполнения |F|°«.20-30897m и |F|o«.20-10299/, выглядят следующим образом. | ||
