Abstract
This paper gives an improved separation between regular and unrestricted resolution. The main result is that there is a sequence Π 1, Π 2, ..., Π i , ... of sets of clauses for which the minimum regular resolution refutation of Π i has size \(2^{\Omega (R_i / ( \log R_i )^7 )}\), where R i is the minimum size of an unrestricted resolution refutation of Π i . This improves earlier lower bounds for which the separations proved were of the form \(2^{\Omega(\sqrt[3]{R})}\) and \(2^{ \Omega( \sqrt[4]{R} / (\log R)^3 ) }\).
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
Tseitin, G.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part 2, pp. 115–125. Consultants Bureau, New York (1970); Reprinted in[15], vol. 2, pp. 466-483
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the Association for Computing Machinery 5, 394–397 (1962); Reprinted in [15], vol. 1, pp. 267-270
Urquhart, A.: The complexity of propositional proofs. The Bulletin of Symbolic Logic 1, 425–467 (1995)
Huang, W., Yu, X.: A DNF without regular shortest consensus path. SIAM Journal on Computing 16, 836–840 (1987)
Goerdt, A.: Regular resolution versus unrestricted resolution. SIAM Journal on Computing 22, 661–683 (1993)
Alekhnovich, M., Johannsen, J., Pitassi, T., Urquhart, A.: An exponential separation between regular and general resolution. Theory of Computing 3, 81–102 (2007); Preliminary version. In: Proceedings of the 34th Annual ACM Symposium on Theory of Computing, May 19-21, 2002, Montréal, Québec, Canada (2002)
Ben-Sasson, E., Impagliazzo, R., Wigderson, A.: Near optimal separation of tree-like and general resolution. Combinatorica, 585–603 (2004); Preliminary version, ECCC TR00-005 (2000)
Krishnamurthy, B.: Short proofs for tricky formulas. Acta Informatica 22, 253–275 (1985)
Stålmarck, G.: Short resolution proofs for a sequence of tricky formulas. Acta Informatica 33, 277–280 (1996)
Bonet, M.L., Galesi, N.: Optimality of size-width tradeoffs for resolution. Computational Complexity 10, 261–276 (2001); Preliminary version: Proceedings 40th FOCS (1999)
Ben-Sasson, E.: Size Space Tradeoffs For Resolution. In: Proceedings of the 34th ACM Symposium on the Theory of Computing, pp. 457–464 (2002)
Kamath, A., Motwani, R., Palem, K., Spirakis, P.: Tail bounds for occupancy and the satisfiability threshold conjecture. Random Structures and Algorithms 7, 59–80 (1995)
McDiarmid, C.: Concentration. In: Habib, M., McDiarmid, C., Ramirez-Alfonsin, J., Reed, B. (eds.) Probabilistic Methods for Algorithmic Discrete Mathematics, vol. 16, pp. 195–248. Springer, Heidelberg (1998); Algorithms and Combinatorics 16
Paul, W., Tarjan, R., Celoni, J.: Space bounds for a game on graphs. Mathematical Systems Theory 10, 239–251 (1977)
Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning. Springer, New York (1983)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Urquhart, A. (2008). Regular and General Resolution: An Improved Separation. In: Kleine Büning, H., Zhao, X. (eds) Theory and Applications of Satisfiability Testing – SAT 2008. SAT 2008. Lecture Notes in Computer Science, vol 4996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79719-7_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-79719-7_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79718-0
Online ISBN: 978-3-540-79719-7
eBook Packages: Computer ScienceComputer Science (R0)