Как решатель SAT создает модель (назначение [я])?

Вот очень простой экземпляр cnf в виде (x1 или x2 или x3)&(x1 или x2)&(x2 или x3), и формула определенно выполнима, решение x1 = x2 = x3 = 1, этого достаточно. Итак, мой вопрос заключается в том, как решатель создает задание с использованием DPLL или другой процедуры? Спасибо.

solver sat dpll

Million 14.04.2015 источник

Ответы (1)

arrow_upward
1
arrow_downward

Ну, в принципе, для случая CDCL

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

это работает следующим образом:

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

введите здесь описание изображения

Теперь примените единичное распространение, в результате чего x4 должно быть равно 1 (т. е. True). Серый кружок означает принудительное присвоение переменной во время распространения модуля. Полученный граф называется графом импликации.

введите здесь описание изображения