Constant-depth Frege systems with counting axioms polynomially simulate Nullstellensatz refutations

ABSTRACT

We show that constant-depth Frege systems with counting axioms modulo m polynomially simulate Nullstellensatz refutations modulo m. Central to this is a new definition of reducibility from propositional formulas to systems of polynomials. Using our definition of reducibility, most previously studied propositional formulas reduce to their polynomial translations. When combined with a previous result of the authors, this establishes the first size separation between Nullstellensatz and polynomial calculus refutations. We also obtain new upper bounds on refutation sizes for certain CNFs in constant-depth Frege with counting axioms systems.

REFERENCES

• 1: Ajtai, M. 1990. Parity and the pigeonhole principle. In Feasible Mathematics: A Mathematical Sciences Institute Workshop (FEASMATH). Birkhauser.
• 2: Ajtai, M. 1994. The complexity of the pigeonhole principle. Combinatorica 14, 4, 417--433.
• 3: Miklos Ajtai, The independence of the modulo p counting principles, Proceedings of the twenty-sixth annual ACM symposium on Theory of computing, p.402-411, May 23-25, 1994, Montreal, Quebec, Canada [doi>10.1145/195058.195207]
• 4: M. Alekhnovich , E. Ben-Sasson , A. A. Razborov , A. Wigderson, Pseudorandom generators in propositional proof complexity, Proceedings of the 41st Annual Symposium on Foundations of Computer Science, p.43, November 12-14, 2000
• 5: Beame, P., Impagliazzo, R., Krajíček, J., Pitassi, T., and Pudlák, P. 1996. Lower bounds on Hilbert's Nullstellensatz and propositional proofs. In Proceedings of the London Mathematical Society 73, 3, 1--26.
• 6: Beame, P. and Pitassi, T. 1996. An exponential separation between the parity principle and the pigeonhole principle. Annals Pure Appl. Logic 80, 3(Aug.), 195--228.
• 7: Beame, P. and Pitassi, T. 1998. Propositional proof complexity: Past, present, and future. Bull. European Assoc. Theoret. Comput. Science 65, 66--89.
• 8: Beame, P. and Riis, S. 1998. More one the relative strength of counting principles. In P. Beame and S. Buss Eds. Proof Complexity and Feasible Arithmetics, 13--35. American Mathematical Society.
• 9: Eli Ben-Sasson, Hard examples for the bounded depth Frege proof system, Computational Complexity, v.11 n.3/4, p.109-136, March 2003 [doi>10.1007/s00037-002-0172-5]
• 10: Eli Ben-Sasson , Russell Impagliazzo, Random CNF's are Hard for the Polynomial Calculus, Proceedings of the 40th Annual Symposium on Foundations of Computer Science, p.415, October 17-18, 1999
• 11: Maria Luisa Bonet , Nicola Galesi, A Study of Proof Search Algorithms for Resolution and Polynomial Calculus, Proceedings of the 40th Annual Symposium on Foundations of Computer Science, p.422, October 17-18, 1999
• 12: Joshua Buresh-Oppenheim , Matthew Clegg , Russell Impagliazzo , Toniann Pitassi, Homogenization and the polynomial calculus, Computational Complexity, v.11 n.3/4, p.91-108, March 2003 [doi>10.1007/s00037-002-0171-6]
• 13: Sam Buss , Dima Grigoriev , Russell Impagliazzo , Toniann Pitassi, Linear gaps between degrees for the polynomial calculus modulo distinct primes, Journal of Computer and System Sciences, v.62 n.2, p.267-289, March 2001 [doi>10.1006/jcss.2000.1726]
• 14: S. Buss , R. Impagliazzo , J. Krajíček , P. Pudlák , A. A. Razborov , J. Sgall, Proof complexity in algebraic systems and bounded depth Frege systems with modular counting, Computational Complexity, v.6 n.3, p.256-298, 1997 [doi>10.1007/BF01294258]
• 15: Samuel R. Buss , Toniann Pitassi, Good degree bounds on Nullstellensatz refutations of the induction principle, Journal of Computer and System Sciences, v.57 n.2, p.162-171, Oct. 1998 [doi>10.1006/jcss.1998.1585]
• 16: Matthew Clegg , Jeffery Edmonds , Russell Impagliazzo, Using the Groebner basis algorithm to find proofs of unsatisfiability, Proceedings of the twenty-eighth annual ACM symposium on Theory of computing, p.174-183, May 22-24, 1996, Philadelphia, Pennsylvania, United States [doi>10.1145/237814.237860]
• 17: Cook, S. and Reckhow, R. 1979. The relative efficiency of propositional proof systems. J. Symbol. Logic 44, 1 (March). 36--50.
• 18: Russell Impagliazzo , Pavel Pudlák , Jiří Sgall, Lower bounds for the polynomial calculus and the Gröbner basis algorithm, Computational Complexity, v.8 n.2, p.127-144, Nov. 1999 [doi>10.1007/s000370050024]
• 19: N. Segerlind, Counting Axioms Do Not Polynomially Simulate Counting Gates, Proceedings of the 42nd IEEE symposium on Foundations of Computer Science, p.200, October 14-17, 2001
• 20: Jan Krajíček, Bounded arithmetic, propositional logic, and complexity theory, Cambridge University Press, New York, NY, 1996
• 21: Krajíček, J. 2001. Tautologies from pseudo-random generators. Bull. Symbol. Logic 7, 2, 197--212.
• 22: Jan Krajíček , Pavel Pudlák , Alan Woods, An exponential lower bound to the size of bounded depth Frege proofs of the Pigeonhole Principle, Random Structures & Algorithms, v.7 n.1, p.15-39, Aug. 1995 [doi>10.1002/rsa.3240070103]
• 23: Pitassi, T. 1997. Algebraic propositional proof systems. In N. Immerman and P. G. Kolaitis, Eds. Descriptive Complexity and Finite Models vol. 31 DIMACS: Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society.
• 24: Toniann Pitassi , Paul Beame , Russell Impagliazzo, Exponential lower bounds for the pigeonhole principle, Computational Complexity, v.3 n.2, p.97-140, April 1993 [doi>10.1007/BF01200117]
• 25: Pudlák, P. 1998. The lengths of proofs. In S. R. Buss, Eds. Handbook of Proof Theory. Elsevier North-Holland. 547--637.
• 26: Alexander A. Razborov, Lower bounds for the polynomial calculus, Computational Complexity, v.7 n.4, p.291-324, Dec. 1998 [doi>10.1007/s000370050013]
• 27: Riis, S. 1997. Count(q) does not imply Count(p). Annals Pure Appl. Logic 90, 1--3 (Dec.). 1--56.
• 28: Tseitin, G. 1970. On the complexity of proofs in propositional logics. Seminars in Mathematics 8.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory

General Terms:
Theory

Keywords:
Modular counting axioms, Nullstellensatz refutations, propositional proof complexity