Лучшие верхние границы на SAT

43

В другой ветке Джо Фитцсимонс спросил о «лучших текущих нижних границах на 3SAT».

Я хотел бы пойти по другому пути: каковы лучшие текущие верхние границы на 3SAT? Другими словами, какова временная сложность наиболее эффективного SAT-решателя?

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

cc.complexity-theory ds.algorithms sat upper-bounds М.С. Дусти
источник

2

Я не знаю об аналитических результатах, но вы можете найти экспериментальные результаты здесь baldur.iti.uka.de/sat-race-2010/results.html (см. Ссылки "HTML")

Radu GRIGore

1

название этого вопроса немного вводит в заблуждение из-за существования этого вопроса: cstheory.stackexchange.com/questions/1295/sat-solver-download . Я думаю, что вы могли бы перефразировать как «Лучшие верхние границы на SAT»?

Суреш Венкат

@Suresh: вопрос, на который вы ссылаетесь, относится к "#SAT", а этот соответствует SAT. Кроме того, этот вопрос был задан примерно через неделю после этого. В любом случае, вы все еще предлагаете изменить название этих?

MS Dousti

да, потому что "SAT Solver" - это конкретный хорошо известный объект - фактическая кодовая база для решения SAT. Google запутается и перенаправит людей, которые ищут код здесь :).

Суреш Венкат

4

Что касается мотивации этого вопроса, я подумал, что несколько человек попробовали SAT-решатели в 17x17 случаях. Кажется, это граница того, что может быть решено с помощью SAT-решателя. Вместо этого вы могли бы попробовать параллельный решатель, но у меня сложилось впечатление, основываясь на сообщениях Билла Гасарха, что вам потребуются масштабные усилия. Вы также можете применить решатель SMT с подходящей теорией или использовать решатель ограничений, который реализует глобальное ограничение с эффективным пропагатором. В каждом из этих случаев новой идеей будет выражение важного свойства, которое трудно сделать с помощью предложений.

Андрас Саламон

38

Есть два вида «лучших» SAT решателей, один для теории, один для практики.

теория

Казуо Ивама, Казухиса Сето, Тадаши Такаи, Сугуру Тамаки, « Улучшенные рандомизированные алгоритмы для 3-SAT », ISAAC 2010.

рандомизированный для 3SAT. $O(1.32113^n)$

Тимон Хертли, Робин А. Мозер, Доминик Шедер, « Улучшение PPSZ для 3-SAT с использованием критических переменных », 2011.

рандомизированный для 3SAT. $O(1.321^n)$

Константин Куцков, Доминик Шедер, « Использование CSP для улучшения детерминированного 3-SAT », 2010.

детерминированный для 3SAT. $O(1.439^n)$

практика

Проверьте конференцию SAT на результаты соревнований за каждый год.

Тян Лю
источник

Я нашел ссылку на Ивама и соавт. бумага . Итак, действительно ли самый последний и лучший результат для решения SAT до сих пор?

O ({1.32113}^{n})

$O(1.32113^n)$

MS Dousti

@ Садек: Я так думаю, но только для 3-SAT, а не SAT.

Тян Лю

2

Теперь лучший алгоритм за времени - Тимон Хертли, Робин А. Мозер и Доминик Шедер.

O ({1.321}^{n})

$O(1.321^n)$

Тянь Лю

10

Еще одно обновление: в FOCS 2011 Тимон Хертли ( arxiv.org/abs/1103.2165 ) доказал, что алгоритм PPSZ решает каждый экземпляр 3SAT за раза.

{1.308}^{n}

$1.308^n$

Райан Уильямс

21

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

Алгоритм дерандомизации HSSW для 3-SAT показывает, что

«Проблема 3-SAT детерминированно разрешима во времени ». $\overset{\sim}{O}(1.3303^n)$

Дерандомизация PPSZ для Unique-k-SAT показывает, что:

«Для однозначно удовлетворяемого 3-CNF (соответственно 4-CNF) по переменным удовлетворяющее назначение может быть найдено в детерминированном времени выполнения не более (соответственно ). " $n$
$O\hspace{.02 in}(1.3071^n)$ $O\hspace{.02 in}(1.4699^n)$

3-SAT быстрее и проще - границы уникального SAT для удержания PPSZ в целом показывают, что (первоначально упоминалось в комментарии Райана )

«Существует рандомизированный алгоритм для 3-SAT с
односторонней ошибкой, который выполняется во времени ». $O\hspace{.02 in}(1.30704^n)$

«Существует рандомизированный алгоритм для 4-SAT с
односторонней ошибкой, который выполняется во времени ». $O\hspace{.02 in}(1.46899^n)$

Преодоление барьера PPSZ для уникального 3-SAT
требует результата, который можно суммировать следующим образом:

«Существует рандомизированный алгоритм для уникального 3-SAT, такой что для и - действительное число, позволяющее ограничить время выполнения предыдущей статьи для 3-SAT в виде , Настоящий документ в алгоритм работает во времени . " $\: \epsilon = 1\hspace{-0.03 in}\big/\hspace{-0.06 in}\left(\hspace{-0.03 in}10^{\hspace{.02 in}24}\hspace{-0.04 in}\right) \:$
$S$
$\: O\hspace{-0.04 in}\left(2^{(S+o(1))\cdot n}\right) \:$ $\;$ $\: O\hspace{-0.04 in}\left(2^{(S-\epsilon+o(1))\cdot n}\right)$

Сообщество
источник

16

Алгоритм Шенинга является вероятностным алгоритмом для k-SAT со временем выполнения , где . Это приводит к алгоритму для 3SAT, алгоритму для 4SAT и т. Д. $O(a^n)$ $a = 2(k-1)/k$ $O(1.33334^n)$ $O(1.5^n)$

Алгоритм также (почти полностью) дерандомизирован Мозером и Шедером, которые дают детерминистический алгоритм для решения времени работы kSAT где такая же константа, как и раньше, и может быть сделано сколь угодно маленьким. $O((a+\epsilon)^n)$ $a$ $\epsilon>0$

Примечание. В этом ответе в большой записи Oh скрываются поли (n) факторы. Я хотел использовать нотацию , но она не отображается должным образом. $O^*$

Робин Котари
источник

1

Почему вы говорите «почти полностью»? Я что-то пропустил в газете?

Андрас Саламон

1

Существует восемь детерминистических алгоритмов для k-SAT, поэтому, пожалуйста, прости меня, не упоминая их всех. Вот ссылка: linkinghub.elsevier.com/retrieve/pii/S0304397501001748 . Таким образом, для у нас есть и это не так хорошо, как другие оценки для 3-SAT, представленные здесь, но для k-SAT это лучший, насколько я знаю.

O ((2 - \frac{2}{k + 1})^{n})

$O((2 - \frac{2}{k + 1})^n)$

k = 3

$k = 3$

O ({1.5}^{n})

$O(1.5^n)$

Григорий Ярославцев

4

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

Робин Котари

1

@ Григорий Ярославцев: Не является ли детерминированный алгоритм Мозера-Шедера для kSAT, который я упомянул, быстрее, чем тот, который вы цитировали? Я что-то пропустил?

Робин Котари

1

Я просто беспокоился об этом в вашей записи, так что это действительно быстрее. Похоже, что статья появилась на arXiv всего несколько дней назад: arxiv.org/PS_cache/arxiv/pdf/1008/1008.4067v1.pdf , поэтому неудивительно, что я не знал об этом.

ϵ

$\epsilon$

Григорий Ярославцев

12

Как уже упоминалось, если вас интересуют теоретические гарантии времени выполнения, этот вопрос является дубликатом.

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

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

Юкка Суомела
источник

8

В дополнение к резюме Юкки, также стоит отметить, что есть два основных типа решателей SAT: те, которые основаны на распространении результатов опроса, которые хорошо работают для случайных экземпляров SAT, и те, которые используют обучение по пунктам в сочетании с разрешением по единицам, что имеет тенденцию работать хорошо открыть комбинаторную структуру. У них совсем другое поведение. Наихудшими случаями для решателей SAT являются, как правило, случаи, которые не могут быть удовлетворены, но где пространство nogoods имеет сложную структуру, которая не допускает большого сокращения. К сожалению, примеры из комбинаторики, как правило, такого рода.

Андрас Саламон

11

Тимон Хертли, « 3-SAT быстрее и проще - уникальные SAT границы для удержания PPSZ в целом », FOCS 2011.

детерминированный для 3SAT. $O(1.308^n)$

каве
источник

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

Тайфун платят

@TayfunPay: нижняя статья в моем ответе цитирует эту статью.

$\:$

$\;\;\;\;$

@RickyDemer Ух! это лучше, чем это связано? Запись не так понятна для меня.

Tayfun Pay

@TayfunPay: Да, и вы можете охотиться через две бумаги, как описано ниже. На странице 5 общей статьи 3-SAT они дают значение , сообщают время выполнения алгоритма PPSZ для уникального k-SAT в терминах и говорят, что они имеют одинаковую границу для общего k-SAT. В верхней части страницы 11 эта статья говорит, что их алгоритм дает ту же границу, что и PPSZ, что означает, что они не показали ничего большего, чем я упомянул в моем предыдущем предложении. (продолжение ...)

$\:$

S_{3}

$S_3$

S_{k}

$S_k$

$\:$

$\hspace{.35 in}$

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

$\:$

S

$S$

2^{S \cdot n}

$2^{S\cdot n}$

$\:$

S

$S$

S_{3}

$S_3$

$\;\;\;$

8

Для 3SAT невозможно иметь субэкспоненциальные алгоритмы, если гипотеза экспоненциального времени не ложна.

Kazuo Iwama, Suguru Tamaki, Улучшенные верхние границы для 3-SAT , 2004.

рандомизированный алгоритм с ожидаемым временем выполнения для 3SAT. $O({1.324}^n)$

Даниэль Рольф, Улучшенная оценка для алгоритма PPSZ / Schoning для 3-SAT , 2005.

рандомизированный алгоритм с ожидаемым временем выполнения для 3SAT. $O({1.32216}^n)$

Мухаммед Аль-Туркистани
источник

15

Разве это не тавтология?

Цуёси Ито

1

Да, это тавтология: гипотеза экспоненциального времени (ETH) состоит в том, что 3SAT, проблема выполнимости булевых формул в конъюнктивной нормальной форме с не более чем тремя литералами в предложении и с n переменными, не может быть решена за время . (См .: Википедия ).

2^{o (n)}

$2^{o(n)}$

MS Dousti

Работа Kazuo Iwama et al. (2004) новее, чем у Шоенинга (1999). Интересно, есть ли еще более свежие результаты?

MS Dousti

8

Во избежание путаницы мой последний комментарий относится к первому предложению ответа: «Для 3SAT невозможно иметь субэкспоненциальные алгоритмы, если гипотеза об экспоненциальном времени (ETH) не ложна». Я понимаю, что экспоненциальное время Гипотеза является самой гипотезой, утверждающей, что не существует алгоритма для 3SAT, время работы которого является субэкспоненциальным (т.е. 2 ^ {o (n)}) по числу переменных.

Цуёси Ито

10

И чтобы избежать дальнейшей путаницы, я добавлю, что когда Цуёси опубликовал свой комментарий, ответ содержал только одно предложение, что сделало его комментарий очень уместным.

Робин Котари

7

Этот пост посвящен верхним границам SAT. Это одно дело с лучшими нижними границами. По этой ссылке дается подробная информация о ежегодном конкурсе, в котором сравниваются реализации SAT solver, которые можно загрузить. Для простоты вы можете начать с SAT4J , библиотеки на основе Java для решения SAT.

Дэйв Кларк
источник

Оказывается, этот вопрос был уже задан до; Я просто не видел его, когда искал на сайте. Ответ Тянь Лю на вопрос о верхних границах - это именно то, что я искал. Спасибо за ссылки, Дэйв!

Даниэль Апон

1

Это доказательство того, что я провожу здесь слишком много времени ;-)

Дэйв Кларк,

мы рады, что вы делаете :)

Суреш Венкат

2

Я не уверен, что рекомендую sat4J, он не только значительно медленнее, чем современный, но и несколько более сложный. Это правда, однако, что он хорошо настраивается благодаря объектно-ориентированной структуре. MiniSat очень хорошо написан, и 2.2 является современным.

Миколас

3

Лучший детерминированный алгоритм для 3-SAT теперь имеет верхнюю границу 1.32793 ^ n, см. Https://arxiv.org/abs/1804.07901 от Sixue Liu. В основном, верхние границы для всех k-SAT были улучшены в этой статье.

ON KI Wong
источник

Лучшие верхние границы на SAT

Ответы:

теория

практика