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

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

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

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

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

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