Алгоритм CDCL (англ. conflict-driven clause learning — «управляемое конфликтами обучение дизъюнктам») — основанный на алгоритме DPLL эффективный решатель (NP-полных) задач выполнимости булевых формул (SAT-решатель). Основная структура данных в CDCL-решателях — импликационный граф, фиксирующий назначения переменным, а другой особенностью является использование нехронологического возврата и запоминание дизъюнктов в ходе анализа конфликта.
Алгоритм был предложен Жуаном Маркесом-Сильвой (англ. João Marques-Silva) и Каремом Сакаллой (англ. Karem A. Sakallah) в 1996 году[1] и независимо Роберто Байярдо (англ. Roberto J. Bayardo) и Робертом Шрагом (англ. Robert C. Schrag) в 1997 году[2][3].
DPLL-алгоритм, лежащий в основе CDCL-алгоритма, использует поиск с возвратом на конъюнктивных нормальных формах, на каждом шаге которого происходит выбор переменной и присвоения ей значения (0 или 1) для последующего ветвления, заключающегося в присваивании значения переменной, после чего упрощённая формула проходит рекурсивную проверку на выполнимость. В случае, когда встречается конфликт, то есть, полученная формула является невыполнимой, включается механизм возврата (бэктрекинга), при котором отменяются ветвления, в которых для переменной были опробованы оба значения. Если поиск возвращается к ветвлению первого уровня, вся формула объявляется невыполнимой. Такой возврат, свойственный алгоритму DPLL, называется хронологическим[3].
Дизъюнкты, используемые в алгоритме, делятся на выполнимые (satisfied), когда среди входящих в дизъюнкт значений есть 1, невыполнимые (unsatisfied) — все значения нулевые, единичные (unit) — все нули, кроме одной переменной, которой значение ещё не присвоено, и неразрешённые (unresolved) — все остальные. Одной из важнейших составляющих SAT-решателей является правило единичного дизъюнкта, при котором выбор переменной и её значения однозначен. (Следует напомнить, что в дизъюнкт входят как переменные, так и их отрицания.) Процедура распространения переменной (англ. unit propagation) (в современных CDCL-решателях она почти всегда основывается на правиле единичного дизъюнкта) производится после ветвления для вычисления логических следствий сделанного выбора[3].
В дополнение к DPLL и его механизму поиска с возвратом, CDCL использует некоторые другие приёмы[3]:
С каждой переменной проверяемой на выполнимость формулы в CDCL-алгоритме связаны несколько вспомогательных значений[3]:
Схематично типичный CDCL-алгоритм можно представить следующим образом[3]:
Алгоритм CDCL(φ, ν) вход: φ - формула (КНФ) ν - отображение значений переменных в виде множества пар выход: SAT (формула выполнима) или UNSAT (невыполнима) если UnitPropagationConflict(φ, ν) то возврат UNSAT L := 0 -- уровень решения пока NotAllVariablesAssigned(φ, ν) (x, v) := PickBranchingVariable(φ, ν) -- принятие решения L := L + 1 ν := ν ∪ {(x, v)} если UnitPropagationConflict(φ, ν) -- вывод последствий то β := ConflictAnalysis(φ, ν) -- диагностика конфликта если β < 0 то возврат UNSAT иначе Backtrack(φ, ν, β) -- возврат (бэктрекинг) L := β возврат SAT
В этом алгоритме использовано несколько подпрограмм, которые помимо возврата значений могут изменять и переданные им по ссылке переменные φ, ν[3]:
UnitPropagationConflict
итеративно применяет правило единичного дизъюнкта, возвращая значение Истина в случае нахождения невыполнимого дизъюнкта.NotAllVariablesAssigned
проверяет, есть ли ещё неназначенные переменные.PickBranchingVariable
выбирает переменную и назначаемое значение (1 или 0).ConflictAnalysis
анализирует возникший конфликт, запоминает новый дизъюнкт и даёт уровень решения, к которому необходимо вернуться.Backtrack
производит возврат к уровню, вычисленному в ходе анализа конфликта.Процедура анализа конфликта является центральной для CDCL алгоритма.
Основной структурой данных, используемой в CDCL-решателях, является импликационный граф (англ. implication graph), фиксирующий назначения переменным (как в результате решений, так и применением правила единичного дизъюнкта), в котором вершины соответствуют литералам формулы, а дуги фиксируют структуру импликаций[4][5].
Процедура анализа конфликта (см. схему алгоритма) вызывается при обнаружении конфликта по правилу единичного дизъюнкта, и на её основе пополняется множество запомненных дизъюнктов. Процедура начинает с узла импликационного графа, в котором обнаружен конфликт, и охватывает уровни решения с меньшими номерами, переходя назад по импликациям пока не встречает самую свежую назначенную (в результате решения) переменную[3]. Запомненные дизъюнкты применяются в нехронологическом возврате (англ. non-chronological backtracking) — ещё одном характерном для CDCL-решателей приёме[6].
Для сравнения:
Идея использования структуры импликаций, приведших к конфликту, была развита в сторону применения UIP (англ. Unit Implication Points — «точки единичной импликации»). UIP — это доминатор импликационного графа, который у этого вида графа можно вычислить за линейное время. UIP представляет собой альтернативный вариант назначения переменных и дизъюнкт, запомненный в первой такой точке, гарантированно имеет наименьший размер и обеспечивает наибольшее уменьшение уровня решения. В связи с применением эффективных ленивых структур данных, авторы многих SAT-решателей, например, Chaff, применяют метод первого UIP для запоминания дизъюнктов (англ. first UIP clause learning)[3].
Как и DPLL, алгоритм CDCL является корректным и полным SAT-решателем. Так, запоминание дизъюнктов не влияет на полноту и корректность, так как каждый запомненный дизъюнкт может быть выведен из начальных дизъюнктов и других запомненных дизъюнктов методом резолюции. Изменённый механизм возврата также не влияет на полноту и корректность, так как информация о возврате сохраняется в запомненном дизъюнкте[3].
Иллюстрация работы алгоритма:
SAT-решатели на основе CDCL-алгоритма находят применение в автоматическом доказательстве теорем, криптографии, проверке моделей и тестировании аппаратного и программного обеспечения, биоинформатике, определении зависимостей в системах управления пакетами и т. п.[3]
Эта статья входит в число добротных статей русскоязычного раздела Википедии. |
Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".
Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.
Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .