An introduction to lower bounds on resolution proof systems. (English) Zbl 1486.03097
Summary: Proof complexity, a measure to estimate the sizes of proofs in propositional logics, is studied as one of the fundamental approaches to the \(\mathcal{P}\) versus \(\mathcal{NP}\) problem, and has some practical applications such as automated theorem proving. It is a very hard task to prove lower bounds on strong proof systems such as Frege systems, for which no non-trivial lower bound is known yet. On the other hand, we have some rich success stories on weaker proof systems such as resolution proof systems. In this paper, we focus on resolution proof systems and review some of the existing techniques for proving lower bounds.
MSC:
| 03F20 | Complexity of proofs |
References:
| [1] | Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. Space complexity in propositional calculus. SIAM J. Comput., 31(4):1184-1211, 2002. · Zbl 1004.03047 |
| [2] | Paul Beame, Christopher Beck, and Russell Impagliazzo. Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space. In STOC, pages 213-232, 2012. · Zbl 1286.68180 |
| [3] | Paul Beame, Richard M. Karp, Toniann Pitassi, and Michael E. Saks. On the complexity of unsatisfiability proofs for random k-cnf formulas. In STOC, pages 561-571, 1998. · Zbl 1028.68067 |
| [4] | Paul Beame and Toniann Pitassi. Propositional proof complexity: Past, present, and future. In Current Trends in Theoretical Computer Science, pages 42-70, 2001. · Zbl 1049.03040 |
| [5] | Christopher Beck and Russell Impagliazzo. Strong eth holds for regular resolution. In STOC, pages 487-494, 2013. · Zbl 1293.03032 |
| [6] | Eli Ben-Sasson and Nicola Galesi. Space complexity of random formulae in resolution. Random Struct. Algorithms, 23(1):92-109, 2003. · Zbl 1048.03046 |
| [7] | Eli Ben-Sasson and Jakob Nordström. Short proofs may be spacious: An optimal separation of space and length in resolution. Electronic Colloquium on Computational Complexity (ECCC), 16:2, 2009. |
| [8] | Eli Ben-Sasson and Jakob Nordström. Understanding space in resolution: Optimal lower bounds and exponential trade-offs. Electronic Colloquium on Computational Complexity (ECCC), 16:34, 2009. |
| [9] | Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow-resolution made simple. J. ACM, 48(2):149-169, 2001. · Zbl 1089.03507 |
| [10] | Samuel R. Buss. Towards np-p via proof complexity and search. Ann. Pure Appl. Logic, 163(7):906-917, 2012. · Zbl 1257.03086 |
| [11] | Samuel R. Buss and Toniann Pitassi. Resolution and the weak pigeonhole principle. In CSL, pages 149-156, 1997. · Zbl 0910.03036 |
| [12] | Samuel R. Buss and György Turán. Resolution proofs of generalized pigeonhole principles. Theor. Comput. Sci., 62(3):311-317, 1988. · Zbl 0709.03006 |
| [13] | Vasek Chvátal and Endre Szemerédi. Many hard examples for resolution. J. ACM, 35(4):759-768, 1988. · Zbl 0712.03008 |
| [14] | Matthew Clegg, Jeff Edmonds, and Russell Impagliazzo. Using the groebner basis algorithm to find proofs of unsatisfiability. In STOC, pages 174-183, 1996. · Zbl 0938.68825 |
| [15] | Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. J. Symb. Log., 44(1):36-50, 1979. · Zbl 0408.03044 |
| [16] | Juan Luis Esteban and Jacobo Torán. Space bounds for resolution. In STACS, pages 551-560, 1999. · Zbl 0924.03020 |
| [17] | Armin Haken. The intractability of resolution. Theor. Comput. Sci., 39:297-308, 1985. · Zbl 0586.03010 |
| [18] | Philipp Hertel and Toniann Pitassi. An exponential time/space speedup for resolution. Electronic Colloquium on Computational Complexity (ECCC), 14(046), 2007. |
| [19] | Jakob Nordström. Narrow proofs may be spacious: Separating space and width in resolution. SIAM J. Comput., 39(1):59-121, 2009. · Zbl 1192.03042 |
| [20] | Jakob Nordström. A simplified way of proving trade-off results for resolution. Inf. Process. Lett., 109(18):1030-1035, 2009. · Zbl 1202.68388 |
| [21] | Jakob Nordström. On the relative strength of pebbling and resolution. ACM Trans. Comput. Log., 13(2):16, 2012. · Zbl 1352.03069 |
| [22] | Jakob Nordström. Pebble games, proof complexity, and time-space trade-offs. Logical Methods in Computer Science, 9(3), 2013. · Zbl 1285.03070 |
| [23] | Jakob Nordström and Johan Håstad. Towards an optimal separation of space and length in resolution. Electronic Colloquium on Computational Complexity (ECCC), 15(026), 2008. · Zbl 1231.68243 |
| [24] | Pavel Pudlák. Twelve problems in proof complexity. In CSR, pages 13-27, 2008. · Zbl 1142.03369 |
| [25] | Pavel Pudlák. A lower bound on the size of resolution proofs of the ramsey theorem. Inf. Process. Lett., 112(14-15):610-611, 2012. · Zbl 1243.68187 |
| [26] | Ran Raz. Resolution lower bounds for the weak pigeonhole principle. J. ACM, 51(2):115-138, 2004. · Zbl 1317.03036 |
| [27] | Alexander A. Razborov. Resolution lower bounds for perfect matching principles. J. Comput. Syst. Sci., 69(1):3-27, 2004. · Zbl 1106.03049 |
| [28] | Alexander A. Razborov, Avi Wigderson, and Andrew Chi-Chih Yao. Read-once branching programs, rectangular proofs of the pigeonhole principle and the transversal calculus. Combinatorica, 22(4):555-574, 2002. · Zbl 1027.03043 |
| [29] | Nathan Segerlind. The complexity of propositional proofs. Bulletin of Symbolic Logic, 13(4):417-481, 2007. · Zbl 1133.03037 |
| [30] | G. S. Tseitin. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, 2:115-125, 1968. · Zbl 0197.00102 |
| [31] | Alasdair Urquhart. Hard examples for resolution. J. ACM, 34(1):209-219, 1987. · Zbl 0639.68093 |
| [32] | Alasdair Urquhart. The complexity of propositional proofs. Bulletin of Symbolic Logic, 1(4):425-467, 1995. · Zbl 0845.03025 |
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.
