Построение алгоритмов для задач булевой логики при помощи автоматизации, комбинированных мер сложности и запоминания дизъюнктов тема диссертации и автореферата по ВАК РФ 05.13.17, кандидат физико-математических наук Куликов, Александр Сергеевич

• Куликов, Александр Сергеевич
• кандидат физико-математических наук
• 2009

Оглавление диссертации кандидат физико-математических наук Куликов, Александр Сергеевич

Введение

1 Определения

1.1 Задачи булевой логики.

1.1.1 Формулы в КНФ.

1.1.2 Задачи выполнимости и максимальной выполнимости

1.2 Алгоритм расщепления.

1.3 Анализ алгоритмов расщепления.

1.4 Класс формул.

2 Методы доказательства верхних оценок, использующиеся в работе

2.1 Пример простого алгоритма расщепления.

2.2 Общее правило упрощения.

2.3 Автоматический анализ сложности алгоритмов расщепления

2.4 Комбинированные меры сложности

2.5 Запоминание дизъюнктов.

3 Автоматическое порождение правил упрощения

3.1 Известные правила упрощения для SAT и MAX-SAT

3.2 Общее правило упрощения.

3.3 Алгоритм для (n, 3)-MAX-SAT.

4 Автоматический анализ времени работы

4.1 Описание программы

4.1.1 Входные и выходные данные.

4.1.2 Алгоритм построения доказательства.

4.1.3 Детали реализации.

4.1.4 Правила упрощения.

4.1.5 Правило расщепления.

4.1.6 Мера сложности.

4.1.7 Инвариант.

4.2 Автоматически доказанные верхние оценки.

4.3 Подобные работы.

5 Комбинированные меры сложности и запоминание дизъюнктов

5.1 Решение MAX-SAT на формулах константной плотности быстрее, чем за 2м.

5.2 Алгоритм для MAX-2-SAT.

5.2.1 Правила упрощения.

5.2.2 Правила расщепления.

5.2.3 Алгоритм для MAX-2-SAT.

5.2.4 (n, 3)-М AX-2-SAT.

Введение диссертации (часть автореферата) на тему «Построение алгоритмов для задач булевой логики при помощи автоматизации, комбинированных мер сложности и запоминания дизъюнктов»

Интерес к доказательству экспоненциальных верхних оценок для КР-трудных задач в последние несколько десятилетий остается на стабильно высоком уровне. Одним из наиболее хорошо изученных подходов к доказательству таких оценок является метод расщепления. Впервые данный метод был предложен в 1960-м году Дэвисом и Патнемом [19] и сформулирован в более современном виде Дэвисом, Лоджеманном и Лавлэндом [18] в 1962-м году. Его основная идея заключается в расщеплении входного примера задачи на несколько более простых примеров (упрощаемых в дальнейшем некоторыми правилами упрощения), таких что, построив решение для каждого из них, возможно за полиномиальное время построить решение для исходного примера. В списке ниже мы приводим некоторые верхние оценки на время решения ЫР-трудных задач в наихудшем случае, доказанные методом расщепления и являющиеся наилучшими из известных (здесь и на протяжении всей работы мы опускаем полиномиальные от размера входа множители в оценках, указывая только экспоненциальную составляющую):

1. 1.0741, для задачи пропозициональной выполнимости формул в КНФ, где Ь — длина (то есть общее количество литералов) входной формулы [23];

2. 1.341294^ для задачи максимальной выполнимости, где К — количество дизъюнктов входной формулы [14];

3. 1.122463™ для задачи о максимальном разрезе, где т — количество ребер входного графа [36];

4. 1.328971 для задачи о З-раскрашиваемости графа, где п — количество вершин входного графа [12].

В диссертации рассматриваются алгоритмы расщепления в применении к задачам выполнимости и максимальной выполнимости. Обе задачи формулируются на языке булевых формул, являющемся очень удобным для кодирования многих алгоритмических задач (таких, например, как автоматическое доказательство теорем, составление расписаний, оптимизационные задачи на графах). Задача пропозициональной выполнимости (satisfiability problem, SAT) является одной из наиболее известных NP-полных задач (см., например, [1]). Данной задаче посвящена международная ежегодная конференция (The International Conference on Theory and Applications of Satisfiability Testing), проводящаяся уже более десяти лет, а также научный журнал (Journal on Satisfiability, Boolean Modeling and Computation). Поскольку NP-трудные задачи часто возникают в практических приложениях (например, при разработке микросхем, в распознавании образов), важное место в исследовании задачи выполнимости занимает разработка программ, решающих SAT (такие программы называются SAT-солверами). Ежегодно проводятся соревнования таких программ.

Современные SAT-солверы способны быстро решать многие задачи, считавшиеся нерешаемыми несколько лет назад.

Важным оптимизационным обобщением задачи выполнимости является задача максимальной выполнимости (maximum satisfiability problem, MAX-SAT). В терминах задачи MAX-SAT могут быть естественным образом переформулированы многие оптимизационные NP-трудные задачи, к примеру, такие оптимизационные задачи на графах, как задача о максимальном разрезе (maximum cut problem, MAX-CUT), задача о минимальном вершинном покрытии (minumum vertex cover problem), задача о максимальном независимом множестве (maximum independent set problem). Задача MAX-SAT возникает также в задачах искусственного интеллекта и комбинаторной оптимизации [37, 22]. В статье Кресензи и Канна [15] перечислены 15 самых популярных задач комбинаторной оптимизации, в число которых входит и задача MAX-SAT.

Для задачи MAX-SAT существуют приближенные алгоритмы, находящие за полиномиальное время решение с некоторой гарантированной точностью. Например, алгоритм Асано и др. [8] выдает набор, выполняющий хотя бы долю 0.77 количества дизъюнктов, выполненных оптимальным набором. В то же время известно, что в предположении P^NP не существует полиномиального по времени алгоритма, находящего приближенное решение, сколь угодно близкое к оптимальному. Алгоритм Данцина и др. [17] находит такое приближение, но за экспоненциальное время. Известно также много алгоритмов, решающих практические примеры задачи максимальной выполнимости (см., например, [13, 10, 39]). Для данных алгоритмов, однако, неизвестно никаких оценок (кроме тривиальных) на время работы в наихудшем случае.

Наряду с общей задачей максимальной выполнимости мы рассматриваем следующие ее частные случаи:

• (n, 3)-MAX-SAT — вариант задачи MAX-SAT для формул, в которых каждая переменная содержится не более, чем в трех дизъюнктах;

• MAX-2-SAT — вариант задачи MAX-SAT, где каждый дизъюнкт входной формулы содержит не более двух литералов;

• (п, 3)-MAX-2-SAT — вариант задачи MAX-SAT, где каждый дизъюнкт входной формулы содержит не более двух литералов и каждая переменная входит не более, чем в три дизъюнкта.

Известно, что все перечисленные выше задачи являются NP-трудными (доказательство NP-трудности задачи (п, 3)-MAX-2-SAT см., например, в [34]). Таким образом, в предположении P^NP не существует полиномиальных по времени алгоритмов для данных задач. Тем не менее, поскольку подобные задачи часто возникают в практических приложениях, важно понять, какое время требуется для их решения, даже если это время экспоненциально.

Как сказано выше, лучшие известные оценки для многих NP-трудных задач получены именно методом расщепления. Простейший алгоритм расщепления для задачи выполнимости на формуле с N переменными имеет время работы порядка 2N. Первые улучшения данной оценки были получены в начале 1980-х годов Мониеном и Шпекенмейером [30] и Данциным [2] для формул, длины дизъюнктов которых ограничены некоторой константой. Позднее было получено много оценок, улучшающих тривиальную для некоторых МР-полных подклассов задач выполнимости и максимальной выполнимости. Вопрос о том, могут ли данные две задачи быть решены за время с^, где с < 2 — константа, до сих пор остается открытым и является одним из самых знаменитых вопросов современной теоретической информатики. Однако недавно были разработаны алгоритмы, решающие задачи выполнимости и максимальной выполнимости быстрее, чем за для формул константной плотности, то есть формул, у которых отношение количества дизъюнктов к количеству переменных ограничено сверху некоторой константой [7, 16].

Типичный алгоритм расщепления сначала некоторым образом расщепляет формулу, после чего производит рекурсивные вызовы для формул меньшей сложности. Анализ такого алгоритма содержит разбор большого количества случаев, в каждом из которых показывается, что алгоритм всегда производит рекурсивные вызовы для формул, сложность которых меньше сложности исходной формулы хотя бы на некоторую константу. Для улучшения оценки на время работы алгоритма можно добавлять в алгоритм новые правила упрощения либо же проводить более детальный разбор случаев.

Основные результаты работы перечислены ниже.

1. Реализована программа, автоматически доказывающая верхние оценки на время работы алгоритмов расщепления путем анализа случаев. При помощи данной программы получено несколько новых оценок.

2. Разработано правило упрощения для задач выполнимости и максимальной выполнимости, обобщающее известные правила упрощения, присваивающие значения переменным формулы.

3. Разработан алгоритм, решающий задачу MAX-SAT на формулах константной плотности А за время cN, где с = с(Д) < 2 — константа, с использованием лишь полиномиальной памяти.

4. Доказаны следующие новые верхние оценки на время работы алгоритмов расщепления:

• 2к/61 где К — количество дизъюнктов входной формулы, для MAX-2-SAT;

• 2ЛГ/6"7, где N — количество дизъюнктов входной формулы, для (n, 3)-MAX-2-SAT.

Алгоритмы для (n, 3)-MAX-SAT и MAX-2-SAT являются самыми быстрыми из известных. Алгоритм для MAX-SAT, работающий на формулах константной плотности быстрее, чем 2N, является первым известным алгоритмом для данной задачи, улучшающим тривиальную оценку и при этом пользующимся лишь полиномиальной памятью. Реализованная программа для автоматического анализа алгоритмов расщепления и обобщенное правило упрощения являются первыми в своем роде.

Основные результаты диссертации опубликованы в семи работах [3, 5, 6, 25, 24, 26, 4].

Список литературы диссертационного исследования кандидат физико-математических наук Куликов, Александр Сергеевич, 2009 год

1. Гэри М., Джонсон Д. Вычислительные машины и труднорешаемые задачи. М., Мир, 1982. Пер. с англ.

2. Данцин Е. Я. Системы доказательства тавтологичности, основанные на методе расщеплений. Диссертация на соискание степени канд. ф.-м. н. — Л., ЛОМИ. 1983.

3. Куликов А. С. Верхняя оценка О(20 16254п) для точной 3-выполнимости: более простое доказательство // Записки научных семинаров ПОМИ. 2002. Т. 293. С. 118-128.

4. Куликов А. С., Куцков К. Новые верхние оценки для задачи максимальной выполнимости // Дискретная математика. 2009. Т. 21, № 1. С. 139-157.

5. Куликов А. С., Федин С. С. Решение задачи о максимальном разрезе за время 21-Б1/4 // Записки научных семинаров ПОМИ. 2002. Т. 293. С. 129-138.

6. Куликов А. С., Федин С. С. Автоматические доказательства верхних оценок на время работы алгоритмов расщепления // Записки научных семинаров ПОМИ. 2004. Т. 316. С. 111-128.

7. Arvind V., Schuler R. The quantum query complexity of 0-1 knapsack and associated claw problems // Proceedings of the 14th Annual International Symposium on Algorithms and Computation. Vol. 2906 of Lecture Notes in Computer Science. 2003. P. 168-177.

8. Asano T., Hori K., Ono T., Hirata T. A theoretical framework for hybrid approaches to MAX SAT // Proceedings of the 8th International Symposium on Algorithms and Computation. Vol. 1350 of Lecture Notes in Computer Science. 1997. P. 153-162.

9. Bansal N., Raman V. Upper Bounds for MaxSat: Further Improved // Proceedings of ISAAC'99. Vol. 1741 of Lecture Notes in Computer Science. 1999. P. 247-258.

10. Battiti R., Protasi M. Reactive search, a history-base heuristic for MAXSAT // ACM Journal of Experimental Algorithmics. 1997. Vol. 2.

11. Beame P., Impagliazzo R., Pitassi T., Segerlind N. Memoization and DPLL: formula caching proof systems // Proceedings of 18th IEEE Annual Conference on Computational Complexity. 2003. P. 248-259.

12. Beigel R., Eppstein D. 3-coloring in time 0(1.3289n) // Journal of Algorithms. 2005. Vol. 54, N. 2. P. 168-204.

13. Borchers B., Furman J. A two-phase exact algroithm for MAX-SAT and weighted MAX-SAT problems // Journal of Combinatorial Optimization. 1999. Vol. 2, N. 4. P. 299-306.

14. Chen J., Kanj I. Improved exact algorithms for MAX-SAT // Proceedings of the 5th LATIN. Vol. 2286 of Lecture Notes in Computer Science. 2002. P. 341-355.

15. Crescenzi P., Kann V. How to find the best approximation results — a follow-up to Garey and Johnson // ACM SIGACT News. 1998. Vol. 29, N. 4. P. 90-97.

16. Dantsin E. Y., Hirsch E. A., Gavrilovich M. R., Konev B. Y. MAX SAT approximation beyond the limits of polynomial-time approximation // Annals of Pure and Applied Logic. 2001. Vol. 113, N. 1-3. P. 81-94.

17. Davis M., Logemann G., Loveland D. A machine program for theorem proving 11 Comm. ACM. 1962. Vol. 5. P. 394-397.

18. Davis M., Putnam H. A computing procedure for quantification theory // J. Assoc. Comp. Mach. 1960. Vol. 7. P. 201-215.

19. Gramm J., Guo J., Hiiffner F., Niedermeier B. Automated Generation of Search Tree Algorithms for Hard Graph Modification Problems // Algorithmica. 2002. Vol. 39, N. 4. P. 321-347.

20. Gramm J., Hirsch E. A., Niedermeier R., Rossmanith P. Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT // Discrete Applied Mathematics. 2003. Vol. 130, N. 2. P. 139-155.

21. Hansen P., Jaumard B. Algorithms for the maximum satisfiability problem 11 Computing. 1990. Vol. 44. P. 279-303.

22. Hirsch E. A. New Worst-Case Upper Bounds for SAT // Journal of Automated Reasoning. 2000. Vol. 24, N. 4. P. 397-420.

23. Kojevnikov A., Kulikov A. S. A New Approach to Proving Upper Bounds for MAX-2-SAT // Proceedings of the Seventeenth Annual ACM-SIAM Symposium on Discrete Algorithms. 2006. P. 11-17.

24. Kulikov A. S. Automated Generation of Simplification Rules for SAT and MAXSAT // Proceedings of the Eighth International Conference on Theory and Applications of Satisfiability Testing. Vol. 3569 of Lecture Notes in Computer Science. 2005. P. 430-436.

25. Kulikov A. S., Kutzkov K. New Bounds for MAX-SAT by Clause Learning // Proceedings of the 2nd International Computer Science Symposium in Russia. Vol. 4649 of Lecture Notes in Computer Science. 2007. P. 194-204.

26. Kullmann 0. New methods for 3-SAT decision and worst-case analysis // Theoretical Computer Science. 1997. Vol. 223. P. 1-72.

27. Kullmann O., Luckhardt H. Algorithms for SAT/TAUT decision based on various measures. Preprint. 1998.

28. Marques-Silva J., Sakallah K. GRASP: a search algorithm for prepositional satisfiability // IEEE Transactionon Computers. 1999. Vol. 48, N. 5. P. 506-521.

29. Monien B., Speckenmeyer E. Solving satisfiability in less than 2n steps // Discrete Applied Mathematics. 1985. Vol. 10. P. 287-295.

30. Moskewicz M., Madigan C., Zhao Y., Zhang L., Malik S. Chaff: engineering- an efficient SAT solver // Proceedings of the 38th Design Automation Conference. 2001. P. 530-535.

31. Niedermeier R., Rossmanith P. New upper bounds for Maximum Satisfiability // Journal of Algorithms. 2000. Vol. 36. P. 63-88.

32. Nikolenko S. I., Sirotkin A. V. Worst-case upper bounds for SAT: automated proof // Proceedings of the 8th ESSLLI Student Session. 2003. P. 225-232.

33. Raman V., Ravikumar B., Srinivasa Rao S. A simplified NP-complete MAXSAT problem // Information Processing Letters. 1998. Vol. 65, N. 1. P. 1-6.

34. Robson J. Algorithms for maximum independent sets // Journal of Algorithms. 1986. Vol. 7, N. 3. P. 425-440.

35. Wallace R. J. Enhancing maximum satisfiability algorithms with pure literal strategies // Proceedings of the 11th Canadian Conference on Artificial Intelligence. Vol. 1081 of Lecture Notes in Computer Science. 1996. P. 388-401.

36. Williams R. On Computing A;-CNF Formula Properties // Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing. Vol. 2919 of Lecture Notes in Computer Science. 2003. P. 330-340.

37. Yagiura M., Ibaraki T. Efficient 2 and 3-flip neighborhood search algorithms for MAX SAT // Proceedings of the Fourth Annual International Computing and Combinatorics Conference. Vol. 1449 of Lecture Notes in Computer Science. 1998. P. 105-116.

38. Zhang H. SATO: An Efficient Propositional Prover // Proceedings of the 14th International Conference on Automated Deduction. Vol. 1249 of Lecture Notes in Computer Science. 1997. P. 272-275.