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