Рецензия на статью М. И. Тельпиза “NP-полнота, суперприведение и проблема четырех красок”

 

Рецензируемая работа посвящена построению алгоритмов (или, как их иногда называют в данном контексте, эвристик) для решения NP-полной задачи “ВЫПОЛНИМОСТЬ”, т.е. поиску назначений, выполняющих данную пропозициональную формулу. Большое число известных эвристик такого рода основано на той или иной пропозициональной системе доказательств (очень хорошее популярное введение в последний предмет со списком литературы для дальнейшего чтения может быть найдено в [1]) и устроены следующим образом.

Пусть имеется КНФ формула, состоящая из семейств клашей (т.е. дизьюнкций литералов) C1(x1,...,xn),...,Cm(x1,...,xn). Мы хотим узнать выполнима ли эта формула и, если да, построить для нее выполняющее назначение. Для этой цели фиксируется некоторый класс пропозициональных формул C, включающий в себя, в частности, все клаши и некоторый набор правил вывода, позволяющий из формул F1,...,Fr C вывести новую формулу F C с тем свойством, что всякий выполняющий набор для F1,...,Fr также выполняет F. Предполагается, что эта система доказательств полна, т.е. если система клашей {C1,...,Cm} невыполнима, то из нее выводится противоречие. Алгоритм, основанный на такой системе доказательств, последовательно выводит из {C1,...,Cm} новые формулы из класса C, определяя в соответствии с собственными внутренними предпочтениями какое именно правило вывода применять на каждом шаге (набор этих предпочтений и называется эвристикой). Если алгоритму удается вывести противоречие, он останавливается и исходная формула объявляется невыполнимой. В противном случае в какой-то момент накопленной информации оказывается достаточно, чтобы “считать” с нее выполняющее назначение, и на этом работа алгоритма также прекращается.

 

Настоящая статья целиком укладывается в эту распространенную схему. При этом автор использует свою собственную систему обозначений, называемую им принципом позиционности. Хотя у меня имеются серьезные сомнения в продуктивности этой системы, к чести автора следует отметить, что им не было предпринято попыток специально затемнить существо дела, и перевод его обозначений на общепринятый язык проводится в-общем без особых затруднений. Описанная автором пропозициональная система доказательств в системе Q3 – не что иное, как классическая система резолюций (см., например, вышеупомянутый обзор [1]). Ее расширение (в авторских обозначениях – система Q2) оперирует с формулами несколько более общего вида

 

(((i11i22)i22)...)iw∊w;

 

где i1 < i2 < ... < iw , 1,...,w {0, 1}, x1x, x0 ≡ (¬x) и всякая – одна из двух операций {, }. Используемое в этой системе правило вывода называется автором коньюнктивной резолюцией; оно достаточно подробно описано в §4.

 

Основной (и единственный) содержательный математический результат данной работы состоит в том, что некоторая эвристика, основанная на такой пропозициональной системе доказательств работает за полиномиальное время, из чего непосредственно вытекает P = NP. В отличие от пропозициональной системы и правила вывода, описание самой эвристики (т.е., инструкций, в соответствии с которыми алгоритм определяет какое именно правило выода применять в каждый конкретный момент времени) является весьма приблизительным и туманным. При этом именно в тех местах, когда детали алгоритма приобретают особое значение для понимания его работы, изложение становится наиболее загадочным. В качестве особо яркого примера я могу отметить §7:4: как именно проводится то, что автор называет “сегментацией” – это один из наиболее тонких и ключевых моментов в понимании всего алгоритма, и понять, как именно это делается, из текста не представляется возможным.

Впрочем, все эти детали не слишком важны, так как из известных в теории сложности доказательств результатов вытекает существование конкретных невыполнимых КНФ, для которых вообще никакая эвристика, основанная на системе Q2 , не в состоянии вывести противоречие за полиномиальное время. Для системы Q3 (т.е. резолюций) – это классический результат, впервые доказанный в [2]. Система Q2 , насколько мне известно, никем специально ранее не рассматривалась. Однако практически любые современные методы доказательства сложности вывода противоречия в системе резолюций легко обобщаются на систему Q2. Просмотрев имеющуюся литературу, я могу, например, порекомендовать ознакомиться с доказательством экспоненциальной нижней оценки для случайных КНФ из [3, §4], обобщение которого на систему Q2 получается особенно естественно и просто.

 

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

 

 

 

 

 

 

А. А. Разборов


Список литературы

 

[1]   P. Beame and T. Pitassi. Propositional proof complexity: Past, present and future. Technical Report TR98-067, Electronic Colloquium on Computational Complexity, 1998. Available at ftp://ftp.eccc.uni-trier.de/pub/eccc/reports/1998/TR98-067/index.html.

[2]   A. Haken. The intractability or resolution. Theoretical Computer Science,  39:297–308, 1985.

[3]   P. Beame and T. Pitassi. Simplified and improved resolution lower bounds. In Proceedings of the 37th IEEE FOCS, pages 274–282, 1996. Also available at http://www.cs.washington.edu/homes/beame/papers/clause.ps.