A reduction of proof complexity to computational complexity for 𝐴𝐶⁰[𝑝] Frege systems

Krajíček, Jan

doi:10.1090/S0002-9939-2015-12610-X

A reduction of proof complexity to computational complexity for $AC^0[p]$ Frege systems
HTML articles powered by AMS MathViewer

by Jan Krajíček PDF

Proc. Amer. Math. Soc. 143 (2015), 4951-4965 Request permission

Abstract:

We give a general reduction of lengths-of-proofs lower bounds for constant depth Frege systems in DeMorgan language augmented by a connective counting modulo a prime $p$ (the so-called $AC^0[p]$ Frege systems) to computational complexity lower bounds for search tasks involving search trees branching upon values of maps on the vector space of low degree polynomials over ${\textbf {F}_p}$.

References

M. Ajtai, $\Sigma ^{1}_{1}$-formulae on finite structures, Ann. Pure Appl. Logic 24 (1983), no. 1, 1–48. MR 706289, DOI 10.1016/0168-0072(83)90038-6
Miklos Ajtai, The complexity of the pigeonhole principle, in: Proc. IEEE 29$^{\mbox {th}}$ Annual Symp. on Foundation of Computer Science, (1988), pp. 346-355.
M. Ajtai, Parity and the pigeonhole principle, Feasible mathematics (Ithaca, NY, 1989) Progr. Comput. Sci. Appl. Logic, vol. 9, Birkhäuser Boston, Boston, MA, 1990, pp. 1–24. MR 1232921
Miklos Ajtai, The independence of the modulo $p$ counting principles, in: Proceedings of the 26th Annual ACM Symposium on Theory of Computing, (1994), pp.402-411. ACM Press.
Miklos Ajtai, Symmetric Systems of Linear Equations modulo p, in: Electronic Colloquium on Computational Complexity (ECCC), TR94-015, (1994).
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. (3) 73 (1996), no. 1, 1–26. MR 1387081, DOI 10.1112/plms/s3-73.1.1
Toniann Pitassi, Paul Beame, and Russell Impagliazzo, Exponential lower bounds for the pigeonhole principle, Comput. Complexity 3 (1993), no. 2, 97–140. MR 1233662, DOI 10.1007/BF01200117
Samuel R. Buss, Lower bounds on Nullstellensatz proofs via designs, Proof complexity and feasible arithmetics (Rutgers, NJ, 1996) DIMACS Ser. Discrete Math. Theoret. Comput. Sci., vol. 39, Amer. Math. Soc., Providence, RI, 1998, pp. 59–71. MR 1486614, DOI 10.1006/jcss.1998.1585
S. Buss, R. Impagliazzo, J. Krajíček, P. Pudlák, A. A. Razborov, and J. Sgall, Proof complexity in algebraic systems and bounded depth Frege systems with modular counting, Comput. Complexity 6 (1996/97), no. 3, 256–298. MR 1486929, DOI 10.1007/BF01294258
Samuel R. Buss, Leszek A. Kolodziejczyk, and Konrad Zdanowski: Collapsing modular counting in bounded arithmetic and constant depth propositional proofs, Trans. Amer. Math. Soc, to appear.
Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo, Using the Groebner basis algorithm to find proofs of unsatisfiability, Proceedings of the Twenty-eighth Annual ACM Symposium on the Theory of Computing (Philadelphia, PA, 1996) ACM, New York, 1996, pp. 174–183. MR 1427512, DOI 10.1145/237814.237860
Stephen A. Cook and Robert A. Reckhow, The relative efficiency of propositional proof systems, J. Symbolic Logic 44 (1979), no. 1, 36–50. MR 523487, DOI 10.2307/2273702
Merrick Furst, James B. Saxe, and Michael Sipser, Parity, circuits, and the polynomial-time hierarchy, Math. Systems Theory 17 (1984), no. 1, 13–27. MR 738749, DOI 10.1007/BF01744431
Johan Hastad, Almost optimal lower bounds for small depth circuits. in: Randomness and Computation, ed. S.Micali, Ser.Adv.Comp.Res., 5, (1989), pp.143-170. JAI Pres.
Russell Impagliazzo, Pavel Pudlák, and Jiří Sgall, Lower bounds for the polynomial calculus and the Gröbner basis algorithm, Comput. Complexity 8 (1999), no. 2, 127–144. MR 1724604, DOI 10.1007/s000370050024
Russell Impagliazzo and Nathan Segerlind, Counting axioms do not polynomially simulate counting gates (extended abstract), 42nd IEEE Symposium on Foundations of Computer Science (Las Vegas, NV, 2001) IEEE Computer Soc., Los Alamitos, CA, 2001, pp. 200–209. MR 1948708
Jan Krajíček, Lower bounds to the size of constant-depth propositional proofs, J. Symbolic Logic 59 (1994), no. 1, 73–86. MR 1264964, DOI 10.2307/2275250
Jan Krajíček, Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and its Applications, vol. 60, Cambridge University Press, Cambridge, 1995. MR 1366417, DOI 10.1017/CBO9780511529948
Jan Krajíček, Lower bounds for a proof system with an exponential speed-up over constant-depth Frege systems and over polynomial calculus, Mathematical foundations of computer science 1997 (Bratislava), Lecture Notes in Comput. Sci., vol. 1295, Springer, Berlin, 1997, pp. 85–90. MR 1640210, DOI 10.1007/BFb0029951
Jan Krajíček, On the degree of ideal membership proofs from uniform families of polynomials over a finite field, Illinois J. Math. 45 (2001), no. 1, 41–73. MR 1849985
Jan Krajíček, Forcing with random variables and proof complexity, London Mathematical Society Lecture Note Series, vol. 382, Cambridge University Press, Cambridge, 2011. MR 2768875
Jan Krajíček, Pavel Pudlák, and Alan Woods, An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle, Random Structures Algorithms 7 (1995), no. 1, 15–39. MR 1346282, DOI 10.1002/rsa.3240070103
Alexis Maciel and Toniann Pitassi, Towards lower bounds for bounded-depth Frege proofs with modular connectives, Proof complexity and feasible arithmetics (Rutgers, NJ, 1996) DIMACS Ser. Discrete Math. Theoret. Comput. Sci., vol. 39, Amer. Math. Soc., Providence, RI, 1998, pp. 195–227. MR 1486622, DOI 10.1090/dimacs/039/12
Alexis Maciel and Toniann Pitassi, A Conditional Lower Bound for a System of Constant-Depth Proofs with Modular Connectives, in: Proc. of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS 06), IEEE Computer Society Press, (August 2006).
Toniann Pitassi, Paul Beame, and Russell Impagliazzo, Exponential lower bounds for the pigeonhole principle, Comput. Complexity 3 (1993), no. 2, 97–140. MR 1233662, DOI 10.1007/BF01200117
Pavel Pudlák, The lengths of proofs, Handbook of proof theory, Stud. Logic Found. Math., vol. 137, North-Holland, Amsterdam, 1998, pp. 547–637. MR 1640332, DOI 10.1016/S0049-237X(98)80023-2
Pavel Pudlák and Samuel R. Buss, How to lie without being (easily) convicted and the lengths of proofs in propositional calculus, Computer science logic (Kazimierz, 1994) Lecture Notes in Comput. Sci., vol. 933, Springer, Berlin, 1995, pp. 151–162. MR 1471224, DOI 10.1007/BFb0022253
A. A. Razborov, Lower bounds on the dimension of schemes of bounded depth in a complete basis containing the logical addition function, Mat. Zametki 41 (1987), no. 4, 598–607, 623 (Russian). MR 897705
Alexander A. Razborov, Lower bounds for the polynomial calculus, Comput. Complexity 7 (1998), no. 4, 291–324. MR 1691494, DOI 10.1007/s000370050013
Roman Smolensky, Algebraic methods in the theory of lower bounds for Boolean circuit complexity, in: Proc. 19th Ann. ACM Symp. on Th. of Computing, (1987), pp. 77–82.
Andrew C.-C. Yao, Separating the polynomial-time hierarchy by oracles, in: Proc. 26th Ann. IEEE Symp. on Found. of Comp. Sci., (1985), pp. 1–10.