Зачем нам всем нужен SAT и все эти P-NP (часть первая)

[Sayonji]

Только это преобразование не за полином делается.

[Sayonji]

Автор неявно предложил этот алгоритм как решение SAT в P, в этом и заключалась задача.

[WarAngel_alk]

Радуют попытки объяснить подобные вещи доступным языком, но всё равно получилось как-то скомкано. Хотя ближе к концу статьи начал понимать что к чему.

[middle]

.

[engine9]

Здравствуйте! Мой не зарегистрированный на хабре товарищ просит передать вопрос: <<Не могли бы вы рассказать про SAT competition? Какие задачи там решают?>>
Спасибо заранее.

[hellman]

www.satcompetition.org/

[varagian]

Обычно к каждому SAT competition идут сборники с описаниями задач и самих solver'ов от участников, например в этом году это описано тут:
helda.helsinki.fi/bitstream/handle/10138/40026/sc2013_proceedings.pdf?sequence=2
helda.helsinki.fi/handle/10138/40026

Если в кратце, то всегда есть random instances — причем известно, как генерировать случайные «сложные» примеры (это опишу в следующий раз в части «зависимость сложности от числа переменных»), всегда есть набор сложных комбинаторных задач в духе задач на графы — клика с весами, случайные графы и что-нибудь в духе графа Petersen'а c задачей найти какой-нибудь путь, задачи планирования и расписаний популярны. Как правило идет отдельный benchmark с индустриальными задачами — их даёт какой-нибудь Boeing или Microsoft (это для примера), отдельный набор с невыполнимыми задачами — проверить насколько быстро solver'ы определяют, что формула UNSAT.

Сейчас набирает популярность pseudo-boolean instances — Satisfibility Modulo Theories:
вот тут можно об это прочитать
research.microsoft.com/en-us/um/people/leonardo/sbmf09.pdf

Если это интересно, могу расспросить участников\организаторов SAT competition и написать короткий обзор.

[hellman]

Еще пару интересных ссылок в копилку:
rjlipton.wordpress.com/2009/07/03/is-pnp-an-ill-posed-problem/
www.win.tue.nl/~gwoegi/P-versus-NP.htm

[amarao]

Пример насчёт газона — 99% американский. В пост-советских домохозяйствах так не живут, чтобы открытый газон перед домом, выходящий на улицу, относился к ИЖС, да ещё, чтобы такие ИЖС в ряд стояли.

[soniq]

Попытка написать про сложные вещи простым языком удалась так себе.

В следующий раз постарайтесь в одной статье не рисовать картинки про импликацию и одновременно использовать символ ■

[mynameco]

На фоне таких фундаментальных работ как то не по себе, когда кто то продает модификацию алгоритма сортировки за деньги.

[mikhaelkh]

Про то, что будет, если P=NP. Доказательство может быть неконструктивным или алгоритм может быть настолько сложным, что для задач, встречающихся на практике, он будет непрактичен. Из P=NP следует только возможность данных новостей.

[arni]

По P, NP, SAT и историю доказательств можно послушать в Ruby NoName Podcast, s04e10 начиная примерно с десятиминутной отметки. ИМХО, очень занимательно и, главное, доходчиво.

[DmitriyN]

Технически это будет означать, что P!=NP, т.к. любая реализация чего-либо, сводящаяся к обратному, была бы доказательством.

[dmitrygusev]

Теоремы о невыразимости: почему статью Романова [3] ожидает reject

[3] Открытое письмо ученым и эталонная реализация алгоритма Романова для NP-полной задачи 3-ВЫП

Это не самая последняя версия работы Романова. Ошибку мы в ней нашли достаточно быстро после публикации. Очень помогла готовая реализация и тестовые наборы, которые мы нашли в SAT Competitions.

Недавно Владимир Федорович опубликовал продолжение своей работы:

romvf.wordpress.com/2013/09/25/development-of-the-concept/

В ней удалось избавиться от той части алгоритма, в которой была ошибка — от гиперструктур.
Хотя, это именно развитие предыдущей работы, поскольку многие положения остаются теми же.

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

[varagian]

Да, видел её у вас в блоге.

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

[bya]

Есть более универсальный (это можно доказать строго) алгоритм/подход (правильнее алгоритмы) из коммутативной алгебры. Это алгоритмы построения базисов Грёбнера.
ru.wikipedia.org/wiki/Базис_Грёбнера
Он в частности решает и SAT задачи и более общие как и постановке, так и по выходной информации.
magma.maths.usyd.edu.au/~allan/gb
В качестве примера готовое ПО
polybori.sourceforge.net
тут и тут
bitbucket.org/fokinpv/ginv
(http://cag.jinr.ru/wiki/Results_of_boolGInv_in_Z_on_Xeon-5410 результаты).
Кнут, который сейчас пишет «The Art of Computer Programming: Volume 4B, Pre-fascicle 6A Satisfiability», на самом деле заинтересовали ZDD диаграммы, которые используются при построении булевых базисов Грёбнера.

[worker4food]

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

[aml]

Так решение задачки-то написали?

Насколько я понимаю, ...

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

[varagian]

всё так и есть, длина DNF растет экспоненциально от n — в этом решение.