Журнал «Компьютерра» №31 от 30 августа 2005 года
Шрифт:
Одна из этих задач - центральная проблема современной теории сложности: равны ли P и NP? Sapienti sat, а поля этой статьи не настолько шире полей «Арифметики» Диофанта, чтобы вдаваться в подробные объяснения того, что же такое класс задач NP (с P мы уже разобрались - это задачи, которые можно решить полиномиальным алгоритмом). Однако простую переформулировку привести можно: рассмотрим булевскую формулу - то есть формулу, составленную из логических переменных при помощи дизъюнкции, конъюнкции и отрицания (обычно рассматривают формулы в конъюнктивной нормальной форме - это когда формула представлена как большая конъюнкция маленьких дизъюнкций, а отрицания бывают только непосредственно перед входящими в эти дизъюнкции переменными). Внимание, вопрос: существуют ли такие значения
А пока информатика ждет новых гениев, простые (и даже совсем не простые) смертные совершенствуют экспоненциальные алгоритмы для решения этой задачи - ибо она тоже весьма полезна, а кое-где жизненно важна.
Лирическое отступление. Помните знаменитый баг в процессорах Intel, который принес компании несколько миллиардов долларов убытка? Подобные истории до сих пор не редкость. Схемы современных процессоров (и даже отдельных компонентов этих процессоров) настолько сложны, что вручную проверить их соответствие спецификациям не представляется возможным. Оказывается, математически проверка на вшивость базовой схемы из логических компонентов записывается именно в виде SAT, когда решения описывающей схему (точнее - описывающей соответствие схемы модельной схеме или спецификации) формулы соответствуют ошибкам. Невыполнима формула - значит, багов нет, можно запускать в производство.
Сейчас существуют два основных типа алгоритмов для решения SAT: алгоритмы локального поиска, которые начинают с какого-то набора значений (он, конечно, не выполняет всю формулу), а затем модифицируют его, пытаясь последовательно приблизиться к выполняющему набору, и так называемые DPLL-алгоритмы[По именам создателей: Davis, Putnam, Logemann, Loveland; их описание базовых принципов работы этого метода относится к 1968 году], которые обходят дерево всевозможных наборов и выполняют поиск в глубину. Анализ сложности алгоритмов локального поиска, как правило, носит вероятностный характер - ведь нужно начать с какого-то набора, который иначе как случайно выбрать трудно, а от него может зависеть очень многое.
Анализ же сложности DPLL-подобных алгоритмов более детерминирован, во многом благодаря развитой Оливером Кульманом (Oliver Kullmann) и Хорстом Люкхардтом (Horst Luckhardt) теории, связывающей эти оценки с решением рекуррентных уравнений, - их идея оказалась столь плодотворной, что позволила даже создать программы, автоматически доказывающие новые верхние оценки сложности для основанных на этих принципах алгоритмов.
В результате получается вот какая картина: алгоритмы, основанные на локальном поиске, выигрывают практически, а DPLL-подобные алгоритмы - теоретически, для них удается доказать более сильные верхние оценки. Текущий рекорд принадлежит петербургскому математику Эдуарду Алексеевичу Гиршу (он составляет 20,30897K, если за основу измерения взять количество дизъюнкций K в конъюнктивной нормальной форме формулы, и 20,10299L для оценок относительно длины формулы L). Однако практического значения этот алгоритм не имеет: то, что ему нужно сделать в каждом узле дерева, хоть и полиномиально, но чересчур сложно для практических применений[Любопытный факт: один американский студент создал-таки программную реализацию алгоритма Гирша. Несмотря на то что простейший SAT solver (программу, решающую задачу выполнимости) можно написать на коленке за полчаса (трудно писать промышленные солверы - те, которые должны решать большие задачи; там требуются нетривиальные инженерные решения), реализация алгоритма Гирша стала для него дипломным проектом].
Ещё одно отступление. По предыдущим примерам может показаться, что эта деятельность бессмысленна в принципе: если размеры практических задач исчисляются миллионами и миллиардами, улучшения константы в показателе экспоненты имеет весьма малое отношение к практике (хоть и интересно теоретически). Однако программы, решающие SAT, сейчас находят практическое применение (например, в уже упоминавшейся выше верификации логических схем); размеры задач, решаемых сейчас промышленными солверами, исчисляются сотнями и тысячами переменных - что уже свидетельствует о высокой эффективности, ведь базовый-то алгоритм всё равно экспоненциален.
Но практические алгоритмы - основанные на локальном поиске - все же непосредственно пользуются теоретическими наработками, которые позволяют DPLL-алгоритмам держать пальму первенства в области доказанных верхних оценок. DPLL-алгоритмы основаны на правилах упрощения, позволяющих в определенных ситуациях сокращать размер формулы, не меняя того, выполнима ли она. За счет тех же правил упрощения (хотя и не только, конечно) становятся все быстрее и алгоритмы локального поиска.
Такая модель представляется мне весьма характерной для современной теории сложности: разумеется, алгоритмы, являющиеся асимптотически самыми лучшими, далеко не всегда могут стать практически подходящими. Однако идеи, положенные в основу их теоретического успеха, вполне могут найти применение и на практическом поприще - но совершенно не обязательно в первозданном виде.
А напоследок пожалуюсь в личном порядке: кажется, дальнейшее улучшение теоретических оценок на решение SAT уже мало кому интересно (конечно, менее чем экспоненциальная оценка была бы интересна всем и каждому, но в существование таких алгоритмов верится с трудом). На последней конференции SAT-2005, целиком посвященной проблеме решения задачи пропозициональной выполнимости, была только одна работа с теоретическими оценками. Причем была улучшена оценка относительно количества переменных в формуле - что, как правило, гораздо сложнее и интереснее, нежели улучшать оценки относительно длины (теория Кульмана-Люкхардта плохо работает). Но ее приняли только в качестве постера. Зато в докладах были бесконечные «мы написали еще один солвер, вот как он работает»… Совсем в индустрию ударились… ну и ладно, мы им всем еще покажем.
Триптих неестественного богословия
Сегодня мы опять, вслед за майской статьей Якова Кротова в «КТ» #592 и темой #545 «КТ» «Бога нет?», обращаемся к теме «религия и инфотех». Михаил Ваннах рассказывает о проблемах церкви в цифровую эпоху, а также о преломлении кибернетических и эволюционных идей в современном богословии.
– Л.Л.-М.
Использовать данные позитивных наук для вынесения суждений по проблемам теологии занятие довольно бесполезное. Но если взять «классическое» естествознание - физику до относительности и квантов плюс эволюционизм (времен до «нового синтеза») и проэкстраполировать их на жизнь общества, а затем и на богословие, можно получить довольно странный результат.
Апофеоз богословия естественного
«Tantum religio potuit suadere malorum».
T. Lucretius Carus, «De rerum natura» ["Сколько злодеяний вытекают из религии". Тит Лукреций Кар (98-55 до Х.Э.), «О природе вещей»]
«Gott mit uns» («С нами Бог») - так было написано на пряжках солдат Третьего Рейха. Солдат, присягавших вождю германской нации Адольфу Гитлеру, который предпочитал античность из-за отсутствия сифилиса и христианства. Солдат, ложившихся в песок Африки и суглинок России под гимны евангелических пасторов. Как же разрешается этот парадокс?
Стандартный ответ прост. Гитлер с его неоязычеством тактически отложил борьбу с христианской церковью до успешного завершения Второй мировой. Потом христиан ждала бы судьба иудеев. А на пряжках солдат, по образцу эсэсманов, появилось бы политкорректное «Честь в верности». Но из этой схемы выпадает несколько фактов.
Во-первых - язычество, религия примитивных народов. Белокурые арийские девушки в долгополых одеяниях, вершащие обряды плодородия. Описанные у криптоисториков и спародированные Пелевиным да Лазарчуком с Успенским тибетцы в эсэсовских мундирах. В эру ракет и реактивных истребителей!