Диссертация (Исследование и разработка методов автоматического вывода геометрических ограничений с использованием декларативного программирования и формальных методов), страница 11

Вданной работе описан подход, упрощающий проверку, тестирование, отладкуи настройку программного обуспечения (ПО) на основе перечисления всехвозможных конфигураций.При решении различных комбинаторных задач значительное влияниена общую производительность алгоритма поиска оказывает различнаявспомогательная информация о предметной области, в рамках которой решаетсяпоставленная задача. В работе [74] описывается подход, позволяющей приформулировании ASP проблемы дополнительно описывать специфичныеэвристики для поиска решений.

В качестве реализации предлагается использоватьспециальный оператор при описании задачи. Полученная таким образоминформация учитыватся решателем логических формул при выборе следующейпеременной, которая будет рассмотрена. Экспериментальные результатыпоказывают, что удачно подобранная эвристика может в разы скоратить время,требуемое для завершения алгоритмом работы.Задача поиска стабильных моделей может быть представлена в виде задачиSAT. Такая задача называется AllSAT, ее решение зклюдчается в перечислениивсех наборов значений входных параметров, выполняющих заданную КНФформулу.2.1.4 Метод перечисления решений задачи SATРешение различных практических задач может быть основано не на поискеодного выполняющего набора значений для заданной КНФ формулы, а наперечислении всех возможных решений. Подобные задачи нередко возникаютпри решении практических задач верификации, в частности, при решении49проблемы абстракции предикатов.

В работе [75] рассматривается подход сиспользованием компактных блокирующих утверждений. Эти утверждения могутбыть выведены из частинчых выполняющих наборов. Экспериментальныерезультаты показывают, что рассматриваемый подход позволяет сократитьпотребление памяти (генерируется в 14 раз меньше частичных наборов) и в трираза сократить затрачиваемое на поиск решений время.В работе [76] рассматривается метод перечисления всех выполняющихнаборов переменных для КНФ (англ. All–SAT). Алгоритм основан на решенииSAT задачи, с использованием CDCL подхода и нехронолического поиска свозвратами. Исключение из поиска уже исследованных решений выполняетсясамим алгоритмом поиска, без использования блокирующих утверждений, чтопозволяет существенно сократить потребление памяти. Поиск нового решениятребует такого объема ресурсов, что и поиск самого первого решения, чтопозволяет решать задачи, решения которых могут занять памяти больше, чемдоступно.

Предложенный алгоритм не использует бинарные диаграммы принятиярешений (англ. binary decision diagramms). В основе рассматриваемого алгоритмалежит решатель SAT Chaff. Экспериментальные результаты показывают, чтопредложенный подход требует меньше времени для поиска решений, потребляетменьше памяти и требует меньшего числа шагов для построения решений, чемалгоритмы на базе блокирующих утверждений.В работе [77] рассматривается метод перечисления выполняющих наборов,основанный на использовании мембранных систем [78] — подходе к построениюраспределенных вычислительных систем.

Традиционные алгоритмы решениязадачи AllSAT требуют экспоненциально много временных ресурсов дляпоиска решения. Предлагаемый метод позволяет выполнить построениеэкспоненциально большого числа наборов за линейное время методовмембранного разделения. В работе подробно описывается предлагаемыйалгоритм, использующий мембранную вычислительную модель. Такжепредлагается соответствующие модели мембранной системы и самой мембраны.Далее описыыаются правила развития предлагаемой системы. Описанная модельсодержить меньшее число вложенных мембран и более простые правила вывода,в сравнении с существующими решениями и, как следствие, обладает болеевысокой производительностью, что было продемнстрировано при проведенииэкспериментов.50В работе [79] иной подход к решению задачи AllSAT, основанныйна использовании упорядоченных бинарных диаграмм принятия решения(англ.

ordered binary decision diagramm, OBDD). В данной работе описываетсямодификация существующего алгоритма построения всех выполняющихнаборов. Полученные диаграммы не обязательно оптимальны. В работеобсуждаются техники “ленивого” кэширования результатов и способыуточнения процедры кэширования методами распространения констант.Полученные алгоритмы были реализованы поверх современного решателяSAT задачи. Экспериментальные результаты показывают, что использованиепредложенных техник позволяет значительно повысить производительностьисходного алгоритма, а более точное кэширование сокращает размер полученнойдиаграммы решений.Для ряда прикладных задач большое значение имеет представлениебулевой формулы. В работе [80] предлагается метод построения ДНФформулы для заданной КНФ формулы в каноничном виде.

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

Традиционно эти задачи решаютсяпри помощи бинарных диграммрешений. Преимуществом обсуждаемого подхода является возможность строитьлокально оптимальные формулы, что позволяет улучшить масштабируемость ипроизводительность, в сравнении с диаграммами решений. Экспериментальныерезультаты показывают, что полученные ДНФ формулы в среднем на 10%короче, чем построенные с использованием традиционных подходов. Также врамках экспериментов была произведена процедура перестроения полученнойлогической схемы. Предложенный алгоритм позволил улучшить оценкуплощади–задержек на 36% в сравнении с подходом, использующим диаграммырешений.Количественный анализ информационных потоков (англ.

quantitativeinformation flow analysis, QIF) — семейство методов и алгоритмов, позволяющих51проводить анализ процессов передачи приватных данных по публичнымканалам. В работе [81] рассматривается подход к анализу исходных кодовпрограмм с использованием логической проекции и перечисления моделей. Вкачестве примера рассматриваются программы на языке ANSI C. Реализованнаяпрограммная система использует современные алгоритмы SAT для анализаограниченных моделей, #SAT с учетом проекций и предварительную обработкуSAT задач. В качестве экспериментов были использованы синтетические иполуреалистичные тестовые примеры.

В следующей своей работе [82] авторыпродолжают исследования надежных вероятностных методов перечислениямоделей. Рассматриваются различные области применения данных алгоритмовдля решения задач обеспечения информационной безопасности и распределенияресурсов. Также рассматриваются различные аспекты реализации подоныхсистем.Подход, предложенный в работе [81] опирается на алгоритм,реализованный в работе [83]. В его основе лежит использовании методаразложения на компоненты [84] и на кэшировании обнаруженных компонент[85; 86]. Компонентой называется сильносвязное подмножество графа,соответствующего заданным булевым ограничениям. Общее число выполняющихнаборов определяется произведением количества наборов, описываемых каждойкомпонентой графа.

Это следует из того, то каждая подзадача, входящая вкомпоненту, ника не зависит от других компонент. Таким образом, для подсчетаобщего числа решений используется базовый алгоритм DPLL. При выбореследующей исследуемой переменной, выполняется поиск сильносвязныхкомпонент графа ограничений, после чего рекурсивно выполняется решениеполученных подзадач.В работе [83] для построения компонент используются только толькоутверждения, содержащие не менее двух литералов без присвоенныхзначений. Пустые утверждения соответствуют конфликтным ситуациям,утверждения, содержащие один свободный литерал обрабатываются процедуройраспространения констант. Компактное описание каждой компонентысохраняется в ассоциативную таблицу, которая затем используется для быстрогопоиска числа уже полученных решений для соответствующей компоненты.Процедура распространения значения переменной оказывает значительноевлияние на общую производительность процедуры перечисления решений.

В52работе [83] используется алгоритм, основанный на поиска конфликтующихлитералов. Процедура поиска конфликтующих литералов вызывается независимоот процедуры ветвления, при этом сохраняются только конфликтующие литералы.Процедура распространения констант завершается при нахождении конфликтаили когда не больше не удается найти конфликтующие литералы. При решениитрадиционной задачи SAT подобный подход не оказывает влияния на общих ходрешения, однако, при решении задачи AllSAT этол позволяет избежать лишнихвызовов процедуры анализа компонент. Также стоит отметить, что литералы,который могут стать конфликтующими, выбираются только из множестваисходных утверждений.За последние двадцать лет методы был достигнут большой прогресс вразвитие методов и подходов решения задачи SAT. Современные алгоритмыпозволяют решать практические задачи, возникающие в различных областяхпромышленности, которые могут включать в себя тысячи и десятки тысячпеременных и ограничений, с учетом ограничений на затрачиваемое время и врамках ограниченного потребления оперативной памяти.

Развитие алгоритмоврешения SAT позволило также и решать более сложные проблемы, в частности,задачу перечисления всех возможных решений заданной декларативной модели— задачу поиска стабильных моделей и задачу All–SAT. Алгоритм перечислениявсех выполняющих наборов, описанный в работах [81; 83] используется вдиссертационной работе.2.2Элементы теории графов, используемые в работеРассмотрим неориентированный граф G =< V,E >, где V —множество вершин, E — множество ребер. Соседними называются двевершины, соединенные ребром.

Кликой называют такое множество вершин,что любая пара соединена ребрами. Размером клики назввают число вершин,которое она включает. Максимальной назвают клику, которая не может бытьрасширена добавлением вершин. Степенью вершины называется число вершин,соединенных с заданной.53Известны два варианта задачи о клике. Первой можно назвать задачу“распознавания”, в рамках которой необходимо определить, содержит лизаданный граф клику размера k.