Total space in resolution. (English) Zbl 1402.03080
Summary: We show quadratic lower bounds on the total space used in resolution refutations of random \(k\)-CNFs over \(n\) variables and of the graph pigeonhole principle and the bit pigeonhole principle for \(n\) holes. This answers the open problem of whether there are families of \(k\)-CNF formulas of polynomial size that require quadratic total space in resolution. The results follow from a more general theorem showing that, for formulas satisfying certain conditions, in every resolution refutation there is a memory configuration containing many clauses of large width.
MSC:
| 03F20 | Complexity of proofs |
References:
| [1] | M. Alekhnovich, E. Ben-Sasson, A. A. Razborov, and A. Wigderson, {\it Space complexity in propositional calculus}, SIAM J. Comput., 31 (2002), pp. 1184-1211, . · Zbl 1004.03047 |
| [2] | A. Atserias and V. Dalmau, {\it A combinatorial characterization of resolution width}, J. Comput. System Sci., 74 (2008), pp. 323-334, . · Zbl 1133.03034 |
| [3] | E. Ben-Sasson, {\it Expansion in Proof Complexity}, Ph.D. thesis, Hebrew University, Jerusalem, 2001. |
| [4] | E. Ben-Sasson and N. Galesi, {\it Space complexity of random formulae in resolution}, Random Struct. Algorithms, 23 (2003), pp. 92-109, . · Zbl 1048.03046 |
| [5] | E. Ben-Sasson and J. Nordström, {\it Understanding space in resolution: Optimal lower bounds and exponential trade-offs}, in Computational Complexity of Discrete Problems, P. B. Miltersen, R. Reischuk, G. Schnitger, and D. van Melkebeek, eds., Dagstuhl Seminar Proceedings, 08381, Schloss Dagstuhl, Leibniz-Zentrum für Informatik, Germany, 2008, . |
| [6] | E. Ben-Sasson and J. Nordström, {\it A space hierarchy for \(k\)-DNF resolution}, Electronic Colloquium on Computational Complexity, 16 (2009), p. 47, . |
| [7] | E. Ben-Sasson and J. Nordström, {\it Understanding space in proof complexity: Separations and trade-offs via substitutions}, in Proceedings of Innovations in Computer Science, ICS 2010, Tsinghua University, Beijing, China, B. Chazelle, ed., Tsinghua University Press, 2011, pp. 401-416, . |
| [8] | E. Ben-Sasson and A. Wigderson, {\it Short proofs are narrow–resolution made simple}, J. ACM, 48 (2001), pp. 149-169, . · Zbl 1089.03507 |
| [9] | P. Bennett, I. Bonacina, N. Galesi, T. Huynh, M. Molloy, and P. Wollan, {\it Space proof complexity for random 3-CNFs}, CoRR abs/1503.01613, 2015, . · Zbl 1423.03242 |
| [10] | O. Beyersdorff and O. Kullmann, {\it Unified characterisations of resolution hardness measures}, in Theory and Applications of Satisfiability Testing, C. Sinz and U. Egly, eds., Lecture Notes in Comput. Sci. 8561, Springer, New York, 2014, pp. 170-187, . · Zbl 1423.68409 |
| [11] | I. Bonacina, {\it Space in Weak Propositional Proof Systems}, Ph.D. thesis, Sapienza University of Rome, Italy, 2015. |
| [12] | I. Bonacina, {\it Total space in resolution is at least width squared}, in 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016), LIPIcs. Leibniz Int. Proc. Inform 55, I. Chatzigiannakis, M. Mitzenmacher, Y. Rabani, and D. Sangiorgi, eds., Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 2016, pp. 56:1-56:13. · Zbl 1387.03066 |
| [13] | I. Bonacina and N. Galesi, {\it A framework for space complexity in algebraic proof systems}, J. ACM, 62 (2015), pp. 23:1-23:20, . · Zbl 1333.03238 |
| [14] | I. Bonacina, N. Galesi, and N. Thapen, {\it Total space in resolution}, in Proceedings of the 55th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2014, Philadelphia, PA, IEEE Computer Society, 2014, pp. 641-650, . · Zbl 1402.03080 |
| [15] | H. K. Büning and T. Lettmann, {\it Propositional Logic–Deduction and Algorithms}, Cambridge University Press, Cambridge, UK, 1999. · Zbl 0957.03001 |
| [16] | S. A. Cook and R. A. Reckhow, {\it The relative efficiency of propositional proof systems}, J. Symbolic Logic, 44 (1979), pp. 36-50, . · Zbl 0408.03044 |
| [17] | J. L. Esteban, N. Galesi, and J. Messner, {\it On the complexity of resolution with bounded conjunctions}, Theoret. Comput. Sci., 321 (2004), pp. 347-370, . · Zbl 1056.03036 |
| [18] | J. L. Esteban and J. Torán, {\it Space bounds for resolution}, Inform. and Comput., 171 (2001), pp. 84-97, . · Zbl 1005.03009 |
| [19] | Y. Filmus, M. Lauria, M. Mikša, J. Nordström, and M. Vinyals, {\it Towards an understanding of polynomial calculus: New separations and lower bounds}, in Proceedings of Automata, Languages, and Programming — 40th International Colloquium, ICALP 2013, Riga, Latvia, Part I, F. V. Fomin, R. Freivalds, M. Z. Kwiatkowska, and D. Peleg, eds., Lecture Notes in Comput. Sci. 7965, Springer, New York, 2013, pp. 437-448, . · Zbl 1336.03065 |
| [20] | Y. Filmus, M. Lauria, J. Nordström, N. Ron-Zewi, and N. Thapen, {\it Space complexity in polynomial calculus}, SIAM J. Comput., 44 (2015), pp. 1119-1153, . · Zbl 1372.03099 |
| [21] | J. Nordström, {\it Narrow proofs may be spacious: Separating space and width in resolution}, SIAM J. Comput., 39 (2009), pp. 59-121, . · Zbl 1192.03042 |
| [22] | J. Nordström, {\it Pebble games, proof complexity, and time-space trade-offs}, Log. Methods Comput. Sci., 9 (2013), . · Zbl 1285.03070 |
| [23] | J. Nordström, {\it On the interplay between proof complexity and SAT solving}, ACM SIGLOG News, 2 (2015), pp. 19-44. |
| [24] | J. Nordström and J. H\aastad, {\it Towards an optimal separation of space and length in resolution}, Theory Comput., 9 (2013), pp. 471-557, . · Zbl 1366.68098 |
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.
