Работа посвящена изучению пропозициональной сложности доказательств. Основыным объектом изучения сложности доказательств являются пропозициональные системы доказательств. Пропозициональные системы доказательств используются для доказательства того, что данная КНФ формула невыполнима. Исследование пропозициональных систем доказательств связано с созданием алгоритмов для задачи выполнимости (SAT-solvers). Протокол работы любого такого алгоритма на невыполнимой формуле можно рассматривать как доказательство ее невыполнимости. Многие алгоритмы для задачи выполнимости основаны на системах доказательств. Например, алгоритм CDCL основан системе доказательств Resolution [1], алгоритм Pseudo Boolean solver основан на Cutting Planes [2], а алгоритмы, использующие в ходе своей работы упорядоченные бинарные диаграммы решений (OBDD), связаны с системами доказательств, основанными на OBDD [3] и т.д.
Минимальный размер опровержения формулы является естественной нижней оценкой на время работы соответствующего алгоритма на этой формуле. В нашей работе мы изучаем глубину опровержений, т.е. наибольшую длину пути от дизъюнкта исходной формулы до противоречия. Глубина является естественной, хоть и мало исследованной характеристикой опровержений. Минимальная глубина доказательства является нижней оценкой на время работы параллельных алгоритмов для задачи выполнимости...
Определение 17 (Исчисление опровержений [4]). Пусть Г = {тДщх - множество пропозициональных формул.
Строка доказательства арности k это предикат P : {0,1}k ^ {0,1} вместе с набором (ii,...,ik) G Zk. Строка доказательства ограничивает возможные значения переменных Xi1,..., xik до тех, для которых P (xi1,... ,xik) = 1. Пусть Lp это множество всех строк доказательства, заданных с помощью предикатов из множества P.
Каждое исчисление опровержений П работает с некоторым множеством допустимых предикатов P вместе с представлениями для этих предикатов. Например, Resolution использует в качестве предикатов различные дизъюнкты, а OBDD(A) представляет предикаты в виде OBDD.
Каждое исчисление опровержений имеет свой конечный набор правил вывода. Каждое правило вывода арности l задает множество R С Lp, для которого верно, что если (Q, P1,..., Pi) G R, то мы можем вывести Q из Pi,... , Pi. Все правила вывода должны быть корректными: если набор значений для переменных выполняет Pi,..., Pi, то он выполняет Q.
Опровержение формулы ф в исчислении опровержений это набор строк доказательства Fi,...Fs таких, что для любого j G [s], Fj либо представляет дизъюнкт ф, либо получен из Fj1,..., Fjl, для некоторых ji,..., ji < s по правилам вывода. При этом Fs представляет тождественно нулевой предикат.
Размером опровержения называет сумма размеров для представлений предикатов из этого опровержения.
Каждое опровержение в исчислении опровержений может быть представлено в виде направленного ациклического графа, подобно тому, как это было сделано для OBDD(A) доказательств (отметим, что OBDD(A) является примером исчисления опровержений). Глубиной опровержения называется глубина его графа, то есть размер длиннейшего пути от истока к стоку.
Исчисление опровержений должно быть полным, то есть все невыполнимые формулы должны иметь опровержение.
Мы говорим, что исчисление опровержений П является системой доказательств (в смысле определения 1), если корректность доказательства можно проверить за полиномиальное от длин формулы и доказательства время.
Определение 18 (Балансируемые системы доказательств). Пусть П это исчисление опровержений, которое также является системой доказательств. Тогда П называется балансируемой, если существует полином p такой, что для любой невыполнимой КНФ формулы ф и для любого ее П-опровержения w размера S, существует опровержение w1, размера p(S) и глубины O(log(S)).
Следствие 19. Системы доказательств OBDD(A), OBDD(A, reordering), а также их древовидные версии не балансируемы.
Доказательство. Формула Peb(Gridn) имеет древовидное OBDD(A) доказательство размера O(n4) по лемме 7 (следовательно и полиномиальное древовидное OBDD(A, reordering) доказательство). Но у Peb(Gridn) не может быть OBDD(A, reordering) доказательства размера poly(n) и при этом глубины O(log poly(n)) = O(log n) по теореме 14 (следовательно маленького доказательства нет и в остальных рассматриваемых системах). Значит балансировка невозможна.
