Albert Atserias
Jakob Nordström
Skip Abstract Section
Abstract
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 size nO(w) is essentially tight. Moreover, our lower bound generalizes to polynomial calculus resolution and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. The lower bound does not extend all the way to Lasserre, however, since we show that there the formulas we study have proofs of constant rank and size polynomial in both n and w.
- Michael Alekhnovich. 2004. Mutilated chessboard problem is exponentially hard for resolution. Theor. Comput. Sci. 310, 1--3 (Jan. 2004), 513--525. Google Scholar
Digital Library
- 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 ScholarDigital Library
- Michael Alekhnovich and Alexander A. Razborov. 2003. Lower bounds for polynomial calculus: Non-binomial case. Proc. Steklov Institute of Mathematics 242 (2003), 18--35. Available at http://people.cs.uchicago.edu/razborov/files/misha.pdf. Preliminary version appeared in FOCS’01. Google ScholarDigital 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, Johannes Klaus Fichte, and Marc Thurley. 2011. Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res. 40 (Jan. 2011), 353--373. Preliminary version appeared in SAT’09. 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
- Albert Atserias, Moritz Müller, and Sergi Oliva. 2013. Lower bounds for DNF-refutations of a relativized weak pigeonhole principle. In Proceedings of the 28th Annual IEEE Conference on Computational Complexity (CCC’13). 109--120.Google ScholarCross Ref
- Boaz Barak, Fernando G. S. L. Brandão, Aram Wettroth Harrow, Jonathan A. Kelner, David Steurer, and Yuan Zhou. 2012. Hypercontractivity, sum-of-squares proofs, and their applications. In Proceedings of the 44th Annual ACM Symposium on Theory of Computing (STOC’12). 307--326. Google ScholarDigital Library
- Roberto J. Bayardo Jr. and Robert Schrag. 1997. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of the 14th National Conference on Artificial Intelligence (AAAI’97). 203--208. Google ScholarDigital Library
- Paul Beame and Toniann Pitassi. 1998. Propositional proof complexity: Past, present, and future. Bulletin of the European Association for Theoretical Computer Science. 65 (1998), 66--89.Google Scholar
- 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
- Paul Beame, Toniann Pitassi, and Nathan Segerlind. 2007. Lower bounds for Lovász--Schrijver systems and beyond follow from multiparty communication complexity. SIAM J. Comput. 37, 3 (2007), 845--869. Preliminary version appeared in ICALP’05. 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 Struct. Algor. 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.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
- Christoph Berkholz. 2012. On the complexity of finding narrow proofs. In Proc. 53rd Annual IEEE Symposium on Foundations of Computer Science (FOCS’12). IEEE, Washington, DC, 351--360. Google ScholarDigital Library
- Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. 2013. Parameterized complexity of DPLL search procedures. ACM Trans. Comput. Logic 14, 3 (Aug. 2013), 20. Preliminary version appeared in SAT’11. Google ScholarDigital Library
- Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, and Alexander A. Razborov. 2012. Parameterized bounded-depth Frege is not optimal. ACM Trans. Comput. Theor. 4 (Sept. 2012), 7:1--7:16. Issue 3. Preliminary version appeared in ICALP’11. Google ScholarDigital Library
- Archie Blake. 1937. Canonical Expressions in Boolean Algebra. Ph.D. Dissertation. University of Chicago.Google Scholar
- Ilario Bonacina and Nicola Galesi. 2015. A framework for space complexity in algebraic proof systems. J. ACM 62, 3, Article 23 (June 2015), 23:1--23:20 pages. Preliminary version in ITCS’13. Google ScholarDigital Library
- Ilario Bonacina, Nicola Galesi, Tony Huynh, and Paul Wollan. 2014b. Space Proof Complexity for Random 3-CNFs via a (2 − ε)-Hall’s Theorem. Technical Report TR14-146. Electronic Colloquium on Computational Complexity (ECCC).Google Scholar
- Ilario Bonacina, Nicola Galesi, and Neil Thapen. 2014a. Total space in resolution. In Proceedings of the 55th Annual IEEE Symposium on Foundations of Computer Science (FOCS’14). 641--650. Google ScholarDigital Library
- Maria Luisa Bonet and Nicola Galesi. 2001. Optimality of size-width tradeoffs for resolution. Computational Complexity 10, 4 (Dec. 2001), 261--276. Preliminary version appeared in FOCS’99. Google ScholarDigital Library
- Michael Brickenstein and Alexander Dreyer. 2009. PolyBoRi: A framework for Gröbner-basis computations with Boolean polynomials. J. Symbol. Comput. 44, 9 (Sept. 2009), 1326--1345. Google ScholarDigital Library
- Michael Brickenstein, Alexander Dreyer, Gert-Martin Greuel, Markus Wedler, and Oliver Wienand. 2009. New developments in the theory of Gröbner bases and applications to formal verification. J. Pure Appl. Algebr. 213, 8 (Aug. 2009), 1612--1635.Google ScholarCross Ref
- Eden Chlamtáč and Madhur Tulsiani. 2012. Convex relaxations and integrality gaps. In Handbook on Semidefinite, Conic and Polynomial Optimization, Miguel F. Anjos and Jean B. Lasserre (Eds.). Springer, Berlin, 139--169.Google Scholar
- Vašek Chvátal. 1973. Edmond polytopes and a hierarchy of combinatorial problems. Discr. Math. 4, 1 (1973), 305--337. 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). ACM, New York, NY, 174--183. Google ScholarDigital Library
- Stephen A. Cook and Robert Reckhow. 1979. The relative efficiency of propositional proof systems. J. Symbol. Logic 44, 1 (March 1979), 36--50.Google ScholarCross Ref
- William Cook, Collette Rene Coullard, and Gyorgy Turán. 1987. On the complexity of cutting-plane proofs. Discr. Appl. Math. 18, 1 (Nov. 1987), 25--38. Google ScholarDigital Library
- Stefan S. Dantchev and Barnaby Martin. 2014. Relativization makes contradictions harder for resolution. Ann. Pure. Appl. Logic 165, 3 (March 2014), 837--857.Google ScholarCross Ref
- Stefan S. Dantchev, Barnaby Martin, and Martin Rhodes. 2009. Tight rank lower bounds for the Sherali-Adams proof system. Theor. Comput. Sci. 410, 21--23 (May 2009), 2054--2063. Google ScholarDigital Library
- Stefan S. Dantchev and Søren Riis. 2001. “Planar” tautologies hard for resolution. In Proceedings of the 42nd Annual IEEE Symposium on Foundations of Computer Science (FOCS’01). IEEE, Washington, DC, 220--229. Google ScholarDigital Library
- Juan Luis Esteban and Jacobo Torán. 2001. Space bounds for resolution. Inform. Comput. 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, Berlin, 437--448. Google ScholarDigital Library
- Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga Ron-Zewi, and Neil Thapen. 2015. Space complexity in polynomial calculus. SIAM J. Comput. 44, 4 (Aug. 2015), 1119--1153. Preliminary version in CCC’12.Google ScholarCross Ref
- Merrick Furst, James B. Saxe, and Michael Sipser. 1984. Parity, circuits, and the polynomial-time hierarchy. Math. Syst. Theor. 17, 1 (1984), 13--27.Google ScholarCross Ref
- Zvi Galil. 1977. On resolution with clauses of bounded size. SIAM J. Comput. 6, 3 (1977), 444--459.Google ScholarDigital Library
- Ralph E. Gomory. 1963. An algorithm for integer solutions of linear programs. In Recent Advances in Mathematical Programming, R. L. Graves and P. Wolfe (Eds.). McGraw-Hill, New York, NY, 269--302.Google Scholar
- Dima Grigoriev. 2001. Linear lower bound on degrees of positivstellensatz calculus proofs for the parity. Theor. Comput. Sci. 259, 1--2 (May 2001), 613--622.Google ScholarCross Ref
- Dima Grigoriev, Edward A. Hirsch, and Dmitrii V. Pasechnik. 2002. Complexity of semialgebraic proofs. Moscow Math. J. 2, 4 (2002), 647--679.Google ScholarCross Ref
- Dima Grigoriev and Nicolai Vorobjov. 2001. Complexity of null- and positivstellensatz proofs. Ann. Pure Appl. Logic 113, 1--3 (Dec. 2001), 153--160.Google ScholarCross Ref
- Mika Göös and Toniann Pitassi. 2014. Communication lower bounds via critical block sensitivity. In Proceedings of the 46th Annual ACM Symposium on Theory of Computing (STOC’14). ACM, New York, NY, 847--856. Google ScholarDigital Library
- Armin Haken. 1985. The intractability of resolution. Theor. Comput. Sci. 39, 2--3 (Aug. 1985), 297--308.Google ScholarCross Ref
- Johan Håstad. 1987. Computational Limitations of Small-depth Circuits. Ph.D. Dissertation. Massachussetts Institute of Technology.Google Scholar
- Russell Impagliazzo, Pavel Pudlák, and Jiri Sgall. 1999. Lower bounds for the polynomial calculus and the Gröbner basis algorithm. Comput. Complex. 8, 2 (1999), 127--144. Google ScholarDigital Library
- Jean B. Lasserre. 2001. An explicit exact SDP relaxation for nonlinear 0-1 programs. In Proceedings of the 8th International Conference on Integer Programming and Combinatorial Optimization (Lecture Notes in Computer Science), Vol. 2081. Springer, Berlin, 293--303. Google ScholarDigital Library
- Monique Laurent. 2001. A comparison of the Sherali-Adams, Lovász-Schrijver and Lasserre relaxations for 0-1 programming. Math. Oper. Res. 28 (2001), 470--496. Google ScholarDigital Library
- Massimo Lauria and Jakob Nordström. 2015. Tight size-degree bounds for sums-of-squares proofs. In Proceedings of the 30th Annual Computational Complexity Conference (CCC’15) (Leibniz International Proceedings in Informatics (LIPIcs)), Vol. 33. 448--466. Google ScholarDigital Library
- László Lovász and Alexander Schrijver. 1991. Cones of matrices and set-functions and 0-1 optimization. SIAM J. Optimiz. 1, 2 (1991), 166--190.Google ScholarCross Ref
- João P. Marques-Silva and Karem A. Sakallah. 1999. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Comput. 48, 5 (May 1999), 506--521. Preliminary version appeared in ICCAD’96. Google ScholarDigital Library
- Mladen Mikša and Jakob Nordström. 2015. A generalized method for proving polynomial calculus degree lower bounds. In Proceedings of the 30th Annual Computational Complexity Conference (CCC’15) (Leibniz International Proceedings in Informatics (LIPIcs)), Vol. 33. 467--487. Google ScholarDigital Library
- Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. 2001. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference (DAC’01). 530--535. Google ScholarDigital Library
- Ryan O’Donnell and Yuan Zhou. 2013. Approximability and proof complexity. In Proceedings of the 24th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA’13). 1537--1556. Google ScholarDigital Library
- Pablo A. Parrilo. 2000. Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization. Ph.D. Dissertation. California Institute of Technology.Google Scholar
- Pavel Pudlák. 1999. On the complexity of propositional calculus. In Sets and Proofs, S. Barry Cooper and John K. Truss (Eds.). London Mathematical Society Lecture Note Series, Vol. 258. Cambridge University Press, 197--218.Google Scholar
- Pavel Pudlák. 2000. Proofs as games. Am. Math. Mon. (2000), 541--550.Google Scholar
- Alexander A. Razborov. 1998. Lower bounds for the polynomial calculus. Comput. Complex. 7, 4 (Dec. 1998), 291--324. Google ScholarDigital Library
- Grant Schoenebeck. 2008. Linear level Lasserre lower bounds for certain k-CSPs. In Proceedings of the 49th Annual IEEE Symposium on Foundations of Computer Science (FOCS’08). 593--602. Google ScholarDigital Library
- Hanif D. Sherali and Warren P. Adams. 1990. A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems. SIAM J. Discr. Math. 3 (1990), 411--430. Google ScholarDigital Library
- Neil Thapen. 2014. A Trade-off Between Length and Width in Resolution. Technical Report TR14-137. Electronic Colloquium on Computational Complexity (ECCC).Google Scholar
- Alasdair Urquhart. 1987. Hard examples for resolution. J. ACM 34, 1 (Jan. 1987), 209--219. Google ScholarDigital Library
Index Terms
- Narrow Proofs May Be Maximally Long
Recommendations
From Small Space to Small Width in Resolution
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 ...
A generalized method for proving polynomial calculus degree lower bounds
CCC '15: Proceedings of the 30th Conference on Computational ComplexityWe study the problem of obtaining lower bounds for polynomial calculus (PC) and polynomial calculus resolution (PCR) on proof degree, and hence by [Impagliazzo et al. '99] also on proof size. [Alekhnovich and Razborov '03] established that if the clause-...
Some trade-off results for polynomial calculus: extended abstract
STOC '13: Proceedings of the forty-fifth annual ACM symposium on Theory of ComputingWe present size-space trade-offs for the polynomial calculus (PC) and polynomial calculus resolution (PCR) proof systems. These are the first true size-space trade-offs in any algebraic proof system, showing that size and space cannot be simultaneously ...
Comments