Yuval Filmus
Jakob Nordström
Abstract
In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of a Conjunctive Normal Form (CNF) formula is always an upper bound on the width needed to refute the formula. Their proof is beautiful but uses a nonconstructive argument based on Ehrenfeucht-Fraïssé games. We give an alternative, more explicit, proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a “black-box” technique for proving space lower bounds via a “static” complexity measure that works against any resolution refutation—previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similar methods.
- Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. 2002. Space complexity in propositional calculus. SIAM J. Comput. 31, 4 (2002), 1184--1211. Preliminary version appeared in STOC’00. Google Scholar
Digital Library
- Albert Atserias and Víctor Dalmau. 2008. A combinatorial characterization of resolution width. J. Comput. System Sci. 74, 3 (May 2008), 323--334. Preliminary version appeared in CCC’03. Google ScholarDigital Library
- Albert Atserias, Massimo Lauria, and Jakob Nordström. 2014. Narrow proofs may be maximally long. In Proceedings of the 29th Annual IEEE Conference on Computational Complexity (CCC’14). 286--297. Google ScholarDigital Library
- Paul Beame, Chris Beck, and Russell Impagliazzo. 2012. Time-space tradeoffs in resolution: Superpolynomial lower bounds for superlinear space. In Proceedings of the 44th Annual ACM Symposium on Theory of Computing (STOC’12). 213--232. Google ScholarDigital Library
- Chris Beck, Jakob Nordström, and Bangsheng Tang. 2013. Some trade-off results for polynomial calculus. In Proceedings of the 45th Annual ACM Symposium on Theory of Computing (STOC’13). 813--822. Google ScholarDigital Library
- Eli Ben-Sasson. 2009. Size space tradeoffs for resolution. SIAM J. Comput. 38, 6 (May 2009), 2511--2525. Preliminary version appeared in STOC’02. Google ScholarDigital Library
- Eli Ben-Sasson and Nicola Galesi. 2003. Space complexity of random formulae in resolution. Random Structures and Algorithms 23, 1 (Aug. 2003), 92--109. Preliminary version appeared in CCC’01. Google ScholarDigital Library
- Eli Ben-Sasson and Jakob Nordström. 2008. Short proofs may be spacious: An optimal separation of space and length in resolution. In Proceedings of the 49th Annual IEEE Symposium on Foundations of Computer Science (FOCS’08). 709--718. Google ScholarDigital Library
- Eli Ben-Sasson and Jakob Nordström. 2011. Understanding space in proof complexity: Separations and trade-offs via substitutions. In Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS’11). 401--416. Full-length version available at http://eccc.hpi-web.de/report/2010/125/.Google Scholar
- Eli Ben-Sasson and Avi Wigderson. 2001. Short proofs are narrow-Resolution made simple. J. ACM 48, 2 (March 2001), 149--169. Preliminary version appeared in STOC’99. Google ScholarDigital Library
- Ilario Bonacina and Nicola Galesi. 2013. Pseudo-partitions, transversality and locality: A combinatorial characterization for the space measure in algebraic proof systems. In Proceedings of the 4th Conference on Innovations in Theoretical Computer Science (ITCS’13). 455--472. Google ScholarDigital Library
- Vašek Chvátal and Endre Szemerédi. 1988. Many hard examples for resolution. J. ACM 35, 4 (Oct. 1988), 759--768. Google ScholarDigital Library
- Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. 1996. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the 28th Annual ACM Symposium on Theory of Computing (STOC’96). 174--183. Google ScholarDigital Library
- Juan Luis Esteban and Jacobo Torán. 2001. Space bounds for resolution. Information and Computation 171, 1 (2001), 84--97. Preliminary versions of these results appeared in STACS’99 and CSL’99. Google ScholarDigital Library
- Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals. 2013. Towards an understanding of polynomial calculus: New separations and lower bounds (extended abstract). In Proceedings of the 40th International Colloquium on Automata, Languages and Programming (ICALP’13) Lecture Notes in Computer Science, Vol. 7965. Springer, 437--448. Google ScholarDigital Library
- Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals. 2014. From small space to small width in resolution. In Proceedings of the 31st Symposium on Theoretical Aspects of Computer Science (STACS’14). Leibniz International Proceedings in Informatics, Vol. 25. 300--311.Google Scholar
- Armin Haken. 1985. The intractability of resolution. Theoretical Computer Science 39, 2-3 (Aug. 1985), 297--308.Google ScholarCross Ref
- Jan Krajíček. 2001. On the weak pigeonhole principle. Fundamenta Mathematicae 170, 1-3 (2001), 123--140.Google ScholarCross Ref
- Jakob Nordström. 2009. A simplified way of proving trade-off results for resolution. Inform. Process. Lett. 109, 18 (Aug. 2009), 1030--1035. Preliminary version appeared in ECCC report TR07-114, 2007.Google ScholarDigital Library
- Jakob Nordström. 2013. Pebble games, proof complexity and time-space trade-offs. Log. Meth. Comput. Sci. 9, 3, Article 15 (Sept. 2013), 15:1--15:63.Google Scholar
- Alexander Razborov. 2014. Personal communication.Google Scholar
- Alasdair Urquhart. 1987. Hard examples for resolution. J. ACM 34, 1 (Jan. 1987), 209--219. Google ScholarDigital Library
Index Terms
- From Small Space to Small Width in Resolution
Recommendations
Narrow Proofs May Be Maximally Long
We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size nΩ(w). This shows that the simple counting argument that any formula refutable in width w must have a proof in ...
Space Complexity in Polynomial Calculus
During the last 10 to 15 years, an active line of research in proof complexity has been to study space complexity and time-space trade-offs for proofs. Besides being a natural complexity measure of intrinsic interest, space is also an important concern in ...
Space Complexity in Polynomial Calculus
CCC '12: Proceedings of the 2012 IEEE Conference on Computational Complexity (CCC)During the last decade, an active line of research in proof complexity has been to study space complexity and time-space trade-offs for proofs. Besides being a natural complexity measure of intrinsic interest, space is also an important issue in SAT ...
Comments