Нижние оценки сложности вывода комбинаторных принципов

АННОТАЦИЯ 2
Введение 3
1 Предварительные сведения 5
2 Формулировка и доказательство основного результата 8
2.1 Конфигурации, трудные для OBDD 9
2.2 Доказательство теоремы 14 13
2.3 Невозможность балансировки OBDD (A, reordering) 14
Список литературы 16
Купить

Работа посвящена изучению пропозициональной сложности доказательств. Основыным объек­том изучения сложности доказательств являются пропозициональные системы доказательств. Пропозициональные системы доказательств используются для доказательства того, что данная КНФ формула невыполнима. Исследование пропозициональных систем доказательств связа­но с созданием алгоритмов для задачи выполнимости (SAT-solvers). Протокол работы любо­го такого алгоритма на невыполнимой формуле можно рассматривать как доказательство ее невыполнимости. Многие алгоритмы для задачи выполнимости основаны на системах доказа­тельств. Например, алгоритм CDCL основан системе доказательств Resolution [1], алгоритм Pseudo Boolean solver основан на Cutting Planes [2], а алгоритмы, использующие в ходе своей работы упорядоченные бинарные диаграммы решений (OBDD), связаны с системами доказа­тельств, основанными на OBDD [3] и т.д.
Минимальный размер опровержения формулы является естественной нижней оценкой на время работы соответствующего алгоритма на этой формуле. В нашей работе мы изучаем глу­бину опровержений, т.е. наибольшую длину пути от дизъюнкта исходной формулы до проти­воречия. Глубина является естественной, хоть и мало исследованной характеристикой опро­вержений. Минимальная глубина доказательства является нижней оценкой на время работы параллельных алгоритмов для задачи выполнимости.
Балансировка систем доказательств
Все системы доказательств, которые мы рассматриваем в нашей работе, являются исчислениями опровержений (см. [4]). Каждое исчисление опровержений П работает со строками доказатель­ства. Строка доказательства — это булев предикат вместе с некоторым своим представлением. Опровержения в П устроены следующим образом: изначально все дизъюнкты опровергаемой формулы представляются в виде строк доказательства, затем новые строки доказательства вы­водятся из предыдущих при помощи конечного набора правил вывода. Цель — вывести строку доказательства, соответствующую тождественно ложному предикату. Например, в Resolution строки доказательства — это дизъюнкты, в Cutting Planes — это линейные неравенства над булевыми переменными с целыми коэффициентами, в Frege Systems — это формулы пропози­циональной логики и т.д.
Размер опровержения в исчислении опровержений — это суммарный размер представлений всех выведенных строк доказательства.
Каждое опровержение может быть представлено в виде направленного ациклического гра­фа с одним истоком, каждая вершина которого помечена строкой доказательства. При этом исток помечен противоречием (тождественно ложной строкой доказательства), а строка дока­зательства в каждой вершине получается из строк доказательств в потомках этой вершины при помощи правил вывода. Глубина опровержения определяется как глубина соответствующего графа, т.е. наибольшая длина пути от истока к стоку.
Система доказательств называется балансируемой, если любое ее опровержение может быть переделано таким образом, что его глубина станет логарифмической от его размера, при этом увеличение размера опровержения ограничено полиномом от размера исходного доказательства.
Далее мы приведем сводку известных результатов о балансируемости некоторых систем до­казательств.
Для системы Resolution вопрос о балансировке в его изначальной форме тривиален. Дей­ствительно, несложно видеть, что любое опровержение формулы (xi V... xn) Л (-xi) Л... Л (-xn) должно иметь глубину п, следовательно в общем случае балансируемости нет. Уркхарт иссле­довал возможность балансировки [5] для формул в О(1)-КНФ, для которых этот вопрос менее тривиален. Было показано, что существует семейство 3-КНФ формул Fni от щ переменных, име­ющих опровержение полиномиального размера в Resolution, но минимальная глубина любого их опровержения должна быть хотя бы П(пДlogni). Следовательно Resolution не балансируется и для случая О(1)-КНФ формул.
Атсериас, Бонет и Леви доказали, что Cutting Planes также не балансируемая [6]. Про Frege Systems, наоборот, известно, что она балансируется (см. [7]).
Системы доказательств, основанные на OBDD
В 1986 Браянт предложил важный способ представления булевых функций [8]. Каждая такая функция может быть представлена в виде ветвящейся программы с двумя стоками, так что пе­ременные на любом пути из корня в стоки идут в одном и том же порядке п. Такое представление называется упорядоченной бинарной диаграммой решений (OBDD или п-OBDD). Ограничение на порядок переменных позволяет эффективно выполнять различные операции над OBDD, на­пример, делать проекции, проверять выполнимость, брать конъюнкцию двух OBDD (если их переменные в одном и том же порядке) и т.п. [9]
Атсериас, Колаитис и Варди предложили [3] системы доказательств, основанные на п-OBDD, для некоторого, заранее зафиксированного порядка п. Среди них нам более всего ин­тересна OBDD(A). В ней дизъюнкты невыполнимой формулы представляются в виде п-OBDD для некоторого заранее зафиксированного порядка п , а единственное правило вывода позволяет получить из двух, ранее выведенных п-OBDD, их конъюнкцию.
Ицыксон, Кноп, Ромащенко и Соколов предложили [10] систему доказательств OBDD(A, reordering), которая получается из OBDD(A) добавлением правила смена порядка, которое позволяет менять порядок переменных в OBDD из доказательства. Теперь OBDD в доказательстве не обязаны находиться все в одном порядке, и правило конъюнкции может быть применено только к OBDD с одним и тем же порядком переменных (иначе проверить коррект­ность доказательства было бы NP-трудной задачей [11]).
Заметим также, что формулы (xi V ... xn) A (-X1) A ... A (-xn), которые мы рассматривали выше, имеют древовидное OBDD(A) доказательство полиномиального размера и логарифмиче­ской глубины.
Как для Resolution так и для Cutting Planes можно привести примеры семейств формул, которые имеют полиномиальное опровержения большой глубины, но не имеют ни одного опро­вержения логарифмической глубины. Для OBDD(A, reordering) такого семейства формул найти нельзя. Действительно, каждая КНФ формула с m дизъюнктами имеет OBDD(A) опровержение глубины log(m) - графом такого доказательства будет полное бинарное дерево с m листьями. Заметим, что размер такого доказательства может значительно отличаться от размера наимень­шего доказательства. Поэтому мы требуем, чтобы после балансировки рост размера доказатель­ства был бы ограничен полиномом от размера исходного доказательства. Заметим, что именно в таком смысле балансируются Frege Systems, и интересно было бы узнать, верно ли аналогичное утверждение для систем, основанных на OBDD.
Наши результаты
Основным результатом нашей работы является теорема о компромиссе между глубиной и разме­ром доказательства (см. Теорему 14). Мы строим семейство невыполнимых формул Fn, которые имеют полиномиальное древовидное OBDD(A) опровержение, но для которых верно следующее: для любого a G (0,1), любое OBDD(A, reordering) опровержение формулы Fn глубины O(n1-a) имеет размер хотя бы 2Q(n“). Из этого следует, что OBDD(A), OBDD(A, reordering), а также их древовидные версии не балансируются.
Формулы Fn это Pebbling формулы для графов сеток n х n: Peb(Gridn). Pebbling формулы хорошо изучены и широко используются при доказательстве нижних оценок (см. например [12], [5], [13]). Примечательно также, что они были использованы при доказательстве нижних оценок на глубину резолюционных доказательств в [5]. Однако, обычно их используют вместе с Pebbling играми и Pebbling числом. Мы не используем эти методы в нашей работе, вместо них мы существенно используем комбинаторную структуру графа сетки (включая самоподобие и расширительную способность).
В разделе 1 мы даем необходимые определения и доказываем предварительные результаты. В разделе 2.1 мы доказываем нижние оценки на некоторое семейство трудных подформул фом- рулы Peb(Gridn). В разделе 2.2 мы доказываем основную теорему. В разделе 2.3 мы доказываем отсутствие балансируемости для OBDD(A), OBDD(A, reordering), а также для их древовидных версий как следствие компромиссов между размером и глубиной, полученных в разделе 2.2.
Купить