SAT-решение: DPLL против?

Question

прямо сейчас я пишу о SAT-решении, и я застрял в точке. Я надеюсь, что вы можете мне помочь.

Я хочу описать некоторые методы решения SAT-проблем. Сейчас у меня есть три различных способа:

1. BruteForce
2. Random (наивный)
3. DPLL (с ​​различными эвристики)
4. ? отсутствует ?
5. ...

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

Мой вопрос: Было бы здорово, если бы вы могли сказать мне некоторые алгоритмы, которые не основаны на DPLL (DP), с которыми я могу сравнить его.

Вот некоторые, что я нашел, но не может решить, будут ли они быть хорошим выбором, или если есть лучшие из них:

• Monien-Speckenmeyer
• Данцин, Goerdt, Hirsch и Schöning
• Патури-Pudlák-Зейн-Algorithmus
• Гофмейстер, Шёнинг, Шулер и Ватанабе

Спасибо за вашу помощь.

Answer 1

Современный спутниковый решатель в настоящее время использует CDCL (Conflict Drive Clause Learning) на основе DPLL.

Answer 2

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

Если вы хотите обсудить альтернативы, я бы рекомендовал посмотреть на Неполные алгоритмы. Они часто основаны на стохастическом локальном поиске и включают GSAT и WalkSAT. Хотя этим алгоритмам не гарантированно найти ответ, они традиционно очень хорошо разбираются в случайных (как это связано с промышленными) проблемах SAT. Они также использовались для решения больших проблем с SAT, чем мог решить любой решатель, реализующий алгоритмы на основе DPLL.

Для дальнейших исследований я рекомендую замечательную книгу Бире «Руководство по удовлетворенности».