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

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

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

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

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

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