Abstract
We define a collection of Prover-Delayer games to characterise some subsystems of propositional resolution. We give some natural criteria for the games which guarantee lower bounds on the resolution width. By an adaptation of the size-width tradeoff for resolution of [10] this result also gives lower bounds on proof size.
We also use games to give upper bounds on proof size, and in particular describe a good strategy for the Prover in a certain game which yields a short refutation of the Linear Ordering principle.
Using previous ideas we devise a new algorithm to automatically generate resolution refutations. On bounded width formulas, our algorithm is as least as good as the width based algorithm of [10]. Moreover, it finds short proofs of the Linear Ordering principle when the variables respect a given order.
Finally we approach the question of proving that a formula F is hard to refute if and only if is “almost” satisfiable. We prove results in both directions when “almost satisfiable” means that it is hard to distuinguish F from a satisfiable formula using limited pebbling games.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alekhnovich, M., Ben-Sasson, E., Razborov, A., Wigderson, A.: Space complexity in propositional calculus. SIAM J. Comput. 31(4), 1184–1211 (2002)
Alekhnovich, M., Razborov, A.A.: Resolution is not automatizable unless W[P] is not tractable. In: 42nd IEEE Symposium on Foundations of Computer Science, FOCS 2001, pp. 210–219 (2001)
Atserias, A., Dalmau, V.: A combinatorial characterization of Resolution Width. In: 18th IEEE Conference on Computational Complexity (CCC), pp. 239–247 (2003)
Atserias, A., Kolaitis, P., Vardi, M.: Constraint Propagation as a Proof System. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 77–91. Springer, Heidelberg (2004)
Beame, P., Karp, R.M., Pitassi, T., Saks, M.E.: On the Complexity of Unsatisfiability Proofs for Random k-CNF Formulas. SIAM J. Comput. 31(4), 1048–1075 (2002)
Beame, P., Kautz, H.: A Sabharwal Understanding the power of clause learning. In: Proceedings IJCAI, pp. 1194–1201 (2003)
Beame, P., Pitassi, T.: Simplified and Improved Resolution Lower Bounds. In: 37th IEEE Symposium on Foundations of Computer Science, FOCS 1996, pp. 274–282 (1996)
Ben-Sasson, E., Galesi, N.: Space Complexity of Random Formulae in Resolution. In: 16th IEEE Annual Conference on Computational Complexity, CCC 2001, pp. 42–51 (2001)
Ben-Sasson, E., Impagliazzo, R., Wigderson, A.: Near optimal separation of treelike and general Resolution. In: Electronic Colloquium on Computational Complexity (ECCC) TR00-005 (2000) To appear in Combinatorica
Ben-Sasson, E., Wigderson, A.: Short Proofs Are Narrow—Resolution Made Simple. J. ACM 48(2), 149–168 (2001)
Bonet, M.L., Galesi, N.: Optimality of Size-Width Tradeoffs for Resolution. Computational Complexity 10(4), 261–276 (2001)
Esteban, J.L., Galesi, N., Messner, J.: On the Complexity of Resolution with Bounded Conjunctions. Theoretical Computer Science 321(2-3), 347–370 (2004)
Esteban, J.L., Torán, J.: Space bounds for Resolution. Inform. and Comput. 171(1), 84–97 (2001)
Galesi, N., Thapen, N.: The Complexity of Treelike Systems over λ Local Formuale. In: Proceedings of IEEE Conference on Computational Complexity (2004)
Galesi, N., Thapen, N.: Resolution and Pebbling Games. ECCC Technical Report TR04-112, http://www.eccc.uni-trier.de/eccc-reports/2004/TR04-112/index.html
Haken, A.: The Intractability of Resolution. Theoret. Comp. Sci. 39, 297–308 (1985)
Krajíček, J.: Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications, vol. 60. Cambridge University Press, Cambridge (1995)
Krajíček, J.: On the weak pigeonhole principle. Fund. Math. 170(1-3), 123–140 (2001); J. Symbolic Logic 59(1), 73–86 (1994)
Pudlak, P.: Proofs as Games. American Math. Monthly 107(6), 541–550 (2000)
Pudlák, P., Impagliazzo, R.: A lower bound for DLL algorithms for k-SAT. In: Conference Proceeding of Symposium on Distributed Algorithms, pp. 128–136 (2000)
Riis, S.: A complexity gap for tree-resolution. Computational Complexity 10(3), 179–209 (2001)
Urquhart, A.: Hard examples for Resolution. J. ACM 34(1), 209–219 (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Galesi, N., Thapen, N. (2005). Resolution and Pebbling Games. In: Bacchus, F., Walsh, T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11499107_6
Download citation
DOI: https://doi.org/10.1007/11499107_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26276-3
Online ISBN: 978-3-540-31679-4
eBook Packages: Computer ScienceComputer Science (R0)