Pseudo-partitions, transversality and locality: a combinatorial characterization for the space measure in algebraic proof systems

ABSTRACT

We devise a new combinatorial framework for proving space lower bounds in algebraic proof systems like Polynomial Calculus (Pc) and Polynomial Calculus with Resolution (Pcr). Our method can be thought as a Spoiler-Duplicator game, which is capturing boolean reasoning on polynomials instead that clauses as in the case of Resolution. Hence, for the first time, we move the problem of studying the space complexity for algebraic proof systems in the range of 2-players games, as is the case for Resolution.

A very simple case of our method allows us to obtain all the currently known space lower bounds for Pc/Pcr (CT_n, PHP^m_n, BIT-PHP^m_n, XOR-PHP^m_n). The way our method applies to all these examples explains how and why all the known examples of space lower bounds for Pc/Pcr are an application of the method originally given by [Alekhnovich et al 2002] that holds for set of contradictory polynomials having high degree. Our approach unifies in a clear way under a common combinatorial framework and language the proofs of the space lower bounds known so far for Pc/Pcr.

More importantly, using our approach in its full potentiality, we answer to the open problem [Alekhnovich et al 2002, Filmus et al 2012] of proving space lower bounds in Polynomial Calculus and Polynomials Calculus with Resolution for the polynomial encoding of randomly chosen k-CNF formulas. Our result holds for k>= 4. Then, as proved for Resolution in [BenSasson and Galesi 2003], also in Pc and in Pcr refuting a random k-CNF over n variables requires high space measure of the order of Omega(n). Our method also applies to the Graph-PHP^m_n, which is a PHP^m_n defined over a constant (left) degree bipartite expander graph. We develop a common language for the two examples.

References

1. Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. Space complexity in propositional calculus. SIAM J. Comput., 31(4):1184--1211, 2002.
2. Michael Alekhnovich and Alexander A. Razborov. Lower bounds for polynomial calculus: Non-binomial case. In 42nd Annual Symposium on Foundations of Computer Science, pages 190--199, 2001.
3. Albert Atserias. On sufficient conditions for unsatisfiability of random formulas. Journal of ACM, 51(2):281--311, 2004. A preliminary version appeared in the Proceedings of the 17th IEEE Symposium on Logic in Computer Sience (LICS), pagine 325--334, 2002.
4. Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. J. Comput. Syst. Sci., 74(3):323--334, 2008.
5. Albert Atserias, J. Fichte, and M. Thurley. Clause-learning algorithms with many restarts and bounded-width resolution. Theory and Applications of Satisfiability Testing-SAT 2009, pages 114--127, 2009.
6. Paul Beame, Henry A. Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. (JAIR), 22:319--351, 2004.
7. Paul Beame and Toniann Pitassi. Simplified and improved resolution lower bounds. In 37th Annual Symposium on Foundations of Computer Science, pages 274 -- 282. IEEE, 1996.
8. Eli Ben-sasson. Expansion in Proof Complexity. PhD thesis, Hebrew University, 2001.
9. Eli Ben-Sasson and Nicola Galesi. Space complexity of random formulae in resolution. Random Struct. Algorithms, 23(1):92--109, 2003.
10. Eli Ben-Sasson and Russell Impagliazzo. Random CNFs are hard for the polynomial calculus. In 40th Annual Symposium on Foundations of Computer Science, pages 415--421, 1999.
11. Eli Ben-Sasson and Jan Johannsen. Lower bounds for width-restricted clause learning on small width formulas. Theory and Applications of Satisfiability Testing--SAT 2010, pages 16--29, 2010.
12. Eli Ben-Sasson and Jakob Nordström. A space hierarchy for k-dnf resolution. Electronic Colloquium on Computational Complexity (ECCC), 16(047), 2009.
13. Eli Ben-Sasson and Jakob Nordström. Understanding space in resolution: Optimal lower bounds and exponential trade-offs. Electronic Colloquium on Computational Complexity (ECCC), 16(034), 2009.
14. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. J. ACM, 48(2):149--169, 2001.
15. Archie Blake. Canonical Expressions in Boolean Algebra. PhD thesis, University of Chicago, 1938.
16. Michael Brickenstein and Alexander Dreyer. Polybori: A framework for gröbner-basis computations with boolean polynomials. J. Symb. Comput, 44(9):1326--1345, 2009.
17. Sam Buss, Maria Luisa Bonet, and Jan Johannsen. Improved separations of regular resolution from clause learning proof systems. Submitted, 2012.
18. Sam Buss, Jan Hoffman, and Jan Johannsen. Resolution trees with lemmas - resolution refinements that characterize dll-algorithms with clause learning. Logical Methods in Computer Science, 4,:4:13, 2008.
19. Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi. Linear gaps between degrees for the polynomial calculus modulo distinct primes. J. Comput. Syst. Sci., 62(2):267--289, 2001.
20. Samuel R. Buss, Russell Impagliazzo, Jan Krajícek, Pavel Pudlák, Alexander A. Razborov, and Jirí Sgall. Proof complexity in algebraic systems and bounded depth frege systems with modular counting. Computational Complexity, 6(3):256--298, 1997.
21. Vasek Chvátal and Endre Szemerédi. Many hard examples for resolution. J. ACM, 35(4):759--768, 1988.
22. Matthew Clegg, Jeff Edmonds, and Russell Impagliazzo. Using the Gröebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, pages 174--183, 1996.
23. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44:36--50, 1979.
24. David Cox, John Little, and Donal O'Shea. Ideals, Varieties, and Algorithms : An Introduction to Computational Algebraic Geometry and Commutative Algebra, 3rd edition. Springer, 2007.
25. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Commun. ACM, 5:394--397, July 1962.
26. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. ACM, 7:201--215, July 1960.
27. Juan Luis Esteban, Nicola Galesi, and Jochen Messner. On the complexity of resolution with bounded conjunctions. Theor. Comput. Sci., 321(2--3):347--370, 2004.
28. Juan Luis Esteban and Jacobo Torán. Space bounds for resolution. Information and Computation, 171(1):84--97, 2001.
29. Tomás Feder and Moshe Y. Vardi. The computational structure of monotone monadic snp and constraint satisfaction: A study through datalog and group theory. SIAM J. Comput., 28(1):57--104, 1998.
30. Yuval Filmus, Massimo Lauria, Jakob Nordström, Neil Thapen, and Noga Zewi. Space complexity in polynomial calculus. In IEEE Conference on Computational Complexity 2012, 2012. To appear.
31. Nicola Galesi and Massimo Lauria. On the automatizability of polynomial calculus. Theory of Computing Systems, 47(2):491--506, 2010.
32. Nicola Galesi and Massimo Lauria. Optimality of size-degree trade-offs for polynomial calculus. ACM Transactions on Computational Logic, 12(1):??, 2010. To appear.
33. Russell Impagliazzo, Pavel Pudlák, and Jirí Sgall. Lower bounds for the polynomial calculus and the gröbner basis algorithm. Computational Complexity, 8(2):127--144, 1999.
34. Jan Krajícek. Propositional proof complexity i. 2009.
35. Joao P. Marques-Silva and Karem A. Sakallah. Grasp--a new search algorithm for satisfiability. In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD '96),, pages 220--227, 1996.
36. Jakob Nordström. Narrow proofs may be spacious: separating space and width in resolution. In STOC, pages 507--516, 2006.
37. Jakob Nordström and Johan Håstad. Towards an optimal separation of space and length in resolution. In STOC, pages 701--710, 2008.
38. Pavel Pudlák and Jirí Sgall. Algebraic models of computation and interpolation for algebraic proof systems. DIMACS series in Theoretical Computer Science, 39:279--296, 1998.
39. Alexander Razborov. Pseudorandom generators hard for k-dnf resolution and polynomial calculus resolution. Manuscript availbale at author's webpage, 2003.
40. Alexander A. Razborov. Lower bounds for the polynomial calculus. Computational Complexity, 7(4):291--324, 1998.

Index Terms

• Computing methodologies

  • Symbolic and algebraic manipulation

    • Symbolic and algebraic algorithms

      • Theorem proving algorithms

• Theory of computation

  • Computational complexity and cryptography

    • Interactive proof systems

    • Proof complexity

  • Logic

    • Proof theory

  • Models of computation

    • Computability