Сложность пропозициональных систем доказательств, оперирующих неравенствами тема диссертации и автореферата по ВАК РФ 01.01.06, кандидат физико-математических наук Кожевников, Арист Александрович

• Кожевников, Арист Александрович
• кандидат физико-математических наук
• 2007

Оглавление диссертации кандидат физико-математических наук Кожевников, Арист Александрович

Введение

Полуалгебраические системы доказательств

Статические полуалгебраические системы доказательств.

Полуалгебраические системы доказательств генценовского типа

Полуалгебраические системы с ограниченной степенью ложности

Структура диссертации.

1 Используемые системы доказательств и семейства тавтологий

1.1 Пропозициональные системы доказательств.

1.2 Алгебраические системы доказательств.

1.3 Полуалгебраические системы доказательств

1.4 Статические полуалгебраические системы доказательств

1.5 Полуалгебраические системы доказательств генценовского типа.

1.6 Понятие степени ложности.

1.7 Понятия и обозначения теории графов.

1.8 Формулы, кодирующие принцип Дирихле.

1.9 Формулы, кодирующие принцип нераскрашиваемости графа, содержащего клику.

1.10 Цейтинские формулы на графах-расширителях.

2 Сложность статических полуалгебраических систем

2.1 Короткое статическое доказательство тавтологии о нераскрашиваемости графа, содержащего клику.

2.2 Нижние экспоненциальные оценки на длину вывода цейт-инских формул в статической полуалгебраической системе доказательств Ловаса-Схрайвера.

2.2.1 Процедура очищения расширителей.

2.2.2 Линейная нижняя оценка на булеву степень вывода биномиальных цейтипских формул в системе доказательств PS

2.2.3 Нижние оценки на булеву степень PS-доказательства биномиальных цейтинских формул.

2.2.4 Преобразование доказательства цейтинских формул в статической LS+ в доказательство в PS.

2.2.5 Нижняя экспоненциальная оценка на размер доказательства в статической LS+

3 Сложность полуалгебраических систем генценовского типа

3.1 Полиномиальная эквивалентность R(L&P) и R(LP), связь R(CP) и R(LP).

3.2 Полиномиальное моделирование L&Pi в CPi.

3.3 Доказательство полиномиального размера цейтинских формул в R(LP).

3.4 Вещественная коммуникационная сложность и нижние экспоненциальные оценки для R(CP).

4 Сложность полуалгебраических систем с ограниченной степенью ложности

4.1 Верхние полиномиальные оценки на размер доказательств принципа Дирихле и принципа нераскрашиваемости графа, содержащего клику.

4.2 Полиномиальное моделирование LS^'+CP^ с ограниченной степенью ложности в Res (к).

4.3 Нижние экспоненциальные оценки для LSfc+CPfc с линейной от количества переменных степенью ложности.

Введение диссертации (часть автореферата) на тему «Сложность пропозициональных систем доказательств, оперирующих неравенствами»

Необходимость математического изучеиия понятия доказательства была сформулирована и обоснована Д. Гильбертом совместно с П. Бер-найсом в "Основаниях математики". Д. Гильберта интересовала непротиворечивость всей математики и, в частности, непротиворечивость доказательств основных теорем. Для того, чтобы проверить корректность доказательства за разумное время, необходимо, чтобы само доказательство было разумного размера. Отсюда возникает важный вопрос о сложности систем доказательств, изучение которого было инициировано работой [21]: в естественном предположении, что каждый шаг доказательства проверяется за полиномиальное время, требуется оценить количество шагов доказательства.

Пропозициональной системой доказательств называется система доказательств для языка TAUT пропозициональных тавтологий в ДНФ. Поскольку такой язык содержится в co-NP, то любую систему доказательств для co-NP-трудного языка L можно считать пропозициональной системой доказательств, для этого необходимо лишь зафиксировать конкретное сведение.

С практической точки зрения системы доказательств интересны тем, что обобщают понятие алгоритма. За одной фиксированной системой доказательств П скрывается целое семейство алгоритмов, оперирующих правилами П. Если мы доказали невозможность существования короткого доказательства для тавтологии х, значит все алгоритмы, применяющие правила из П, будут долго работать на х вне зависимости от того, в каком порядке применяются правила.

Одними из самых известных системам доказательств являются системы Фреге, к которым, например, относятся системы гильбертовского типа и генцсновская система с правилом сечения. С. А. Кук и Р. А. Рекхоу в [21] доказали, что различные системы Фреге полиномиально моделируются друг в друге. Для них, в частности, известны верхние полиномиальные оценки для семейств формул, кодирующих принцип Дирихле [1G] и нераскрашиваемость графа, содержащего клику [54], имеющих экспоненциальную сложность, например, в резолюционной системе доказательств.

Для частного случая систем Фреге, систем Фреге ограниченной глубины, доказано несколько экспоненциальных нижних оценок [52,12,13,18, 45]. Эти системы отличаются от исходных константными ограничениями на глубину промежуточных формул.

Многие системы доказательств не имеют коротких выводов простых фактов, например, известная резолюционная система доказательств, введённая в [55], не имеет короткого доказательства принципа Дирихле. С другой стороны, можно естественным образом переписать данную формулу в виде системы линейных неравенств, например, записав каждую дизъюнкцию следующем образом:

Далее, при помощи полуалгебраических систем доказательств можно выводить из неравенств новые полиномиальные неравенства, являющиеся полуалгебраическими следствиями искомых. В частности, для принципа Дирихле в используемых полуалгебраических системах это приводит к короткому доказательству. На эффективность данной техники для других тавтологий мог бы позволить надеяться предложенный в 1979 JI. Г. Хачия-ном полиномиальный алгоритм решения задачи линейного программирования, а также различные алгоритмы, основанные на методе внутренней точки.

Полуалгебраические системы доказательств

Первая полуалгебраическая система доказательств, "секущие плоскости" (CP), оперирующая только линейными неравенствами, была введена в 6070 годах прошлого века в работах [26,19, 22]. Система основана на простом соображении о том, что сумма целых чисел также должна быть целым числом. Доказательство нижней экспоненциальной оценки для системы "секущие плоскости" долгое время оставалось важным открытым вопросом. В работе [25] была доказана нижняя экспоненциальная оценка для CP с ограниченной степенью ложности (т.е. с ограничением на свободный член неравенства), в работах [15, 41] для CP с унарными (полиномиально ограниченными) коэффициентами, в работах [36, 43] для древовидных "секущих плоскостей", в которых мы не имеем возможности использовать уже доказанные факты многократно и обязаны выводить их каждый раз заново. Для системы без ограничений нижняя экспоненциальная оценка была доказана в [53] для формул, кодирующих ослабленный принцип нераскрашиваемости графа, содержащего клику. Нижняя экспоненциальная оценка для системы "поднять и спроецировать" (L&P) [9], что также оперирует только линейными неравенствами, была доказана техникой, аналогичной технике доказательства вышеупомянутых нижних оценок для CP, в работе [24].

В разделе 3.2 данной диссертации приводится способ преобразования Ь&Р-доказательства в доказательство в CP размера, полиномиально зависящего от размера исходного доказательства и коэффициентов в нём, из которого следует, например, альтернативный метод доказательства нижней экспоненциальной оценки для системы L&Pi с унарными коэффициентами.

Для системы Ловаса-Схрайвера (LS) [48, 47], оперирующей квадратичными неравенствами, нижние экспоненциальные оценки были известны только для древовидных доказательств систем неравенств, не обладающих короткой записью в виде булевой формулы (один из результатов работы [30]). Также было известно несколько условных нижних оценок: для системы, объединённой с CP [54], и для древовидной версии системы [И]. Описанные выше системы можно усилить, позволив им оперировать неравенствами старших степеней [30].

Статические полуалгебраические системы доказательств

Статические системы доказательств интересны тем, что являются удобными для исследования аналогами древовидных систем доказательств (в которых однажды выведенный факт нельзя использовать в качестве леммы, если факт потребуется в дальнейшем выводе, его надо будет доказывать повторно).

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

Впервые формулы, основанные на противоречии, заключающемся в том, что в графе количество рёбер вокруг всех вершин не может быть нечётным, были использованы в работе [3] для получения нижней оценки для регулярной резолюции. Позднее эти оценки были расширены для общей резолюции и улучшены до экспоненциальных для графов-расширителей.

Вторая глава диссертации также содержит короткое статическое доказательство в LS+ четвёртой степени формулы, кодирующей ослабленный принцип нераскрашиваемости графа, содержащего клику. Из этого следует, что статическая система LS+ экспоненциально сильнее системы СР. Данный результат можно рассматривать, как усиление полиномиальной верхней оценки для системы LS+, оперирующей неравенствами четвёртой степени, для аналогичных тавтологий, предложенный в [30].

Полуалгебраические системы доказательств генценовского типа

Полуалгебраическая система генценовского типа R(6) [42] представляет собой естественное усиление 6 — любой из известных ранее полуалгебраических систем — позволяющее работать с предположениями: можно предположить, что сумма мономов с целочисленными коэффициентами / больше чем целое с или, наоборот, / не больше чем с и вывести в каждом предположении противоречие. Через R(LP) мы будем обозначать генце-новское расширение системы, оперирующей исключительно правилом сложения с неотрицательными коэффициентами. Хотя LP не является полной пропозициональной системой (в ней нельзя вывести все тавтологии из TAUT) и для неё существуют эффективные алгоритмы поиска доказательства (первый из которых был предложен JI. Г. Хачияном), её ген-ценовское расширение является полной системой доказательств.

Третья глава целиком посвящена исследованию полуалгебраических систем генценовского типа: в первом разделе доказывается полиномиальная эквивалентность систем R(LP) и R(L&P), а так же R(LPi) и R(CPi) с унарными коэффициентами, в следующем разделе приводится доказательство верхней полиномиальной оценки на размер R(LP)-дoкaзaтeльeтв цейтинских тавтологий. Идея последнего доказательства взята из работы [30], где аналогичная верхняя оценка доказывалась для систем LS больших степеней.

Принадлежащая Я. Крайчеку идея доказательства нижних оценок для формул, кодирующих принцип нераскрашиваемости графа, содержащего клику, заключается в преобразовании доказательства в булеву монотонную схему (интерполяцию схемой) полиномиального размера от размера исходного доказательства. В свою очередь, получаемая схема может быть только экспоненциального размера по теореме Разборова, следовательно, исходное доказательство могло быть только экспоненциального размера.

Я. Крайчек в [42] доказал экспоненциальную нижнюю оценку на размер ЩСР^-доказательств при условии, что каждая дизъюнкция содержит не более, чем 0(пе) неравенств, где п — количество переменных в выводимой формуле. С. Даш в [23, 24] приводит доказательства нижних экспоненциальных оценок на размер доказательств в ограниченной версии древовидной R(L&P). Мы расширяем его оценку для всех древовидных R(6), оперирующих дизъюнкциями линейных неравенств при помощи правил с константным количеством посылок.

В последнем разделе третьей главы вводится понятие вещественной коммуникационной сложности и показывается, как переделать доказательство в Я(СР)-подобной системе доказательств (что может использовать в качестве правил вывода все допустимые двухпосылочные правила вывода) в протокол вещественной игры (в котором два игрока, обмениваясь вещественными числами, должны найти решение поставленной задачи; отметим, что сложность протокола равна количеству переданных чисел). Понятие вещественной коммуникационной игры напрямую связано с понятием вещественной схемы и используемая техника представляет собой частный случай интерполяции схемой. Нижняя экспоненциальная оценка для древовидных 11(СР)-подобных систем получается из оценки на размер древовидного протокола вещественной игры, решающей известную теорему Холла.

Полуалгебраические системы с ограниченной степенью ложности

В работе [25] было введено естественное ограничение на количество дизъюнкций, при помощи которых можно записать данное линейное неравенство, называемое степень ложности линейного неравенства. Неформально, если d — степень ложности данного линейного неравенства с п переменными, то его можно эквивалентно записать при помощи (^Д) дизъюнкций.

В настоящей диссертации мы обобщаем понятие степени ложности на случай неравенств больших степеней и исследуем сложность систем LSfc+CPfc, оперирующих неравенствами степени не превосходящей к с ограниченной степенью ложности при помощи правил LS и СР. В первом разделе четвёртой главы мы доказываем верхние полиномиальные оценки на размер Ь82+СР2-доказательств со степенью ложности, ограниченной корнем от количества переменных, формул, кодирующих принцип Дирихле, и ослабленный принцип нераскрашиваемости графа, содержащего клику. Для этого мы переделываем короткие Ь82+СР2-доказательства, описанные в работе [30], в доказательства с ограниченной степенью ложности.

В разделе 4.2 показано как доказательство в LSfc+CPfc с ограничением на степень ложности можно переделать в доказательство в Res (к) (обобщение резолюционной системы доказательств, оперирующей формулами в fc-ДНФ). Получаемый результат представляет собой обобщение результата [34].

Объединяя результат из предыдущего раздела с нижней экспоненциальной оценкой для Res (к), доказанной в [4], в разделе 4.3 мы показываем нижнюю экспоненциальную оценку для LS^'-f СРА со степенью ложности, ограниченной линейной от количества переменных функцией, для цейтинских формул, построенных по графам-расширителям.

Структура диссертации

Диссертация состоит из введения и четырёх глав. Нумерация разделов, формул, примеров, лемм и теорем ведётся отдельно для каждой главы.

Список литературы диссертационного исследования кандидат физико-математических наук Кожевников, Арист Александрович, 2007 год

1. Кожевников, А. А. Нижние оценки на длину вывода цейтинских формул в статической системе доказательств Ловаса-Схрайвера / Д. М.Ицыксон, А.А.Кожевников // Записки научных семинаров ПОМИ. - СПб.: 2006.- Т. 340.- С. 10-23.

2. Маргулис, Г. А. Явные конструкции расширителей / Г. А. Мар-гулис // Проблемы передачи информации. — 1973. — Т. 9, № 4. — С. 71-80.

3. Цейтин, Г. С. О сложности вывода в исчислении высказываний / Г. С. Цейтин // Записки научных семинаров ЛОМИ. — Л. 1968. — Т. 8. С. 234-259.

4. Alekhnovich, М. Lower bounds for k-DNF resolution on random 3-CNFs / M. Alekhnovich // Proceedings of the 37th annual ACM symposium on Theory of computing. — ACM Press: 2005. — P. 251-256.

5. Alekhnovich, M. Pseudorandom generators in propositional proof complexity / M. Alekhnovich, E. Ben-Sasson, A. A. Razborov and A. Wigderson // SIAM Journal on Computing. 2004. - Vol.34 № 1. - P. 67-88.

6. Alekhnovich, M. Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas / M. Alekhnovich, E. A. Hirsch and D. Itsykson // Journal of Automated Reasoning. — Springer: 2005. Vol. 35 № 1-3. - P. 51-72.

7. Alekhnovich, M. Resolution is not automatizable unless WP] is tractable / M. Alekhnovich and A. A. Razborov // Proceedings of the 42nd Annual IEEE Symposium on Foundations of Computer Science. — 2001. P. 210-219.

8. Atserias, A. On the automatizability of resolution and related propositional proof systems / A. Atserias and M. L. Bonet // Informationand Computation. 2004. - Vol. 189 № 2. - P. 182-201.

9. Balas, E. A lift-and-project cutting plane algorithm for mixed 0-1 programs / E. Balas, S. Ceria and G. Cornuejols // Mathematical Programming. 1993. - Vol. 58 3. - P 295-324.

10. Beame, P. Lower bounds on Hilbert's Nullstellensatz and propositional proofs / P. Beame, R. Impagliazzo, J. Krajicek, T. Pitassi and P. Pudlak. Proc. London Math. Soc. 1996. - Vol. 73 № 3. - P. 1-26.

11. Ben-Sasson, E. Hard examples for bounded depth Frege / E. Ben-Sasson // Proceedings of the 34th Annual ACM Symposium on Theory of Computing. 2002. - P. 563-572.

12. Ben-Sasson, E. Lower bounds for bounded depth Frege proofs via Buss-Pudlak games / E. Ben-Sasson and P. Harsha. — Electronic Colloquium on Computational Complexity. 2003. - TR004. - 16 p.

13. Ben-Sasson, E. Short proofs are narrow — resolution made simple / E. Ben-Sasson and A. Wigderson // Journal of ACM. 2001. - Vol. 48 № 2. - P. 149-169.

14. Bonet, M. Lower Bounds for Cutting Planes Proofs with Small Coefficients / M. Bonet, T. Pitassi and R. Raz // The Journal of Symbolic Logic. 1997. - Vol. 62 № 3. - P. 708-728.

15. Buss, S. R. Polynomial size proofs of the propositional pigeonhole principle / S. R. Buss // The Journal of Symbolic Logic. — 1987. — Vol. 52 № 4. P. 916-927.

16. Buss, S. R. Linear gaps between degrees for the polynomial calculus modulo distinct primes / S. R. Buss, D. Grigoriev, R. Impagliazzo, andT. Pitassi // JCSS. 2001. - Vol. 62. - P. 267-289.

17. Buss, S. R. Proof complexity in algebraic systems and bounded depth Frege systems with modular counting / S. R. Buss, R. Impagliazzo, J. Krajicek, P. Pudlak, A. A. Razborov, and J. Sgall // Computational Complexity. 1996. - Vol. 6 № 3. - P. 256-298.

18. Chvatal, V. Edmonds polytopes and a hierarchy of combinatorial problems / V. Chvatal // Discrete Mathematics. — 1973. — Vol. 4. — P. 305-337.

19. Clegg, M. Using the Groebner basis algorithm to find proofs of unsatisfiability / M. Clegg, J. Edmonds, and R. Impagliazzo // Proceedings of the 28th Annual ACM Symposium on Theory of Computing. 1996. - P. 174-183.

20. Cook, S. A. The relative efficiency of propositional proof systems / S. A. Cook and R. A. Reckhow // The Journal of Symbolic Logic. — 1979. Vol. 44 № 1. - P. 36-50.

21. Cook, W. On the complexity of cutting-plane proofs / W. Cook, C. R. Coullard and G. Turan // Discrete Applied Mathematics. — 1987. Vol. 18 № 1. - P. 25-38.

22. Dash, S. On the Matrix Cuts of Lovasz and Schrijver and their use in Integer Programming : PhD thesis / S. Dash. — 2001. Rice University Technical Report 01-08.

23. Dash, S. An exponential lower bound on the length of some classes of branch-and-cut proofs / S. Dash // Proceedings of IPCO 2002. — Springer: 2002. LNCS 2337. - P. 145-160.

24. Goerdt, A. The Cutting Plane Proof System with Bounded Degree of Falsity / A. Goerdt // Proceedings of CSL 1991. Springer: 1991. -LNCS 626. - P. 119-133.

25. Gomory, R.E. An algorithm for integer solutions of linear programs / Ralph E. Gomory; Editors R. L. Graves and P. Wolfe. — Recent Advancesin Mathematical Programming. McGraw-Hill: 1963. - P. 269-302.

26. Grigoriev, D. Linear lower bound on degrees of Positivstellensatz Calculus proofs for the Parity / D. Grigoriev // TCS. 2001. - Vol. 259. - P. 613-622.

27. Grigoriev, D. Complexity of Null- and Positivstellensatz Proofs /D. Grigoriev and N. Vorobjov// APAL. 2001. - Vol. 113 № 1-3. -P. 153-160.

28. Grigoriev, D. Algebraic proof systems over formulas / D. Grigoriev andE. A. Hirsch // TCS. 2003. - Vol. 303 № 1. - P. 83-102.

29. Grigoriev, D. Complexity of semi-algebraic proofs / D. Grigoriev, E. A. Hirsch, and D. V. Pasechnik // Moscow Mathematical Journal.- M., 2002. Vol. 2 № 4. - P. 647-679.

30. Haken, A. The intractability of resolution / A. Haken // TCS. 1985.- Vol. 39. P. 297-308.

31. Hirsch, E. A. Several notes on the power of Gomory-Chvatal cuts / E. A. Hirsch and A. Kojevnikov // Electronic Colloquium on Computational Complexity. — 2003, January. — TR012. — 10 p.

32. Hirsch, E. A. Several notes on the power of Gomory-Chvatal cuts / E. A. Hirsch and A. Kojevnikov // Annals of Pure and Applied Logic. — 2006. Vol. 141 № 3. - P. 429-436.

33. Hirsch, E. A. Simulating Cutting Plane proofs with restricted degree of falsity by Resolution / E. A. Hirsch and S. I. Nikolenko // Proceedings of SAT 2005. Springer-Verlag: 2005. - LNCS 3569. - P. 135-142.

34. Impagliazzo, R. Lower Bounds for the Polynomial Calculus and the Groebner Basis Algorithm / R. Impagliazzo, P. Pudlak and J. Sgall // Computational Complexity. 1999. - Vol. 3 № 2. - P. 127-144.

35. Impagliazzo, R. Upper and Lower Bounds for Tree-like Cutting Planes Proofs / R. Impagliazzo, T. Pitassi and A. Urquhart // Proceedings of Symposium on Logic in Computer Science. — IEEE: 1994. — P. 220-228.

36. Karchmer, M. Monotone circuits for connectivity require super-logarithmic depth / M. Karchmer and A. Wigderson // SIAM Journal on Discrete Mathematics. 1990. - Vol. 3 № 2. - P. 255-265.

37. Kojevnikov, A. Exponential Lower Bound on the Size of Static Lovasz-Schrijver Calculus / A. Kojevnikov, D. Itsykson // Proceedings of the 33rd International Colloquium on Automata, Languages and Programming. — Springer: 2006. LNCS 4052. - P. 323-334.

38. Kojevnikov, A. Improved Lower Bounds for Resolution over Linear Inequalities / A. Kojevnikov. — Electronic Colloquium on Computational Complexity. 2007, January. - TR010. - 10 p.

39. Kraji'Cek, J. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic / J. Krajicek // Journal of Symbolic Logic. 1997. - Vol. 62 № 2. - P. 457-486.

40. Krajicek, J. Discretely ordered modules as a first-order extension of the cutting planes proof system / J. Krajicek // Journal of Symbolic Logic.- Vol. 63 № 4. P. 1582-1596.

41. Krajicek, J. Interpolation by a game / J. Krajicek // Mathematical Logic Quarterly. 1998. - Vol. 44 № 4. - P. 450-458.

42. Krajicek, J. On the weak pigeonhole principle / J. Krajicek // Fundamenta Mathematicae. 2001. -Vol. 170 № 1-3. - P 123-140.

43. Krajicek, J. An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle / J. Krajicek, P. Pudlak and A. Woods // Random Structures and Algorithms. — 1995. — Vol. 7 № 1.- P. 15-39.

44. Kushilevitz, E. Communication Complexity / E. Kushilevitz andN. Nisan. — 1997. — Cambridge University Press. — p. 189.

45. Lovasz, L. Stable sets and polynomials / L. Lovasz // Discrete Mathematics. 1994. - Vol. 124. - P. 137-153.

46. Lovasz, L. Cones of matrices and set-functions and 0-1 optimization / L. Lovasz and A. Schrijver // SIAM J. Optimization. 1991. - Vol. 1 № 2. - P. 166-190.

47. Lubotzky, A. Ramanujan graphs / A. Lubotzky, R. Phillips and P. Sarnak // Combinatorica. 1988. - Vol. 8 № 3. - P. 261-277.

48. Murty, R. Ramanujan graphs / R. Murty // Journal of the Ramanujan Math. Society. 2003. - Vol. 18 № 1. - P. 1-20.

49. Pitassi, T. Algebraic propositional proof systems / T. Pitassi // Descriptive complexity and finite models (Princeton, NJ, 1996); DIMACS Series in Discrete Mathematics and TCS. — Amer. Math. Soc., Providence: 1997. Vol. 31. - P. 215-244.

50. Pitassi, T. Exponential lower bounds for the pigeonhole principle / T. Pitassi, P. Beame and R. Impagliazzo // Computational Complexity.- 1993. Vol. 3. - P. 97-140.

51. Pudlak, P. Lower bounds for resolution and cutting plane proofs and monotone computations / P. Pudlak // Journal of Symbolic Logic. — 1997. Vol. 62 № 3. - P. 981-998.

52. Pudlak, P. On the complexity of the propositional calculus / P. Pudlak // Sets and Proofs: Invited papers from Logic Colloquium'97.- Cambridge University Press: 1999. P. 197-218.

53. Robinson, J. A. The generalized resolution principle / J. A. Robinson // Machine Intelligence. — American Elsevier: 1968. — Vol 3. — P. 77-94.

54. Segerlind, N. A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution / N. Segerlind, S. R. Buss, and R. Impagliazzo // SIAM Journal on Computing. 2004. - Vol. 33 № 5.- P. 1171-1200.

55. Urquhart, A. Hard examples for resolution / A. Urquhart // Journal of ACM. 1987. - Vol. 34 № 1. - P. 209-219.