×

zbMATH — the first resource for mathematics

Narrow proofs may be maximally long. (English) Zbl 1367.03104
Summary: 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^{\Omega(w)}\). This shows that the simple counting argument that any formula refutable in width \(w\) must have a proof in size \(n^{O(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\).
Reviewer: Reviewer (Berlin)

MSC:
03F20 Complexity of proofs
Software:
Chaff; PolyBoRi
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Michael Alekhnovich. 2004. Mutilated chessboard problem is exponentially hard for resolution. Theor. Comput. Sci. 310, 1–3 (Jan. 2004), 513–525. · Zbl 1071.68028
[2] 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. · Zbl 1004.03047
[3] 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.
[4] 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. · Zbl 1133.03034
[5] 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. · Zbl 1214.68340
[6] 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. · doi:10.1109/CCC.2014.36
[7] 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. · Zbl 1386.03070 · doi:10.1109/CCC.2013.20
[8] 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. · Zbl 1286.68176 · doi:10.1145/2213977.2214006
[9] 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.
[10] 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. · Zbl 0908.68164
[11] 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. · Zbl 1286.68180 · doi:10.1145/2213977.2213999
[12] 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. · Zbl 1148.68023
[13] 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. · Zbl 1293.03031 · doi:10.1145/2488608.2488711
[14] Eli Ben-Sasson. 2009. Size space tradeoffs for resolution. SIAM J. Comput. 38, 6 (May 2009), 2511–2525. Preliminary version appeared in STOC’02. · Zbl 1191.68617
[15] 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. · Zbl 1048.03046
[16] 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. · doi:10.1109/FOCS.2008.42
[17] 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.
[18] 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. · Zbl 1089.03507
[19] 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. · doi:10.1109/FOCS.2012.48
[20] 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. · Zbl 1354.68105
[21] 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. · Zbl 1322.68082
[22] Archie Blake. 1937. Canonical Expressions in Boolean Algebra. Ph.D. Dissertation. University of Chicago. · Zbl 0018.38601
[23] 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. · Zbl 1333.03238
[24] 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). · Zbl 1423.03242
[25] 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. · Zbl 1402.03080 · doi:10.1109/FOCS.2014.74
[26] 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. · Zbl 1024.03012
[27] 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. · Zbl 1186.68571 · doi:10.1016/j.jsc.2008.02.017
[28] 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. · Zbl 1164.68019 · doi:10.1016/j.jpaa.2008.11.043
[29] 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. · Zbl 1334.90099 · doi:10.1007/978-1-4614-0769-0_6
[30] Vašek Chvátal. 1973. Edmond polytopes and a hierarchy of combinatorial problems. Discr. Math. 4, 1 (1973), 305–337. · Zbl 0253.05131 · doi:10.1016/0012-365X(73)90167-2
[31] Vašek Chvátal and Endre Szemerédi. 1988. Many hard examples for resolution. J. ACM 35, 4 (Oct. 1988), 759–768. · Zbl 0712.03008 · doi:10.1145/48014.48016
[32] 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. · Zbl 0938.68825 · doi:10.1145/237814.237860
[33] Stephen A. Cook and Robert Reckhow. 1979. The relative efficiency of propositional proof systems. J. Symbol. Logic 44, 1 (March 1979), 36–50. · Zbl 0408.03044 · doi:10.2307/2273702
[34] 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. · Zbl 0625.90056 · doi:10.1016/0166-218X(87)90039-4
[35] Stefan S. Dantchev and Barnaby Martin. 2014. Relativization makes contradictions harder for resolution. Ann. Pure. Appl. Logic 165, 3 (March 2014), 837–857. · Zbl 1277.68093 · doi:10.1016/j.apal.2013.10.009
[36] 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. · Zbl 1168.03043
[37] 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. · doi:10.1109/SFCS.2001.959896
[38] 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.
[39] 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. · Zbl 1336.03065
[40] 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.
[41] Merrick Furst, James B. Saxe, and Michael Sipser. 1984. Parity, circuits, and the polynomial-time hierarchy. Math. Syst. Theor. 17, 1 (1984), 13–27. · Zbl 0534.94008 · doi:10.1007/BF01744431
[42] Zvi Galil. 1977. On resolution with clauses of bounded size. SIAM J. Comput. 6, 3 (1977), 444–459. · Zbl 0368.68085 · doi:10.1137/0206031
[43] 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. · Zbl 0235.90038
[44] 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. · Zbl 0974.68192
[45] Dima Grigoriev, Edward A. Hirsch, and Dmitrii V. Pasechnik. 2002. Complexity of semialgebraic proofs. Moscow Math. J. 2, 4 (2002), 647–679. · Zbl 1027.03044
[46] Dima Grigoriev and Nicolai Vorobjov. 2001. Complexity of null- and positivstellensatz proofs. Ann. Pure Appl. Logic 113, 1–3 (Dec. 2001), 153–160. · Zbl 0992.03073
[47] 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. · Zbl 1315.68153 · doi:10.1145/2591796.2591838
[48] Armin Haken. 1985. The intractability of resolution. Theor. Comput. Sci. 39, 2–3 (Aug. 1985), 297–308. · Zbl 0586.03010
[49] Johan Håstad. 1987. Computational Limitations of Small-depth Circuits. Ph.D. Dissertation. Massachussetts Institute of Technology.
[50] 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. · Zbl 0946.68129 · doi:10.1007/s000370050024
[51] 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. · Zbl 1010.90515
[52] 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. · Zbl 1082.90084 · doi:10.1287/moor.28.3.470.16391
[53] 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. · Zbl 1422.03126
[54] 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. · Zbl 0754.90039 · doi:10.1137/0801013
[55] 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. · Zbl 1392.68388
[56] 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. · Zbl 1434.03134
[57] 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. · doi:10.1145/378239.379017
[58] 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. · doi:10.1137/1.9781611973105.111
[59] Pablo A. Parrilo. 2000. Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization. Ph.D. Dissertation. California Institute of Technology.
[60] 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. · Zbl 0939.03065 · doi:10.1017/CBO9781107325944.010
[61] Pavel Pudlák. 2000. Proofs as games. Am. Math. Mon. (2000), 541–550. · Zbl 0983.03045 · doi:10.2307/2589349
[62] Alexander A. Razborov. 1998. Lower bounds for the polynomial calculus. Comput. Complex. 7, 4 (Dec. 1998), 291–324. · Zbl 1026.03043 · doi:10.1007/s000370050013
[63] 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. · doi:10.1109/FOCS.2008.74
[64] 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. · Zbl 0712.90050 · doi:10.1137/0403036
[65] Neil Thapen. 2014. A Trade-off Between Length and Width in Resolution. Technical Report TR14-137. Electronic Colloquium on Computational Complexity (ECCC). · Zbl 1355.03047
[66] Alasdair Urquhart. 1987. Hard examples for resolution. J. ACM 34, 1 (Jan. 1987), 209–219. · Zbl 0639.68093 · doi:10.1145/7531.8928
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.