Изучение оговорок, обусловленных конфликтами - Conflict-driven clause learning

В Информатика, изучение оговорок, обусловленных конфликтами (CDCL) - алгоритм решения Проблема логической выполнимости (СИДЕЛ). Для булевой формулы задача SAT требует присвоения переменных, чтобы вся формула была истинной. Внутренняя работа решателей CDCL SAT была вдохновлена Решатели DPLL.

Изучение клаузулы, основанное на конфликте, было предложено Marques-Silva и Sakallah (1996, 1999).^[1]^[2] и Баярдо и Шраг (1997).^[3]

Фон

Чтобы иметь четкое представление об алгоритме CDCL, необходимы базовые знания по следующим вопросам.

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

Проблема выполнимости состоит в нахождении удовлетворительного задания для данной формулы в конъюнктивная нормальная форма (CNF).

Пример такой формулы:

( (не А) или (нет C) ) и (B или C),

или, используя общепринятые обозначения:^[4]

{ Displaystyle (А ' лор С') земля (В лор С)}

куда А,B,C являются логическими переменными, ${ displaystyle A '}$ , ${ displaystyle C '}$ , ${ displaystyle B}$ , и ${ displaystyle C}$ буквальные, и ${ Displaystyle A ' lor C'}$ и ${ Displaystyle B lor C}$ статьи.

Удовлетворительное назначение для этой формулы, например:

{ displaystyle A = False, B = False, C = True}

так как он делает первое предложение истинным (поскольку ${ displaystyle A '}$ верно), а также второй (поскольку ${ displaystyle C}$ правда).

В этом примере используются три переменные (А, B, C), и для каждого из них есть два возможных назначения (Истина и Ложь). Итак, есть ${ displaystyle 2 ^ {3} = 8}$ возможности. В этом небольшом примере можно использовать перебор чтобы попробовать все возможные назначения и проверить, удовлетворяют ли они формуле. Но в реалистичных приложениях с миллионами переменных и предложений перебор непрактичен. Задача решателя SAT - эффективно и быстро находить удовлетворительное назначение, применяя различные эвристики для сложных формул CNF.

Правило предложения единицы (распространение единицы)

Если в невыполненном предложении все литералы или переменные, кроме одного, имеют значение False, то свободный литерал должен быть True, чтобы предложение было True. Например, если нижеследующее неудовлетворенное предложение оценивается с помощью ${ displaystyle A = False}$ и ${ displaystyle B = False}$ мы должны иметь ${ displaystyle C = True}$ для того, чтобы пункт ${ Displaystyle (А лор В лор С)}$ быть правдой.

Распространение логических ограничений (BCP)

Итеративное применение правила предложения единицы называется распространением единицы или распространением логических ограничений (BCP).

Разрешение

Рассмотрим два пункта ${ Displaystyle (А лор В лор С)}$ и ${ displaystyle ( neg C lor D lor neg E)}$ .Положение ${ Displaystyle (А лор В лор D лор нег Е)}$ , полученный путем слияния двух предложений и удаления обоих ${ displaystyle neg C}$ и ${ displaystyle C}$ , называется резольвентой двух клозов.

Алгоритм DP

Алгоритм DP был представлен Дэвисом и Патнэмом в 1960 году. Неформально алгоритм итеративно выполняет следующие шаги до тех пор, пока в формуле не останутся переменные:

Выберите переменную ${ displaystyle A}$ и добавить все нетавтологические противовоспалительные ${ displaystyle A}$ (резольвента нетавтологична, если она не содержит ${ displaystyle V}$ и ${ displaystyle neg V}$ для какой-то переменной ${ displaystyle V}$ ).
Удалите все исходные предложения, содержащие ${ displaystyle A}$ .

Алгоритм DPLL

Дэвис, Патнэм, Логеманн, Лавленд (1962) разработали этот алгоритм. Некоторые свойства этого алгоритма:

Он основан на поиске.
Это основа почти всех современных решателей SAT.
Он использует хронологический возврат без обучения.

Пример с визуализацией алгоритма DPLL с хронологическим возвратом:

Все статьи, составляющие формулу CNF
Выберите переменную
Примите решение, переменная a = False (0), при этом зеленые предложения станут True
После принятия нескольких решений мы находим граф импликации что приводит к конфликту.
Теперь вернитесь на немедленный уровень и принудительно назначьте противоположное значение этой переменной.
Но вынужденное решение все равно приводит к новому конфликту
Вернитесь на предыдущий уровень и примите вынужденное решение
Примите новое решение, но оно приводит к конфликту
Принять вынужденное решение, но оно снова приводит к конфликту
Вернуться на предыдущий уровень
Продолжайте таким же образом, и окончательный граф импликации

CDCL (изучение положений, обусловленных конфликтами)

Основное различие между CDCL и DPLL заключается в том, что прыжки назад CDCL не хронологические.

Изучение оговорок, обусловленных конфликтами, работает следующим образом.

Выберите переменную и присвойте ей значение True или False. Это называется состоянием принятия решения. Запомните задание.
Примените логическое распространение ограничения (единичное распространение).
Постройте граф импликации.
Если есть конфликт
1. Найдите разрез в графе импликации, который привел к конфликту
2. Вывести новый пункт, который отрицает задания, которые привели к конфликту.
3. Не хронологически возврат ("прыжок назад") к соответствующему уровню принятия решения, где была назначена первая назначенная переменная, участвующая в конфликте.
В противном случае продолжайте с шага 1, пока не будут присвоены все значения переменных.

Пример

Наглядный пример алгоритма CDCL:

Сначала выберите переменную ветвления, а именно x1. Желтый кружок означает произвольное решение.
Теперь примените единичное распространение, которое дает x4 должно быть 1 (т.е. истина). Серый кружок означает принудительное присвоение переменной во время распространения объекта. Полученный граф называется граф импликации.
Произвольно выберите другую переменную ветвления, x3.
Примените единичное распространение и найдите новый граф импликации.
Здесь переменная x8 и x12 принудительно равны 0 и 1 соответственно.
Выберите другую переменную ветвления, x2.
Найдите граф импликации.
Выберите другую переменную ветвления, x7.
Найдите граф импликации.
Обнаружен конфликт!
Найдите порез, который привел к этому конфликту. Найдите в разрезе противоречивое состояние.
Возьмите отрицание этого условия и сделайте его предложением.
Добавьте к проблеме пункт о конфликте.
Нехронологический обратный переход к соответствующему уровню принятия решения, который в данном случае является вторым по величине уровнем решения литералов в изученном предложении.
Вернитесь назад и установите соответствующие значения переменных.

Полнота

DPLL - это надежный и полный алгоритм для SAT. Решатели CDCL SAT реализуют DPLL, но могут изучать новые предложения и возвращаться не в хронологическом порядке. Изучение статей с анализом конфликтов не влияет на надежность или полноту. Анализ конфликтов определяет новые пункты с помощью операции разрешения. Следовательно, каждое заученное предложение может быть выведено из исходных предложений и других изученных предложений с помощью последовательности шагов разрешения. Если cN - это новое заученное предложение, то ϕ выполнимо тогда и только тогда, когда ϕ ∪ {cN} также выполнимо. Более того, измененный шаг обратного отслеживания также не влияет на правильность или полноту, поскольку информация об обратном отслеживании получается из каждого нового изученного предложения.^[5]

Приложения

Основное применение алгоритма CDCL находится в различных решателях SAT, включая:

MiniSAT
Zchaff SAT
Z3
Глюкоза^[6]
ManySAT и др.

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

Связанные алгоритмы

Алгоритмы, связанные с CDCL, - это алгоритмы DP и DPLL, описанные ранее. Алгоритм DP использует опровержение разрешения и имеет потенциальную проблему доступа к памяти. В то время как алгоритм DPLL подходит для случайно сгенерированных экземпляров, он плох для экземпляров, сгенерированных в практических приложениях. CDCL - более эффективный подход для решения таких проблем, поскольку применение CDCL обеспечивает меньше поиск в пространстве состояний по сравнению с DPLL.

DPLL: без обучения и хронологического возврата.
CDCL: изучение оговорок, обусловленное конфликтом, и не хронологический возврат.

Процитированные работы

^ J.P. Marques-Silva; Карем А. Сакаллах (ноябрь 1996 г.). "GRASP-Новый алгоритм поиска выполнимости". Дайджест Международной конференции IEEE по автоматизированному проектированию (ICCAD). С. 220–227. CiteSeerX 10.1.1.49.2075. Дои:10.1109 / ICCAD.1996.569607. ISBN 978-0-8186-7597-3.
^ J.P. Marques-Silva; Карем А. Сакаллах (май 1999 г.). "GRASP: алгоритм поиска пропозициональной выполнимости" (PDF). Транзакции IEEE на компьютерах. 48 (5): 506–521. Дои:10.1109/12.769433.
^ Роберто Х. Баярдо-младший; Роберт С. Шраг (1997). «Использование методов ретроспективного анализа CSP для решения реальных экземпляров SAT» (PDF). Proc. 14-й Нац. Конф. по искусственному интеллекту (AAAI). С. 203–208.
^ На картинках ниже " ${ displaystyle +}$ «используется для обозначения« или », а умножение - для обозначения« и ».
^ Биэр, Хеул, Ван Маарен, Уолш (февраль 2009 г.). Справочник по выполнимости (PDF). IOS Press. п. 138. ISBN 978-1-60750-376-7.CS1 maint: несколько имен: список авторов (связь)
^ https://www.labri.fr/perso/lsimon/gluosis/