Алгоритм CDCL: различия между версиями
[отпатрулированная версия] | [отпатрулированная версия] |
РоманСузи (обсуждение | вклад) дополнение |
РоманСузи (обсуждение | вклад) дополнение |
||
Строка 59: | Строка 59: | ||
Процедура анализа конфликта является центральной для CDCL алгоритма.<!-- и требует отдельного описания --> |
Процедура анализа конфликта является центральной для CDCL алгоритма.<!-- и требует отдельного описания --> |
||
Основной структурой данных, используемой в CDCL-решателях, является '''''импликационный граф''''' (implication graph), фиксирующий назначения переменным (как в результате решений, так и применением правила единичного дизъюнкта), в котором вершины соответствуют литералам формулы, а дуги фиксируют структуру импликаций{{sfn|A Generalized Framework for Conflict Analysis|2008}}{{sfn|Hamadi|2013}}. |
Основной структурой данных, используемой в CDCL-решателях, является '''''импликационный граф''''' (implication graph), фиксирующий назначения переменным (как в результате решений, так и применением правила единичного дизъюнкта), в котором вершины соответствуют литералам формулы, а дуги фиксируют структуру импликаций{{sfn|A Generalized Framework for Conflict Analysis|2008}}{{sfn|Hamadi|2013}}. |
||
== Анализ конфликта == |
|||
Процедура анализа конфликта (см. схему алгоритма) вызывается при обнаружении конфликта по правилу единичного дизъюнкта и на её основе пополняется множество «выученных» дизъюнктов. Процедура начинает с узла импликационного графа, в котором обнаружен конфликт, и охватывает уровни решения с меньшими номерами, переходя назад по импликациям пока не встречает самую свежую назначенную (в результате решения) переменную{{sfn|Conflict-Driven Clause Learning SAT Solvers|2008}}. Выученные дизъюнкты применяются в '''''нехронологическом возврате''''' ({{lang-en|non-chronological backtracking}}) — ещё одном характерном для CDCL-решателей приёме{{sfn|Pradhan, Harris|2009}}. |
|||
== Применения == |
== Применения == |
||
Строка 96: | Строка 99: | ||
| ref = A Generalized Framework for Conflict Analysis |
| ref = A Generalized Framework for Conflict Analysis |
||
}} |
}} |
||
* {{книга |
|||
| автор = Pradhan, D.K. and Harris, I.G. |
|||
| заглавие = Practical Design Verification |
|||
| издательство = Cambridge University Press |
|||
| год = 2009 |
|||
| allpages = |
|||
| pages = 252-254 |
|||
| isbn = 9780521859721 |
|||
| ref = Pradhan, Harris |
|||
}} |
|||
* {{книга |
|||
| автор = Järvisalo, M.; Van Gelder, A. |
|||
| заглавие = Theory and Applications of Satisfiability Testing |
|||
| издание = SAT 2013: 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings |
|||
| издательство = Springer Berlin Heidelberg |
|||
| год = 2013 |
|||
| allpages = |
|||
| isbn = 9783642390715 |
|||
| ref = Järvisalo, Van Gelder |
|||
}} |
|||
== Ссылки == |
== Ссылки == |
Версия от 19:21, 2 марта 2015
Алгоритм CDCL (англ. conflict-driven clause learning — «управляемое конфликтами обучение дизъюнктам») — основанный на алгоритме DPLL эффективный решатель (NP-полных) задач выполнимости булевых формул (SAT-решатель).
Алгоритм был предложен Маркесом-Сильвой (Marques-Silva) и Сакаллой (Sakallah) в 1996 году[1] и независимо Байярдо (Roberto J. Bayardo) и Шрагом (Robert C. Schrag) в 1997 году[2][3].
Описание
DPLL-алгоритм, лежащий в основе CDCL-алгоритма, использует поиск с возвратом на конъюнктивных нормальных формах, на каждом шаге которого происходит выбор переменной и присвоения ей значения (0 или 1) для последующего ветвления, заключающегося в присваивании значения переменной, после чего упрощённая формула проходит рекурсивную проверку на выполнимость. В случае, когда встречается конфликт, то есть, полученная формула является невыполнимой, включается механизм возврата (бэктрекинга), при котором отменяются ветвления, в которых для переменной были опробованы оба значения. Если поиск возвращается к ветвлению первого уровня, вся формула объявляется невыполнимой. Такой возврат, свойственный алгоритму DPLL, называется хронологическим[3].
Дизъюнкты, используемые в алгоритмы, делятся на выполнимые (satisfied), когда среди входящих в дизъюнкт значений есть 1, невыполнимые (unsatisfied) — все значения нулевые, единичные (unit) — все нули, кроме одной переменной, которой значение ещё не присвоено, и неразрешённые (unresolved) — все остальные. Одной из важнейших составляющих SAT-решателей является правило единичного дизъюнкта, при котором выбор переменной и её значения однозначен. (Следует напомнить, что в дизъюнкт входят как переменные, так и их отрицания.) Процедура распространения переменной[англ.] (в современных CDCL-решателях она почти всегда основывается на правиле единичного дизъюнкта) производится после ветвления для вычисления логических следствий сделанного выбора[3].
В дополнение к DPLL и его механизму поиска с возвратом, CDCL использует некоторые другие приёмы[3]:
- обучение новым дизъюнктам в ходе поиска с возвратом.
- использование структуры конфликтов во время обучения дизъюнктам.
- применение ленивых структур данных для представления формул.
- эвристики ветвления имеют низкие затраты вычислительных ресурсов и получают обратную связь от поиска с возвратами.
- периодический перезапуск поиска с возвратами.
- политики удаления для выученных дизъюнктов.
- другие виды оптимизации.
Схема алгоритма
С каждой переменной проверяемой на выполнимость формулы в CDCL-алгоритме связаны несколько вспомогательных значений[3]:
- значение переменных ν(vi)∈{0,u,1} для всех переменных vi, где u служит для обозначения ещё не назначенной переменной
- уровень решения, на котором переменной было присвоено значение от -1 (не присвоено) до количества переменных.
- предпосылка (antecendent) - единичный дизъюнкт формулы, на основе которого последовало значение переменной по правилу единичного дизъюнкта. Для ещё неназначенных переменных и переменных, по которым было принято решение, имеет значение None.
Схематично типичный 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
анализирует возникший конфликт, запоминает (learn - «заучивает») новый дизъюнкт и даёт уровень решения, к которому необходимо вернуться.Backtrack
производит возврат к уровню, вычисленному при анализу конфликта.
Процедура анализа конфликта является центральной для CDCL алгоритма.
Основной структурой данных, используемой в CDCL-решателях, является импликационный граф (implication graph), фиксирующий назначения переменным (как в результате решений, так и применением правила единичного дизъюнкта), в котором вершины соответствуют литералам формулы, а дуги фиксируют структуру импликаций[4][5].
Анализ конфликта
Процедура анализа конфликта (см. схему алгоритма) вызывается при обнаружении конфликта по правилу единичного дизъюнкта и на её основе пополняется множество «выученных» дизъюнктов. Процедура начинает с узла импликационного графа, в котором обнаружен конфликт, и охватывает уровни решения с меньшими номерами, переходя назад по импликациям пока не встречает самую свежую назначенную (в результате решения) переменную[3]. Выученные дизъюнкты применяются в нехронологическом возврате (англ. non-chronological backtracking) — ещё одном характерном для CDCL-решателей приёме[6].
Применения
SAT-решатели на основе CDCL-алгоритма находят применение в автоматическом доказательстве теорем, криптографии, проверке моделей и тестировании аппаратного и программного обеспечения, биоинформатике, определении зависимостей в системах управления пакетами и т. п.[3]
Примечания
- ↑ 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.
- ↑ 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
- ↑ 1 2 3 4 5 6 7 8 9 Conflict-Driven Clause Learning SAT Solvers, 2008.
- ↑ A Generalized Framework for Conflict Analysis, 2008.
- ↑ Hamadi, 2013.
- ↑ Pradhan, Harris, 2009.
Литература
- Armin Biere, Marijn Heule, Hans van Maaren and Toby Walsch. Chapter 4. Conflict-Driven Clause Learning SAT Solvers // Handbook of Satisfiability. — IOS Press, 2008.
- Matthew W. Moskewicz; Conor F. Madigan; Ying Zhao; Lintao Zhang; Sharad Malik (2001). "Chaff: Engineering an Efficient SAT Solver". Annual ACM IEEE Design Automation Conference. pp. 530–535. Chaff.
{{cite conference}}
: Неизвестный параметр|booktitle=
игнорируется (|book-title=
предлагается) (справка)Википедия:Обслуживание CS1 (множественные имена: authors list) (ссылка) - Hamadi, Y. Combinatorial Search: From Algorithms to Systems. — Springer Berlin Heidelberg, 2013. — 152 p. — ISBN 9783642414824.
- Audemard, Gilles; Bordeaux, Lucas; Hamadi, Youssef; Jabbour, Saïd; Sais, Lakhdar (2008). "A Generalized Framework for Conflict Analysis". SAT. Lecture Notes in Computer Science. Springer. pp. 21–27.
{{cite conference}}
: Неизвестный параметр|booktitle=
игнорируется (|book-title=
предлагается) (справка)Википедия:Обслуживание CS1 (множественные имена: authors list) (ссылка) - Pradhan, D.K. and Harris, I.G. Practical Design Verification. — Cambridge University Press, 2009. — P. 252-254. — ISBN 9780521859721.
- Järvisalo, M.; Van Gelder, A. Theory and Applications of Satisfiability Testing. — SAT 2013: 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings. — Springer Berlin Heidelberg, 2013. — ISBN 9783642390715.
Ссылки
- Marques-Silva & Mikolas Janota. CDCL SAT Solvers & SAT-Based Problem Solving. SAT/SMT Summer School 2013, Aalto University, Espoo, Finland.