Журнал «Компьютерра» №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, сейчас находят практическое применение (например, в уже упоминавшейся выше верификации логических схем); размеры задач, решаемых сейчас промышленными солверами, исчисляются сотнями и тысячами переменных - что уже свидетельствует о высокой эффективности, ведь базовый-то алгоритм всё равно экспоненциален.
Но практические алгоритмы - основанные на локальном поиске - все же непосредственно пользуются теоретическими наработками, которые позволяют DPLL-алгоритмам держать пальму первенства в области доказанных верхних оценок. DPLL-алгоритмы основаны на правилах упрощения, позволяющих в определенных ситуациях сокращать размер формулы, не меняя того, выполнима ли она. За счет тех же правил упрощения (хотя и не только, конечно) становятся все быстрее и алгоритмы локального поиска.
Такая модель представляется мне весьма характерной для современной теории сложности: разумеется, алгоритмы, являющиеся асимптотически самыми лучшими, далеко не всегда могут стать практически подходящими. Однако идеи, положенные в основу их теоретического успеха, вполне могут найти применение и на практическом поприще - но совершенно не обязательно в первозданном виде.
А напоследок пожалуюсь в личном порядке: кажется, дальнейшее улучшение теоретических оценок на решение SAT уже мало кому интересно (конечно, менее чем экспоненциальная оценка была бы интересна всем и каждому, но в существование таких алгоритмов верится с трудом). На последней конференции SAT-2005, целиком посвященной проблеме решения задачи пропозициональной выполнимости, была только одна работа с теоретическими оценками. Причем была улучшена оценка относительно количества переменных в формуле - что, как правило, гораздо сложнее и интереснее, нежели улучшать оценки относительно длины (теория Кульмана-Люкхардта плохо работает). Но ее приняли только в качестве постера. Зато в докладах были бесконечные «мы написали еще один солвер, вот как он работает»… Совсем в индустрию ударились… ну и ладно, мы им всем еще покажем.
Триптих неестественного богословия
Сегодня мы опять, вслед за майской статьей Якова Кротова в «КТ» #592 и темой #545 «КТ» «Бога нет?», обращаемся к теме «религия и инфотех». Михаил Ваннах рассказывает о проблемах церкви в цифровую эпоху, а также о преломлении кибернетических и эволюционных идей в современном богословии.
– Л.Л.-М.
Использовать данные позитивных наук для вынесения суждений по проблемам теологии занятие довольно бесполезное. Но если взять «классическое» естествознание - физику до относительности и квантов плюс эволюционизм (времен до «нового синтеза») и проэкстраполировать их на жизнь общества, а затем и на богословие, можно получить довольно странный результат.
Апофеоз богословия естественного
«Tantum religio potuit suadere malorum».
T. Lucretius Carus, «De rerum natura» ["Сколько злодеяний вытекают из религии". Тит Лукреций Кар (98-55 до Х.Э.), «О природе вещей»]
«Gott mit uns» («С нами Бог») - так было написано на пряжках солдат Третьего Рейха. Солдат, присягавших вождю германской нации Адольфу Гитлеру, который предпочитал античность из-за отсутствия сифилиса и христианства. Солдат, ложившихся в песок Африки и суглинок России под гимны евангелических пасторов. Как же разрешается этот парадокс?