Какие проблемы SAT легко?

27

Что такое «легкие регионы» для удовлетворения? Другими словами, достаточные условия для того, чтобы некоторые SAT-решатели могли найти удовлетворяющее назначение, предполагая, что оно существует.

Одним из примеров является то, что, когда каждое предложение совместно использует переменные с несколькими другими предложениями, из-за конструктивного доказательства LLL, есть ли какие-либо другие результаты в этом направлении?

Есть большая литература по легким регионам распространения веры, есть ли что-то в этом роде для удовлетворения?

Ярослав Булатов
источник
2
Вас также интересует случайный фазовый переход SAT?
Суреш Венкат
Как выглядит достаточное условие? Питер Шор упомянул в другом посте, что экземпляр SAT должен обладать «случайной структурой», чтобы сделать соотношение предложений и переменных релевантным. Интересно, можно ли это закодировать в достаточных условиях
Ярослав Булатов

Ответы:

33

Полагаю, вы знаете классический результат Шефера из 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).

Standa Zivny
источник
3
Есть более поздняя статья, уточняющая этот результат: сложность проблем выполнимости: «Уточнение теоремы Шефера» Эрик Аллендер, Майкл Бауланд, Нил Иммерман, Хеннинг Шноор и Гериберт Воллмер
Виниций душ Сантуш
1
Спасибо, вот этот doi: dx.doi.org/10.1016/j.jcss.2008.11.001
Standa Zivny
Обратите внимание, что это проблемы удовлетворения ограничений, а не SAT (хотя они могут быть переписаны как экземпляры SAT, но технически SAT означает CSP с предикатами OR).
MCH
14

Я не уверен, что это то, что вы ищете, но есть значительная литература по 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 имеют алгоритмы, которые хорошо работают для удовлетворительных экземпляров, близких к критическому порогу или ниже его (распространение съемки, ходьба и т. Д.), Но не имеют эффективных алгоритмов выше критического порога, чтобы доказать неудовлетворенность.

user834
источник
Интересно, перенесут ли эти какие-либо из этих "случайных результатов k-SAT" в реальные экземпляры SAT, иными словами, если отношение предложений к переменным все еще является полезным показателем твердости
Ярослав Булатов,
1
@ Ярослав, по моему опыту, нет. Многие проблемы реального мира (даже сокращения) имеют (или вводят) такую ​​структуру, чтобы уничтожить случайность, для которой оптимизированы многие решатели. Кажется, что в какой-то момент мы могли бы каким-то образом объяснить эту структуру и сосредоточиться только на части случайности (или «сущности» случайной проблемы), но я не вижу никакого общего способа сделать это, ни Я действительно знаю какие-либо примеры, которые используют эту стратегию.
user834
R(F)Fr[0,1]F
5

Есть много достаточных условий. В некотором смысле, большая часть теоретических CS была посвящена сбору этих условий - фиксированному параметру управляемости, 2-SAT, случайному 3-SAT различной плотности и т. Д.

Питер Бут
источник
2
Это правда, можно взять любую проблему X, которую легко решить, и сказать, что «любая формула, соответствующая проблеме X, проста». Я думаю, что я ищу достаточные условия, которые были бы более эффективными для суммирования простой области, чем «все известные проблемы в P», больше похоже на то, что делает конструктивная локальная лемма Ловаша
Ярослав Булатов
3

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

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

Вот одна из замечательных ссылок в этом отношении, кандидатская диссертация Хервига, есть много других.

[1] Разложение проблем выполнимости или Использование графиков для лучшего понимания проблем выполнимости , Herwig 2006 (83pp)

ВЗН
источник
это график зависимости при применении локальной леммы и вариантов Ловаша к выполнимости. в этом смысле граф предложений был рассмотрен много . Ширер характеризует графы, для которых справедлива локальная лемма, а Колипака и Сегеди сделали результат Шефера конструктивным. Если вы не знаете много, пожалуйста, не делайте вывод, что никто не знает!
Сашо Николов
В ответе Зивного упоминается разбивка шейферов на несколько поддающихся изучению классов, но этот анализ графа раздела относительно новее, глубже и более детализирован, а скорее эмпирически. Что касается цитат, которые вы упоминаете, то, кажется, не упоминается часто в документах / исследованиях по твердости SAT ... есть многократные / параллельные переплетенные линии исследования ...
vzn
Шефер был опечаткой, я имел в виду Ширер. LLL и его варианты - это основной инструмент для разграничения сложных экземпляров k-SAT, поиск в Google покажет тонны ссылок. Теорема Ширера показывает, какие графы предложений гарантируют, что любой экземпляр SAT с этим графом обязательно выполним. Посмотрите в этом обзоре подробные связи с пороговыми значениями жесткости, сложностью построения сложных экземпляров, алгоритмами и т. Д. Disco.ethz.ch/lectures/fs11/seminar/paper/barbara-3.pdf
Сашо Николов
1
общая мысль: каждый раз , когда вы говорите что - то терра инкогнита есть большая вероятность того, что это терра инкогнита для вас . в любом случае комментарии такого рода бесполезны, если только вы не являетесь признанным и опубликованным экспертом в этой области. было бы лучше, если вы ограничите свои ответы тем, что знаете, и оставите комментарии о том, что, по вашему мнению, никто не знает.
Сашо Николов
1
LLL - это один из инструментов для анализа SAT, изобретенный в 1975 году, и с тех пор, возможно, с некоторыми улучшениями. Это рецепт для достаточно простых или сложных случаев, но не обязательно . с тех пор существуют другие подходы, которые все больше заполняют этот пробел новыми способами, т.е. расширяют и обходят его. Вы, должно быть, путаете этот ответ с чем-то другим, в вышеприведенном вопросе термин «terra incognita» не используется. и предлагаю вам ограничиться фактическими письменными ответами, а не размышлять о том, что другие знают или не знают =)
vzn
1

Легко переместить все экземпляры рядом с точкой «перехода» так далеко от точки «перехода», как пожелаете. Движение включает в себя полиномиальное время / пространство.

Если экземпляры, удаленные от точки «перехода», легче решить, то те, которые находятся рядом с точкой перехода, должны быть одинаково легко решены. (Полиномиальные преобразования и все.)

GHR
источник
Можете ли вы уточнить, или у вас есть ссылка на это?
vzn
1

κ

он находит очевидную фрактальную структуру самоподобия жестких экземпляров с параметром restinedess, так что решатель DP (LL) во время поиска имеет тенденцию находить подзадачи с той же критической ограниченностью независимо от того, какая переменная выбрана рядом с ответвлением. есть некоторый дальнейший анализ фрактальной структуры в случаях SAT (например, размерность Хаусдорфа формул SAT и связь с твердостью), например, в [2,3]

другая, несколько взаимосвязанная линия исследования - это связь графов малых миров со (жесткой) структурой SAT, например [4,5].

=?

[1] Острый край ножа , Тоби Уолш, 1998

[2] САМОСТОЯТЕЛЬНОСТЬ СООТВЕТСТВУЮЩИХ БУЛЕВЫХ ВЫРАЖЕНИЙ, ДЕФЕРИРОВАННЫХ В УСЛОВИЯХ НАПРАВЛЕННЫХ ГРАФИЧЕСКИМИ ФУНКЦИОНАЛЬНЫМИ СИСТЕМАМИ Ni и Wen

[3] Визуализация внутренней структуры экземпляров SAT (предварительный отчет) Sinz

[4] Поиск в маленьком мире Уолша 1999

[5] Моделирование более реалистичных задач SAT , Слейтер 2002

ВЗН
источник
3
Это DPLL, а не DP (LL), кстати. Кроме того, есть значительно более поздние работы по фазовому переходу в SAT (см., Например, работу Achlioptas).
Виджай Д
есть алгоритм DP, который предшествует DPLL, который имеет похожее поведение. в другом ответе пользователя 834 в основном упоминалось исследование точки перехода SAT со многими ссылками, но в этом ответе подчеркивается другой (но взаимосвязанный) угол
vzn
1
Я в курсе этих алгоритмов. Я только указывал на стандартное типографское соглашение, которое заключается в написании DP, или DPLL, или DPLL (T), или DPLL (Join), для случая первого порядка без квантификатора. Никто не пишет DP (LL), и это добавляет путаницы с DPLL (T) и DPLL (Join)
Виджай Д
DP (LL) - это то, что подразумевалось под DP + DPLL
vzn