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

Спасибо, очень интересно!
В начале обещали рассказать о теоремах о невыразительности, но не рассказали :(

каюсь, надо будет рассказать в следующих сериях

Автор, а в чём именно нестыковка трёх утверждений в конце?

вики о тьюринг-полноте:

In the late 19th century, Leopold Kronecker formulated notions of computability, defining primitive recursive functions. These functions can be calculated by rote computation, but they are not enough to make a universal computer, because the instructions which compute them do not allow for an infinite loop. In the early 20th century, David Hilbert led a program to axiomatize all of mathematics with precise axioms and precise logical rules of deduction which could be performed by a machine. Soon, it became clear that a small set of deduction rules are enough to produce the consequences of any set of axioms. These rules were proved to be enough to produce every theorem by Kurt Gödel in 1930. Gödel's completeness theorem of 1930 implicitly contains a definition of a universal computer, because the logical rules acting on some axioms of arithmetic will eventually prove as a theorem the result of any computation.

The actual notion of computation was isolated soon after, starting with Gödel's incompleteness theorem. This theorem showed that axiom systems were limited when reasoning about the computation which deduces their theorems. Church and Turing independently demonstrated that Hilbert's Entscheidungsproblem (decision problem) was unsolvable,[1] thus identifying the computational core of the incompleteness theorem. This work, along with Gödel's work on general recursive functions, established that there are sets of simple instructions, which, when put together, are able to produce any computation. The work of Gödel showed that the notion of computation is essentially unique.

— формальные определения FOL можно посмотреть здесь

Автору. У Вас интересная подборка, но мне кажется есть перекос в сторону рассуждений про P, NP. Вы также упорно игнорируете более универсальные методы коммутативной алгебры. Хотелось бы познакомится именно с алгоритмической составляющей. Какие идеи построения алгоритмов, в чем их преимущество и недостатки. Сложность по времени выполнения и требуемой памяти, тоже интересно, но для практики, как правило дает мало.

Некоторое философствование.

Математиков (и естественно математику) условно можно разделить на «чистых» и тех кто пытается решать конкретные задачи или стремится к этому. Есть в математике разделы про «чистые алгоритмы» там как раз и есть P, NP. Только это не к разработке алгоритмов не к их реализации никакого отношения не имеет. Это «чистая» математика. Я против нее ничего не имею. Пример «чистой» математике принесшей конкретные результаты (в криптографии) это «теория чисел» (но уже есть, хоть и слабые, квантовые компьютеры). Но это скорее исключение из правила.

Например возьмем понятие интеграла. Есть интеграл Римана и Римана — Стилтьеса, он покрывает 99% всех случаев. Есть интеграл Лебега и Лебега — Стилтьеса оставшиеся. Есть еще, не помню как называется, другое понятие интеграла. Я слушал по нему лекцию. Да интересно, он сложней формулируется, но зато много свойств проще доказывается, а некоторые вообще получаются из определения. Ну и что. Когда в тервере начинают рассуждать в крутых понятиях по интегральному исчислению, я считаю это избыточным. Сейчас полно работ по ТФКП и они говорят есть типа приложение профиль Жуковского для задачи аэрогидродинамики. Но его сто лет уже никто не использует и тем более методами ТФКП уравнение Лапласа никто не решает.

Моя интуиция говорит, что P=NP или нет нужно задавать аксиоматически и строить «чистую теорию алгоритмов» в зависимости от принятой аксиомы. Но я сомневаюсь, что на этом пути получится что-нибудь путное для практики. Например придумают «быстрый» алгоритм. которой посчитает трудную задачу за время превышающие возраст нашей Вселенной, но зато он будет из класса P, правда с очень большой константой. Вспомните, например, метод эллипсоидов (алгоритм класса P), который был предложен в 1979 году советским математиком Л. Хачияном для задачи линейного программирования.

Природу обмануть нельзя.

Со стороны всегда просто рассуждать, почему одну работу ждет провал, а другую успех.

Конечно, на весь ваш список «здравого смысла» у меня (и, я уверен, у Владимира Федоровича) есть положительные ответы, но дело даже не в этом.

Статья не претендует на доказательства P ?= NP, в ней просто предлагается алгоритм решения 3-SAT и предлагается новый взгляд на представление этой задачи в виде структур компактных троек, который никто за 40 лет не предлагал, поэтому и нет ссылок — это новая работа, новый подход. И новая NP-полная задача. Искать сходства или различия с существующими подходами и алгоритмами — это не то, чем занимался автор.

В последней работе, на которую вы приводите ссылку, вводятся еще структуры компактных пар и метод, который лежит в основе решения доработанного алгоритма, очень схож с подходами к решению 2-SAT. Но там, например, нет никаких графов, о которых вы пишете. Вы сами-то не разобрались в этой работе, просто ссылаетесь?

Я могу понять, что у вас (и остальных) нет желания разбираться в новой статье, пока даже Романов не исследовал свой подход на практике и не опубликовал результаты. Не исследовал, в частности, потому что нет прототипа. Но его пока нет, и нет только потому, что его просто некому написать. Все действительно так просто.

Я также соглашусь, что в статье нет формального описания алгоритма. Его не было и в прошлой работе, прототип для которой был написан несколько раз. Один, последний, написал я в свое свободное время, постоянно консультируясь с Владимиром Федоровичем в течение 3-х месяцев. Видимо, с этой статьей нужно работать так же… кто возьмется пока я занят? Контакты обеспечу.

Если говорить о статье, в ней приводится именно конструктивное доказательство алгоритма и, кстати, solver от предыдущей работы ни разу не дал ложного решения с практической точки зрения — если формула выполнима он давал выполняемый набор, если нет — набора, соответственно, не выдавалось. И все это за полиномиальное время. 100% верно на всех наших экспериментах (включая формулы из SAT Comp). То есть всегда. Правда, во время своей работы он нарушал теорему из статьи, чего быть, конечно, не должно. Но это ошибка в теории, которая на практике не мешала никак. Еще одной проблемой этого solver'а (точнее самого алгоритма), являлась память — ее нужно было очень (полиномиально) много — поэтому на SAT Competitions с ним делать нечего.

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

Я не могу утверждать, что новая работа 100% верна, но если новый solver будет работать качественно также как предыдущий, только быстрее и потреблять меньше памяти — это уже будет хорошо.