Любопытно о компьютерных доказательствах NP-полноты

22

В статье Томаса Дж. Шефера « Сложность проблем с удовлетворенностью» автор упомянул, что

This raises the intriguing possibility of computer-assisted NP-completeness proofs. Once the researcher has established the basic framework for simulating conjunctions of clauses, the relational complexity could be explored with the help of a computer. The computer would be instructed to randomly generate various input configurations and test whether the defined relation was non-affine, non-bijunctive, etc.

Конечно, это ограничение:

The fruitfulness of such an approach remains to be proved: the enumeration of the elements of a relation on lO or 15 variables is Surely not a light computational task.

Мне любопытно, что

  1. Проводятся ли последующие исследования для разработки этой идеи "доказательств полноты NP с помощью компьютера"? Каково современное состояние (может быть характерно для или )? Так как Шефер предложил идею «NP- доказательства с помощью компьютера» (по крайней мере, для сокращений из ), означает ли это, что существуют некоторые общие принципы / структуры, лежащие в основе этих сокращений (для тех, которые из или )? Если так, то кто они? 3SAT3-раздела
    СИДЕЛ3SAT3-раздела
  2. У кого-нибудь есть опыт доказательства NP-полноты с помощью компьютера-помощника? Или кто-нибудь может сделать искусственный пример?
Hengxin
источник
3
Это не то же самое, что «доказательство с помощью компьютера», однако я использовал SAT-решатель, чтобы проверить правильность поведения гаджетов, используемых в сокращениях, чтобы доказать NP-полноту следующих игр: Binary Puzzle, Tents, Rolling cube головоломка без свободных клеток, нетто; последние два довольно сложные гаджеты.
Марцио Де Биаси
1
это статья 1978 года, которая в настоящее время является пророческой в ​​этом отношении, если ее интерпретировать широко, а не узко. Существует много эмпирического анализа полных задач SAT и NP. исследование точки перехода можно рассматривать как большое проявление этой идеи. Также был недавний прорыв по проблеме несоответствия Эрдоса с SAT. Еще одной новой областью является поиск небольших сетей сортировки, закодированных в SAT. Еще один пример - преобразование сложных задач в SAT, например, факторинг и изучение примеров. не видел, чтобы кто-нибудь написал большой обзор всего этого. может попытаться вбить что-то из этого в ответ.
ВЗН
1
@MarzioDeBiasi Хотели бы вы поделиться своим опытом в этом отношении (использование SAT-решателя для проверки гаджетов также высоко ценится)? Спасибо.
hengxin
@vzn Звучит очень интересно и захватывающе. С нетерпением жду вашего ответа. Заранее спасибо. Вы можете интерпретировать его широко, как хотите, и, пожалуйста, не стесняйтесь редактировать пост, чтобы сделать его более привлекательным для хороших ответов.
hengxin
1
Есть хорошая статья Trevisan et al. который строит оптимальные гаджеты, используя LP: теория.stanford.edu/~trevisan/pubs/gadgetfull.ps
Диего де Эстрада

Ответы:

22

Что касается вопроса 2, то есть по крайней мере два примера доказательств полноты, в которых участвует компьютер-помощник.Nп

Эриксон и Руски предоставили компьютерное доказательство того, что Domino Tatami Covering является NP-полным. Они дали сокращение полиномиального времени от плоского 3-SAT до покрытия татами домино. SAT-решатель (Minisat) был использован для автоматизации обнаружения гаджетов в сокращении. Никакого другого доказательства полноты ему не известно.Nп

Рупп и Хольцер доказали, что карандашная головоломка Какуро является -полной. Некоторые части доказательства N P- полноты были сгенерированы автоматически с использованием SAT-решателя (опять же Minisat).NпNп

Мухаммед Аль-Туркистани
источник
1
По крайней мере, отчасти это похоже на «Триангуляция с минимальным весом NP-hard» по Малзеру и Роте. Компьютер использовался для установления правильности гаджетов (но, возможно, гаджеты были найдены «вручную»).
Juho
15

В этой статье я показал, что если для некоторого существует график с максимальной степенью k и силой хроматического края, строго превышающей k , то Θ p 2 -полноценно решить, является ли прочность хроматического края не более k . Такие графики были известны для k > 3, и я провел компьютерный поиск, чтобы найти подходящий 12- вершинный граф для k = 3 .К3ККΘ2пКК>312Кзнак равно3

Сложность хроматической прочности и хроматической кромочной прочности. Вычислительная сложность, 14 (4): 308-340, 2006

Даниэль Маркс
источник
13

Из комментария выше:

Я использовал библиотеку Choco Java для программирования Constraint, чтобы проверить правильность поведения гаджетов, используемых для доказательства NP-полноты следующих головоломок: Binary Puzzle, Tents, Rolling cube головоломки без свободных ячеек, Net. У меня еще не было времени их публиковать, но проекты статей доступны в моем блоге.

01N×N

(A) логические элементы (И + ИЛИ) и ссылки, если мы хотим использовать PLANAR SAT в качестве проблемы исходного NPC; или

(B) узел степени 3, в котором ровно 1 вход и 1 выход могут быть активированы одновременно, если мы хотим использовать ГАМИЛЬТОНОВЫЙ ЦИКЛ на сеточных графах в качестве проблемы NPC-источника (обратите внимание, что в этом случае должен быть другой условие, которое заставляет "подключенный путь").

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

Например, чтобы смоделировать AND:

***C***   *=fixed elements (initial config. of the puzzle)
*xxxxx*   x=internal logic (some elements can be fixed,
AxxxxxB     other must be completed/traversed)
*xxxxx*   A,B,C=elements shared with adjacent gadgets
*******

На этом этапе для проверки гаджета с помощью решателя SAT (лучше использовать CPL) достаточно реализовать правила головоломки, а затем проверить выполнимость, когда A, B, C принимают все возможные комбинации значений; и посмотреть, соответствуют ли они желаемому поведению. Например, в случае AND во всех допустимых (выполнимых) конфигурациях гаджета, в которых C равно true (C представляет логическое значение true), и A, и B должны быть true.

Если гаджеты очень сложны (например, в головоломке с вращающимся кубом), я думаю, что это единственный способ убедиться, что они работают правильно (и что доказательство NPC верное).

Марцио де Биаси
источник
11

Я сделал именно это - доказательство полноты NP с помощью компьютера - в моей дипломной работе!

Плохая часть - она ​​на русском и не переведена на английский. http://is.ifmo.ru/diploma-theses/_dvorkin_bachelor.pdf

Я работал с логическими воротами в 2D задачах. План такой:

  • Вручную спроектируйте, как выглядит «провод» в вашей задаче.
  • Используйте очень умный и оптимизированный поиск (фактически динамическое программирование по наборам профилей), чтобы автоматически спроектировать все необходимые логические элементы.
  • PROFIT!

Код доступен, кстати: https://code.google.com/p/metadynamic-programming/

Таким образом, с ручной работой только для проектирования провода и кодирования правил для конкретной 2D-задачи, я смог доказать NP-полноту:

  • Тральщик
  • Зона покрытия горизонтальными домино и вертикальными тримино
  • КК4К[4,6]
Михаил Дворкин
источник
2
Даже если вы не планируете публиковать статью об автоматической генерации гаджетов, все же стоит написать краткое резюме вашей диссертации на английском языке и включить файл в ваш репозиторий кода.
Андрас Саламон
-4

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

исходное утверждение (с. 7 p225) ясно в своих намерениях, что проиллюстрировано на примере полного сокращения NP с 2-х цветных совершенных совпадений thm 7.1 с использованием «дихотомии thm» 2.1.

F(Икс)

F(Икс)Икс

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

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

  • Разоблачение проблем выполнимости или Использование графиков для лучшего понимания проблем выполнимости , Herwig 2006 (83pp). это несколько новаторский подход по сравнению с другими опубликованными исследованиями, в которых рассматривается структура графа с переменным предложением сгенерированных экземпляров SAT и анализируется их структура / метрики, чтобы найти корреляции с твердостью.

  • Можно принять сложные предположительные задачи и закодировать их как экземпляры SAT, а затем исследовать их структуру или запустить на них решатели SAT и наблюдать за динамическим поведением решателей SAT. не легко понять, когда это было сделано 1-м, но ранний случай связан с факторингом, вероятно, в середине 1990-х или около того, и эти случаи обнаружились в конкурсах решателей DIMACS SAT. к сожалению, в то время это не обязательно рассматривалось отдельно публикуемыми результатами исследований. есть намеки в нескольких статьях SAT.

    см., например, « Удовлетворение этим: попытка решения факторизации простых чисел с использованием решателей удовлетворенности » Стефана Шенмеккера, Анны Кавендер и также вопрос cs.se, сводящий проблему целочисленной факторизации к полной проблеме NP & (есть некоторые другие связанные / разбросанные (T) вопросы обмена стека CS на это).

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

  • проблема Erdos Расхождение связано с ограничениями на случайных блужданий очень трудно , и прогресс был ограничен с аналитическими подходами, и роман / беспрецедентный, эмпирический подход с SAT недавно был взят для достижения некоторых ключевых результатов на родственном открытых проблем, отмечаемый многими как настоящий прорыв. SAT-атака на гипотезу несоответствия Эрдоса Конев, Лисица

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

ВЗН
источник