Введение к работе
Актуальность темы. Сложность задач пропозициональной логики является важной тематикой в теории сложности вычислений и доказательств, составляющей важную область математической логики. Более сорока лет назад независимо С.А.Куком и Л.А.Левиным было предложено понятие NP-полноты, оказавшееся ключевым для современной теории сложности. В 1971 г. С.А.Куком была доказана NP-полнота задачи выполнимости формул логики высказываний, а затем С.А.Кук и Р.А.Рекхоу определили понятие пропозициональной системы доказательств. Последние несколько десятилетий теоретические исследования по оценкам сложности этой задачи велись в двух основных направлениях:
построение новых систем пропозициональных доказательств, анализ отношений моделируемости между ними, построение в них эффективных доказательств важных семейств тавтологий, доказательство нижних оценок сложности для этих систем (первой была работа Г.С.Цейтина 1968 года, затем работы А.Хакена и А.Уркхарта и, наконец, многочисленные работы С.Басса, П.Бима, Я.Крайчека, П.Пудлака, А.А.Разборова и др.);
построение новых алгоритмов для задачи выполнимости пропозициональных формул и связанных с ней задач, доказательство верхних оценок на время их работы (первыми были независимые работы Е.Я.Данцина и Б.Мониена и Э.Шпекенмейера начала 1980-х гг., а затем многочисленные работы О.Кульмана, М.Патури, У.Шонинга и др.).
Задача выполнимости формул в конъюнктивной нормальной форме является NP-полной уже для случая 3-КНФ, причём сведения многих важных задач из NP к этой задаче являются очень естественными. Подавляющая часть известных алгоритмов предназначена для решения задачи выполнимости именно для формул в конъюнктивной нормальной форме, и подавляющая часть систем доказательств также работает с формулами в конъюнктивной
нормальной форме (являющимися отрицаниями формул в дизъюнктивной нормальной форме). Поэтому язык SAT, состоящий из выполнимых формул в конъюнктивной нормальной форме, является одним из наиболее важных изучаемых объектов теории сложности вычислений и доказательств.
Самая известная система доказательств — метод резолюций, восходящий к работам П.С.Порецкого конца XIX века, — имеет непосредственное отношение к алгоритмам, использующим метод расщепления задачи. Хотя большинство применяемых на практике алгоритмов принадлежит к этому классу, первые суперполиномиальные нижние оценки на размер вывода для различных вариантов метода резолюций (из которых следуют нижние оценки на время работы таких алгоритмов) были получены Г.С.Цейтиным для формул, основанных на раскраске рёбер графа в два цвета, ещё в 1960-х гг. (затем они были обобщены и усилены А.Хакеном для пропозиционального принципа Дирихле и А.Уркхартом для формул, аналогичных формулам Цейтина, но построенных на графах-расширителях). Поэтому построение систем доказательств и алгоритмов, основанных на других принципах, является актуальной задачей, важной не только в контексте поиска новых подходов к доказательству нижних оценок сложности, но и для расширения круга задач, которые могут быть решены реализациями алгоритмов на практике.
Наиболее привычными системами доказательств являются системы Фре-ге, названные в честь Готлоба Фреге, который, однако, в своей монографии 1879 года использовал более общие системы, включающие правило подстановки; считается, что первым такие системы без правила подстановки использовал Джон фон Нейман. Экспоненциальных нижних оценок для них не известно и по сей день; однако известны такие оценки для систем, промежуточных между системами Фреге и резолюций: систем Фреге ограниченной глубины (работы Я.Крайчека, П.Пудлака и А.Вудса, Т.Питасси, П.Бима и Р.Импальяццо) и обобщения метода резолюций для формул, являющихся конъюнкциями формул в /с-ДНФ (работа М.Алехновича). Все системы Фреге
эквивалентны, как доказано в диссертации Р.А.Рекхоу 1976 года, и эквивалентны (по их определению) пропозициональному фрагменту генценовского секвенциального исчисления (с правилом сечения). Они обладают определёнными возможностями рассуждений о целых числах (представленных при помощи векторов пропозициональных переменных) — например, имеют полиномиального размера (хоть и технически непростые) доказательства пропозиционального принципа Дирихле, как показано С.Бассом.
Важной для этой задачи тематикой является развитие алгебраических методов, когда рассматриваются системы, в которых можно непосредственно производить вычисления в целых, рациональных, вещественных числах или конечных полях. Такие системы бывают двух типов: основанные на равенствах (такие системы будем называть алгебраическими) и на неравенствах (такие системы будем называть полу алгебраическими).
Алгебраические системы, основаны на слабой теореме Гильберта о нулях. Эти системы были предложены в работах Бима и др. и М.Клегга, Дж.Эдмондса и Р.Импальяццо. Экспоненциальные нижние оценки для этих двух систем были доказаны в серии работ С.Басса, Р.Импальяццо, А.А.Разборова и др. Обобщения алгебраических систем, в которых полиномы могут быть записаны произвольными алгебраическими формулами, были кратко рассмотрены в работах Т.Питасси (с вероятностной проверкой корректности доказательства) и П.Бима и др.
Полуалгебраические системы оперируют неравенствами: формулы в конъюнктивной нормальной форме естественным образом записываются в виде системы линейных неравенств в переменных, принимающих значения О и 1. Одно из важных различий между ними — способ, при помощи которого гарантируется, что решения системы принимают только значения 0 и 1.
Первые такие системы берут начало из исследований по целочисленной линейной оптимизации. Система секущих плоскостей использует правило округления (тот факт, что для целого числа х неравенство х ^ г влечёт
неравенство х ^ М); её полнота была доказана Е.Гомори, далее она подробно изучалась В.Хваталом в контексте целочисленного линейного программирования, а как пропозициональная система она была впервые использована в работе У.Кука, К.Р.Кулларда и Г.Турана. Экспоненциальная нижняя оценка для неё была доказана П.Пудлаком. Другой способ обеспечить принадлежность решений множеству {0,1} — использовать квадратичные неравенства; такие системы берут начало из работы Л.Ловаса и А.Схрайвера 1991 года (полнота более простой системы доказательств, использующей правило "поднять-и-спроектировать", доказана в работе Е.Баласа, С.Керна и Г.Корнуеолса 1993 года). Во всех этих системах пропозициональный принцип Дирихле имеет короткие доказательства.
К другому типу полуалгебраических систем относятся система Positiv-stellensatz и Positivstellensatz-исчисление, берущие начало от работы X.Ломбарди, Н.Мнёва и М.-Ф.Руа и введённые как пропозициональные системы в работах Д.Григорьева и Н.Воробьёва. Хотя фактически для полноты их пропозиционального варианта достаточно слабой теоремы Гильберта о нулях, размер вывода существенно уменьшается за счёт использования неравенств и аксиом, постулирующих неотрицательность квадрата любого полинома. Нижние оценки на степень вывода в этих системах доказаны Д.Григорьевым, однако они не приводят непосредственно к экспоненциальным нижним оценкам на размер вывода.
Наконец, Я.Крайчеком были предложены системы, комбинирующие секвенциальный вывод с использованием неравенств.
Поскольку задача пропозициональной выполнимости NP-полна, маловероятно, что она может быть решена за полиномиальное время. Тем не менее, важно понять, какое время требуется для её решения, даже если это время экспоненциально: алгоритм, решающий SAT, скажем, за время 2П', был бы весьма полезен для многих приложений, например, для современных задач разработки микросхем.
Для некоторых алгоритмов для задачи выполнимости имеются теоретические асимптотические оценки на время их работы; работа других алгоритмов изучена лишь экспериментально, то есть в результате вычислительных экспериментов определено, какие конкретно задачи они способны решить за разумное время. Основные известные подходы таковы.
Алгоритмы, использующие метод расщепления, сводят задачу для входной формулы F к задаче для полиномиального числа формул F\,... , Fp. Это сведение может быть детерминированным (рекурсивно вызывать алгоритм для каждой из формул F{) или вероятностным (случайно выбирать одну из формул F{). Естественно разделить современные расщепляющие алгоритмы на два семейства: классические (DPLL) алгоритмы и алгоритмы, основанные на лемме о кодировании случайного набора.
DPLL-алгоритмы основаны на процедурах, описанных в работах Дэвиса и Патнема и Дэвиса, Лоджмана и Лавлэнда начала 1960-х гг. Грубо говоря, такой алгоритм заменяет входную формулу F двумя формулами F[x] и F[—їж], полученными присваиванием некоторой переменной ж значений true и false соответственно. Затем алгоритм упрощает каждую из полученных формул и рекурсивно вызывает процедуру для каждой из упрощенных формул. Переменная для расщепления на каждом шаге выбирается обычно с учётом лишь "локальных" свойств формулы. В разных ветвях дерева расщепления переменные выбираются независимо (исключением являются экспериментальные алгоритмы, использующие метод запоминания конфликтов). Основным методом анализа таких алгоритмов являются рекуррентные соотношения для количества листьев в дереве рекурсии. Используя этот метод, Е.Я.Данцин и Б.Мониен и Э.Шпекенмейер получили в начале 1980-х гг. первые нетривиальные верхние оценки для k-SAT.
В настоящее время методом, близким к данному, получены наилучшие оценки для задачи выполнимости формул в конъюнктивной нормальной форме (К.Калабро, Р.Импальяццо и М.Патури). Также этот метод является наи-
более популярным среди методов, используемых для построения экспериментальных алгоритмов.
Алгоритмы, основанные на лемме о кодировании выполняющего набора, были предложены М.Патури, П.Пудлаком, М.Саксом и Ф.Зейном. Главное отличие этих алгоритмов от DPLL-алгоритмов заключается в том, что для них важен порядок, в котором переменные выбираются для присваивания, и этот порядок не может быть определён по формуле, как для DPLL-алгоритмов; поэтому либо упорядочение переменных, выбираемых для присваивания, берётся случайным образом, либо (для детерминированного варианта) перебираются все перестановки из некоторого семейства с подходящими свойствами (не зависящими от конкретной формулы). Анализ основан не на локальных (как для DPLL-алгоритмов), а на глобальных рассуждениях, например оценке количества переменных, которые никогда не используются для рекурсивных вызовов, поскольку удаляются во время упрощения. Для этих алгоритмов более простыми являются их вероятностные варианты, когда и упорядочение переменных, и значение переменной на каждом шаге выбираются случайным образом, а вместо возврата из рекурсии используется новый запуск алгоритма с самого начала.
Метод локального поиска используется как в экспериментальных алгоритмах, так и для доказательства верхних оценок (работы Х.Пападимитриу и У.Шонинга). В частности, У.Шонингом доказано, что задача/c-SAT может быть решена алгоритмом, основанным на случайных блужданиях, за время (2 — 2/к)п с точностью до полиномиального сомножителя.
Алгоритмы для других задач пропозициональной логики. Исследования в области верхних оценок в наихудшем случае для трудных задач не ограничиваются SAT. В частности, обобщением SAT является задача максимальной выполнимости, в которой требуется не только найти набор, выполняющий все дизъюнкции входной формулы, если он имеется, но и набор, выполняющий максимально возможное количество дизъюнкций, если выполняющего набо-
pa нет. Для этой задачи применяются методы, похожие на методы для задачи SAT. В особенности популярны DPLL-алгоритмы, однако специфика задачи требует соответствующей модификации этих методов (в частности, правил эквивалентных преобразований формул).
Известно, что степень полиномиального по времени приближения для некоторых трудных задач имеет некоторые границы в предположении, что Р ф NP (работы С.Ароры и др., основанные на так называемой РСР-теореме). В частности, для задачи максимальной выполнимости для формул в 3-КНФ не существует полиномиального алгоритма (еслиР ^ NP), который находил бы набор, выполняющий ^ (g + е)М клозов, где М — максимально возможное число одновременно выполнимых клозов, а є > 0 — сколь угодно малое число. Поэтому представляют интерес алгоритмы, которые находят такие приближенные решения быстрее, чем наилучшие на данный момент алгоритмы находят точные решения.
Цель работы. Основной целью работы является исследование сложности задач пропозициональной логики. К вопросам, охватываемым этой целью, относится построение и анализ алгоритмов для задачи выполнимости пропозициональных формул и связанных с ней задач и построение и анализ систем доказательств для языка пропозициональных тавтологий (или языка невыполнимых пропозициональных формул). В рамках общей задачи требуется разработать новые принципы, на которых могут быть построены такие алгоритмы и системы доказательств, и доказать верхние и нижние оценки их сложности.
Методы исследований. В работе используются методы теории сложности вычислений и доказательств, а также алгебраические методы. В частности, используются методы теории кодирования, строятся системы доказательств, использующие полиномиальные равенства и неравенства, используются методы расщепления и локального поиска.
Теоретическая и практическая ценность. Диссертация имеет теоретический характер. Разработанные в ней методы и полученные результаты могут быть применены для дальнейшего изучения сложности систем доказательств и алгоритмов для задач пропозициональной логики и могут оказаться полезными при разработке систем решения задач пропозициональной логики и систем автоматического доказательства теорем. Материалы диссертации могут составить и частично уже включены в содержание специальных курсов для студентов и аспирантов, обучающихся по специальностям, связанным с теоретической и прикладной математикой и информатикой.
Научная новизна. В диссертации получены следующие новые научные результаты:
Предложен ряд полуалгебраических систем доказательств, в том числе
статических (представляемых одной формулой без вывода); доказаны
возможность эффективных рассуждений о целых числах в системах третьей степени, существование доказательств полиномиального размера для тавтологий о раскраске графа, содержащего клику, и цей-тинских тавтологий в системах ограниченной степени,
экспоненциальная нижняя оценка на размер статических доказательств,
эквивалентность систем доказательств генценовского типа, основанных на принципе "поднять-и-спроектировать", на линейном программировании и на системе секущих плоскостей, при унарной записи коэффициентов.
Предложены алгебраические системы доказательств F-NS и F-PC, опе
рирующие формулами; доказана эквивалентность F-NS и древесного ва
рианта F-PC.
Доказано, что задача максимальной выполнимости для булевых формул
в 2-КНФ, состоящих из К дизъюнкций, может быть решена за время ко(1) . 0(2*/5).
Доказано существование вероятностного (1 — є)-приближенного алгоритма для задачи максимальной выполнимости формул в/с-КНФ, использующего время 0(п^ (2 — k 2ее ке)п) (для произвольного є > 0).
Предложен новый экспериментальный алгоритм для задачи выполнимости, комбинирующий методы локального поиска и устранения единичных дизъюнкций; эффективность алгоритма подтверждена вычислительными экспериментами; доказана его вероятностная приближённая полнота.
Доказано, что задача выполнимости булевых формул в /с-КНФ, использующих п переменных, может быть решена детерминированным алгоритмом, использующим время 0((2 — т—т + є)п) и память полиномиального размера (для произвольного є > 0).
Доказано, что задача выполнимости булевых формул вЗ-КНФ, использующих п переменных, может быть решена детерминированным алгоритмом, использующим время 0(1.481п) и память полиномиального размера.
Апробация работы. Результаты работы докладывались и обсуждались, в частности, на следующих конференциях и семинарах: 27-й международный коллоквиум по автоматам, языкам и программированию (ICALP 2000, Женева, Швейцария, 9-15 июля 2000 г.), 29-й международный коллоквиум по автоматам, языкам и программированию (ICALP 2002, Малага, Испания, 8-13 июля 2002 г.), 17-м ежегодный симпозиум по теоретическим аспектам информатики (STACS 2000, Лилль, Франция, 17-19 февраля 2000 г.), 19-м ежегодный симпозиум по теоретическим аспектам информатики (STACS 2002, Жуан ле Пен, Франция, 14-16 марта 2002 г.), международный ворк-
шоп по логике и сложности в информатике (Университет Париж-12, Франция, 3-5 сентября 2001 г.), 7-й международная конференция по принципам и практике программирования с использованием условий (СР 2001, Пафос, Кипр, 26 ноября - 1 декабря 2001 г.), городской семинар Санкт-Петербурга по математической логике под руководством акад. Ю.В.Матиясевича, общеинститутский математический семинар ПОМП РАН под руководством проф., д.ф.-м.н. А. М.Вершика.
Публикация результатов. Результаты исследований отражены в 19 работах [1]—[19], в том числе 11 работах в изданиях, входящих в Перечень ведущих научных журналов и изданий, в которых должны быть опубликованы основные научные результаты диссертаций на соискание учёной степени доктора наук (издания [1, 3, 8] входили в Перечень на момент публикации; журналы [2, 4, 5, 6, 7, 9, 10, 11] входят в систему цитирования ISI Web of Knowledge).
Совместная работа [2] является объединением трёх независимых работ: работы [3] (а также [12]) и двух работ коллективов соавторов; диссертанту принадлежат в ней алгоритм для &-SAT, использующий память полиномиального размера, улучшенный алгоритм для 3-SAT и доказательства верхних оценок для этих алгоритмов (леммы 7-10, теорема 2 и следствие 2). Эти же принадлежащие диссертанту результаты приводятся в пятом разделе совместной работы [1] и третьем разделе работы [13].
В работе [4] диссертанту принадлежит алгоритм для MAX-2-SAT и доказательство верхней оценки для него (теорема 10). В работе [5] диссертанту принадлежит доказательство эквивалентности системы F-NS и системы древесного вывода F-PC (теорема 6), доказательство моделируемости систем Фреге в F-PC (теорема 3) и короткое доказательство принципа Дирихле в системе F-NS константной глубины (раздел 6). В работе [6] диссертанту принадлежат утверждения о возможности эффективных рассуждений о целых
числах в системах третьей степени (теоремы 5.1 и 5.2, леммы 5.1 и 5.2), теорема о существовании доказательств полиномиального размера для тавтологий о раскраске графа, содержащего клику (теорема 4.1), и цейтинских тавтологий в системах ограниченной степени (теорема 6.1), экспоненциальная нижняя оценка на размер статических доказательств (теоремы 9.1-9.3, следствие 9.1; необходимые для доказательства леммы о нижних оценках на степень доказательств (раздел 8) получены в неразрывном соавторстве). Эти результаты диссертанта также приводятся в совместных работах [14] (разделы 4-6) и [15] (разделы 3 и 4). В работах [8, 9, 18] диссертанту принадлежит алгоритм и доказательство его вероятностной приближённой полноты, соавтору — реализация алгоритма и экспериментальная часть. В работе [11] диссертанту принадлежит методика оценивания, соавторам — реализация системы оценивания. В работе [10] диссертанту принадлежит доказательство эквивалентности алгебраических и полуалгебраических систем доказательств ген-ценовского типа (результаты раздела 2). В работе [19] диссертанту принадлежит доказательство моделирования системы СР с ограниченной степенью ложности методом резолюций (теорема 3).
Остальные результаты в совместных работах принадлежат соавторам. Все результаты, включенные в диссертацию, принадлежат диссертанту.
Структура и объем диссертации. Диссертация изложена на 152 страницах и состоит из введения и двух глав, разбитых на 5 основных разделов, и списка использованной литературы. Библиография включает 91 наименование.
