В статье Томаса Дж. Шефера « Сложность проблем с удовлетворенностью» автор упомянул, что
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.
Мне любопытно, что
- Проводятся ли последующие исследования для разработки этой идеи "доказательств полноты NP с помощью компьютера"? Каково современное состояние (может быть характерно для или )? Так как Шефер предложил идею «NP- доказательства с помощью компьютера» (по крайней мере, для сокращений из ), означает ли это, что существуют некоторые общие принципы / структуры, лежащие в основе этих сокращений (для тех, которые из или )? Если так, то кто они?
- У кого-нибудь есть опыт доказательства NP-полноты с помощью компьютера-помощника? Или кто-нибудь может сделать искусственный пример?
Ответы:
Что касается вопроса 2, то есть по крайней мере два примера доказательств полноты, в которых участвует компьютер-помощник.Nп
Эриксон и Руски предоставили компьютерное доказательство того, что Domino Tatami Covering является NP-полным. Они дали сокращение полиномиального времени от плоского 3-SAT до покрытия татами домино. SAT-решатель (Minisat) был использован для автоматизации обнаружения гаджетов в сокращении. Никакого другого доказательства полноты ему не известно.Nп
Рупп и Хольцер доказали, что карандашная головоломка Какуро является -полной. Некоторые части доказательства N P- полноты были сгенерированы автоматически с использованием SAT-решателя (опять же Minisat).Nп Nп
источник
В этой статье я показал, что если для некоторого существует график с максимальной степенью k и силой хроматического края, строго превышающей k , то Θ p 2 -полноценно решить, является ли прочность хроматического края не более k . Такие графики были известны для k > 3, и я провел компьютерный поиск, чтобы найти подходящий 12- вершинный граф для k = 3 .k ≥ 3 К К Θп2 К к > 3 12 к = 3
Сложность хроматической прочности и хроматической кромочной прочности. Вычислительная сложность, 14 (4): 308-340, 2006
источник
Из комментария выше:
Я использовал библиотеку Choco Java для программирования Constraint, чтобы проверить правильность поведения гаджетов, используемых для доказательства NP-полноты следующих головоломок: Binary Puzzle, Tents, Rolling cube головоломки без свободных ячеек, Net. У меня еще не было времени их публиковать, но проекты статей доступны в моем блоге.
(A) логические элементы (И + ИЛИ) и ссылки, если мы хотим использовать PLANAR SAT в качестве проблемы исходного NPC; или
(B) узел степени 3, в котором ровно 1 вход и 1 выход могут быть активированы одновременно, если мы хотим использовать ГАМИЛЬТОНОВЫЙ ЦИКЛ на сеточных графах в качестве проблемы NPC-источника (обратите внимание, что в этом случае должен быть другой условие, которое заставляет "подключенный путь").
В обоих случаях мы используем исходную конфигурацию, которая фиксирует границы гаджетов (чтобы запретить нежелательные взаимодействия), и мы разрешаем взаимодействие между двумя соседними гаджетами только через центральный элемент (или группу элементов). Конфигурация такого центрального элемента должна представлять логическое значение в случае (A) или обход в случае (B).
Например, чтобы смоделировать AND:
На этом этапе для проверки гаджета с помощью решателя SAT (лучше использовать CPL) достаточно реализовать правила головоломки, а затем проверить выполнимость, когда A, B, C принимают все возможные комбинации значений; и посмотреть, соответствуют ли они желаемому поведению. Например, в случае AND во всех допустимых (выполнимых) конфигурациях гаджета, в которых C равно true (C представляет логическое значение true), и A, и B должны быть true.
Если гаджеты очень сложны (например, в головоломке с вращающимся кубом), я думаю, что это единственный способ убедиться, что они работают правильно (и что доказательство NPC верное).
источник
Я сделал именно это - доказательство полноты NP с помощью компьютера - в моей дипломной работе!
Плохая часть - она на русском и не переведена на английский. http://is.ifmo.ru/diploma-theses/_dvorkin_bachelor.pdf
Я работал с логическими воротами в 2D задачах. План такой:
Код доступен, кстати: https://code.google.com/p/metadynamic-programming/
Таким образом, с ручной работой только для проектирования провода и кодирования правил для конкретной 2D-задачи, я смог доказать NP-полноту:
источник
спрашивающий указал, что он согласен с более широкой интерпретацией высказывания Шефера в ответе. по совпадению собирал ссылки для блога на соседнюю тему и напишу здесь.
исходное утверждение (с. 7 p225) ясно в своих намерениях, что проиллюстрировано на примере полного сокращения NP с 2-х цветных совершенных совпадений thm 7.1 с использованием «дихотомии thm» 2.1.
В широком понимании можно увидеть, что эти общие идеи выросли и были исследованы во многих областях исследований с тех пор, как эти размышления / «начальные идеи» 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 и использовании на них стандартных решателей. Новые границы оптимальных сортировочных сетей Элерс, Мюллер, также цитирует другие недавние работы.
источник