Обеспечение конкурентоспособности SAT решателей с помощью специализированных алгоритмов

11

Что мешает сделать решатели SAT конкурентоспособными с помощью специализированных графовых алгоритмов? Другими словами, возможно ли ожидать SAT-решателей, которые могут заменить роль разработчика алгоритма, т. Е. Иметь возможность автоматически распознавать структуру проблемы и затем решать ее так же быстро, как специализированный алгоритм?

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

  • Подсчет независимых наборов размера . Кодирование «x - это независимый набор размера k» ​​дает большую формулу, которую трудно решить. Идеальный SAT решатель признал бы, что эта проблема проста на ограниченном графике ширины дерева с добавлением дополнительной переменной "count" для сумок.К

  • Нахождение минимального дерева Штейнера. Опять же, «дерево Штейнера» имеет глобальное ограничение, однако специальный алгоритм (как здесь ) облегчает задачу, добавляя дополнительную переменную

  • Любая проблема, которая сводится к плоским идеальным соответствиям.

Ярослав Булатов
источник
разве это уже не происходит? Это популярная уловка, чтобы свести проблему к SAT, а затем запустить решатель.
Суреш Венкат
Да, но они конкурентоспособны? Мне интересно, есть ли какой-нибудь SAT-решатель, который мог бы взять простой набор ограничений, описывающих эйлеровый подграф плоского графа, и выполнить #SAT за полиномиальное время
Ярослав Булатов

Ответы:

7

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

Основное утверждение заключается в том, что эти методы визуализации можно использовать для определения структуры и разработки подходящего алгоритма для нее. Однако до сих пор неясно, как мы можем эффективно обнаружить структуры, подобные представленной в статье. Хорошо известно, что алгоритмы SAT для одной конкретной проблемы ведут себя плохо в других задачах. Таким образом, существует «свободный обед», хотя, насколько я знаю, это утверждение не может быть официально заявлено.

Маркос Вильягра
источник
Я думаю, что релевантная теорема «без бесплатного обеда» - это «без бесплатного обеда для поиска» no-free-lunch.org . По сути, мы не можем позволить себе поиск по всем возможным проблемным структурам, и нам приходится ориентировать наш поиск на конкретные структуры. Я думаю, что это нормально, так как разработчики алгоритмов для людей уже делают это
Ярослав Булатов