SAT алгоритмы, не основанные на DPLL

Существуют ли алгоритмы решения SAT, не основанные на DPLL? Или все алгоритмы, используемые решателями SAT, основаны на DPLL?

Поиск разрешения (просто применение правила разрешения с некоторой хорошей эвристикой) - еще одна возможная стратегия для решателей SAT. Теоретически он экспоненциально более мощный (т. Е. Существуют проблемы, для которых он имеет экспоненциально более короткие доказательства), чем DPLL (который просто разрешает дерево, хотя вы можете дополнить его хорошим обучением, чтобы увеличить его мощность - независимо от того, делает ли он его таким же мощным, как и общее разрешение - все еще откройте, насколько я знаю), но я не знаю фактической реализации, которая работает лучше.

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

Изменить: Забыл добавить - также можно использовать плоскости резания (сокращая SAT до целочисленной программы). В частности, сокращения Гомори достаточны для оптимального решения любой целочисленной программы. Опять же в худшем случае может понадобиться экспоненциальное число. Я думаю, что в книге «Вычислительная сложность» Ароры и Барака есть еще несколько примеров систем доказательств, которые теоретически можно использовать для чего-то вроде SAT-решения. Опять же, я не видел быстрой реализации чего-либо, кроме методов на основе DPLL или локального поиска.

Распространение опроса - это еще один алгоритм, который с успехом использовался для некоторых видов проблем SAT, особенно случайных экземпляров SAT. Как и WalkSAT, его нельзя использовать для доказательства неудовлетворенности, но он основан на совершенно разных идеях (алгоритмах передачи сообщений) из WalkSAT.

Есть SAT решатели на основе локального поиска. Смотрите, например, эту статью для экспозиции.

Можно также сказать, что все решатели CSP также являются решателями SAT. И, насколько мне известно, в CSP используются два метода:

• Исчерпывающая DFS с сокращением пространства поиска и проверкой согласованности дуг, возможно, с использованием процесса бритья, чтобы обеспечить согласованность как можно скорее.
• Локальные методы (поиск табу, имитация отжига)

Поиск по дереву Монте-Карло (MCTS) недавно достиг некоторых впечатляющих результатов в таких играх, как Go. Грубая основная идея - чередование случайного моделирования с поиском по дереву. Он легок и прост в реализации, на странице исследовательского центра, на которую я ссылаюсь, содержится много примеров, статей и некоторого кода.

Превити и соавт. [1] провели предварительное расследование MCTS, примененной к SAT. Они называют алгоритм поиска на основе MCTS UCTSAT («верхние доверительные границы применяются к деревьям SAT», если хотите). Они сравнили производительность DPLL и UCTSAT на экземплярах из репозитория SATLIB с целью выяснить, будет ли UCTSAT создавать значительно меньшие деревья поиска, чем DPLL.

Для единообразных случайных раскрасок 3-SAT и плоского графа разных размеров существенных различий не было. Тем не менее, UCTSAT работает лучше для реальных случаев. Средние размеры дерева (с точки зрения количества узлов) для четырех разных экземпляров анализа сбоев цепи SSA составляли несколько тысяч для DPLL, но всегда меньше 200 для UCTSAT.

[1] Превити, Алессандро, Рагурам Рамануджан, Марко Шаерф и Барт Сельман. «UCT ищет в стиле Монте-Карло логическую удовлетворенность». В AI * IA 2011: Искусственный интеллект вокруг человека и за его пределами, стр. 177-188. Springer Berlin Heidelberg, 2011.

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

• Руководство по SAT-решению в реальном мире с разложением динамического разделителя гиперграфа Li, van Beek

• Разложение проблем удовлетворительности или использование графиков для лучшего понимания проблем удовлетворительности Хервиг

• Край ножа (1998) Уолша