Proof Complexity Lower Bounds from Algebraic Circuit Complexity

by Michael A. Forbes, Amir Shpilka, Iddo Tzameret, and Avi Wigderson

Theory of Computing, Volume 17(10), pp. 1-88, 2021

Bibliography with links to cited articles

[1]   Manindra Agrawal: Proving lower bounds via pseudo-random generators. In Proc. 25th Found. Softw. Techn. Theoret. Comp. Sci. Conf. (FSTTCS’05), pp. 92–105. Springer, 2005. [doi:10.1007/11590156_6]

[2]   Manindra Agrawal, Rohit Gurjar, Arpita Korwar, and Nitin Saxena: Hitting-sets for ROABP and sum of set-multilinear circuits. SIAM J. Comput., 44(3):669–697, 2015. [doi:10.1137/140975103, arXiv:1406.7535, ECCC:TR14-085]

[3]   Manindra Agrawal, Chandan Saha, and Nitin Saxena: Quasi-polynomial hitting-set for set-depth-Δ formulas. In Proc. 45th STOC, pp. 321–330. ACM Press, 2013. [doi:10.1145/2488608.2488649, arXiv:1209.2333]

[4]   Michael Alekhnovich and Alexander A. Razborov: Lower bounds for polynomial calculus: Non-binomial case. Trudy Mat. Inst. Steklova, 242:23–43, 2003 (Russian). MathNet.Ru. Preliminary version in FOCS’01.

[5]    Yaroslav Alekseev, Dima Grigoriev, Edward A. Hirsch, and Iddo Tzameret: Semi-algebraic proofs, IPS lower bounds, and the τ  -conjecture: Can a natural number be negative? In Proc. 52nd STOC, pp. 54–67. ACM Press, 2020. [doi:10.1145/3357713.3384245, arXiv:1911.06738, ECCC:TR19-142]

[6]   Matthew Anderson, Michael A. Forbes, Ramprasad Saptharishi, Amir Shpilka, and Ben Lee Volk: Identity testing and lower bounds for read-k oblivious algebraic branching programs. ACM Trans. Comput. Theory, 10(1):1–30, 2018. Preliminary version in CCC’16. [doi:10.1145/3170709, arXiv:1511.07136, ECCC:TR15-184]

[7]   Matthew Anderson, Dieter van Melkebeek, and Ilya Volkovich: Derandomizing polynomial identity testing for multilinear constant-read formulae. In Proc. 26th IEEE Conf. on Comput. Complexity (CCC’11), pp. 273–282. IEEE Comp. Soc., 2011. [doi:10.1109/CCC.2011.18, ECCC:TR10-188]

[8]   Vikraman Arvind, Pushkar S. Joglekar, Partha Mukhopadhyay, and S. Raja: Randomized polynomial-time identity testing for noncommutative circuits. Theory of Computing, 15(7):1–36, 2019. Preliminary version in STOC’17. [doi:10.4086/toc.2019.v015a007, arXiv:1606.00596, ECCC:TR16-089]

[9]   Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák: Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. Proc. London Math. Soc., s3-73(1):1–26, 1996. Preliminary version in FOCS’94. [doi:10.1112/plms/s3-73.1.1]

[10]   Paul Beame and Toniann Pitassi: Propositional proof complexity: Past, present and future. Bull. EATCS, 65:66–89, 1998. [ECCC:TR98-067]

[11]   Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi: Linear gaps between degrees for the polynomial calculus modulo distinct primes. J. Comput. System Sci., 62(2):267–289, 2001. Preliminary versions in CCC’99 and STOC’99. [doi:10.1006/jcss.2000.1726]

[12]   Samuel R. Buss, Russell Impagliazzo, Jan Krajíček, Pavel Pudlák, Alexander A. Razborov, and Jiří Sgall: Proof complexity in algebraic systems and bounded depth Frege systems with modular counting. Comput. Complexity, 6(3):256–298, 1996. [doi:10.1007/BF01294258]

[13]   Matthew Clegg, Jeff Edmonds, and Russell Impagliazzo: Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proc. 28th STOC, pp. 174–183. ACM Press, 1996. [doi:10.1145/237814.237860]

[14]   Stephen A. Cook and Robert A. Reckhow: Corrections for “On the lengths of proofs in the propositional calculus (Preliminary version)”. SIGACT News, 6(3):15–22, 1974. Preliminary version in STOC’74. [doi:10.1145/1008311.1008313]

[15]   Stephen A. Cook and Robert A. Reckhow: The relative efficiency of propositional proof systems. J. Symbolic Logic, 44(1):36–50, 1979. [doi:10.2307/2273702]

[16]   David Cox, John Little, and Donal O’Shea: Ideals, Varieties, and Algorithms. Springer, 3rd edition, 2007. [doi:10.1007/978-3-319-16721-3]

[17]   Richard A. DeMillo and Richard J. Lipton: A probabilistic remark on algebraic program testing. Inform. Process. Lett., 7(4):193–195, 1978. [doi:10.1016/0020-0190(78)90067-4]

[18]   Zeev Dvir, Amir Shpilka, and Amir Yehudayoff: Hardness-randomness tradeoffs for bounded depth arithmetic circuits. SIAM J. Comput., 39(4):1279–1293, 2010. Preliminary version in STOC’08. [doi:10.1137/080735850]

[19]   Ismor Fischer: Sums of like powers of multivariate linear forms. Math. Magazine, 67(1):59–61, 1994. [doi:10.1080/0025570X.1994.11996185]

[20]   Michael A. Forbes: Polynomial Identity Testing of Read-Once Oblivious Algebraic Branching Programs. Ph. D. thesis, MIT, 2014. LINK at

[21]   Michael A. Forbes: Deterministic divisibility testing via shifted partial derivatives. In Proc. 56th FOCS, pp. 451–465. IEEE Comp. Soc., 2015. [doi:10.1109/FOCS.2015.35]

[22]   Michael A. Forbes, Ankit Gupta, and Amir Shpilka: Personal Communication to Gupta, Kamath, Kayal, Saptharishi [37], 2013.

[23]   Michael A. Forbes, Mrinal Kumar, and Ramprasad Saptharishi: Functional lower bounds for arithmetic circuits and connections to boolean circuit complexity. In Proc. 31st Comput. Complexity Conf. (CCC’16), pp. 33:1–19. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2016. [doi:10.4230/LIPIcs.CCC.2016.33, arXiv:1605.04207]

[24]   Michael A. Forbes, Ramprasad Saptharishi, and Amir Shpilka: Hitting sets for multilinear read-once algebraic branching programs, in any order. In Proc. 46th STOC, pp. 867–875. ACM Press, 2014. [doi:10.1145/2591796.2591816, arXiv:1309.5668]

[25]   Michael A. Forbes and Amir Shpilka: On identity testing of tensors, low-rank recovery and compressed sensing. In Proc. 44th STOC, pp. 163–172. ACM Press, 2012. [doi:10.1145/2213977.2213995, arXiv:1111.0663, ECCC:TR11-147]

[26]   Michael A. Forbes and Amir Shpilka: Explicit Noether Normalization for simultaneous conjugation via polynomial identity testing. In Proc. 17th Internat. Workshop on Randomization and Computation (RANDOM’13), pp. 527–542. Springer, 2013. [doi:10.1007/978-3-642-40328-6_37, arXiv:1303.0084, ECCC:TR13-033]

[27]   Michael A. Forbes and Amir Shpilka: Quasipolynomial-time identity testing of non-commutative and read-once oblivious algebraic branching programs. In Proc. 54th FOCS, pp. 243–252. IEEE Comp. Soc., 2013. [doi:10.1109/FOCS.2013.34, arXiv:1209.2408, ECCC:TR12-115]

[28]   Michael A. Forbes and Amir Shpilka: Complexity theory column 88: Challenges in polynomial factorization. SIGACT News, 46(4):32–49, 2015. [doi:10.1145/2852040.2852051]

[29]   Michael A. Forbes, Amir Shpilka, Iddo Tzameret, and Avi Wigderson: Proof complexity lower bounds from algebraic circuit complexity. In Proc. 31st Comput. Complexity Conf. (CCC’16), pp. 32:1–17. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2016. [doi:10.4230/LIPIcs.CCC.2016.32, arXiv:1606.05050, ECCC:TR16-098]

[30]   Joachim von zur Gathen and Erich L. Kaltofen: Factoring sparse multivariate polynomials. J. Comput. System Sci., 31(2):265–287, 1985. Preliminary version in FOCS’83. [doi:10.1016/0022-0000(85)90044-3]

[31]   Dima Grigoriev: Tseitin’s tautologies and lower bounds for Nullstellensatz proofs. In Proc. 39th FOCS, pp. 648–652. IEEE Comp. Soc., 1998. [doi:10.1109/SFCS.1998.743515]

[32]   Dima Grigoriev and Edward A. Hirsch: Algebraic proof systems over formulas. Theoret. Comput. Sci., 303(1):83–102, 2003. [doi:10.1016/S0304-3975(02)00446-2, ECCC:TR01-011]

[33]   Dima Grigoriev and Marek Karpinski: An exponential lower bound for depth 3 arithmetic circuits. In Proc. 30th STOC, pp. 577–582. ACM Press, 1998. [doi:10.1145/276698.276872]

[34]   Dima Grigoriev and Alexander A. Razborov: Exponential lower bounds for depth 3 arithmetic circuits in algebras of functions over finite fields. Applicable Algebra Eng. Commun. Comput., 10(6):465–487, 2000. Preliminary version in FOCS’98. [doi:10.1007/s002009900021]

[35]   Joshua A. Grochow and Toniann Pitassi: Circuit complexity, proof complexity, and polynomial identity testing: The ideal proof system. J. ACM, 65(6):37:1–59, 2018. [doi:10.1145/3230742]

[36]   Ankit Gupta, Pritish Kamath, Neeraj Kayal, and Ramprasad Saptharishi: Approaching the chasm at depth four. J. ACM, 61(6):33:1–16, 2014. Preliminary version in CCC’13. [doi:10.1145/2629541]

[37]   Ankit Gupta, Pritish Kamath, Neeraj Kayal, and Ramprasad Saptharishi: Arithmetic circuits: A chasm at depth three. SIAM J. Comput., 45(3):1064–1079, 2016. Preliminary version in FOCS’13. [doi:10.1137/140957123, ECCC:TR13-026]

[38]   Rohit Gurjar, Arpita Korwar, Nitin Saxena, and Thomas Thierauf: Deterministic identity testing for sum of read-once oblivious arithmetic branching programs. Comput. Complexity, 26(4):1–46, 2016. Preliminary version in CCC’15. [doi:10.1007/s00037-016-0141-z, arXiv:1411.7341]

[39]   Joos Heintz and Claus-Peter Schnorr: Testing polynomials which are easy to compute (extended abstract). In Proc. 12th STOC, pp. 262–272. ACM Press, 1980. [doi:10.1145/800141.804674]

[40]   Pavel Hrubeš and Iddo Tzameret: Short proofs for the determinant identities. SIAM J. Comput., 44(2):340–383, 2015. Preliminary version in STOC’12. [doi:10.1137/130917788, arXiv:1112.6265, ECCC:TR11-174]

[41]   Russell Impagliazzo, Pavel Pudlák, and Jiří Sgall: Lower bounds for the polynomial calculus and the Gröbner basis algorithm. Comput. Complexity, 8(2):127–144, 1999. [doi:10.1007/s000370050024, ECCC:TR97-042]

[42]   Russell Impagliazzo and Avi Wigderson: P=BPP if E requires exponential circuits: Derandomizing the XOR lemma. In Proc. 29th STOC, pp. 220–229. ACM Press, 1997. [doi:10.1145/258533.258590]

[43]   Valentine Kabanets and Russell Impagliazzo: Derandomizing polynomial identity tests means proving circuit lower bounds. Comput. Complexity, 13(1–2):1–46, 2004. Preliminary version in STOC’03. [doi:10.1007/s00037-004-0182-6]

[44]   Erich L. Kaltofen: Factorization of polynomials given by straight-line programs. In Silvio Micali, editor, Randomness and Computation, volume 5 of Adv. Comput. Res., pp. 375–412. JAI Press, Inc., 1989. LINK at author’s website.

[45]   Neeraj Kayal: Personal Communication to Saxena [71], 2008.

[46]   Neeraj Kayal: An exponential lower bound for the sum of powers of bounded degree polynomials. Electron. Colloq. Comput. Complexity, TR12-081(81), 2012. [ECCC]

[47]   Adam Klivans and Daniel A. Spielman: Randomness efficient identity testing of multivariate polynomials. In Proc. 33rd STOC, pp. 216–223. ACM Press, 2001. [doi:10.1145/380752.380801]

[48]   Jan Krajíček: Bounded Arithmetic, Propositional Logic, and Complexity Theory. Volume 60 of Encycl. Math. Appl. Cambridge Univ. Press, 1995. [doi:10.1017/CBO9780511529948]

[49]   Mrinal Kumar and Ramprasad Saptharishi: An exponential lower bound for homogeneous depth-5 circuits over finite fields. In Proc. 32nd Comput. Complexity Conf. (CCC’17), pp. 31:1–30. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2017. [doi:10.4230/LIPIcs.CCC.2017.31, arXiv:1507.00177, ECCC:TR15-109]

[50]    Fu Li, Iddo Tzameret, and Zhengyu Wang: Characterizing propositional proofs as noncommutative formulas. SIAM J. Comput., 47(4):1424–1462, 2018. [doi:10.1137/16M1107632, arXiv:1412.8746]

[51]   Meena Mahajan, BV Raghavendra Rao, and Karteek Sreenivasaiah: Building above read-once polynomials: Identity testing and hardness of representation. Algorithmica, 76(4):890–909, 2016. Preliminary version in COCOON’14. [ECCC:TR15-202]

[52]   Noam Nisan: Lower bounds for non-commutative computation. In Proc. 23rd STOC, pp. 410–418. ACM Press, 1991. [doi:10.1145/103418.103462]

[53]   Noam Nisan and Avi Wigderson: Hardness vs randomness. J. Comput. System Sci., 49(2):149–167, 1994. Preliminary version in FOCS’88. [doi:10.1016/S0022-0000(05)80043-1]

[54]   Noam Nisan and Avi Wigderson: Lower bounds on arithmetic circuits via partial derivatives. Comput. Complexity, 6(3):217–234, 1996. Preliminary version in FOCS’95. [doi:10.1007/BF01294256]

[55]   Rafael Oliveira: Personal communication, 2015.

[56]   Rafael Oliveira: Factors of low individual degree polynomials. Comput. Complexity, 25(2):507–561, 2016. Preliminary version in CCC’15.

[57]   Rafael Oliveira, Amir Shpilka, and Ben lee Volk: Subexponential size hitting sets for bounded depth multilinear formulas. Comput. Complexity, 25(2):455–505, 2016. Preliminary version in CCC’15.

[58]   Øystein Ore: Über höhere Kongruenzen. Norsk Mat. Forenings Skrifter Ser. I, 7(15):27, 1922.

[59]   Toniann Pitassi: Algebraic propositional proof systems. In Descriptive Complexity and Finite Models, volume 31 of DIMACS Ser. Discr. Math. and Theoret. Comp. Sci., pp. 215–244. Amer. Math. Soc., 1997. LINK at author’s website. [doi:10.1090/dimacs/031]

[60]   Toniann Pitassi and Iddo Tzameret: Algebraic proof complexity: progress, frontiers and challenges. ACM SIGLOG News, 3(3):21–43, 2016. [doi:10.1145/2984450.2984455]

[61]   Pavel Pudlák: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symbolic Logic, 62(3):981–998, 1997. [doi:10.2307/2275583]

[62]   Ran Raz: Separation of multilinear circuit and formula size. Theory of Computing, 2(6):121–135, 2006. Preliminary version in FOCS’04. [doi:10.4086/toc.2006.v002a006]

[63]   Ran Raz: Multi-linear formulas for permanent and determinant are of super-polynomial size. J. ACM, 56(2):8:1–17, 2009. Preliminary version in STOC’04. [doi:10.1145/1502793.1502797, ECCC:TR03-067]

[64]   Ran Raz and Amir Shpilka: Deterministic polynomial identity testing in non-commutative models. Comput. Complexity, 14(1):1–19, 2005. Preliminary version in CCC’04. [doi:10.1007/s00037-005-0188-8]

[65]   Ran Raz and Iddo Tzameret: Resolution over linear equations and multilinear proofs. Ann. Pure Appl. Logic, 155(3):194–224, 2008. [doi:10.1016/j.apal.2008.04.001, arXiv:0708.1529, ECCC:TR07-078]

[66]   Ran Raz and Iddo Tzameret: The strength of multilinear proofs. Comput. Complexity, 17(3):407–457, 2008. [doi:10.1007/s00037-008-0246-0, ECCC:TR06-001]

[67]   Ran Raz and Amir Yehudayoff: Balancing syntactically multilinear arithmetic circuits. Comput. Complexity, 17(4):515–535, 2008. [doi:10.1007/s00037-008-0254-0]

[68]   Ran Raz and Amir Yehudayoff: Lower bounds and separations for constant depth multilinear circuits. Comput. Complexity, 18(2):171–207, 2009. Preliminary version in CCC’08. [doi:10.1007/s00037-009-0270-8, ECCC:TR08-006]

[69]   Alexander A. Razborov: Lower bounds for the polynomial calculus. Comput. Complexity, 7(4):291–324, 1998. [doi:10.1007/s000370050013]

[70]   Ramprasad Saptharishi: 2012. Personal communication to Forbes–Shpilka [27].

[71]   Nitin Saxena: Diagonal circuit identity testing and lower bounds. In Proc. 35th Internat. Colloq. on Automata, Languages, and Programming (ICALP’08), pp. 60–71. Springer, 2008. [doi:10.1007/978-3-540-70575-8_6, ECCC:TR07-124]

[72]   Nitin Saxena: Progress on polynomial identity testing. Bull. EATCS, 99:49–79, 2009. EATCS. [arXiv:1401.0976, ECCC:TR09-101]

[73]   Nitin Saxena: Progress on polynomial identity testing - II. In M. Agrawal and V. Arvind, editors, Perspectives in Computational Complexity: The Somenath Biswas Anniversary Volume, pp. 131–146. Springer, 2014. [doi:10.1007/978-3-319-05446-9_7, arXiv:1401.0976, ECCC:TR13-186]

[74]   Jacob T. Schwartz: Fast probabilistic algorithms for verification of polynomial identities. J. ACM, 27(4):701–717, 1980. Preliminary version in EUROSAM’79. [doi:10.1145/322217.322225]

[75]   Amir Shpilka: Affine projections of symmetric polynomials. J. Comput. System Sci., 65(4):639–659, 2002. Preliminary version in CCC’01. [doi:10.1016/S0022-0000(02)00021-1, ECCC:TR01-035]

[76]   Amir Shpilka and Ilya Volkovich: Improved polynomial identity testing for read-once formulas. In Proc. 13th Internat. Workshop on Randomization and Computation (RANDOM’09), volume 5687, pp. 700–713. Springer, 2009.

[77]   Amir Shpilka and Avi Wigderson: Depth-3 arithmetic circuits over fields of characteristic zero. Comput. Complexity, 10(1):1–27, 2001. [doi:10.1007/PL00001609]

[78]   Amir Shpilka and Amir Yehudayoff: Arithmetic circuits: A survey of recent results and open questions. Found. Trends Theor. Comp. Sci., 5(3–4):207–388, 2010. [doi:10.1561/0400000039]

[79]   Michael Shub and Steve Smale: On the intractability of Hilbert’s Nullstellensatz and an algebraic version of “NPP?”. Duke Math. J., 81:47–54, 1995. Available in the Collected papers of Stephen Smale, pp. 1508–1515, World Scientific 2000.

[80]   Michael Soltys and Stephen A. Cook: The proof complexity of linear algebra. Ann. Pure Appl. Logic, 130(1–3):277–323, 2004. Preliminary version in LICS’02. [doi:10.1016/j.apal.2003.10.018]

[81]   Volker Strassen: Vermeidung von Divisionen. J. reine angew. Math., 264:184–202, 1973. [doi:10.1515/crll.1973.264.184]

[82]   Madhu Sudan, Luca Trevisan, and Salil P. Vadhan: Pseudorandom generators without the XOR lemma. J. Comput. System Sci., 62(2):236–266, 2001. Preliminary version in STOC’99. [doi:10.1006/jcss.2000.1730]

[83]    Iddo Tzameret: Algebraic proofs over noncommutative formulas. Inform. Comput., 209(10):1269–1292, 2011. Preliminary version in TAMC’10. [doi:10.1016/j.ic.2011.07.004, arXiv:1004.2159, ECCC:TR10-097]

[84]   Ilya Volkovich: Computations beyond exponentiation gates and applications. Electron. Colloq. Comput. Complexity, TR15-042, 2015. [ECCC]

[85]   Ilya Volkovich: Deterministically factoring sparse polynomials into multilinear factors and sums of univariate polynomials. In Proc. 19th Internat. Workshop on Randomization and Computation (RANDOM’15), pp. 943–958. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2015. [doi:10.4230/LIPIcs.APPROX-RANDOM.2015.943, ECCC:TR14-168]

[86]   Richard Zippel: Probabilistic algorithms for sparse polynomials. In Proc. Internat. Symp. Symbolic and Algebraic Manipulation (EUROSAM’79), pp. 216–226. Springer, 1979. [doi:10.1007/3-540-09519-5_73]