Аннотация
ПЕРЕЧЕНЬ ОПРЕДЕЛЕНИЙ, УСЛОВНЫХ ОБОЗНАЧЕНИЙ,
СИМВОЛОВ, СОКРАЩЕНИЙ, ТЕРМИНОВ 3
ВВЕДЕНИЕ 4
1 Описание алгоритма CDCL 6
1.1 Выбор переменной 6
1.2 Распространение переменной 6
1.2.1 Граф импликаций 6
1.3 Решение конфликта 12
1.3.1 Построение среза и нового дизъюнкта 12
1.4 Возврат 13
2 Предлагаемая оптимизация 15
3 Программная реализация 20
3.1 Описание используемых классов и методов 20
3.2 Экспериментальные результаты 21
ЗАКЛЮЧЕНИЕ 24
СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ И ЛИТЕРАТУРЫ ... 25
В данной работе будет рассматриваться SAT проблема, суть которой заключается в нахождении набора переменных, для которых булева формула принимает истинное значение, или установлении, что таких наборов не существует. В 1971 году Стивеном Куком и независимо от него Леонидом Левиным была доказана теорема о том, что SAT задача принадлежит классу NP-полных задач. В дальнейшем эти результаты использовались для доказательства NP-полноты большого количества других задач, приведением за полиномиальное время данной задачи к SAT. Поэтому SAT-задача имеет большое распространение в прикладных задачах, например:
• Метод кластеризации k-means (метод к-средних) может быть решен с помощью SAT.
• Задача оптимального распределения задач по процессорам может быть решена с помощью SAT.
• Многие рекомендательные системы используют алгоритм разложения булевых матриц для рекомендации контента. Оптимальное разложение таких матриц может быть найдено с помощью SAT.
• Большое количество задач, связанных с графами, также может быть решено при помощи SAT.
В связи с большой распространенностью в прикладных задачах, в настоящее время проводятся ежегодные соревнования между SAT- решателями, что дает большой толчок в развитии и улучшении алгоритмов. Таким образом можно сделать вывод, что SAT задача является одной из наиболее актуальных современных проблем в виду своей большой распространенности как в теоретических исследованиях, так и в прикладных задачах. Поэтому решение SAT проблемы может оказаться очень важным как с точки зрения ответа на вопрос равенства классов P и NP, так и с точки зрения решения прикладных задач.
Булева формула SAT задачи представляется в виде КНФ: K = 1.
Необходимо найти корень уравнения или убедиться, что решения не существует. Под корнем будем понимать некоторую дизъюнкцию ранга r.
Для выполнимости формулы необходимо, чтобы все дизъюнкты принимали значение 1. В дизъюнктах, для которых все литеры, кроме одной, принимают значение 0, оставшаяся литера обязана принимать значение 1. Переменные, соответствующие таким литерам, будем называть переменными c фиксированными значениями.
Для решения задачи используются алгоритмы, основанные на ветвлении и возврате. Алгоритм DPLL(Davis-Putnam-Logemann-Loveland) является одним из первых и высокоэффективных алгоритмов решения SAT задачи, на основе которого разрабатываются современные SAT-решатели.
DPLL включает в себя 3 основных шага:
1. Выбор переменной ветвления.
2. Распространение переменной.
3. Решение конфликта.
Алгоритм CDCL, который будет рассматриваться в данной работе, является улучшением DPLL. Основные отличия CDCL от DPLL заключаются в использовании графа импликаций для анализа и разрешения конфликта, запоминании новых дизъюнктов в ходе анализа и нехронологическом возврате.
В данной работе будет предложен метод оптимизации алгоритма CDCL, позволяющий уменьшить как ранг получаемого корня, так и время работы.
В данной работе был рассмотрен алгоритм CDCL решения SAT задачи, а также исследован метод оптимизации алгоритма, основанный на представлении КНФ в виде троичной матрицы, разбиении этой матрицы на подмножества и анализе этих подмножеств. Было проведено экспериментальное сравнение скорости и качества решения для классического алгоритма CDCL и алгоритма CDCL с применением предложенной оптимизации, в ходе которого было установлено, что предложенная модификация позволяет добиться уменьшения ранга корня, а также времени работы алгоритма.
Результаты исследования были представлены на IX Международной молодежной научной конференции «Математическое и программное обеспечение информационных, технических и экономических систем». Томск, 26-28 мая 2022 г.
