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

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

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

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

Такая модель представляется мне весьма характерной для современной теории сложности: разумеется, алгоритмы, являющиеся асимптотически самыми лучшими, далеко не всегда могут стать практически подходящими. Однако идеи, положенные в основу их теоретического успеха, вполне могут найти применение и на практическом поприще - но совершенно не обязательно в первозданном виде.

А напоследок пожалуюсь в личном порядке: кажется, дальнейшее улучшение теоретических оценок на решение SAT уже мало кому интересно (конечно, менее чем экспоненциальная оценка была бы интересна всем и каждому, но в существование таких алгоритмов верится с трудом). На последней конференции SAT-2005, целиком посвященной проблеме решения задачи пропозициональной выполнимости, была только одна работа с теоретическими оценками. Причем была улучшена оценка относительно количества переменных в формуле - что, как правило, гораздо сложнее и интереснее, нежели улучшать оценки относительно длины (теория Кульмана-Люкхардта плохо работает). Но ее приняли только в качестве постера. Зато в докладах были бесконечные «мы написали еще один солвер, вот как он работает»… Совсем в индустрию ударились… ну и ладно, мы им всем еще покажем.

Сегодня мы опять, вслед за майской статьей Якова Кротова в «КТ» #592 и темой #545 «КТ» «Бога нет?», обращаемся к теме «религия и инфотех». Михаил Ваннах рассказывает о проблемах церкви в цифровую эпоху, а также о преломлении кибернетических и эволюционных идей в современном богословии. - Л.Л.-М.

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

Апофеоз богословия естественного

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

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

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

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

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

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

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

Никакие данные естествознания не могут служить для подтверждения того, что есть Бог христианской религии. Точно так же они не могут быть употреблены для опровержения Его существования.

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