Оптимизация задачи проверки выполнимости булевских ограничений при помощи кэширования промежуточных результатов

Аннотация

Задача — оптимизировать алгоритм проверки выполнимости булевых формул DPLL (Davis — Putnam — Logemann — Loveland) с помощью кэширования промежуточных результатов. Дополнительная информация для оптимизации алгоритма запоминается на одном из пердыдущих запусков алгоритма. Возможность подобного рода модификации алгоритма основана на особенности последовательностей проверяемых формул.

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

Введение

Задача проверки выполнимости булевых формул

Задача проверки выполнимости булевых формул (SAT, или задача ВЫП) формулируется следующим образом:

Задано множество булевых переменных и определено некоторое выражение над ними. Необходимо определить, существует ли такой набор значений этих переменных, при которых выражение выполнимо, т. е. принимает значение «истина».

Согласно теореме Кука, доказанной им в 1971-м году, задача SAT NP-полна. Она также остаётся NP-полной, если выражение имеет вид конъюнктивной нормальной формы от своих переменных.

Для примера рассмотрим следующую формулу.

Формула выполнима, так как для неё мы можем в явном виде указать набор присваиваний, при которых формула становится равной истине:

x₀ = true,
x₁ = false,
x₂ = true,
x₃ = true,
x₄ = true.

В то же время формула очевидно, невыполнима.

На практике, задача SAT является фундаментальной для решения многих проблем информатики:

искусственного интелекта,
проектирования компьютерных систем,
роботостроения,
криптографии,
анализе исходного кода
и др.

Тема сведения задач из различных областей прикладной математики и информатики к задаче SAT хорошо развивается. Одна из причин этого — возможность решать задачи, возникающие в самых различных областях, единым алгоритмом решения задачи SAT.

Алгоритм DPLL

Наиболее эффективным алгоритмом проверки выполнимости булевых формул является алгортим DPLL (Davis — Putnam — Logemann — Loveland), основанный на бэк-трекинге. Суть алгоритма заключается в том, что для исходной булевой формулы запускается рекуррентная функция, производящая над формулой следующие действия:

Распространение «единичных» конъюнктов (unit propogation). Если в КНФ присутствует конъюнкт, состоящий из одного литерала (отрицания литерала), он удаляется из КНФ, а все вхождения литерала заменяются на true (false).
Удаление «чистых» литералов (pure literal elimination). Производится поиск в формуле «чистых» литералов — переменные в которых встречаются только без отрицаний или только с ними — и вместо них подставляются значения true или false соответственно. Несмотря на то, что этот шаг является частью оригинального алгоритма, на практике, обычно, его опускают, поскольку накладные расходы зачастую превосходят эффект от его применения.
Выбор очередного литерала и запуск рекуррентной функции от формулы, в которой выбранная литера заменена на true и запуск функции, в которой она заменена на false.

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

Постановка задачи

Существует проект Avalanche, в котором в ходе динамического анализа программы встаёт задача проверки выполнимости булевых ограничений, которая сводится к проблеме SAT.

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

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

Требования к решению

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

Исследование и построение решения задачи

Проект Avalanche

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

см. Статью И. Исаева про Avalanche

На одном из этапов работы программы, представленных на схеме, инструменту необходимо проверить набор булевых ограничений.

Работа инструмента Avalanche

Для решения задачи выполнимости булевых ограничений в проекте используется солвер STP. Схема работы солвера представлена ниже.

Работа солвера STP

Решение этой задачи занимает значительную часть работы. Так, на половине проектов, которые были проанализированы инструментом Avalahche, работа STP заняла больше 70 % всего времени, а на таких проектах как «sndfile-mix-to mono» и «cjpeg», солвер работал более 99 % от времени работы инструмента. Следовательно, существует потребность в оптимизации алгоритма решения этой задачи.

STP выполняет некие преобразованя входных формул, в том числе преобразование выражений в КНФ, кототрые он подаёт на вход решателю MiniSat.

Модификация алгоритма DPLL

В решателе MiniSat используется рассмотренный ранее алгоритм DPLL.

Поскольку задача SAT является в общем случае труднорешаемой, стоит попробовать оптимизировать алгоритм с учётом особенностей формул, выполнимость которых необходимо проверять. Зачастую требуется проверить набор ограничений следующего вида:

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

Пример графа потока управления

На схеме представлен граф потока управления некоторой программы. В ходе динамического анализа существует необходимость покрыть как можно больше операторов программы. Для этого необходимо выяснить, какие ограничения (например, значения переменных) должны выполняться, чтобы выполнения программы шло по одному из возможных путей.

На представленном примере возможны три выполнения программы. Им соответствуют следующие ограничения:

Продолжим рассмотрение общей формулы, и поскольку выполнимость формулы и выполнимость её отрицания — вещи, связанные слабо, преобразуем систему к более общему виду:

Заметим, что формулы m-1 и m, соответственно, имеют вид:

При достаточно больших m одинаковая часть обеих формул значительно превышает части, в которых они различаются.

Попробуем использовать информацию, полученную при проверке выполнимости формулы A для проверки выполнимости B = A & C.

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

Пример работы алгоритмов

Рассмотрим предложенный алгоритм на двух следующих конкретных формулах:

Формула B есть конъюнкция формулы A и C = . Рассмотрим, сначала, как работает алгоритм DPLL без pure literal assign для формулы A.

Сплошными линиями на схеме показана работа алгоритма для формулы A. В вершине 3 формула принимает вид false & $mathrm {false} land (overline {x_3} lor x_4)$ и тождественно равна false. После этого вычисление возвращается к последней нерассмотренной ветке, а именно, выбору true в качестве значения переменной x₀. В вершине 6 формула тождественно равна true, следовательно, исходная формула выполнима (значения переменных можно проследить, пройдя из этой вершины к корню). При этом осталась нерассмотренной ветка, выходящая из вершины 5, в которой переменной x₃ присваивается значение true.

Пъимеъ ъабоэы алгоъиэма dpll, Меэками sel, и up обоз�?аче�?ы пъиьваива�?ия, пъоиьњодящие �?а шагањ выбоъа пеъеме�?�?ой и ъаьпъоьэъа�?е�?ия еди�?ич�?ыњ ко�?ъю�?кэов, ьооэвеэьэве�?�?о,

Пример работы алгоритма DPLL. Метками Sel. и UP обозначены присваивания, происходящие на шагах выбора переменной и распространения «единичных» конъюнктов, соответственно.

Рассмотрим теперь работу алгоритма при проверке выполнимости формулы B. Вычисление начнём не с корня дерева, а с точки, на которой мы закончили вычисление при проверке выполнимости формулы A. При этом мы сохранили значения формулы и переменных в вершине 6, а также в вершине 5 — единственной, оставшейся непросмотренной. На схеме вершины, в которых запомнены состояния закрашены.

Пъимеъ ъабоэы модиіиџиъова�?�?ого алгоъиэма dpll,

Пример работы модифицированного алгоритма DPLL.

Например, состояния в вершинах 5 и 6 следующие:

Дальнейшее вычисление на схеме показано сплошными линиями. Добавим к формуле в вершине 6 конъюнкцию и присвоим переменным значения из состояния в этой вершине. Получим формулу . Последующее продвижение единичных конъюнктов в вершине 7 показывает, что формула равна false. Выполнимость формулы B в этой вершине не доказана. Вернёмся к последней нерассмотренной вершине (вершина 5) и продолжим вычисление с этой точки. В вершине 10 формула тождественно равна true и выполнимость формулы B доказана.

Таким образом, для формул

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

Для проверки алгоритма на практике, был написан тестовый солвер на языке Java. Он реализует алгоритм DPLL без шага, на котором удаляются «свободные» литералы. Выбор очередного литерала выполняется только после того, как шаг продвижения единичных конъюнктов более неприменим. Такой подход используется в большинстве реализация алгоритма DPLL.

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

Помимо случайно сгенерированных формул, программа работает с формулами в конъюнктивной нормальной форме, записанными в текстовый файл. Переменные обозначаются символом «x» с индексом, отрицание знаком «~», логическое сложение — знаком «|», логическое умножение — знаком «&». Поскольку формула задаётся только в КНФ, скобки опускаются.

Например, формула

должна быть записана следующим образом: x0|x1&~x1|x2|~x3&x3|x4.

Вывод солвера для входа x0|x1&x0|~x1&~x0|x2&~x3|x4:

(x0 | x1) & (x0 | -x1) & (-x0 | x2) & (-x3 | x4) After UP — (x0 | x1) & (x0 | -x1) & (-x0 | x2) & (-x3 | x4) Select 0 Assign (Select) x0 = false (x1) & (-x1) & (-x3 | x4) Assign (UP) x1 = true After UP — () & (-x3 | x4) <------- SAT is false. Assign (Select) x0 = true (x2) & (-x3 | x4) Assign (UP) x2 = true After UP — (-x3 | x4) Select 3 Assign (Select) x3 = false SAT is true - 1012 - 0, -> 2, => 3, <-

Пример вывода тестового солвера

В последней строке содержится информация о том, что для формулы установлена её выполнимость. Там же содержится вектор присваиваний - 1012, где каждая цифра соответствует значению переменной (true для переменных с номерами 0 и 2, false для переменной с номером 3 и переменная 1 осталась без присваивания. Строка 0, -> 2, => 3, <- — описание ветки, на которой было найдено решение. Все эти результаты сохраняются в памяти.

Сравним время работы алгоритма на примерах указанного вида до и после оптимизации.

Заключение

В ходе исследования эффективности алгоритма, были случайным образом сгенерированы последовательности булевых формул с особенностями, которыми обладают формулы, сгенерированные солвером STP на основе последовательностей булевых ограничений, передаваемых им ядром инструмента Avalanche. Последовательности были проверены на тестовом солвере сначала алгоритмом DPLL, а затем его модифицированным вариантом.

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

Поскольку в среднем алгоритм даёт выигрыш во времени, он может быть применён для указанных выше целей.

В дальнейшие планы входит внедрение алгоритма в решатель MiniSat и проверка его эффективности в работе.

ДАЛЬШЕ