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

Анализ же сложности 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» («С нами Бог») - так было написано на пряжках солдат Третьего Рейха. Солдат, присягавших вождю германской нации Адольфу Гитлеру, который предпочитал античность из-за отсутствия сифилиса и христианства. Солдат, ложившихся в песок Африки и суглинок России под гимны евангелических пасторов. Как же разрешается этот парадокс?

Стандартный ответ прост. Гитлер с его неоязычеством тактически отложил борьбу с христианской церковью до успешного завершения Второй мировой. Потом христиан ждала бы судьба иудеев. А на пряжках солдат, по образцу эсэсманов, появилось бы политкорректное «Честь в верности». Но из этой схемы выпадает несколько фактов.

Во-первых - язычество, религия примитивных народов. Белокурые арийские девушки в долгополых одеяниях, вершащие обряды плодородия. Описанные у криптоисториков и спародированные Пелевиным да Лазарчуком с Успенским тибетцы в эсэсовских мундирах. В эру ракет и реактивных истребителей!

Во-вторых - существование движения Немецких христиан, Имперского епископа Людвига Мюллера и довольно серьезно проработанной ими теологии. Отнюдь не сводимой к зоологическому антисемитизму Нюрнбергских законов, отличной от общепринятого христианства, но, увы, казавшейся привлекательной очень многим в Германии 30-х годов прошлого века - стране, до того четыре десятилетия лидировавшей в мире по числу научных публикаций.

Парадокс этот раскрыл великий богослов XX века Карл Барт (Karl Barth, 1886-1968) в работе «Nein! Antwort an Emil Brunner», 1934 («Нет! Ответ Эмилю Бруннеру» - полемика с другим выдающимся богословом, Генрихом Эмилем Бруннером [1889-1966]). Там Карл Барт пришел к странному на первый взгляд выводу. Выводу, вполне достойному созданной им дисциплины - диалектической теологии.

Начало вероучения Немецких христиан было им прослежено до Theologia Naturalis, до естественного богословия.

Отсылая интересующихся к статье «Место для Бога» ["КТ" #545], скажем вкратце, что естественное богословие - это дисциплина, пытавшаяся вывести бытие Бога из данных позитивных наук. Популярная со времен Фомы Аквината; оттесненная на периферию познания космологией Ньютона-Лапласа; окончательно отброшенная в прошлое с появлением эволюционной теории сэра Чарльза Дарвина.