Abstract
In recent years there has been some progress in our understanding of the proof-search problem for very low-depth proof systems, e.g. proof systems that manipulate formulas of very low complexity such as clauses (i.e. resolution), DNF-formulas (i.e. R(k) systems), or polynomial inequalities (i.e. semi-algebraic proof systems). In this talk I will overview this progress. I will start with bounded-width resolution, whose specialized proof-search algorithm is as easy as uninteresting, but whose proof-search problem is unintentionally solved by certain versions of conflict-driven clause-learning algorithms with restarts. I will continue with R(k) systems, whose proof-search problem turned out to hide the complexity of certain two-player games of interest in the area of systems synthesis and verification. And I will close with bounded-degree semi-algebraic proof systems, whose proof-search problem turned out to hide the complexity of systems of linear equations over finite fields, among other problems.
Research partially supported by project TIN2010-20967-C04-05 (TASSAT).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alekhnovich, M., Razborov, A.A.: Resolution Is Not Automatizable Unless W[P] Is Tractable. SIAM J. Comput. 38(4), 1347–1363 (2008)
Atserias, A., Bonet, M.L.: On the Automatizability of Resolution and Related Propositional Proof Systems. Information and Computation 189(2), 182–201 (2004)
Atserias, A., Fichte, J.K., Thurley, M.: Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution. Journal of Artificial Intelligence Research 40, 353–373 (2011)
Atserias, A., Maneva, E.: Mean-payoff games and propositional proofs. Information and Computation 209(4), 664–691 (2011)
Barak, B., Brandão, F., Harrow, A., Kelner, J., Zhou, Y.: Hypercontractivity, Sum-of-Squares Proofs, and their Applications. In: Proc. of 44th ACM Symposium on Theory of Computing (STOC), pp. 307–326 (2012)
Beame, P., Karp, R., Pitassi, T., Saks, M.: The efficiency of resolution and Davis-Putnam procedures. SIAM J. Comput. 31(4), 1048–1075 (2002)
Beame, P., Kautz, H., Sabharwal, A.: Towards Understanding and Harnessing the Potential of Clause Learning. Journal of Artificial Intelligence Research 22, 319–351 (2004)
Beame, P., Pitassi, T.: Simplified and improved Resolution lower bounds. In: Proc. of the 27th IEEE Foundations of Computer Science (FOCS), pp. 274–282 (1996)
Beckmann, A., Pudlák, P., Thapen, N.: Parity games and propositional proofs (April 2013) (in preparation )
Ben-Sasson, E.: Hard examples for the bounded depth Frege proof system. Computational Complexity 11, 109–136 (2002)
Ben-Sasson, E., Impagliazzo, R., Wigderson, A.: Near Optimal Separation of Tree-Like and General Resolution. Combinatorica 24(4), 585–604 (2003)
Ben-Sasson, E., Wigderson, A.: Short proofs are narrow–resolution made simple. Journal of the ACM 48(2), 149–169 (2001)
Bochnak, J., Coste, M., Roy, M.-F.: Real algebraic geometry. Springer (1999)
Bonet, M.L., Domingo, C., Gavaldà, R., Maciel, A., Pitassi, T.: Non-automatizability of bounded-depth Frege proofs. Computational Complexity 13, 47–68 (2004)
Bonet, M.L., Esteban, J.L., Galesi, N., Johansen, J.: On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems. SIAM J. Comput. 30(5), 1462–1484 (2000)
Bonet, M.L., Galesi, N.: Optimality of Size-Width Tradeoffs for Resolution. Computational Complexity 10(4), 261–276 (2001)
Bonet, M.L., Pitassi, T., Raz, R.: On Interpolation and Automatization for Frege Systems. SIAM J. Comput. 29(6), 1939–1967 (2000)
Chvátal, V.: Edmonds polytopes and a hierarchy of combinatorial problems. Discrete Mathematics 4(4), 305–337 (1973)
Clegg, M., Edmonds, J., Impagliazzo, R.: Using the Groebner basis algorithm to find proofs of unsatisfiability. In: Proc. of the 28th Annual ACM Symposium on Theory of Computing (STOC), pp. 174–183 (1996)
Condon, A.: The Complexity of Stochastic Games. Information and Computation 96, 203–224 (1992)
Cook, S.A., Reckhow, R.A.: The Relative Efficiency of Propositional Proof Systems. J. Symbolic Logic 44(1), 36–50 (1979)
Downey, R.G., Fellows, M.R.: Parameterized Complexity. Monographs in Computer Science. Springer (1999)
Ehrenfeucht, A., Mycielsky, J.: Positional strategies for mean payoff games. International Journal of Game Theory 8(2), 109–113 (1979)
Emerson, E.A., Jutla, C.S.: Tree Automata, Mu-Calculus and Determinacy. In: Proc. of 32nd IEEE Foundations of Computer Science (FOCS), pp. 368–377 (1991)
Esteban, J.L., Galesi, N., Messner, J.: On the Complexity of Resolution with Bounded Conjunctions. Theoretical Computer Science 321(2-3), 347–370 (2004)
Grigoriev, D.: Linear Lower Bound on Degrees of Positivstellensatz Calculus Proofs for the Parity. Theor. Comput. Sci. 259, 613–622 (2001)
Grigoriev, D., Hirsch, E.A., Pasechnik, D.V.: Complexity of semi-algebraic proofs. Moscow Mathematical Journal 2(4), 647–679 (2002)
Huang, L., Pitassi, T.: Automatizability and Simple Stochastic Games. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part I. LNCS, vol. 6755, pp. 605–617. Springer, Heidelberg (2011)
Krajíček, J.: On the weak pigeonhole principle. Fundamenta Mathematicae 170(1-3), 123–140 (2001)
Krajíček, J.: Lower Bounds to the Size of Constant-Depth Propositional Proofs. J. of Symbolic Logic 59(1), 73–86 (1994)
Krajíček, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. of Symbolic Logic 62(2), 457–486 (1997)
Laurent, M.: A comparison of the Sherali-Adams, Lovász-Schrijver and Lasserre relaxations for 0-1 programming. Mathematics of Operations Research 28, 470–496 (2001)
Lovász, L., Schrijver, A.: Cones of matrices and set-functions and 0-1 optimization. SIAM J. Optimization 1, 166–190 (1991)
Marques-Silva, J., Lynce, I., Malik, S.: Conflict-Driven Clause Learning SAT Solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. IOS Press (2009)
Parrilo, P.A.: Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization. Ph.D. Thesis, California Institute of Technology, Pasadena, CA (2000)
Pitassi, T., Segerlind, N.: Exponential Lower Bounds and Integrality Gaps for Tree-Like Lovász-Schrijver Procedures. SIAM J. Comput. 41(1), 128–159 (2012)
Pudlák, P.: On reducibility and symmetry of disjoint NP-pairs. Theor. Comput. Science 295, 323–339 (2003)
Pudlák, P.: On the complexity of propositional calculus. In: Sets and Proofs, Invited papers from Logic Colloquium 1997, pp. 197–218. Cambridge Univ. Press (1999)
Sherali, H.D., Adams, W.P.: A hierarchy of relaxations and convex hull characterizations for mixed-integer zero-one programming problems. Discrete Applied Mathematics 52(1), 83–106 (1994)
Stålmarck, G.: Short resolution proofs for a sequence of tricky formulas. Acta Informatica 33(3), 277–280 (1996)
Stengle, G.: A Nullstellensatz and a Positivstellensatz in Semialgebraic Geometry. Mathematische Annalen 207(2), 87–97 (1974)
Urquhart, A.: Hard examples for resolution. Journal of the ACM 34(1), 209–219 (1987)
Zwick, U., Paterson, M.S.: The complexity of mean payoff games on graphs. Theoretical Computer Science 158, 343–359 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Atserias, A. (2013). The Proof-Search Problem between Bounded-Width Resolution and Bounded-Degree Semi-algebraic Proofs. In: Järvisalo, M., Van Gelder, A. (eds) Theory and Applications of Satisfiability Testing – SAT 2013. SAT 2013. Lecture Notes in Computer Science, vol 7962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39071-5_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-39071-5_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39070-8
Online ISBN: 978-3-642-39071-5
eBook Packages: Computer ScienceComputer Science (R0)