Комментарии 24
НЛО прилетело и опубликовало эту надпись здесь
Радуют попытки объяснить подобные вещи доступным языком, но всё равно получилось как-то скомкано. Хотя ближе к концу статьи начал понимать что к чему.
.
Здравствуйте! Мой не зарегистрированный на хабре товарищ просит передать вопрос: <<Не могли бы вы рассказать про SAT competition? Какие задачи там решают?>>
Спасибо заранее.
Спасибо заранее.
Обычно к каждому 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 и написать короткий обзор.
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 и написать короткий обзор.
Еще пару интересных ссылок в копилку:
rjlipton.wordpress.com/2009/07/03/is-pnp-an-ill-posed-problem/
www.win.tue.nl/~gwoegi/P-versus-NP.htm
rjlipton.wordpress.com/2009/07/03/is-pnp-an-ill-posed-problem/
www.win.tue.nl/~gwoegi/P-versus-NP.htm
НЛО прилетело и опубликовало эту надпись здесь
Пример насчёт газона — 99% американский. В пост-советских домохозяйствах так не живут, чтобы открытый газон перед домом, выходящий на улицу, относился к ИЖС, да ещё, чтобы такие ИЖС в ряд стояли.
Попытка написать про сложные вещи простым языком удалась так себе.
В следующий раз постарайтесь в одной статье не рисовать картинки про импликацию и одновременно использовать символ ■
В следующий раз постарайтесь в одной статье не рисовать картинки про импликацию и одновременно использовать символ ■
На фоне таких фундаментальных работ как то не по себе, когда кто то продает модификацию алгоритма сортировки за деньги.
Про то, что будет, если P=NP. Доказательство может быть неконструктивным или алгоритм может быть настолько сложным, что для задач, встречающихся на практике, он будет непрактичен. Из P=NP следует только возможность данных новостей.
По P, NP, SAT и историю доказательств можно послушать в Ruby NoName Podcast, s04e10 начиная примерно с десятиминутной отметки. ИМХО, очень занимательно и, главное, доходчиво.
НЛО прилетело и опубликовало эту надпись здесь
Теоремы о невыразимости: почему статью Романова [3] ожидает reject
[3] Открытое письмо ученым и эталонная реализация алгоритма Романова для NP-полной задачи 3-ВЫП
Это не самая последняя версия работы Романова. Ошибку мы в ней нашли достаточно быстро после публикации. Очень помогла готовая реализация и тестовые наборы, которые мы нашли в SAT Competitions.
Недавно Владимир Федорович опубликовал продолжение своей работы:
romvf.wordpress.com/2013/09/25/development-of-the-concept/
В ней удалось избавиться от той части алгоритма, в которой была ошибка — от гиперструктур.
Хотя, это именно развитие предыдущей работы, поскольку многие положения остаются теми же.
Готовой программной реализации этого подхода еще нет. Но, если хочется потратить время над исследованиями Романова, то лучше начать с актуальной работы.
Да, видел её у вас в блоге.
В ней присутствует абсолютно те же проблемы, что и в предыдущей версии, но это отдельная тема для обсуждения (постараюсь детально покрыть это в следующий раз). Планирую составить небольшой список здравых вещей, которые должна покрывать статья, чтобы её всерьёз начали рассматривать — это всё довольно известные вещи, никакой магии.
В ней присутствует абсолютно те же проблемы, что и в предыдущей версии, но это отдельная тема для обсуждения (постараюсь детально покрыть это в следующий раз). Планирую составить небольшой список здравых вещей, которые должна покрывать статья, чтобы её всерьёз начали рассматривать — это всё довольно известные вещи, никакой магии.
Есть более универсальный (это можно доказать строго) алгоритм/подход (правильнее алгоритмы) из коммутативной алгебры. Это алгоритмы построения базисов Грёбнера.
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 диаграммы, которые используются при построении булевых базисов Грёбнера.
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 диаграммы, которые используются при построении булевых базисов Грёбнера.
Ничто так не мотивирует, как понимание того, что ты всю сознательную жизнь делил вселенную на бананы и не-бананы.
Так решение задачки-то написали?
Насколько я понимаю, ...
длина дизъюнктивной нормальной формы экспоненциально зависит от n. Добавление ещё одной скобочки к исходной форме увеличивает длину ДНФ в 2-3 раза (в зависимости, сколько слагаемых в новой конъюнкции). Таким образом, само вычисление ДНФ уже займёт экспоненциальное время.
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
Зачем нам всем нужен SAT и все эти P-NP (часть первая)