Немного терминологии.
Любую формулу можно привести к коньюнктивной нормальной форме - конъюнкции дизъюнкций литералов. Конъюнкция - Логическое И. Дизъюнкция - Логическое ИЛИ. Литерал здесь - прямое или обратное значение булевой переменной. x или ~x. Дизъюнкцию ещё можно называть ограничением, именно они ограничивают возможные значения переменных КНФ.
Самый первый алгоритм вычисления выполнимости (Davis-Putnam, DP) делал так называемое разрешение (resolution): если у нас есть в КНФ две дизъюнкции x\/Y и ~x\/Z, то мы можем заменить две эти формулы на формулу y\/z. Здесь x переменная, а Z и Y - дизъюнкции. Алгоритмически это выполняется так: для всех a, содержащих x и всех b, содержащих ~x, выполнить разрешение a и b. Исходные формулы можно убрать. Если разрешение выполнялось для формул вида x\/y\/A и ~x\/~y\/B, то в результате получится тривиальная формула y\/~y\/A\/B - тождественно равная истине.
Если при итеративном применении этого правила мы пришли к пустой дизъюнкции, то формула невыполнима (пример: x/\~x). Если в конце получилась пустая формула (все разрешения завершились тривиально), то формула выполнима. Может также получиться набор независимых формул, в этом случае тоже легко найти решение. Если мы не можем произвести разрешение по какому-то литералу, то по нему нельзя сделать выбор - зафиксируем его переменную в его значении.
Этот вариант требует большого количества пространства.
Второй алгоритм, предложенный Logemann и Loveland (LL в сокращении DPLL), перебирал значения всех переменных КНФ. Зафиксировав значение переменной, он проверял, не выводятся ли значения других переменных из уже зафиксированных и не приводит ли этот вывод к противоречию. Если можно было произвести вывод значений, он производился. Если у нас вывелись два противоположных значения, то это противоречие. При противоречии производился откат, убирались все результаты текущего вывода и фиксированное значение заменялось на противоположное.
Вот простая КНФ: a \/ b \/ c /\ a \/ b \/ c. Если мы зафиксируем значения a=Ложь и b=Ложь, то из первой дизъюнкции выводится c=Истина, а из второй - c=Ложь. Противоречие. Заменив любое из фиксированных значений a и b, мы получим удовлетворяющее присваивание.
Зайдем с другой стороны. Зафиксируем c=False. Вторая дизъюнкция станет тривиально истинной. Останется только первая. Выберем a=Ложь, останется только вывод b=Истина.
Здесь пространство не так важно, зато сложность алгоритма в худшем случае экспоненциальная. Важно, что "в худшем случае". Если мы каким-то образом можем выбирать правильные значения фиксируемых переменных (по структуре задачи, по предыдущему опыту решения похожих задач, наконец, нам подсказали!), то мы можем решить задачу быстрее, чем за полный перебор всех значений.
Это очень важно. Решатель
Minisat показывает отличные результаты в категории "Индустриальные задачи" в соревновании решателей булевой выполнимости в частности потому, что он выбирает для новых переменных значение v=Ложь. Оказывается, большая часть задач этой категории имеет решение с ключевыми переменными, равными Лжи. А вот в категории "Случайные задачи" он отстает - там отлично работают системы, что учитывают структуру задачи (решатель
march_xx из таких, например) или просто стохастические алгоритмы типа WalkSAT.
В середине 90-х решатель GRASP совершил прорыв - он начал запоминать причины, по которым решатель пришёл к конфликту, добавляя дизъюнкции противоречия (conflict clauses) к задаче. Здесь преследуются две цели - избегнуть в будущем похожей ситуации и автоматически перещелкнуть последнее выбранное значение.
Пример приведу все на том же конфликте выше. Мы установили переменные a=Ложь и b=Ложь и получили конфликт c и ~c. Мы говорим, что мы не должны посетить в будущем такой набор переменных, при котором a=Ложь И b=Ложь. Мы добавляем к нашей задаче ещё одно ограничение - ~(~a/\~b)=a\/b. Последней мы выбрали переменную b, отменяем её выбор. Новая задача a\/b\/c /\ a\/b\/~c /\ a\/b с выбором a=Ложь автоматически выберет b=Истина (третье ограничение) и решение будет найдено.
Это риешение важно ещё и потому, что если мы запоминаем все причины конфликтов, то мы (а) экспоненциально быстрее полного перебора (доказано) и (б) можем начинать с чистого листа и не придём к той же ситуации.
Рестарт перебора с чистого листа позволяет избежать перебора в окрестности заведомо плохого решения.
Современные решатели начинают с чистого листа довольно часто - после нескольких сотен конфликтов. Есть тендениця ещё увеличить частоту рестартов.
Надо далее рассказать про способы выбора ограничений противоречий, а также надо рассказать про реальную реализацию перебора в том же MiniSAT.
Последняя ссылка на сегодня -
glueminisat. Это вариант всё того же MiniSAT, только с улучшенным механизмом выбора ограничений противоречий.
