Алгоритмы расщепления для задачи о пропозициональной выполнимости

В статье исследуется задача о пропозициональной выполнимости и известные алгоритмы ее решения. Приведено обоснование её значимости как широко применимой задачи, для которой впервые было сформулировано и доказано свойство NP-полноты. Автором разработана и описана программа, реализованная на основе DPLL-алгоритма, позволяющая найти решение задачи о пропозициональной выполнимости.

Ключевые слова: ВЫПОЛНИМОСТЬ, SAT, конъюнктивная нормальная форма, литерал, клоз, NP-полнота, DPLL-алгоритмы, PPSZ-алгоритмы, алгоритмы расщепления, декомпозиционные алгоритмы, правила редукции.

Задача о пропозициональной выполнимости (англ. вариант — SATISFIABILITY, или SAT) имеет следующую формулировку [1]. Пусть X — это конечное множество переменных со значениями false или true. Формула F в конъюнктивной нормальной форме (КНФ) является конъюнкцией конечного числа клозов, где клоз — это дизъюнкция литералов, не содержащая ни одной переменной одновременно с ее отрицанием, а всякий литерал — это некоторая переменная xX либо ее отрицание ¬x. Необходимо установить, существует ли для некоторой формулы F, заданной в КНФ над множеством переменных X, такой набор значений переменных, при котором каждый клоз формулы F принимает значение true (такой набор называют выполняющим). Формула считается выполнимой, если для нее существует хотя бы один выполняющий набор, и невыполнимой, если такого набора не существует.

Размерность входной формулы F обычно характеризует некая числовая величина, которая принимает неотрицательные целые значения. Величины такого рода называют мерами сложности формулы логики высказываний. Среди основных мер сложности рассматривают: N= |X| — число переменных; K — число клозов; L = |F| — длину формулы F, то есть количество входящих в нее литералов. Относительно этих мер сложности традиционно определяют вычислительную сложность исследуемого алгоритма решения SAT.

Задача SAT является объектом исследований в таких областях как искусственный интеллект, временная и пространственная логика, распознавание образов, автоматическое доказательство теорем, теория реляционных баз данных, теория графов и некоторые разделы комбинаторики, техническое проектирование.

В статье Стивена Кука 1971 года [2] впервые был введен термин «NP-полная задача». Задача SAT была первой задачей, для которой было доказано данное свойство. Многие проблемы из класса NP сводятся к данной задаче [3].

К полиномиально разрешимым случаям для SAT относятся следующие классы формул: пустые формулы (которые не содержат клозов, то есть такая формула интерпретируется как true); формулы в 2-КНФ (каждый их клоз содержит не более двух литералов); хорновские формулы и другие классы формул [4, 5].

Алгоритм полного перебора анализирует все 2^N различных наборов значений N переменных, устанавливая тривиальную верхнюю оценку вычислительной сложности SAT в худшем случае. С начала 60-х годов прошлого века и до настоящего времени активно ведется поиск алгоритмов, работающих быстрее полного перебора [1]. Среди них наиболее известными являются алгоритмы, основанные на локальном поиске, и алгоритмы расщепления [6] (DPLL-алгоритмы, PPSZ-алгоритмы).

Алгоритм, основанный на локальном поиске, прежде всего выбирает начальный набор и далее изменяет его шаг за шагом в попытке приблизиться к выполняющему набору. Если после некоторого количества шагов не удается найти выполняющий набор, то алгоритм выбирает другой начальный набор и вновь изменяет его шаг за шагом. Число этих попыток ограничено и если ни в одной из них не удалось найти выполняющий набор, то алгоритм заканчивает работу с ответом «Невыполнима».

Алгоритмы расщепления являются декомпозиционными, то есть сводят задачу SAT для заданной формулы F к конечному числу подзадач, каждая из которых также является задачей SAT для формул с меньшей сложностью, чем сложность F. При этом такое сведение может быть детерминированным (алгоритм производит рекурсивные вызовы самого себя для формул с меньшей сложностью, полученных путем расщепления F) или вероятностным (случайным образом выбирается одна из образованных расщеплением формул). Детерминированные алгоритмы расщепления обычно называют DPLL-алгоритмами по первым буквам фамилий их авторов: M. Davis, H. Putman, G. Logemann, D. Loveland [7, 8]. Такой алгоритм заменяет заданную формулу F на две формулы F [x] и F [], полученные путем присваивания некоторой переменной x значений true и false соответственно. Далее алгоритм упрощает каждую из полученных формул и после рекурсивно вызывает процедуру для каждой из упрощенных формул. Основное отличие PPSZ-подобных алгоритмов от DPLL-подобных алгоритмов заключается в выборе переменных для присваивания значений (производится случайный выбор вместо детерминированного). Большинство алгоритмов из тех, которые были разработаны за последние пятьдесят лет для SAT, основано на идеях, заложенных в DPLL-алгоритмах.

Всякий DPLL‑алгоритм выполняется по следующей схеме. [1]

Вход: формула F в КНФ над X.

Ответ: «Выполнима» / «Невыполнима».

1.                Редуцирование F, то есть преобразование формулы F в F₀ меньшей сложности путем применения конечного набора правил редукции. Эти правила применяются к F до того момента, пока хотя бы одно из них применимо.
2.                Если SAT тривиально разрешима для F₀, то выдается соответствующий ответ.
3.                Выбор переменной xX по определенному правилу. Таких переменных может быть выбрано несколько. Их количество задается правилом расщепления, используемом на следующем шаге.
4.                Расщепление формулы F₀ на конечное число формул с меньшей сложностью по указанному правилу расщепления, используя различные значения переменных, выбранных на шаге 3.
5.                Осуществление рекурсивных вызовов указанного алгоритма c полученными формулами в качестве входных параметров. Выдача ответа, основанного на результатах, которые были возвращены рекурсивными вызовами. При этом если хотя бы один из рекурсивных вызовов вернул выполняющий набор, то необходимо выдать ответ «Выполнима», в противном случае — «Невыполнима».

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

Сфера применения DPLL‑алгоритмов не ограничивается задачей SAT. Алгоритмы расщепления также успешно применяются для решения многих других NP-полных задач, к примеру, MAX‑SAT, MAX‑2‑SAT [9].

В процессе исследования автором статьи разработана программа DPLL-Solver, реализующая DPLL-алгоритм для задачи SAT. В программе редуцирование входной формулы выполняется по правилам: «чистый литерал», «единичный клоз», «поглощение», «резолюция». Применяемое на шаге 4 правило расщепления заменяет формулу F₀ на две формулы F₁ = F₀ [x] и F₂ = F₀ [¬x], где x на шаге 3 определяется по следующей эвристике: «необходимо выбрать переменную, входящую в наибольшее количество клозов». В качестве тривиальных случаев на шаге 2 выступают: пустой клоз (интерпретируется как false); пустая формула (интерпретируется как true).

Функциональное назначение процедур программы DPLL‑Solver представлено в таблице 1.

Таблица 1

Функциональное назначение процедур

Для эксплуатации программы необходимо иметь персональный компьютер типа IBM PC PentiumIV с операционной системой Windows XP/Vista и оперативной памятью от 512 Мб.

Для создания программы использована среда разработки Microsoft Visual Studio 2010 Express. Программа работает со структурами, объединяющими два динамических контейнера целых чисел типа vector из библиотеки vector в C++. Данные структуры инициализируются для работы с входной формулой в программном виде. Первый вектор задает исходную формулу в КНФ, а второй — набор значений переменных, где в процессе работы алгоритма формируется выполняющий набор.

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

Разработанная программа DPLL-Solver была проверена на большом количестве формул. Приведем одну из них. Рассмотрим формулу большой размерности, включающую в себя 12 переменных и 20 клозов:

F(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = (x1˅ x2˅ ¬x3 ˅ ¬​x6) ˄ (¬​x1 ˅ x4˅ x5˅ x6˅ x7˅ ¬​x9 ˅ x11) ˄ (x3 ˅ ¬​x5 ˅ x8 ˅ ¬​x10 ˅ x12) ˄ (x2 ˅ x4˅ ¬​x6 ˅ ¬​x8˅ x9 ˅ ¬​x11) ˄ (x4˅ x5) ˄ (x2 ˅ ¬​x3 ˅ ¬​x5 ˅ ¬​x7 ˅ x9 ˅ x11) ˄ (¬​x2 ˅ x3 ˅ ¬​x4 ˅ ¬​x8) ˄(x4 ˅x5˅ x6˅ x7˅ ¬​x9  ˅ x10 ˅ x11) ˄ (¬​x5 ˅ x8 ˅ ¬​x10˅ x11) ˄ (x4˅ x6˅ x7˅ ¬​x8˅¬​x9 ˅ x11) ˄ (¬​x7˅ x9 ˅ x10) ˄ (x1˅ x5˅ ¬​x7˅ x8˅ x11) ˄ (¬​x2 ˅ ¬​x5 ˅ ¬​x7 ˅ x8) ˄ (¬​x1 ˅ x4 ˅ x5 ˅ x6 ˅ x7 ˅ ¬​x9 ˅ x11) ˄ (x3 ˅ ¬​x5 ˅ x8˅ ¬​x10 ˅ x12) ˄ (¬​x6 ˅ ¬​x8) ˄(x5) ˄ (x7˅ ¬​x9 ˅ x11) ˄ (¬​x8) ˄ (¬​x10 ˅ x11).

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

Рис. 1. Результат выполнения программы для формулы с 20 клозами

Разработанная программа может быть использована в многочисленных приложениях задачи SAT.

Литература:

1.                Быкова В. В. Об асимптотике решений рекуррентных соотношенийспециального вида и технике Кульмана — Люкхардта // Прикладная дискретная математика. 2013. — № 4(22). — с. 56–66.
2.                Cook S. A. The complexity of theorem proving procedures // Proc. 3rd ACM Symp. on Theory of Computing. 1971. — P. 151–158
3.                Отпущенников И. В., Семенов А. А. Технология трансляции комбинаторных проблем в булевы уравнения // Прикладная дискретная математика. 2011. — № 1(11). — с. 96–115.
4.                Franco J. and Gelder A. V. A perspective on certain polynomial-time solvable classes of Satisfiability // Discr. Appl. Math. 2003. — V. 125. Iss. 2–3. — P. 177–214.
5.                Алексеев В. Б., Носов В. А. NP-полные задачи и их полиномиальные варианты. Обзор // Обозрение прикладной и промышленной математики. 1997. — Т. 4. Вып.2. — с.165–193.
6.                Всемирнов М. А., Гирш Э. А., Данцин Е. Я., Иванов С. В. Алгоритмы для пропозициональной выполнимости и верхние оценки их сложности // Теория сложности вычислений. VI. Зап. научн. сем. ПОМИ. СПб., 2001. — Т. 277. — с.14–46.
7.                Davis M., Logemann G., and Loveland D. A machine program for theorem-proving // Comm. ACM. 1962. — № 5(7). — P. 394–397.
8.                Davis M. and Putman H. A computing procedure for quantification theory // J. ACM. 1960. — № 7(3). — P. 201–215.
9.                Куликов А. С., Куцков К. Новые верхние оценки для задачи максимальной выполнимости // Дискретная математика. 2009. — № 21(1). — с. 139–157.