Что такое «легкие регионы» для удовлетворения? Другими словами, достаточные условия для того, чтобы некоторые SAT-решатели могли найти удовлетворяющее назначение, предполагая, что оно существует.
Одним из примеров является то, что, когда каждое предложение совместно использует переменные с несколькими другими предложениями, из-за конструктивного доказательства LLL, есть ли какие-либо другие результаты в этом направлении?
Есть большая литература по легким регионам распространения веры, есть ли что-то в этом роде для удовлетворения?
cc.complexity-theory
sat
Ярослав Булатов
источник
источник
Ответы:
Полагаю, вы знаете классический результат Шефера из STOC'78, но на всякий случай.
10,1145 / 800133,804350
Шефер доказал, что если SAT параметризуется набором отношений, разрешенных в любом случае, то существует только 6 возможных вариантов: 2-SAT (т. Е. Каждое предложение является двоичным), Horn-SAT, dual-Horn-SAT, affine-SAT ( решения линейных уравнений в GF (2)), 0-действительные (отношения, удовлетворяемые назначением all-0) и 1-действительные (отношения, удовлетворяемые назначением all-1).
источник
Я не уверен, что это то, что вы ищете, но есть значительная литература по 3-SAT фазовому переходу.
Monasson, Zecchina, Kirkpatrcik, Selman и Troyansky по своей природе имели документ, в котором говорится о фазовом переходе случайного k-SAT. Они использовали параметризацию отношения предложений к переменным. Для случайных 3-SAT они численно обнаружили, что точка перехода составляет около 4,3. Выше этой точки случайные 3-SAT экземпляры являются чрезмерно ограниченными и почти наверняка неудовлетворительными, а ниже этой точки проблемы являются ограниченными и выполнимыми (с высокой вероятностью). Мертенс, Мезард и Зекчина используют метод полостного метода для более точной оценки точки фазового перехода.
Вдали от критической точки «тупые» алгоритмы хорошо работают для удовлетворительных случаев (прогулка и т. Д.). Из того, что я понимаю, время выполнения детерминированного решателя растет экспоненциально на фазовом переходе или вблизи него (подробнее см. Здесь ?).
Браунштейн, Мезард и Зекхина (Braunstein, Mezard и Zecchina), близкий родственник по распространению убеждений, представили обзорное распространение, которое, как сообщается, решает удовлетворительные случаи 3-SAT в миллионах переменных, даже очень близко к фазовому переходу. Mezard имеет лекцию здесь на спиновых стеклах (теорию которых он использовал при анализе случайных NP-полных фазовых переходов) и Манево имеет лекцию здесь о распространении обследования.
С другой стороны, похоже, что нашим лучшим решателям требуется экспоненциальное количество времени, чтобы доказать неудовлетворенность. Смотрите здесь , здесь и здесь для доказательства / обсуждения экспоненциальной природы некоторых распространенных методов доказательства неудовлетворенности (процедуры Дэвиса-Путнэма и методы разрешения).
Нужно быть очень осторожным с заявлениями о «легкости» или «твердости» для случайных задач NP-Complete. Наличие отображения проблемы NP-Complete при фазовом переходе не дает никаких гарантий относительно того, где находятся сложные проблемы или есть ли они вообще. Например, задача о цикле Гамильтониана на случайных графах Эрдоша-Реньи доказуемо проста даже в критической точке перехода или вблизи нее. Кажется, что проблема числового разбиения не имеет никаких алгоритмов, которые бы хорошо ее решали в диапазоне вероятностей 1 или 0, не говоря уже о критическом пороге. Из того, что я понимаю, случайные задачи 3-SAT имеют алгоритмы, которые хорошо работают для удовлетворительных экземпляров, близких к критическому порогу или ниже его (распространение съемки, ходьба и т. Д.), Но не имеют эффективных алгоритмов выше критического порога, чтобы доказать неудовлетворенность.
источник
Есть много достаточных условий. В некотором смысле, большая часть теоретических CS была посвящена сбору этих условий - фиксированному параметру управляемости, 2-SAT, случайному 3-SAT различной плотности и т. Д.
источник
пока что в литературе не так широко распространено признание этой концепции, но есть граф предложений задачи SAT (граф с одним узлом на предложение и узлами, связанными, если в предложениях общие переменные), а также другие связанные графы. из представления SAT, кажется, есть много основных подсказок относительно того, насколько сложным будет экземпляр в среднем.
граф выражений может быть проанализирован с помощью всех видов теоретико-графовых алгоритмов, является, по-видимому, естественной мерой «структуры» и имеет сильные связи с измерением / оценкой твердости, и кажется, что исследование этой структуры и ее последствий все еще находится на очень ранней стадии. этапы. не исключено, что исследование точки перехода, традиционный и хорошо изученный способ решения этого вопроса, в конечном итоге может быть соединено с этой структурой графа пункта (в некоторой степени это уже имеет место). другими словами, можно видеть, что точка перехода в SAT существует «из-за» структуры графа предложений.
Вот одна из замечательных ссылок в этом отношении, кандидатская диссертация Хервига, есть много других.
[1] Разложение проблем выполнимости или Использование графиков для лучшего понимания проблем выполнимости , Herwig 2006 (83pp)
источник
Легко переместить все экземпляры рядом с точкой «перехода» так далеко от точки «перехода», как пожелаете. Движение включает в себя полиномиальное время / пространство.
Если экземпляры, удаленные от точки «перехода», легче решить, то те, которые находятся рядом с точкой перехода, должны быть одинаково легко решены. (Полиномиальные преобразования и все.)
источник
он находит очевидную фрактальную структуру самоподобия жестких экземпляров с параметром restinedess, так что решатель DP (LL) во время поиска имеет тенденцию находить подзадачи с той же критической ограниченностью независимо от того, какая переменная выбрана рядом с ответвлением. есть некоторый дальнейший анализ фрактальной структуры в случаях SAT (например, размерность Хаусдорфа формул SAT и связь с твердостью), например, в [2,3]
другая, несколько взаимосвязанная линия исследования - это связь графов малых миров со (жесткой) структурой SAT, например [4,5].
[1] Острый край ножа , Тоби Уолш, 1998
[2] САМОСТОЯТЕЛЬНОСТЬ СООТВЕТСТВУЮЩИХ БУЛЕВЫХ ВЫРАЖЕНИЙ, ДЕФЕРИРОВАННЫХ В УСЛОВИЯХ НАПРАВЛЕННЫХ ГРАФИЧЕСКИМИ ФУНКЦИОНАЛЬНЫМИ СИСТЕМАМИ Ni и Wen
[3] Визуализация внутренней структуры экземпляров SAT (предварительный отчет) Sinz
[4] Поиск в маленьком мире Уолша 1999
[5] Моделирование более реалистичных задач SAT , Слейтер 2002
источник