Алгоритм CDCL

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

Алгоритм был предложен Жуаном Маркесом-Сильвой (англ. João Marques-Silva) и Каремом Сакаллой (англ. Karem A. Sakallah) в 1996 году и независимо Роберто Байярдо (англ. Roberto J. Bayardo) и Робертом Шрагом (англ. Robert C. Schrag) в 1997 году.

Описание

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• CompareCdcl dpll1.png

  DPLL: нет запоминания дизъюнктов, хронологический возврат.

• CompareCdcl dpll2.png

  CDCL: запоминание дизъюнктов в результате анализа конфликтов и нехронологический возврат

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

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

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

Пример

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

• Cdcl1.png

  Выбор переменной для ветвления: x1. Жёлтый кружок означает произвольное решение.

• Cdcl2.png

  По правилу единичного дизъюнкта x4 должно быть 1. Серый кружок — принудительное назначение. Получаемый граф и есть импликационный граф.

• Cdcl3.png

  Произвольный выбор другой переменной, x3.

• Cdcl4.png

  Применение правила единичного дизъюнкта и нахождение нового импликационного графа.

• Cdcl5.png

  Переменные x8 и x12 с логической необходимостью принимают значения 0 и 1 соответственно.

• Cdcl6.png

  Снова выбор переменной ветвления: x2.

• Cdcl7.png

  Построение импликационного графа.

• Cdcl8.png

  Ещё одна переменная: x7.

• Cdcl9.png

  Построение импликационного графа.

• Cdcl10.png

  Новый импликационный граф. Получен конфликт.

• Cdcl11.png

  Нахождение разреза графа, приведшего к конфликту, и конфликтного дизъюнкта.

• Cdcl12.png

  Нахождение дизъюнкта по отрицанию: если из a следует b, то из не-b следует не-a

• Cdcl13.png

  Запоминание дизъюнкта.

• Cdcl14.png

  Нехронологический возврат на соответствующий уровень решения.

• Cdcl15.png

  Соответствующие установки значений.

Применения

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

Литература

• 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: 530-535. 
• 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. A Generalized Framework for Conflict Analysis. — В: Lecture Notes in Computer Science // SAT. — Springer, 2008. — 21-27 с.</span>
• 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. [www.csi.ucd.ie/staff/jpms/talks/talksite/msj-satsmt13-lect.pdf CDCL SAT Solvers & SAT-Based Problem Solving]. SAT/SMT Summer School 2013, Aalto University, Espoo, Finland.
• Masahiro Sakai. [www.slideshare.net/sakai/how-a-cdcl-sat-solver-works How a CDCL SAT solver works] (англ.) (2012).

Отрывок, характеризующий Алгоритм CDCL

– Я не говорю, чтоб это был план, который я одобряю, – сказал сын, – я вам только рассказал, что есть. Наполеон уже составил свой план не хуже этого.
– Ну, новенького ты мне ничего не сказал. – И старик задумчиво проговорил про себя скороговоркой: – Dieu sait quand reviendra. – Иди в cтоловую.


В назначенный час, напудренный и выбритый, князь вышел в столовую, где ожидала его невестка, княжна Марья, m lle Бурьен и архитектор князя, по странной прихоти его допускаемый к столу, хотя по своему положению незначительный человек этот никак не мог рассчитывать на такую честь. Князь, твердо державшийся в жизни различия состояний и редко допускавший к столу даже важных губернских чиновников, вдруг на архитекторе Михайле Ивановиче, сморкавшемся в углу в клетчатый платок, доказывал, что все люди равны, и не раз внушал своей дочери, что Михайла Иванович ничем не хуже нас с тобой. За столом князь чаще всего обращался к бессловесному Михайле Ивановичу.
В столовой, громадно высокой, как и все комнаты в доме, ожидали выхода князя домашние и официанты, стоявшие за каждым стулом; дворецкий, с салфеткой на руке, оглядывал сервировку, мигая лакеям и постоянно перебегая беспокойным взглядом от стенных часов к двери, из которой должен был появиться князь. Князь Андрей глядел на огромную, новую для него, золотую раму с изображением генеалогического дерева князей Болконских, висевшую напротив такой же громадной рамы с дурно сделанным (видимо, рукою домашнего живописца) изображением владетельного князя в короне, который должен был происходить от Рюрика и быть родоначальником рода Болконских. Князь Андрей смотрел на это генеалогическое дерево, покачивая головой, и посмеивался с тем видом, с каким смотрят на похожий до смешного портрет.
– Как я узнаю его всего тут! – сказал он княжне Марье, подошедшей к нему.
Княжна Марья с удивлением посмотрела на брата. Она не понимала, чему он улыбался. Всё сделанное ее отцом возбуждало в ней благоговение, которое не подлежало обсуждению.
– У каждого своя Ахиллесова пятка, – продолжал князь Андрей. – С его огромным умом donner dans ce ridicule! [поддаваться этой мелочности!]
Княжна Марья не могла понять смелости суждений своего брата и готовилась возражать ему, как послышались из кабинета ожидаемые шаги: князь входил быстро, весело, как он и всегда ходил, как будто умышленно своими торопливыми манерами представляя противоположность строгому порядку дома.
В то же мгновение большие часы пробили два, и тонким голоском отозвались в гостиной другие. Князь остановился; из под висячих густых бровей оживленные, блестящие, строгие глаза оглядели всех и остановились на молодой княгине. Молодая княгиня испытывала в то время то чувство, какое испытывают придворные на царском выходе, то чувство страха и почтения, которое возбуждал этот старик во всех приближенных. Он погладил княгиню по голове и потом неловким движением потрепал ее по затылку.
– Я рад, я рад, – проговорил он и, пристально еще взглянув ей в глаза, быстро отошел и сел на свое место. – Садитесь, садитесь! Михаил Иванович, садитесь.
Он указал невестке место подле себя. Официант отодвинул для нее стул.
– Го, го! – сказал старик, оглядывая ее округленную талию. – Поторопилась, нехорошо!
Он засмеялся сухо, холодно, неприятно, как он всегда смеялся, одним ртом, а не глазами.
– Ходить надо, ходить, как можно больше, как можно больше, – сказал он.
Маленькая княгиня не слыхала или не хотела слышать его слов. Она молчала и казалась смущенною. Князь спросил ее об отце, и княгиня заговорила и улыбнулась. Он спросил ее об общих знакомых: княгиня еще более оживилась и стала рассказывать, передавая князю поклоны и городские сплетни.
– La comtesse Apraksine, la pauvre, a perdu son Mariei, et elle a pleure les larmes de ses yeux, [Княгиня Апраксина, бедняжка, потеряла своего мужа и выплакала все глаза свои,] – говорила она, всё более и более оживляясь.
По мере того как она оживлялась, князь всё строже и строже смотрел на нее и вдруг, как будто достаточно изучив ее и составив себе ясное о ней понятие, отвернулся от нее и обратился к Михайлу Ивановичу.
– Ну, что, Михайла Иванович, Буонапарте то нашему плохо приходится. Как мне князь Андрей (он всегда так называл сына в третьем лице) порассказал, какие на него силы собираются! А мы с вами всё его пустым человеком считали.
Михаил Иванович, решительно не знавший, когда это мы с вами говорили такие слова о Бонапарте, но понимавший, что он был нужен для вступления в любимый разговор, удивленно взглянул на молодого князя, сам не зная, что из этого выйдет.
– Он у меня тактик великий! – сказал князь сыну, указывая на архитектора.
И разговор зашел опять о войне, о Бонапарте и нынешних генералах и государственных людях. Старый князь, казалось, был убежден не только в том, что все теперешние деятели были мальчишки, не смыслившие и азбуки военного и государственного дела, и что Бонапарте был ничтожный французишка, имевший успех только потому, что уже не было Потемкиных и Суворовых противопоставить ему; но он был убежден даже, что никаких политических затруднений не было в Европе, не было и войны, а была какая то кукольная комедия, в которую играли нынешние люди, притворяясь, что делают дело. Князь Андрей весело выдерживал насмешки отца над новыми людьми и с видимою радостью вызывал отца на разговор и слушал его.
– Всё кажется хорошим, что было прежде, – сказал он, – а разве тот же Суворов не попался в ловушку, которую ему поставил Моро, и не умел из нее выпутаться?
– Это кто тебе сказал? Кто сказал? – крикнул князь. – Суворов! – И он отбросил тарелку, которую живо подхватил Тихон. – Суворов!… Подумавши, князь Андрей. Два: Фридрих и Суворов… Моро! Моро был бы в плену, коли бы у Суворова руки свободны были; а у него на руках сидели хофс кригс вурст шнапс рат. Ему чорт не рад. Вот пойдете, эти хофс кригс вурст раты узнаете! Суворов с ними не сладил, так уж где ж Михайле Кутузову сладить? Нет, дружок, – продолжал он, – вам с своими генералами против Бонапарте не обойтись; надо французов взять, чтобы своя своих не познаша и своя своих побиваша. Немца Палена в Новый Йорк, в Америку, за французом Моро послали, – сказал он, намекая на приглашение, которое в этом году было сделано Моро вступить в русскую службу. – Чудеса!… Что Потемкины, Суворовы, Орловы разве немцы были? Нет, брат, либо там вы все с ума сошли, либо я из ума выжил. Дай вам Бог, а мы посмотрим. Бонапарте у них стал полководец великий! Гм!…
– Я ничего не говорю, чтобы все распоряжения были хороши, – сказал князь Андрей, – только я не могу понять, как вы можете так судить о Бонапарте. Смейтесь, как хотите, а Бонапарте всё таки великий полководец!
– Михайла Иванович! – закричал старый князь архитектору, который, занявшись жарким, надеялся, что про него забыли. – Я вам говорил, что Бонапарте великий тактик? Вон и он говорит.
– Как же, ваше сиятельство, – отвечал архитектор.
Князь опять засмеялся своим холодным смехом.
– Бонапарте в рубашке родился. Солдаты у него прекрасные. Да и на первых он на немцев напал. А немцев только ленивый не бил. С тех пор как мир стоит, немцев все били. А они никого. Только друг друга. Он на них свою славу сделал.
И князь начал разбирать все ошибки, которые, по его понятиям, делал Бонапарте во всех своих войнах и даже в государственных делах. Сын не возражал, но видно было, что какие бы доводы ему ни представляли, он так же мало способен был изменить свое мнение, как и старый князь. Князь Андрей слушал, удерживаясь от возражений и невольно удивляясь, как мог этот старый человек, сидя столько лет один безвыездно в деревне, в таких подробностях и с такою тонкостью знать и обсуживать все военные и политические обстоятельства Европы последних годов.
– Ты думаешь, я, старик, не понимаю настоящего положения дел? – заключил он. – А мне оно вот где! Я ночи не сплю. Ну, где же этот великий полководец твой то, где он показал себя?
– Это длинно было бы, – отвечал сын.
– Ступай же ты к Буонапарте своему. M lle Bourienne, voila encore un admirateur de votre goujat d'empereur! [вот еще поклонник вашего холопского императора…] – закричал он отличным французским языком.
– Vous savez, que je ne suis pas bonapartiste, mon prince. [Вы знаете, князь, что я не бонапартистка.]
– «Dieu sait quand reviendra»… [Бог знает, вернется когда!] – пропел князь фальшиво, еще фальшивее засмеялся и вышел из за стола.
Маленькая княгиня во всё время спора и остального обеда молчала и испуганно поглядывала то на княжну Марью, то на свекра. Когда они вышли из за стола, она взяла за руку золовку и отозвала ее в другую комнату.
– Сomme c'est un homme d'esprit votre pere, – сказала она, – c'est a cause de cela peut etre qu'il me fait peur. [Какой умный человек ваш батюшка. Может быть, от этого то я и боюсь его.]
– Ax, он так добр! – сказала княжна.


Князь Андрей уезжал на другой день вечером. Старый князь, не отступая от своего порядка, после обеда ушел к себе. Маленькая княгиня была у золовки. Князь Андрей, одевшись в дорожный сюртук без эполет, в отведенных ему покоях укладывался с своим камердинером. Сам осмотрев коляску и укладку чемоданов, он велел закладывать. В комнате оставались только те вещи, которые князь Андрей всегда брал с собой: шкатулка, большой серебряный погребец, два турецких пистолета и шашка, подарок отца, привезенный из под Очакова. Все эти дорожные принадлежности были в большом порядке у князя Андрея: всё было ново, чисто, в суконных чехлах, старательно завязано тесемочками.
В минуты отъезда и перемены жизни на людей, способных обдумывать свои поступки, обыкновенно находит серьезное настроение мыслей. В эти минуты обыкновенно поверяется прошедшее и делаются планы будущего. Лицо князя Андрея было очень задумчиво и нежно. Он, заложив руки назад, быстро ходил по комнате из угла в угол, глядя вперед себя, и задумчиво покачивал головой. Страшно ли ему было итти на войну, грустно ли бросить жену, – может быть, и то и другое, только, видимо, не желая, чтоб его видели в таком положении, услыхав шаги в сенях, он торопливо высвободил руки, остановился у стола, как будто увязывал чехол шкатулки, и принял свое всегдашнее, спокойное и непроницаемое выражение. Это были тяжелые шаги княжны Марьи.