Эвристика алгоритма логической выполнимости

Булеву проблему выполнимости (часто сокращенно SAT) можно формально сформулировать как: задано логическое выражение $B$ с $V=\{v_{0},\ldots ,v_{n}\}$ переменные, нахождение присваивания $V^{*}$ переменных таких, что $B(V^{*})$ это правда. Это рассматривается как каноническая NP-полная задача. Хотя не известно ни одного эффективного алгоритма для решения этой проблемы в общем случае, существуют определенные эвристики , неофициально называемые «эмпирическими правилами» в программировании, которые обычно могут помочь решить проблему достаточно эффективно.

Хотя не известно ни одного известного алгоритма, позволяющего решать SAT за полиномиальное время, существуют классы задач SAT, для которых существуют эффективные алгоритмы их решения. Эти классы проблем возникают из многих практических проблем планирования ИИ , тестирования схем и проверки программного обеспечения. ^{[ 1 ]}^{[ 2 ]} Исследования по созданию эффективных решателей SAT были основаны на различных принципах, таких как разрешение , поиск, локальный поиск и случайное блуждание, бинарные решения и алгоритм Сталмарка. ^{[ 2 ]} Некоторые из этих алгоритмов являются детерминистическими , а другие могут быть стохастическими .

Поскольку существуют алгоритмы с полиномиальным временем для преобразования любого логического выражения в конъюнктивную нормальную форму, такие как алгоритм Цейтина , постановка задач SAT в CNF не меняет их вычислительную сложность. Проблемы SAT канонически выражены в CNF, поскольку CNF обладает определенными свойствами, которые могут помочь сократить пространство поиска и ускорить процесс поиска. ^{[ 2 ]}

Эвристика ветвления в конфликтных алгоритмах

Источник: ^{[ 2 ]}

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

Ранние эвристики ветвления (эвристика Бома, эвристика максимального вхождения в предложениях минимального размера и эвристика Джерослоу-Ванга) можно рассматривать как жадные алгоритмы . Их основная предпосылка — выбрать свободное присвоение переменной, которое будет удовлетворять большинству уже невыполненных условий в логическом выражении. Однако по мере того, как логические выражения становятся больше, сложнее или более структурированными, эти эвристики не могут собрать полезную информацию об этих проблемах, которая могла бы повысить эффективность; они часто застревают в локальных максимумах или не учитывают распределение переменных. Кроме того, более крупные проблемы требуют большей обработки, поскольку операция подсчета свободных переменных в невыполненных предложениях доминирует во время выполнения.

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

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

Стохастические решатели

Источник: ^{[ 3 ]}

Решатели MAX-SAT (версия SAT, в которой максимальное количество удовлетворенных предложений) также могут решаться с использованием вероятностных алгоритмов. Если нам дано логическое выражение $B$ , с $V=\{v_{0},\ldots ,v_{n}\}$ переменные, и мы устанавливаем каждую переменную случайным образом, затем каждое предложение $c$ , с $|c|$ переменных, имеет шанс быть удовлетворен конкретным присвоением переменной Pr( $c$ доволен) = $1-2^{-|c|}$ . Это связано с тем, что каждая переменная в $c$ имеет ${\frac {1}{2}}$ вероятность удовлетворения, и нам нужна только одна переменная в $c$ быть удовлетворенным. Это работает $\forall ~|c|\geq 1$ , поэтому Pr( $c$ доволен) = $1-2^{-|c|}\geq {\frac {1}{2}}$ .

Теперь мы покажем, что случайное присвоение значений переменным является ${\frac {1}{2}}$ -алгоритм аппроксимации, что означает, что это оптимальный алгоритм аппроксимации, если только P = NP. Предположим, нам дано логическое выражение $B=\{c_{i}\}_{i=1}^{n}$ и

\delta _{ij}={\begin{cases}0&{\text{if }}c_{i}{\text{ is satisfied}},\\1&{\text{if }}c_{i}{\text{ is not satisfied}}.\end{cases}}

{\begin{aligned}E[{\text{Num Clauses Satisfied}}]&=\sum _{i}E[\delta _{i}]=\sum _{i}1-2^{-|c_{i}|}\\&\geq \sum _{i}{\frac {1}{2}}={\frac {1}{2}}|i|={\frac {1}{2}}OPT\end{aligned}}

Этот алгоритм не может быть дополнительно оптимизирован с помощью теоремы PCP, если только P = NP.

Другие решатели Stochastic SAT, такие как WalkSAT и GSAT, являются усовершенствованием описанной выше процедуры. Они начинают со случайного присвоения значений каждой переменной, а затем просматривают заданное логическое выражение, чтобы определить, какие переменные нужно перевернуть, чтобы минимизировать количество невыполненных предложений. Они могут случайным образом выбрать переменную для переворота или выбрать новое назначение случайной величины, чтобы избежать локальных максимумов, во многом аналогично алгоритму моделирования отжига .

Взвешенные проблемы SAT

Существует множество взвешенных задач SAT как оптимизационные версии общей задачи SAT. В этом классе задач каждому предложению логического выражения CNF присваивается вес. Целью является максимизация или минимизация общей суммы весов удовлетворенных предложений с учетом логического выражения. взвешенный Max-SAT — это версия максимизации этой задачи, а Max-SAT — это экземпляр взвешенной задачи MAX-SAT, в которой веса каждого предложения одинаковы. Частичная проблема Max-SAT — это проблема, в которой некоторые условия обязательно должны быть выполнены (жесткие условия), а общая сумма весов остальных условий (мягкие условия) должна быть максимизирована или минимизирована, в зависимости от задачи. Частичный Max-SAT представляет собой промежуточное звено между Max-SAT (все пункты мягкие) и SAT (все пункты жесткие).

Обратите внимание, что стохастические вероятностные решатели также можно использовать для поиска оптимальных приближений для Max-SAT.

Разделение переменных

Разделение переменных — это инструмент для поиска верхних и нижних границ задачи Max-SAT. Он включает в себя разделение переменной $a$ в новые переменные для всех случаев, кроме одного $a$ в исходном логическом выражении. Например, учитывая логическое выражение: $B=(a\lor b\lor c)\wedge (\neg a\lor e\lor \neg b)\wedge (a\lor \neg c\lor f)$ станет: $B^{*}=(a\lor b\lor c)\wedge (\neg a_{1}\lor e\lor \neg b)\wedge (a_{2}\lor \neg c\lor f)$ , с $a,a_{1},a_{2},\ldots ,a_{n}$ все они являются отдельными переменными.

Это облегчает проблему за счет введения новых переменных в логическое выражение: ^{[ 4 ]} что приводит к удалению многих ограничений в выражении. Поскольку любое присвоение переменных в $B$ может быть представлено присвоением переменных в $B^{*}$ , минимизация и максимизация весов $B^{*}$ представляют собой нижнюю и верхнюю границы минимизации и максимизации весов $B$ .

Частичный Макс-САТ

Частичный Max-SAT можно решить, сначала рассмотрев все сложные пункты и решив их на примере SAT. Общий максимальный (или минимальный) вес мягких предложений можно оценить, учитывая назначение переменных, необходимое для удовлетворения жестких предложений, и попытку оптимизировать свободные переменные (переменные, от которых не зависит выполнение жестких предложений). Последний шаг представляет собой реализацию Max-SAT с учетом некоторых заранее определенных переменных. Конечно, разные назначения переменных, удовлетворяющие жестким условиям, могут иметь разные оптимальные назначения свободных переменных, поэтому необходимо проверить разные назначения переменных, удовлетворяющие жестким условиям.

Структуры данных для хранения предложений

Источник: ^{[ 2 ]}

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

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

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

Ссылки

^ Алул, Фади А., «О решении задач оптимизации с использованием логической выполнимости», Американский университет Шарджи (2005), http://www.aloul.net/Papers/faloul_icmsao05.pdf
^ Перейти обратно: ^а ^б ^с ^д ^и Чжан, Линтао. Малик, Шарад. «В поисках эффективных решателей булевой выполнимости», факультет электротехники Принстонского университета. https://www.princeton.edu/~chaff/publication/cade_cav_2002.pdf
^ Сунг, Фил. «Максимальная выполнимость» (2006) http://math.mit.edu/~goemans/18434S06/max-sat-phil.pdf
^ Пипацрисават, Узел; Палян, Акоп; Чавира, Марк; Чой, Артур; Дарвич, Аднан (2008). «Решение взвешенных задач Max-SAT в ограниченном пространстве поиска: анализ производительности» . Журнал по логическому моделированию и вычислениям выполнимости (JSAT) . 4 (2008). Калифорнийский университет в Лос-Анджелесе: 4 . Проверено 18 апреля 2022 г.

[1] Алул, Фади А., «О решении задач оптимизации с использованием логической выполнимости», Американский университет Шарджи (2005), http://www.aloul.net/Papers/faloul_icmsao05.pdf

[princeton-2] Перейти обратно: ^а ^б ^с ^д ^и Чжан, Линтао. Малик, Шарад. «В поисках эффективных решателей булевой выполнимости», факультет электротехники Принстонского университета. https://www.princeton.edu/~chaff/publication/cade_cav_2002.pdf

[3] Сунг, Фил. «Максимальная выполнимость» (2006) http://math.mit.edu/~goemans/18434S06/max-sat-phil.pdf

[jsat-4] Пипацрисават, Узел; Палян, Акоп; Чавира, Марк; Чой, Артур; Дарвич, Аднан (2008). «Решение взвешенных задач Max-SAT в ограниченном пространстве поиска: анализ производительности» . Журнал по логическому моделированию и вычислениям выполнимости (JSAT) . 4 (2008). Калифорнийский университет в Лос-Анджелесе: 4 . Проверено 18 апреля 2022 г.

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]