Изучение положений, основанных на конфликте

В информатике ( конфликтно-ориентированное обучение предложений CDCL ) — это алгоритм решения булевой проблемы выполнимости (SAT). Учитывая булевую формулу, задача SAT требует присвоения переменных так, чтобы вся формула имела значение true. Внутренняя работа решателей CDCL SAT была вдохновлена решателями DPLL . Основное различие между CDCL и DPLL заключается в том, что прыжки назад в CDCL не хронологичны.

Изучение предложений, основанное на конфликте, было предложено Маркесом-Сильвой и Каремом А. Сакаллой (1996, 1999). ^{[ 1 ]}^{[ 2 ]} и Баярдо и Шраг (1997). ^{[ 3 ]}

Фон

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

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

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

( ( не A ) или ( не C )) и ( B или C ),

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

(\lnot A\lor \lnot C)\land (B\lor C)

где A , B , C — логические переменные, $\lnot A$ , $\lnot C$ , $B$ , и $C$ являются литералами, и $\lnot A\lor \lnot C$ и $B\lor C$ являются оговорками.

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

A=\mathrm {False} ,B=\mathrm {False} ,C=\mathrm {True}

поскольку это делает первое предложение истинным (поскольку $\lnot A$ верно), а также второй (поскольку $C$ это правда).

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

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

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

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

Разрешение

Рассмотрим два пункта $(A\lor B\lor C)$ и $(\neg C\lor D\lor \neg E)$ . Пункт $(A\lor B\lor D\lor \neg E)$ , полученный путем слияния двух предложений и удаления обоих $\neg C$ и $C$ , называется резольвентой двух предложений.

Алгоритм

Обучение предложению, основанное на конфликте, работает следующим образом.

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

Пример

Наглядный пример алгоритма CDCL: ^{[ 4 ]}

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

Полнота

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

Приложения

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

МиниСАТ
Зчафф САТ
Z3
Глюкоза ^{[ 6 ]}
МногиеSAT и т. д.

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

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

Связанными с CDCL алгоритмами являются алгоритм Дэвиса-Патнэма и алгоритм DPLL . Алгоритм DP использует опровержение резолюции и имеет потенциальную проблему доступа к памяти. ^{[ нужна ссылка ]} Хотя алгоритм DPLL подходит для случайно сгенерированных экземпляров, он плох для экземпляров, сгенерированных в практических приложениях. CDCL — более мощный подход к решению таких проблем, поскольку применение CDCL обеспечивает меньший поиск в пространстве состояний по сравнению с DPLL.

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

Цитируемые работы

^ Ж. П. Маркес-Сильва; Карем А. Сакалла (ноябрь 1996 г.). «GRASP-новый алгоритм поиска выполнимости». Дайджест Международной конференции IEEE по компьютерному проектированию (ICCAD) . стр. 220–227. CiteSeerX 10.1.1.49.2075 . дои : 10.1109/ICCAD.1996.569607 . ISBN 978-0-8186-7597-3 .
^ Ж. П. Маркес-Сильва; Карем А. Сакалла (май 1999 г.). «GRASP: алгоритм поиска выполнимости предложений» (PDF) . Транзакции IEEE на компьютерах . 48 (5): 506–521. дои : 10.1109/12.769433 . Архивировано из оригинала (PDF) 4 марта 2016 г. Проверено 29 ноября 2014 г.
^ Роберто Дж. Баярдо младший; Роберт К. Шраг (1997). «Использование методов обратного анализа CSP для решения реальных экземпляров SAT» (PDF) . Учеб. 14-й Нац. Конф. об искусственном интеллекте (AAAI) . стр. 203–208.
^ Перейти обратно: ^а ^б На фотографиях ниже» $+$ " используется для обозначения "или", умножение для обозначения "и" и постфикс " $'$ «чтобы обозначить «нет».
^ Маркес-Сильва, Жуан; Линс, Инес; Малик, Шарад (февраль 2009 г.). Справочник по выполнимости (PDF) . ИОС Пресс. п. 138. ИСБН 978-1-60750-376-7 .
^ «Домашняя страница Глюкозы» .

Ссылки

Мартин Дэвис; Хилари Патнэм (1960). «Вычислительная процедура для количественной теории» . Дж. АКМ . 7 (3): 201–215. дои : 10.1145/321033.321034 . S2CID 31888376 .
Мартин Дэвис; Джордж Логеманн; Дональд Лавленд (июль 1962 г.). «Машинная программа для доказательства теорем». Коммуникации АКМ . 5 (7): 394–397. дои : 10.1145/368273.368557 . hdl : 2027/mdp.39015095248095 . S2CID 15866917 .
Мэтью В. Москевич; Конор Ф. Мэдиган; Ин Чжао; Линтао Чжан; Шарад Малик (2001). «Chaff: разработка эффективного решателя SAT» (PDF) . Учеб. 38-я Анна. Конференция по автоматизации проектирования (DAC) . стр. 530–535.
Линтао Чжан; Конор Ф. Мэдиган; Мэтью Х. Москевич; Шарад Малик (2001). «Эффективное обучение, основанное на конфликтах, с помощью решателя логической выполнимости» (PDF) . Учеб. IEEE/ACM Международный. Конф. по системе автоматизированного проектирования (ICCAD) . стр. 279–285.
Презентация - «Решение SAT: от Дэвиса-Патнэма до Цчаффа и далее», Линтао Чжан. (Несколько фотографий взяты из его презентации)

[1] Ж. П. Маркес-Сильва; Карем А. Сакалла (ноябрь 1996 г.). «GRASP-новый алгоритм поиска выполнимости». Дайджест Международной конференции IEEE по компьютерному проектированию (ICCAD) . стр. 220–227. CiteSeerX 10.1.1.49.2075 . дои : 10.1109/ICCAD.1996.569607 . ISBN 978-0-8186-7597-3 .

[2] Ж. П. Маркес-Сильва; Карем А. Сакалла (май 1999 г.). «GRASP: алгоритм поиска выполнимости предложений» (PDF) . Транзакции IEEE на компьютерах . 48 (5): 506–521. дои : 10.1109/12.769433 . Архивировано из оригинала (PDF) 4 марта 2016 г. Проверено 29 ноября 2014 г.

[3] Роберто Дж. Баярдо младший; Роберт К. Шраг (1997). «Использование методов обратного анализа CSP для решения реальных экземпляров SAT» (PDF) . Учеб. 14-й Нац. Конф. об искусственном интеллекте (AAAI) . стр. 203–208.

[notation-4] Перейти обратно: ^а ^б На фотографиях ниже» $+$ " используется для обозначения "или", умножение для обозначения "и" и постфикс " $'$ «чтобы обозначить «нет».

[5] Маркес-Сильва, Жуан; Линс, Инес; Малик, Шарад (февраль 2009 г.). Справочник по выполнимости (PDF) . ИОС Пресс. п. 138. ИСБН 978-1-60750-376-7 .

[6] «Домашняя страница Глюкозы» .

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]