Диссертация (1090534), страница 10
Текст из файла (страница 10)
Если есть переменная pi , такая что вКНФ формулу входят соответствующие литералы с одним знаком (pi или¬pi ), то литерал с тем же знаком должен быть добавлен в модель. Всеутверждения, содержащие добавленный литерал, могут быть удалены изКНФ, литерал противоположного знака должны быть удалены из всехутверждений.– Разрешение и ветвление. Необходимо выбрать литерал в КНФформуле, не имеющий присвоенного значения, после чего анализируютсяподформулы (F ∧ pi ) и (F ∧ ¬pi ).Предложенный алгоритм представляет собой процедуру “ветвления и границ”,проверяющую все возможные наборы значений входных параметров дляформулы F .
Пространство поиска может быть представленно в виде дерева,где узлами являются частичные наборы значений, к которым применяетсяпроцедура разрешения и ветвления. Если алгоритм находит противоречие(пустое утверждение), то удаляется все поддерево до момента последнего44выбора переменной. Важно отметить, что информация о структуре возникшегопротиворечия не сохраняется и, таким образом, DPLL алгоритм может снова иснова находить одно и тоже противоречие далее.2.1.2 CDCL алгоритмВ случае, если обнаружен конфлит, алгоритм вынужден отменятьсделанные ранее решения.
Анализ конфликтов — спецаильная процедура,которая ищет причину конфликта и пытается ее разрешить. Эта процедурауказывает алгоритму на те части пространства поиска, где решений не можетбыть, и на те учатски, где стоит начать новый поиск.Первоначальный DPLL алгоритм использовал простейший метод анализаконфликтов.
Для каждой переменной хранится флаг, была ли эта переменнаяиспользована с обоими знаками. В конфликтной ситуации, алгоритм ищетближайшую к текущей переменную, для которой был проверен только одинлитерал, меняет его знак (например, с pi на ¬pi ), отменяет все сделанные выборымежду заданным и текущим, и повторяет анализ.
Такой подход называетсяхронологический поиск с возвратами. Также известны стратегии, которыеанализируют не ближайшие присваивания, а более ранние. Такие методыизвестны под названием нехронологический поиск с возвратами.В процессе анализа конфликтов, информация о конфликте может бытьзаписана в виде избыточного дополнительного утверждения, которое не меняетвыполнимости исходной формулы. Такое утверждение может значительносократить пространство поиска. Подход с использованием выведенныхдополнительных утверждений известен как управляемое конфликтамиобучение дизъюнктам (англ. conflict-driven clause learning).Время, требуемое для нахождения решения, может сильно разниться дажедля похожих задач.
Две задачи, отличающиеся только порядком переменных,могут потребовать совершенного разного количества временных ресурсов прииспользовании одного и того же алгоритма. Для борьбы с этим эффектом,современные SAT алгоритмы используют технику случайных перезапусков.Алгоритм случайным образом отбрасывает некоторые участки пространства45поиска, сохраняя при этом выученные конфликтные утверждения. Такой подходповышает устойчивость алгоритма поиска.Большое значение при построении КНФ формулы для задачи SAT имеетвыбранный способ трансляции (кодировка) утверждений логики высказыванийк КНФ.
Для ряда задач выбранная кодировка является определяющим факторомпринципиальной возможности ее решения. Только самые простые проблемымогут быть решены при использовании тривиальных кодировок. Поискподходящей кодировки — трудоемкая и длительная процедура. Более того,нет методов, которые бы одинаково хорошо работали с любыми задача — длякаждой новой проблемы следуют пробовать несколько вариантов трансляции.Для упрощения SAT формул используется ряд автоматических системупрощения задачи, которые могут улучшить результаты кодирования, особеннопри использовании тривиальных методов трансляции.
Однако, результатывыполнения таких автоматических процедур как правило значительно хужекодировок, разработанных вручную. Улучшение используемого методатрансляции — это, как правило, итеративный процесс проб и ошибок, врамках которого выполняются различные модификации алгоритма трансляции,после чего измеряются общее время работы алгоритма SAT при решении задачи.Ключом к построению оптимальной кодировки является знание обособенностях предметной области. Ответы на такие вопросы как “Какаяинформация необходима для построения решения?”, “Какие решениянеобходимо принять, чтобы найти ответ?” и “Какая важная информациясодержится во входных данных?” позволяют выделить те или переменныеили ограничения, которые могут существенно повлиять на процесс поискарешения в целом.
Например, для задачи может быть известна нижняя границазначения для определенного параметра. Эту информацию стоит отразить ввиде дополнительных ограничений, что позволит алгоритму SAT не тратитьресурсы на поиски решения там, где его не может быть. Аналогично, еслиизвестно, что решения имеют определенные симметрии, это стоит отразить ввиде ограничений, запрещающих некоторые из них.Примером такого итеративного улучшения кодировки может послужитьподход к решению задач биолии, описанный в работе [64]. Первоначальный методтрансляции обеспечивал производительность поиска решения существенно хуже,в сравнении с существовавшими алгоритмами.
Исследование предметной области46и использование полученных знаний при построении алгоритма трансляциипозволили добиться производительности на порядки большей, чем традиционныеметоды решения.Одним из наиболее известных методов трансляции является подход,описанный в работе Цейтина [59]. Данный алгоритм ставит в соответствиекаждой нетривиальной формуле дополнительную переменную, соответвтующуювыходу заданного логического вентиля. Эта переменная затем используетсядля построения сложных составных формул.
Такой подход позволяет такжеиспользовать ряд простых оптимизаций, включая поиск и выделение большихконъюнкий и дизъюнкций, удаление отрицаний переменных при учитыванииполярности переменных.Плайстед и Гринбаум в своей работе [65] предложили модифицированныйвариант трансляции Цейтина, являющийся, по сути, его подмножеством. В основеих работы лежит слежение за полярностью переменных входящих в логическиевыражения. С учетом полученной информации, можно удалить из рассмотрениябольшие части формулы, построенной методом Цейтина.
Для этого к формуледобавляются дополнительные утверждения специального вида. Данный подходпозволяет значительно уменьшить размер результирующего выражения. Однако,как показывают эксперименты, поизводительность процедуры распространенияпеременной при этом может ухудшиться.Более современные работы ( [66–68]) используют различные вариантыпромежучтоного представления исходной формулы. Все эти работы опираютсяна добавление дополнительных связей между переменными и ограничениями.после чего применяют различные трансформации к полученным данным с цельюих упрощения. В частности, в работе [69] используется метод технологическогоотображения, обычно используемый при проектировании интегральных схем.2.1.3 Метод поиска стабильных моделейПрограммирование множеств ответов (англ.
answer set programming,ASP) — подход декларативного программирования к решению вычислительносложных проблем поиска, в частности, N P -сложных (англ. N P -hard) задач.47Понятие стабильных моделей (англ. stable model) является ключевым в теорииASP задач. Стабильная модель [70] — один из способов представлениязаключений при заданных логических правилах, наряду с обоснованным (англ.well-defined semantics) [71] подходом. Понятие стабильных моделей выражаетправило логического вывода “отрицание как неудача” (англ. negation as failure,NAF). NAF — немонотонное правило вывода, позволяющее выводить значениелитерала ¬p через невозможность доказать p.
Немонотонная логика —формальная логика, в которой причинно-следственные отношения немонотонны,т.е. могут становиться как истиными, так и ложными по мере поступления новойинформации о задаче.Стабильные модели и NAF позволяют работать с формальными системамина базе предположения об открытости мира (ПОМ).
Согласно ПОМ, истинноситьутверждения не зависит от того, существуют ли свидетельства о его истинностиили ложности. Утверждения о знании, которые не включены в систему и невыведены из нее, считаются неизвестными, а не ложными, как в случае системс предположением о закрытости мира.ASP подход позволяет формулировать проблему в терминах программнемонотонной логики, решениями же будет наборы множеств ответов илимоделей.
Базовыми элементами таких программ являются правила вывода,факты и ограничения и не включают в себя конкретных алгоритмов решениязадачи. Такой подход позволяет перейти от императивного метода решениязадач (от описания того, “как” решить задачу) к декларативному (“чтовключает в себя задача”). Правильно построенная таким образом спецификация,без неоднозначных или противоречивых утверждений, не будет значительноотличаться от исходной постановки проблемы. Декларативный подход кпостроению задач менее трудоемкий.ASP подход тесно связан с SAT задачей и, в частности, можетрассматриваться как ее расширение. Стабильные модели позволяют вместовопроса “может ли быть выполнена формула F?” задать вопрос “какие естьспособы выполнить формулу F?”В работе [72] процедура перечисления моделей используется для выводалогических ограничений и правил при анализе больших объемов данных,например, биологического или медицинского происхождения.
В данной работерассматривается подход, основанный на использовании техник комбинаторики48и методах решения оптимизационных задач, позволяющий делать логическиезаключения о неявной (непредставленной) информации исходя из имеющейсяинформации. Центральное место рассматриваемого алгоритма занимаетпостроение и решение задачи ASP.Сходный подход представлен и в работе [73], рассматривающей проблемуконфигурирования программных продуктов, которые могут включать в себяобязательные, необязательные и взаимоисключающие друг друга настройки.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
