Abstract
Resolution trees with lemmas (RTL) are a resolution-based propositional proof system that is related to the DPLL algorithm with clause learning. Its fragments \(\ensuremath{\ensuremath{\mathrm{RTL}} ({k})}\) are related to clause learning algorithms where the width of learned clauses is bounded by k.
For every k up to O(logn), an exponential separation between the proof systems \(\ensuremath{\ensuremath{\mathrm{RTL}} ({k})}\) and \(\ensuremath{\ensuremath{\mathrm{RTL}} ({k+1})}\) is shown.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bayardo Jr., R.J., Schrag, R.C.: Using CSP look-back techniques to solve real-world SAT instances. In: Proc. 14th Natl. Conference on Artificial Intelligence, pp. 203–208 (1997)
Ben-Sasson, E.: Size-space tradeoffs for resolution. SIAM Journal on Computing 38(6), 2511–2525 (2009)
Ben-Sasson, E., Impagliazzo, R., Wigderson, A.: Near-optimal separation of general and tree-like resolution. Combinatorica 24(4), 585–604 (2004)
Ben-Sasson, E., Johannsen, J.: Lower bounds for width-restricted clause learning on small width formulas. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 16–29. Springer, Heidelberg (2010)
Ben-Sasson, E., Nordström, J.: Understanding space in proof complexity: Separations and trade-offs via substitutions. In: Chazelle, B. (ed.) Innovations in Computer Science, ICS 2011, pp. 401–416. Tsinghua University Press (2011)
Buss, S.R., Hoffmann, J., Johannsen, J.: Resolution trees with lemmas: Resolution refinements that characterize DLL algorithms with clause learning. Logical Methods in Computer Science 4(4) (2008)
Celoni, J., Paul, W., Tarjan, R.: Space bounds for a game on graphs. Mathematical Systems Theory 10, 239–251 (1977)
Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Communications of the ACM 5(7), 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the Association for Computing Machinery 7(3), 201–215 (1960)
Gomes, C.P., Selman, B., Crato, N.: Heavy-tailed distributions in combinatorial search. In: Smolka, G. (ed.) CP 1997. LNCS, vol. 1330, pp. 121–135. Springer, Heidelberg (1997)
Håstad, J.: The shrinkage exponent of De Morgan formulas is 2. SIAM Journal on Computing 27(1), 48–64 (1998)
Hertel, P., Bacchus, F., Pitassi, T., van Gelder, A.: Clause learning can effectively p-simulate general propositional resolution. In: Fox, D., Gomes, C.P. (eds.) Proceedings of the 23rd AAAI Conference on Artificial Intelligence, AAAI 2008, pp. 283–290. AAAI Press (2008)
Johannsen, J.: An exponential lower bound for width-restricted clause learning. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 128–140. Springer, Heidelberg (2009)
Marques-Silva, J.P., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: Proc. IEEE/ACM International Conference on Computer Aided Design, ICCAD, pp. 220–227 (1996)
Tseitin, G.S.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic, Part 2, 115–125 (1968)
Urquhart, A.: A near-optimal separation of regular and general resolution. SIAM Journal on Computing 40(1), 107–121 (2011)
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
Johannsen, J. (2013). Exponential Separations in a Hierarchy of Clause Learning Proof Systems. 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_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-39071-5_5
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)