×

The complexity of propositional proofs. (English) Zbl 1133.03037

The article is a broad survey of the field of propositional proof complexity, based upon the author’s Ph.D. thesis. It starts with the Cook-Reckhow definition and Frege systems. Next the connection of resolution to satisfiability algorithms such as DLL is explained, and the relationship of the bounded arithmetic \(I\Delta_0(R)\) to constant-depth Frege is mentioned. The author gives a thorough list of proof systems below Frege (such as \(\text{Res}(k)\), constant-depth Frege, polynomial calculus, Lovász-Schrijver), including a discussion of tree-like and dag-like proofs, and a summary of known lower and upper bounds on proofs of variants of the weak pigeonhole principle and random \(3\)-CNFs in these systems. The paper further mentions feasible interpolation, automatizability, and lower bounds for SAT algorithms on satisfiable formulas. It also discusses strong proof systems, like quantified Frege, and the question of the existence of optimal proof systems. The second part of the paper focuses on some lower bound techniques, including proofs of the main results. The first one is the Ben Sasson-Wigderson theorem relating proof size and proof width of resolution, which is then applied to show exponential resolution lower bounds for \(\text{PHP}^{cn}_n\), and random \(k\)-CNFs. The second one is the small restriction switching lemma due to the author, S. Buss, and R. Impagliazzo, which gives \(\text{Res}\bigl(\sqrt{\log n/\log\log n}\bigr)\) lower bounds for \(\text{PHP}^{cn}_n\). Next, the small restriction switching lemma is combined with the so-called expansion clean-up procedure to obtain a \(\text{Res}\bigl(\sqrt{\log n/\log\log n}\bigr)\) lower bound for random 3-CNFs due to M. Alekhnovich. Finally, Razborov’s pseudowidth is introduced, which is used to prove resolution lower bounds for \(\text{PHP}^m_n\) with large \(m\). The author concludes with some open problems.

MSC:

03F20 Complexity of proofs
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
PDFBibTeX XMLCite
Full Text: DOI Euclid

References:

[1] DOI: 10.1137/S0097539799352474 · Zbl 0976.03062 · doi:10.1137/S0097539799352474
[2] Computational Complexity 131 pp 47– (2004) · Zbl 1087.68566
[3] DOI: 10.1137/S0097539798353230 · Zbl 0959.03044 · doi:10.1137/S0097539798353230
[4] DOI: 10.2307/2275569 · Zbl 0889.03050 · doi:10.2307/2275569
[5] Proceedings of the fortieth annual IEEE symposium on foundations of computer science pp 422– (1999)
[6] DOI: 10.1145/375827.375835 · Zbl 1089.03507 · doi:10.1145/375827.375835
[7] DOI: 10.1007/s00493-004-0036-5 · Zbl 1063.03043 · doi:10.1007/s00493-004-0036-5
[8] Fortieth annual IEEE symposium on foundations of computer science pp 415– (1999)
[9] Proceedings of the thirty-fourth annual ACM symposium on theory of computing pp 563– (2002)
[10] Proceedings of the sixth annual IEEE conference on structure in complexity theory pp 367– (1991)
[11] Proof complexity and feasible arithmetics pp 13– (1998)
[12] Proceedings of the thirty-second international colloquium on automata, languages, and programming pp 1176– (2005)
[13] Current trends in theoretical computer science: Entering the 21st century pp 42– (2001)
[14] Journal of Artificial Intelligence Research 22 pp 319– (2004)
[15] DOI: 10.1137/S0097539700369156 · Zbl 1004.03048 · doi:10.1137/S0097539700369156
[16] Proceedings of the eighteenth IEEE conference on computational complexity pp 225– (2003)
[17] Proceedings of the London Mathematical Society 73 pp 1– (1996)
[18] Computational complexity theory 10 pp 199– (2004) · doi:10.1090/pcms/010/07
[19] Proceedings of the second international conference on principles and practice of constraint programming pp 46– (1996)
[20] Proof complexity and feasible arithmetics pp 1– (1997)
[21] Tenth international conference on principles and practice of constraint programming pp 77– (2004)
[22] Proceedings of the eighteenth annual IEEE conference on computational complexity pp 239– (2003)
[23] DOI: 10.1006/inco.2002.3114 · Zbl 1012.03058 · doi:10.1006/inco.2002.3114
[24] DOI: 10.1016/j.ic.2003.10.004 · Zbl 1051.03014 · doi:10.1016/j.ic.2003.10.004
[25] DOI: 10.1016/S0304-3975(02)00394-8 · Zbl 1017.03034 · doi:10.1016/S0304-3975(02)00394-8
[26] Proceedings of the fifth international conference on theory and applications of satisfiability testing pp 346– (2002)
[27] DOI: 10.1109/TC.2006.79 · doi:10.1109/TC.2006.79
[28] DOI: 10.1109/TCAD.2003.816218 · Zbl 05447143 · doi:10.1109/TCAD.2003.816218
[29] Eleventh IEEE/ACM workshop on logic & synthesis pp 131– (2002)
[30] Proceedings of the Steklov Institute of Mathematics 242 pp 18– (2003)
[31] Proceedings of the forty-second annual symposium on foundations of computer science pp 210– (2001)
[32] Journal of Automated Reasoning 35 pp 51– (2005)
[33] DOI: 10.1137/S0097539700366735 · Zbl 1004.03047 · doi:10.1137/S0097539700366735
[34] Proceedings of the thirty-seventh annual ACM symposium on theory of computing pp 294– (2005)
[35] Proceedings of the thirty-seventh annual ACM symposium on the theory of computing pp 251– (2005)
[36] Proceedings of the twenty-sixth annual ACM symposium on the theory of computing pp 402– (1994)
[37] DOI: 10.1007/BF01302964 · Zbl 0811.03042 · doi:10.1007/BF01302964
[38] Feasible mathematics 9 pp 1– (1990)
[39] Principles and practice of constraint programming pp 121– (2001)
[40] Journal of Computer and System Sciences 68 pp 261– (2004)
[41] Proceedings of the fifteenth annual ACM-SIAM symposium on discrete algorithms pp 139– (2004)
[42] SIAM Journal on Computing 7 pp 149– (1978)
[43] The complexity of propositional proofs pp 425– (1995)
[44] Bulletin of the European Association of Theoretical Computer Science 83 pp 86– (2004)
[45] DOI: 10.1016/0004-3702(77)90029-7 · Zbl 0372.94024 · doi:10.1016/0004-3702(77)90029-7
[46] DOI: 10.1016/j.apal.2003.10.018 · Zbl 1059.03064 · doi:10.1016/j.apal.2003.10.018
[47] Proceedings of the nineteenth annual ACM symposium on theory of computing pp 77– (1987)
[48] First international computer science symposium in Russia pp 600– (2006)
[49] DOI: 10.1137/S0097539703428555 · Zbl 1059.03063 · doi:10.1137/S0097539703428555
[50] DOI: 10.1016/j.ipl.2004.09.024 · Zbl 1173.68714 · doi:10.1016/j.ipl.2004.09.024
[51] Proceedings of the eleventh international symposium on fundamentals of computing theory pp 423– (1997)
[52] Subsystems of second-order arithmetic (1999) · Zbl 0909.03048
[53] Descriptive complexity and finite models 31 (1997)
[54] DOI: 10.2307/2274618 · Zbl 0688.03042 · doi:10.2307/2274618
[55] Methods in mathematical logic pp 317– (1985)
[56] DOI: 10.2307/2269958 · Zbl 0243.02037 · doi:10.2307/2269958
[57] The seventh international conference on theory and applications of satisfiability testing (2004)
[58] Proceedings of the thirty-eighth annual ACM symposium on theory of computing pp 507– (2006)
[59] DOI: 10.1007/BF02023010 · Zbl 0511.03004 · doi:10.1007/BF02023010
[60] DOI: 10.1007/s10472-004-8427-2 · Zbl 1099.68102 · doi:10.1007/s10472-004-8427-2
[61] Eleventh IEEE/ACM workshop on logic and synthesis pp 373– (2002)
[62] Fourth international workshop on algorithms engineering and experiments (ALENEX) pp 29– (2002)
[63] Advances in computing research 5 pp 143– (1989)
[64] DOI: 10.1016/0304-3975(85)90144-6 · Zbl 0586.03010 · doi:10.1016/0304-3975(85)90144-6
[65] DOI: 10.1007/BF00121264 · Zbl 1425.68088 · doi:10.1007/BF00121264
[66] DOI: 10.1090/S0002-9904-1958-10224-4 · Zbl 0085.35807 · doi:10.1090/S0002-9904-1958-10224-4
[67] Proceedings of date 2002 (2002)
[68] DOI: 10.1090/S0894-0347-99-00305-7 · Zbl 0932.05084 · doi:10.1090/S0894-0347-99-00305-7
[69] Proceedings of the thiry-fourth annual ACM symposium on theory of computing pp 534– (2002)
[70] DOI: 10.1016/S0168-0072(97)00029-8 · Zbl 0891.03030 · doi:10.1016/S0168-0072(97)00029-8
[71] DOI: 10.1016/j.jcss.2004.01.004 · Zbl 1106.03049 · doi:10.1016/j.jcss.2004.01.004
[72] Proceedings of the the fifth international conference on developments in language theory pp 100– (2001)
[73] Theoretical Computer Science 303 pp 233– (2001)
[74] DOI: 10.1007/s000370050013 · Zbl 1026.03043 · doi:10.1007/s000370050013
[75] Izvestiya of the Russian Academy of Science and Mathematics 59 pp 201– (1995)
[76] Proceedings of the twenty first annual ACM symposium on theory of computing pp 167– (1989)
[77] DOI: 10.1145/972639.972640 · Zbl 1317.03036 · doi:10.1145/972639.972640
[78] DOI: 10.1016/0020-0190(91)90110-4 · Zbl 0735.68035 · doi:10.1016/0020-0190(91)90110-4
[79] Proof complexity and feasible arithmetics 39 pp 279– (1998)
[80] Metamathematics of first-order arithmetic (1993) · Zbl 0781.03047
[81] Sets and proofs: Invited papers from logic colloquium ’97 258 pp 197– (1997)
[82] DOI: 10.2307/2275583 · Zbl 0945.03086 · doi:10.2307/2275583
[83] DOI: 10.1007/s00493-004-0030-y · doi:10.1007/s00493-004-0030-y
[84] DOI: 10.2307/2275250 · Zbl 0798.03056 · doi:10.2307/2275250
[85] DOI: 10.1007/BF01200117 · Zbl 0784.03034 · doi:10.1007/BF01200117
[86] DOI: 10.1016/S0890-5401(03)00058-0 · Zbl 1029.03048 · doi:10.1016/S0890-5401(03)00058-0
[87] Bulletin of the European Association for Theoretical Computer Science pp 88– (2002)
[88] Zapiski Nauchnyh Seminarov POMI 340 pp 10– (2006)
[89] DOI: 10.1145/1131313.1131314 · Zbl 1367.03106 · doi:10.1145/1131313.1131314
[90] Proceedings of the forty-second annual IEEE symposium on foundations of computer science pp 200– (2001)
[91] DOI: 10.1007/s000370050024 · Zbl 0946.68129 · doi:10.1007/s000370050024
[92] Ninth annual symposium on logic in computer science pp 220– (1994)
[93] Proceedings of the sixteenth IEEE conference on tools with artificial intelligence pp 566– (2004)
[94] DOI: 10.1090/S0273-0979-06-01126-8 · Zbl 1147.68608 · doi:10.1090/S0273-0979-06-01126-8
[95] Proceedings of the tenth national conference on artificial intelligence pp 459– (1992)
[96] Algorithms and data structures in VLSI design (1998)
[97] Proceedings of eleventh international conference on tools and algorithms for construction and analysis of systems pp 1– (2005)
[98] Proceedings of fifteenth internation conference on computer aided verification pp 1– (2003)
[99] DOI: 10.1007/978-3-662-12788-9_6 · doi:10.1007/978-3-662-12788-9_6
[100] DOI: 10.1145/368273.368557 · Zbl 0217.54002 · doi:10.1145/368273.368557
[101] Proceedings of IEEE/ACM internation conference on computer-aided design (1996)
[102] DOI: 10.1006/inco.2001.2921 · Zbl 1005.03009 · doi:10.1006/inco.2001.2921
[103] DOI: 10.1006/jcss.2002.1830 · Zbl 1051.03049 · doi:10.1006/jcss.2002.1830
[104] DOI: 10.1016/j.tcs.2004.04.004 · Zbl 1056.03036 · doi:10.1016/j.tcs.2004.04.004
[105] Proceedings of SAT 2003 (2003)
[106] DOI: 10.1023/B:AIRE.0000036255.53433.26 · Zbl 1078.68782 · doi:10.1023/B:AIRE.0000036255.53433.26
[107] Journal of Artificial Intelligence Research 22 pp 481– (2004)
[108] Journal of Artificial Intelligence Research 23 pp 441– (2005)
[109] Proceedings of the eighteenth national conference on artificial intelligence pp 635– (2002)
[110] DOI: 10.1017/S0269888900001041 · Zbl 02020686 · doi:10.1017/S0269888900001041
[111] DOI: 10.1145/321033.321034 · Zbl 0212.34203 · doi:10.1145/321033.321034
[112] DOI: 10.1287/moor.1050.0151 · Zbl 1082.90143 · doi:10.1287/moor.1050.0151
[113] Proceedings of the thirty-eighth design automation conference pp 530– (2001)
[114] Bounded arithmetic, propositional logic and complexity theory (1995) · Zbl 0835.03025
[115] DOI: 10.1023/A:1021264516079 · Zbl 1010.68069 · doi:10.1023/A:1021264516079
[116] DOI: 10.1137/0801013 · Zbl 0754.90039 · doi:10.1137/0801013
[117] Proceedings of the nineteenth annual IEEE symposium on foundations of computer science pp 193– (1978)
[118] DOI: 10.1002/rsa.3240070103 · Zbl 0843.03032 · doi:10.1002/rsa.3240070103
[119] DOI: 10.1006/inco.1997.2674 · Zbl 0892.68029 · doi:10.1006/inco.1997.2674
[120] DOI: 10.2307/2274765 · Zbl 0696.03029 · doi:10.2307/2274765
[121] DOI: 10.4064/fm170-1-8 · Zbl 0987.03051 · doi:10.4064/fm170-1-8
[122] DOI: 10.2307/2275541 · Zbl 0891.03029 · doi:10.2307/2275541
[123] DOI: 10.2307/2273702 · Zbl 0408.03044 · doi:10.2307/2273702
[124] Proceedings of the seventh annual ACM symposium on the theory of computing pp 107– (1975)
[125] Proof complexity and feasible mathematics 39 pp 93– (1998)
[126] Proceedings of the twenty-eighth annual ACM symposium on the theory of computing pp 174– (1996)
[127] Model checking (1999)
[128] DOI: 10.1145/48014.48016 · Zbl 0712.03008 · doi:10.1145/48014.48016
[129] DOI: 10.1016/j.disc.2006.03.009 · Zbl 1106.05070 · doi:10.1016/j.disc.2006.03.009
[130] Proceedings of the seventeenth international conference on automated deduction pp 449– (2000)
[131] Proceedings of the twelfth international conference on tools with artificial intelligence pp 2– (2000)
[132] Theoretical Computer Science 62 pp 211– (1988)
[133] DOI: 10.1006/jcss.1998.1585 · Zbl 0921.68088 · doi:10.1006/jcss.1998.1585
[134] Proceedings of the eleventh internation workshop on computer science logic pp 149– (1997)
[135] Computational Complexity 6 pp 256– (1997) · Zbl 0966.90506
[136] DOI: 10.1006/jcss.2000.1726 · Zbl 1007.03052 · doi:10.1006/jcss.2000.1726
[137] DOI: 10.1016/S0168-0072(98)00030-X · Zbl 0924.03106 · doi:10.1016/S0168-0072(98)00030-X
[138] Proof complexity and feasible arithmetics pp 59– (1998)
[139] Logic and computation pp 67– (1997)
[140] DOI: 10.1016/0168-0072(91)90036-L · Zbl 0749.03040 · doi:10.1016/0168-0072(91)90036-L
[141] DOI: 10.2307/2273826 · Zbl 0636.03053 · doi:10.2307/2273826
[142] Bounded arithmetic 3 (1986) · Zbl 0649.03042
[143] DOI: 10.4086/toc.2006.v002a004 · Zbl 1213.68328 · doi:10.4086/toc.2006.v002a004
[144] DOI: 10.1007/s00037-002-0171-6 · Zbl 1103.68564 · doi:10.1007/s00037-002-0171-6
[145] DOI: 10.1145/136035.136043 · doi:10.1145/136035.136043
[146] IEEE Transactions on Computers 35 pp 677– (1986)
[147] Handbook of theoretical computer science, volume A (1990)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.