4511
правок
K-КНФ-алгоритмы на основе поиска с возвратом: различия между версиями
Перейти к навигации
Перейти к поиску
K-КНФ-алгоритмы на основе поиска с возвратом (посмотреть исходный код)
Версия от 19:54, 24 февраля 2018
, 24 февраля 2018→Основные результаты
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 15: | Строка 15: | ||
== Основные результаты == | == Основные результаты == | ||
Алгоритм ResolveSat | Алгоритм ResolveSat | ||
Алгоритм ResolveSat по сути очень прост. Получив на вход формулу в k-КНФ, он вначале генерирует дизъюнкты, которые могут быть получены путем разложения, длина которых не превышает некоторой величины. Затем он устанавливает некоторый случайный порядок переменных и последовательно присваивает им значения согласно этому порядку. Если рассматриваемая в текущий момент переменная встречается в виде единичного дизъюнкта, ей присваивается единственное значение, при котором этот дизъюнкт выполним. Если она встречается в двух противоречащих друг другу единичных дизъюнктах, алгоритм начинает работу заново. На каждом этапе алгоритм также проверяет, выполнима ли формула. Если выполнима, то входной набор принимается. Процедура повторяется до тех пор, пока не будет найдено присваивание, приводящее к выполнимости формулы, либо пока не истечет выделенное время. | |||
Алгоритм ResolveSat использует следующую процедуру, которая принимает на вход произвольное присваивание y, КНФ-формулу F и перестановку ж и выполняет присваивание u. Присваивание u получается путем рассмотрения переменных y в порядке, заданном ж, и изменении их значений в попытке обеспечить выполнимость формулы F. | |||
Функция Modify(КНФ-формула G(x1, x2, ... . xn), перестановка ж = {1, 2, ..., n}, присваивание y) — ■> (присваивание u) | |||
G’ = G. | |||
for i = 1 to n | |||
if Gj-i единичный дизъюнкт хлщ then ul(i) = 1 | |||
else if Gj-i единичный дизъюнкт %(,) then иж(,) = 0 | |||
else ul(i) = yn(i) | |||
Gi = G;_i Ujr(i)=Kjr(i) | |||
end /* end for loop */ return U; | |||
Алгоритм Search получается в результате выполнения алгоритма Modify(G,7r,y) на нескольких парах (ж,у), где ж – случайная перестановка, а y – случайное присваивание. | |||
Search(КНФ-формула F, целое число I) повторить I раз | |||
ж = равномерно распределенная случайная перестановка 1, : : , n у = равномерно распределенный случайный вектор 2 {0, 1}n и = Modify(F, ж,у)\ if при u формула F выполнима | |||
then output(u); exit; end/* end repeat loop */ output('Unsatisfiable'); | |||
ResolveSat получается в результате сочетания Search с шагом предварительной обработки, заключающейся в ограниченном разложении формулы. Между дизъюнктами Q и C2, Q и C2 возникает конфликт на переменной v, если один из них содержит v, а другой – v. C1 и C2 представляют собой разложимую пару, если они конфликтуют точно на одной переменной v. Для таких пар их резольвентой, обозначаемой R(C1, C2), будет являться дизъюнкт C = D1 _ D2, где D1 и D2 получаются удалением v и v из C1 и C2, соответственно. Легко заметить, что любое присваивание, при котором C1 и C2 выполнимы, приводит также и к выполнимости C. Следовательно, если F выполнимой КНФ-формулой, содержащей разложимую пару C1, C2, то формула F0 = F Л R(C1 ; C2) будет иметь те же удовлетворяющие условию выполнимости присваивания, что и F. Разложимая пара C1, C2 является s-ограниченной, если j C1 j ; j C2j < s и jR(C1 ; C2)j < s. Следующая процедура расширяет формулу F до формулы Fs, применяя s-ограниченное разложение максимально возможное количество раз. | |||
Resolve(КНФ-формула F, целое число s) | |||
Fs = F. | |||
while Fs содержит s-ограниченную разложимую пару C1, C2 | |||
with R(C1;C2) 26Fs Fs = FsAR(d,C2). return (Fs). | |||
Алгоритм для формулы k-КНФ представляет собой простую комбинацию Resolve и Search: | |||
ResolveSat(КНФ-формула F, целое число s, целое положительное число I) | |||
Fs =Resolve(F, s). | |||
Search(Fs, I). | |||
'''Анализ алгоритма ResolveSat''' | |||
Время выполнения ResolveSat(F, s, I) можно ограничить следующим образом. Resolve(F, s) добавляет не более O(ns) дизъюнктов к F за счет сравнения пар дизъюнктов, так что прямолинейная реализация будет выполняться за время n3spoly(n) (эту границу можно улучшить, однако ее улучшение не повлияет на асимптотику основного результата). Search(Fs, I) требует I(jFj + ns)poly(n) времени. Следовательно, полное время выполнения ResolveSat(F, s, I) можно грубо ограничить сверху значением (n3s + I(jFj + ns))poly(n). If s = O(n/log n), общее время выполнения можно ограничить значением IjFj2O(n), поскольку ns = 2O(n). Для этого нужно взять в качестве s некоторую константу достаточно большой величины или медленно растущую функцию от n. Таким образом, s(n) будет стремиться к бесконечности с n, но будет оставаться в пределах O(log n). | |||
В случае, если функция F оказывается невыполнимой, алгоритм Search(F, I) всегда выдает результат «невыполнима». Таким образом, единственной проблемой остается нахождение верхней границы в случае, когда F выполнима. Обозначим за x(F) вероятность того, что Modify(F it,y) найдет некоторое присваивание, обеспечивающее выполнимость. Тогда для выполнимой функции F вероятность ошибки Search(F, I) равна (1 - r(F))1 < e~It(F\, что не превышает e~" при условии I > nlx{F). Следовательно, достаточно получить хорошую верхнюю границу для T(F). | |||
Анализ сложности алгоритма ResolveSat требует определенных констант fik для k > 2: | |||
Легко показать, что fi3 = 4 - 4 ln 2 > 1:226, используя разложение в ряд Тейлора функции ln 2. Используя стандартные способы, также легко показать, что ji^ представляет собой возрастающую функцию от k с пределом P1j=1(1/j2) = (лг2/6) = 1:644. | |||
Результаты работы алгоритма ResolveSat можно изложить в следующих трех теоремах. | |||
Теорема 1 (i). Пусть k > 5, а s(n) – функция, стремящаяся к бесконечности. Тогда для любой выполнимой формулы F в k-КНФ с n переменными верно соотношение r(Fs) > 2-(1-Й)»-°(»). | |||
Следовательно, ResolveSat(F, s, I) при I = 2(1-^l(k-i))n+o(n) имеет вероятность ошибок O(1) и время выполнения 2(i-w/(i-i))n+o(n) на любой выполнимой формуле в k-КНФ при условии, что s(n) стремится к бесконечности достаточно медленно. | |||
(ii) Для k > 3 те же границы действительны для случая, когда формула F является уникально выполнимой. | |||
Для доказательства теоремы 1 вначале рассмотрим случай уникальной выполнимости, а затем свяжем с ним задачу общего вида. При k > 5 из анализа следует, что асимптотика для общего случая оказывается не хуже асимптотики для случая уникальной выполнимости. При k = 3 и k = 4 границы в общем случае оказываются несколько более худшими по сравнению с уникальным. | |||
Теорема 2. Пусть s = s(n) – медленно растущая функция. Для любой выполнимой 3-КНФ-формулы с n переменными r(Fs) > 2~0-521", в силу чего ResolveSat(F, s, I) с I = n2°:521n вероятность ошибок O(1) и время выполнения 2°:521n+O(n). | |||
Теорема 3. Пусть s = s(n) – медленно растущая функция. Для любой выполнимой 4-КНФ-формулы с n переменными T(FS) > 2-о.5б25И) md, в силу чего ResolveSat(F, s, I) с I = n2°:5625n вероятность ошибок O(1) и время выполнения 2°:5625n+O(n). | |||
== Применение == | |||
Различные эвристики применялись для создания алгоритмов выполнимости формул в 3-КНФ, значительно превосходящих эффективностью алгоритмы перебора. Алгоритм ResolveSat и его анализ представляют строгое объяснение этой эффективности и обозначают структурные параметры (к примеру, длину дизъюнктов и количество решений), влияющие на сложность. | |||
== Открытые вопросы == | |||
Разрыв между границами для общего случая и для случая уникальной выполнимости при k 2 {3, 4} связан со слабостью анализа; было высказано предположение, что асимптотические границы для случая уникальной выполнимости выполняются в общем случае для всех k. Если это предположение верно, из него следует, что ResolveSat оказывается быстрее любого существующего алгоритма и в случае k = 3. | |||
к uniquek-SAT [ ] k-SAT [ ] k-SAT [ ] k-SAT [1 , , 11] k-SAT [6] | |||
3 0,386... 0,521 ... 0,415... 0,409... 0,404... | |||
4 0,554... 0,562... 0,584... 0,559... | |||
5 0,650... 0,678... | |||
6 0,711 ... 0,736... | |||
Таблица 1 | |||
В таблице представлен показатель c, используемый в значении границы 2c"~oW для уникального и общего случаев задачи k-КНФ, решаемой при помощи алгоритма ResolveSat, границы для k-КНФ и алгоритма Шонинга [ ], его улучшенной версии для 3-КНФ [1, 5, 11] и гибридной версии из работы [6] | |||
Еще одной любопытной задачей было бы более четкое понимание связи между количеством присваиваний, приводящих к выполнимости, и сложностью поиска такого присваивания [2]. Сильная гипотеза заключается в том, что выполнимость формул с большим количеством подходящих присваиваний доказать намного проще, чем в случае формул с меньшим числом решений. | |||
Наконец, важным открытым вопросом остается разработка улучшенного алгоритма для k-КНФ, который выполнялся бы быстрее по сравнению с представленными выше границами для случая уникальной выполнимости формул в k-КНФ. | |||
== См. также == | |||
* [[Алгоритмы локального поиска для k-КНФ]] | |||
* [[Задача максимальной выполнимости формул в 2-КНФ]] | |||
* [[Параметризованная задача выполнимости КНФ]] | |||
* [[Пороги в задаче выполнимости случайной k-КНФ]] | |||
== Литература == | |||
1. Baumer, S., Schuler, R.: Improving a Probabilistic 3-SAT Algorithm by Dynamic Search and Independent Clause Pairs. In: SAT 2003, pp. 150-161 | |||
2. Calabro, C., Impagliazzo, R., Kabanets, V., Paturi, R.: The Complexity of Unique k-SAT: An Isolation Lemma for k-CNFs. In: Proceedings of the Eighteenth IEEE Conference on Computational Complexity, 2003 | |||
3. Dantsin, E., Goerdt, A., Hirsch, E.A., Kannan, R., Kleinberg, J., Papadimitriou, C., Raghavan, P., Schoning, U.: A deterministic (2 — k+12)n algorithm for k-SAT based on local search. Theor. Comp. Sci. 289(1), 69-83 (2002) | |||
4. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun.ACM 5, 394-397 (1962) | |||
5. Hofmeister, T., Schoning, U., Schuler, R., Watanabe, O.: A probabilistic 3-SAT algorithm further improved. In: STACS 2002. LNCS, vol. 2285, pp. 192-202. Springer, Berlin (2002) | |||
6. Iwama, K., Tamaki, S.: Improved upper bounds for 3-SAT. In: Proceedings of the fifteenth annual ACM-SIAM symposium on Discrete algorithms, 2004, pp. 328-329 | |||
7. Kullmann,O.: New methods for 3-SAT decision and worst-case analysis. Theor. Comp. Sci. 223(1-2), 1 -72 (1999) | |||
8. Monien, B., Speckenmeyer, E.: Solving Satisfiability In Less Than 2n Steps. Discret. Appl. Math. 10,287-295 (1985) | |||
9. Paturi, R., Pudlak, P., Saks, M., Zane, F.: An Improved Exponential-time Algorithm for k-SAT. J. ACM 52(3), 337-364 (2005) (более ранняя версия публиковалась в источнике "39th Annual IEEE Symposium on Foundations of Computer Science, 1998, pp. 628-637") | |||
10. Paturi, R., Pudlak, P., Zane, F.: Satisfiability Coding Lemma. In: Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science, 1997, pp. 566-574. Chicago J. Theor. Comput. Sci. (1999), http://cjtcs.cs.uchicago.edu/ | |||
11. Rolf, D.: 3-SAT 2 RTIME(1 :32971n). In: ECCC TR03-054, 2003 | |||
12. Schoning, U.: A probabilistic algorithm fork-SAT based on limited local search and restart. Algorithmica 32, 615-623 (2002) (более ранняя версия публиковалась в источнике "40th Annual Symposium on Foundations of Computer Science (FOCS '99), pp. 410-414") | |||