Журнал «Компьютерра» №31 от 30 августа 2005 года

Хотите миллион долларов? Нет проблем. Clay Mathematics Institute давно уже опубликовал список математических «задач на миллион». Решайте любую, ждите два года после публикации (нужно, чтобы никто не нашел ошибок в течение двух лет) - и золотой ключик у вас в кармане[Наш соотечественник, петербуржец Григорий Перельман уже года два как одну из них решил. Но почему-то не хочет публиковать свое решение (которое уже, по всей видимости, общепризнано) в официальных журналах, а интернет-публикации и прочие препринты для доллароносного фонда не годятся (что вполне логично). Но это, опять же, тема для совсем другого разговора]. Кстати, заработаете вы, конечно, гораздо больше миллиона, хоть бы и с учетом налогов: положение человека, решившего великую задачу, весьма завидно.

Одна из этих задач - центральная проблема современной теории сложности: равны ли P и NP? Sapienti sat, а поля этой статьи не настолько шире полей «Арифметики» Диофанта, чтобы вдаваться в подробные объяснения того, что же такое класс задач NP (с P мы уже разобрались - это задачи, которые можно решить полиномиальным алгоритмом). Однако простую переформулировку привести можно: рассмотрим булевскую формулу - то есть формулу, составленную из логических переменных при помощи дизъюнкции, конъюнкции и отрицания (обычно рассматривают формулы в конъюнктивной нормальной форме - это когда формула представлена как большая конъюнкция маленьких дизъюнкций, а отрицания бывают только непосредственно перед входящими в эти дизъюнкции переменными). Внимание, вопрос: существуют ли такие значения переменных, входящих в формулу, что значение всей формулы будет истинным? Такая задача называется задачей пропозициональной выполнимости (satisfiability, SAT). Если вам удастся найти полиномиальный (от длины формулы) алгоритм для решения SAT, вам обеспечен не только миллион долларов, но и вечная память благодарного потомства.

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

Лирическое отступление. Помните знаменитый баг в процессорах Intel, который принес компании несколько миллиардов долларов убытка? Подобные истории до сих пор не редкость. Схемы современных процессоров (и даже отдельных компонентов этих процессоров) настолько сложны, что вручную проверить их соответствие спецификациям не представляется возможным. Оказывается, математически проверка на вшивость базовой схемы из логических компонентов записывается именно в виде SAT, когда решения описывающей схему (точнее - описывающей соответствие схемы модельной схеме или спецификации) формулы соответствуют ошибкам. Невыполнима формула - значит, багов нет, можно запускать в производство.

Сейчас существуют два основных типа алгоритмов для решения SAT: алгоритмы локального поиска, которые начинают с какого-то набора значений (он, конечно, не выполняет всю формулу), а затем модифицируют его, пытаясь последовательно приблизиться к выполняющему набору, и так называемые DPLL-алгоритмы[По именам создателей: Davis, Putnam, Logemann, Loveland; их описание базовых принципов работы этого метода относится к 1968 году], которые обходят дерево всевозможных наборов и выполняют поиск в глубину. Анализ сложности алгоритмов локального поиска, как правило, носит вероятностный характер - ведь нужно начать с какого-то набора, который иначе как случайно выбрать трудно, а от него может зависеть очень многое.

Анализ же сложности DPLL-подобных алгоритмов более детерминирован, во многом благодаря развитой Оливером Кульманом (Oliver Kullmann) и Хорстом Люкхардтом (Horst Luckhardt) теории, связывающей эти оценки с решением рекуррентных уравнений, - их идея оказалась столь плодотворной, что позволила даже создать программы, автоматически доказывающие новые верхние оценки сложности для основанных на этих принципах алгоритмов.

В результате получается вот какая картина: алгоритмы, основанные на локальном поиске, выигрывают практически, а DPLL-подобные алгоритмы - теоретически, для них удается доказать более сильные верхние оценки. Текущий рекорд принадлежит петербургскому математику Эдуарду Алексеевичу Гиршу (он составляет 20,30897K, если за основу измерения взять количество дизъюнкций K в конъюнктивной нормальной форме формулы, и 20,10299L для оценок относительно длины формулы L). Однако практического значения этот алгоритм не имеет: то, что ему нужно сделать в каждом узле дерева, хоть и полиномиально, но чересчур сложно для практических применений[Любопытный факт: один американский студент создал-таки программную реализацию алгоритма Гирша. Несмотря на то что простейший SAT solver (программу, решающую задачу выполнимости) можно написать на коленке за полчаса (трудно писать промышленные солверы - те, которые должны решать большие задачи; там требуются нетривиальные инженерные решения), реализация алгоритма Гирша стала для него дипломным проектом].