Русская Википедия:Алгоритм CDCL

Материал из Онлайн справочника
Перейти к навигацииПерейти к поиску

Алгоритм CDCL (Шаблон:Lang-en — «управляемое конфликтами обучение дизъюнктам») — основанный на алгоритме DPLL эффективный решатель (NP-полных) задач выполнимости булевых формул (SAT-решатель). Основная структура данных в CDCL-решателях — импликационный граф, фиксирующий назначения переменным, а другой особенностью является использование нехронологического возврата и запоминание дизъюнктов в ходе анализа конфликта.

Алгоритм был предложен Шаблон:Нп2 и Каремом Сакаллой (Шаблон:Lang-en) в 1996 году[1] и независимо Роберто Байярдо (Шаблон:Lang-en) и Робертом Шрагом (Шаблон:Lang-en) в 1997 году[2]Шаблон:Sfn.

Описание

DPLL-алгоритм, лежащий в основе CDCL-алгоритма, использует поиск с возвратом на конъюнктивных нормальных формах, на каждом шаге которого происходит выбор переменной и присвоения ей значения (0 или 1) для последующего ветвления, заключающегося в присваивании значения переменной, после чего упрощённая формула проходит рекурсивную проверку на выполнимость. В случае, когда встречается конфликт, то есть, полученная формула является невыполнимой, включается механизм возврата (бэктрекинга), при котором отменяются ветвления, в которых для переменной были опробованы оба значения. Если поиск возвращается к ветвлению первого уровня, вся формула объявляется невыполнимой. Такой возврат, свойственный алгоритму DPLL, называется хронологическимШаблон:Sfn.

Дизъюнкты, используемые в алгоритме, делятся на выполнимые (satisfied), когда среди входящих в дизъюнкт значений есть 1, невыполнимые (unsatisfied) — все значения нулевые, единичные (unit) — все нули, кроме одной переменной, которой значение ещё не присвоено, и неразрешённые (unresolved) — все остальные. Одной из важнейших составляющих SAT-решателей является правило единичного дизъюнкта, при котором выбор переменной и её значения однозначен. (Следует напомнить, что в дизъюнкт входят как переменные, так и их отрицания.) Шаблон:Нп2 (в современных CDCL-решателях она почти всегда основывается на правиле единичного дизъюнкта) производится после ветвления для вычисления логических следствий сделанного выбораШаблон:Sfn.

В дополнение к DPLL и его механизму поиска с возвратом, CDCL использует некоторые другие приёмыШаблон:Sfn:

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

Схема алгоритма

С каждой переменной проверяемой на выполнимость формулы в CDCL-алгоритме связаны несколько вспомогательных значенийШаблон:Sfn:

  • значение переменных ν(vi)∈{0,u,1} для всех переменных vi, где u служит для обозначения ещё не назначенной переменной
  • уровень решения, на котором переменной было присвоено значение от −1 (не присвоено) до количества переменных.
  • предпосылка (antecendent) — единичный дизъюнкт формулы, на основе которого последовало значение переменной по правилу единичного дизъюнкта. Для ещё неназначенных переменных и переменных, по которым было принято решение, имеет значение None.

Схематично типичный CDCL-алгоритм можно представить следующим образомШаблон:Sfn: 

   Алгоритм CDCL(φ, ν)
   вход: 
     φ - формула (КНФ)
     ν - отображение значений переменных в виде множества пар
   выход:
     SAT (формула выполнима) или UNSAT (невыполнима)
   если UnitPropagationConflict(φ, ν)
   то 
     возврат UNSAT
   L := 0                                    -- уровень решения
   пока NotAllVariablesAssigned(φ, ν)
     (x, v) := PickBranchingVariable(φ, ν)   -- принятие решения
     L := L + 1
     ν := ν ∪ {(x, v)}
     если UnitPropagationConflict(φ, ν)      -- вывод последствий
     то
       β := ConflictAnalysis(φ, ν)           -- диагностика конфликта
       если β < 0
       то
         возврат UNSAT
       иначе
         Backtrack(φ, ν, β)                  -- возврат (бэктрекинг)
         L := β
   возврат SAT

В этом алгоритме использовано несколько подпрограмм, которые помимо возврата значений могут изменять и переданные им по ссылке переменные φ, νШаблон:Sfn:

  • UnitPropagationConflict итеративно применяет правило единичного дизъюнкта, возвращая значение Истина в случае нахождения невыполнимого дизъюнкта.
  • NotAllVariablesAssigned проверяет, есть ли ещё неназначенные переменные.
  • PickBranchingVariable выбирает переменную и назначаемое значение (1 или 0).
  • ConflictAnalysis анализирует возникший конфликт, запоминает новый дизъюнкт и даёт уровень решения, к которому необходимо вернуться.
  • Backtrack производит возврат к уровню, вычисленному в ходе анализа конфликта.

Процедура анализа конфликта является центральной для CDCL алгоритма.

Основной структурой данных, используемой в CDCL-решателях, является импликационный граф (Шаблон:Lang-en), фиксирующий назначения переменным (как в результате решений, так и применением правила единичного дизъюнкта), в котором вершины соответствуют литералам формулы, а дуги фиксируют структуру импликацийШаблон:SfnШаблон:Sfn.

Анализ конфликта

Процедура анализа конфликта (см. схему алгоритма) вызывается при обнаружении конфликта по правилу единичного дизъюнкта, и на её основе пополняется множество запомненных дизъюнктов. Процедура начинает с узла импликационного графа, в котором обнаружен конфликт, и охватывает уровни решения с меньшими номерами, переходя назад по импликациям пока не встречает самую свежую назначенную (в результате решения) переменнуюШаблон:Sfn. Запомненные дизъюнкты применяются в нехронологическом возврате (Шаблон:Lang-en) — ещё одном характерном для CDCL-решателей приёмеШаблон:Sfn.

Для сравнения:

Идея использования структуры импликаций, приведших к конфликту, была развита в сторону применения UIP (Шаблон:Lang-en — «точки единичной импликации»). UIP — это доминатор импликационного графа, который у этого вида графа можно вычислить за линейное время. UIP представляет собой альтернативный вариант назначения переменных и дизъюнкт, запомненный в первой такой точке, гарантированно имеет наименьший размер и обеспечивает наибольшее уменьшение уровня решения. В связи с применением эффективных ленивых структур данных, авторы многих SAT-решателей, например, Chaff, применяют метод первого UIP для запоминания дизъюнктов (Шаблон:Lang-en)Шаблон:Sfn.

Корректность и полнота

Как и DPLL, алгоритм CDCL является корректным и полным SAT-решателем. Так, запоминание дизъюнктов не влияет на полноту и корректность, так как каждый запомненный дизъюнкт может быть выведен из начальных дизъюнктов и других запомненных дизъюнктов методом резолюции. Изменённый механизм возврата также не влияет на полноту и корректность, так как информация о возврате сохраняется в запомненном дизъюнктеШаблон:Sfn.

Пример

Иллюстрация работы алгоритма:

Применения

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

Примечания

Шаблон:Примечания

Литература

Ссылки

Шаблон:Добротная статья

Партнерские ресурсы
Криптовалюты
Магазины
Хостинг
Разное

  1. ↑ J. P. Marques-Silva and K. A. Sakallah. GRASP: A new search algorithm for satisfiability. In International Conference on Computer-Aided Design, pages 220—227, November 1996.
  2. ↑ R. Bayardo Jr. and R. Schrag. Using CSP look-back techniques to solve real-world SAT instances. In National Conference on Artificial Intelligence, pages 203—208, July 1997
Источник — http://wikihandbk.com/ruwiki/index.php?title=Русская_Википедия:Алгоритм_CDCL&oldid=8939930