Resolution is one of the best-studied systems for refuting unsatisfiable propositional formulas. This is due to its theoretical simplicity, as well as its practical importance since it is the proof system at the root of many modern SAT solvers. Several complexity measures for the analysis of resolution refutations have been used in the last decades. In this talk, we will mainly concentrate on space bounds, which measure the amount of memory that is needed in a resolution refutation. Intuitively, the clause space (CS) measures the number of clauses required simultaneously in a refutation, while the variable space (VS) measures the maximum number of distinct variables kept simultaneously in memory during this process. Experimental results have shown that space measures for resolution correlate well with the hardness of refuting unsatisfiable formulas with SAT solvers in practice [ABLM08, JMNŽ12].
Tree-like resolution is a restricted kind of resolution that is especially important since the original DPLL algorithm [DP60, DLL62] on which many SAT solvers are based, is equivalent to this restriction of the resolution system. Contrary to general resolution, in tree-like resolution, if a clause is needed more than once in a refutation, it has to be rederived each time. It is known that general resolution can be exponentially more efficient than tree-like resolution in terms of length (number of clauses in a refutation) [BEGJ98, BIW04]. In [BIW04], the authors give an almost optimal separation between general and tree-like resolution.
In this talk, we show a new connection between the space measure in tree-like resolution and the reversible pebble game in graphs. Using this connection, we provide several formula classes for which there is a logarithmic factor separation between the space complexity measure in tree-like and general resolution. We show that these separations are not far from optimal by proving upper bounds for tree-like resolution space in terms of general resolution clause and variable space. In particular, we show that for any formula F, its tree-like resolution space is upper bounded by space(\pi) log time(\pi), where \pi is any general resolution refutation of F. This holds considering as space(\pi) the clause space of the refutation as well as considering its variable space. For the concrete case of Tseitin formulas, we are able to improve this bound to the optimal bound space(\pi) log n, where n is the number of vertices of the corresponding graph.
The talk will conclude with some future directions of research in both the worlds of proof complexity and pebbling.
[ABLM08] Carlos Ansótegui, María Luisa Bonet, Jordi Levy, and Felip Manyà. Measuring the hardness of SAT instances. In Proceedings of the 23rd National Conference on Artificial Intelligence (AAAI ’08), pages 222–228, July 2008.
[BIW04] Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson. Near optimal separation of tree-like and general resolution. Combinatorica, 24(4):585–603, September 2004.
[BEGJ98] María Luisa Bonet, Juan Luis Esteban, Nicola Galesi, and Jan Johannsen. Exponential separations between restricted resolution and cutting planes proof systems. In Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science (FOCS ’98), pages 638–647, November 1998.
[DLL62] Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem proving. Communications of the ACM, 5(7):394–397, July 1962.
[DP60] Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201–215, 1960.
[JMNŽ12] Matti Järvisalo, Arie Matsliah, Jakob Nordström, and Stanislav Živný. Relating proof complexity measures and practical hardness of SAT. In Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming (CP ’12), volume 7514 of Lecture Notes in Computer Science, pages 316–331. Springer, October 2012.
[TW19] Jacobo Torán and Florian Wörz. Reversible pebble games and the relation between tree-like and general resolution space. Technical Report TR19-097, Electronic Colloquium on Computational Complexity (ECCC), 2019. URL: https://eccc.weizmann.ac.il/report/2019/097. Accepted for publication in the Proceedings of the 37th Symposium on Theoretical Aspects of Computer Science (STACS '20).