4446
правок
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида: различия между версиями
Материал из WEGA
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида (посмотреть исходный код)
Версия от 18:24, 25 июля 2020
, 25 июля 2020→Процедура S
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 115: | Строка 115: | ||
'''Процедура S''' | |||
Дано: КНФ-формула F и положительное целое число k. | Дано: КНФ-формула F и положительное целое число k. | ||
1. Предположим, формула F состоит из дизъюнктов | 1. Предположим, формула F состоит из дизъюнктов <math>C_1, ..., C_m</math>. Заменим каждый дизъюнкт <math>C_i</math> дизъюнктом <math>D_i</math> следующим образом: если <math>|C_i| > k</math>, выбрать любые k литералов в <math>C_i</math> и отбросить все остальные литералы; в противном случае оставить <math>C_i</math> неизменным, т. е. <math>D_i = C_i</math>. Обозначить полученную формулу как F'. | ||
2. Проверить выполнимость формулы | 2. Проверить выполнимость формулы F' с помощью алгоритма k-КНФ с временем выполнения <math>m \cdot poly(n) \cdot (2 - 2/(k + 1))^n</math>, определенного в работе [3]. | ||
3. Если формула | 3. Если формула F' является выполнимой, вывести «Формула выполнима» и остановить выполнение. В противном случае для каждого значения i выполнить следующее: | ||
(а) Преобразовать F в | (а) Преобразовать F в <math>F_i</math> следующим образом: | ||
11. Заменить | 11. Заменить <math>C_j</math> на <math>D_j</math> для всех j < i; | ||
12. Присвоить всем литералам | 12. Присвоить всем литералам <math>D_i</math> значение ''false''. | ||
(б) | (б) Рекурсивно вызвать процедуру S для значений (<math>F_i</math>, k). | ||
4. Вернуть «Формула невыполнима». | 4. Вернуть «Формула невыполнима». | ||
Алгоритм вызывает процедуру S для исходной формулы и целочисленного параметра k = k * (m, n). Из наиболее точного анализа данного семейства алгоритмов, выполненного Калабро, Импальяццо и Патури [ ], следует, что, предполагая, что m > n, можно получить следующую границу, приняв k(m | Алгоритм вызывает процедуру S для исходной формулы и целочисленного параметра k = k * (m, n). Из наиболее точного анализа данного семейства алгоритмов, выполненного Калабро, Импальяццо и Патури [1], следует, что, предполагая, что m > n, можно получить следующую границу, приняв k(m, n) = 2 log(m/n) + const. (Эта явная граница не задана в [1] и выводится в [4].) | ||
'''Теорема 4 (Данцин, Хирш [ ]). Предполагая, что m > n, задачу SAT можно решить за время''' | '''Теорема 4 (Данцин, Хирш [4]). Предполагая, что m > n, задачу SAT можно решить за время <math>|F|^{O(1)} \cdot 2^{n \big (1 - \frac{1}{O(log(m/n))} \big ) }.</math>''' | ||
== Применение == | == Применение == | ||
