Abstract
Pool Resolution for propositional CNF formulas is introduced. Its relationship to state-of-the-art satisfiability solvers is explained. Every regular-resolution derivation is also a pool-resolution derivation. It is shown that a certain family of formulas, called NT**(n) has polynomial sized pool-resolution refutations, whereas the shortest regular refutations have an exponential lower bound. This family is a variant of the GT(n) family analyzed by Bonet and Galesi (FOCS 1999), and the GT’n family shown to require exponential-length regular-resolution refutations by Alekhnovitch, Johannsen, Pitassi and Urquhart (STOC 2002). Thus, Pool Resolution is exponentially stronger than Regular Resolution. Roughly speaking a general-resolution derivation is a pool-resolution derivation if its directed acyclic graph (DAG) has a depth-first search tree that satisfies the regularity restriction: on any path in this tree no resolution variable is repeated. In other words, once a clause is derived at a node and used by its tree parent, its derivation is forgotten, and subsequent uses of that clause treat it as though it were an input clause. This policy is closely related to DPLL search with recording of so-called conflict clauses. Variations of DPLL plus conflict analysis currently dominate the field of high-performance satisfiability solving. The power of Pool Resolution might provide some theoretical explanation for their success.
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
Alekhnovich, M., Johannsen, J., Pitassi, T., Urquhart, A.: An exponential separation between regular and unrestricted resolution. In: Proc. 34th ACM Symposium on Theory of Computing, pp. 448–456 (2002)
Anderson, R., Bledsoe, W.W.: A linear format for resolution with merging and a new technique for establishing completeness. Journal of the ACM 17, 525–534 (1970)
Bayardo Jr., R.J., Schrag, R.C.: Using CSP look-back techniques to solve real-world SAT instances. In: Proc. AAAI, pp. 203–208 (1997)
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. 28th ACM Symposium on Theory of Computing (1996)
Ben-Sasson, E., Wigderson, A.: Short proofs are narrow — resolution made simple. JACM 48, 149–168 (2001)
Bonet, M., Galesi, N.: A study of proof search algorithms for resolution and polynomial calculus. In: Proc. 40th Symposium on Foundations of Computer Science, pp. 422–432 (1999)
Bonet, M., Galesi, N.: Optimality of size-width tradeoffs for resolution. Computational Complexity 10, 261–276 (2001)
Clegg, M., Edmonds, J., Impagliazzo, R.: Using the Groebner basis algorithm to find proofs of unsatisfiability. In: Proc. 28th ACM Symposium on Theory of Computing, pp. 174–183 (1996)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM 5, 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the Association for Computing Machinery 7, 201–215 (1960)
Dechter, R., Rish, I.: Directional resolution: the davis-putnam procedure, revisited. In: Proc. 4th Int’l Conf. on Principles of Knowledge Representation and Reasoning (KR 1994), pp. 134–145. Morgan Kaufmann, San Francisco (1994)
Goldberg, E., Novikov, Y.: Berkmin: a fast and robust sat-solver. In: Proc. Design, Automation and Test in Europe, pp. 142–149 (2002)
Johnson, D.S., Trick, M.A. (eds.): Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26. American Mathematical Society (1996)
Krishnamurthy, B.: Short proofs for tricky formulas. Acta Informatica 22, 253–274 (1985)
Lee, S.J., Plaisted, D.A.: Eliminating duplication with the hyper-linking strategy. Journal of Automated Reasoning 9, 25–42 (1992)
Letz, R., Mayr, K., Goller, C.: Controlled integration of the cut rule into connection tableau calculi. Journal of Automated Reasoning 13, 297–337 (1994)
Marques-Silva, J.P., Sakallah, K.A.: GRASP–a search algorithm for propositional satisfiability. IEEE Transactions on Computers 48, 506–521 (1999)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: 39th Design Automation Conference (2001)
Plaisted, D.A.: (private communication) (1984)
Plaisted, D.A.: The search efficiency of theorem proving strategies. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 57–71. Springer, Heidelberg (1994)
Stälmarck, G.: Short resolution proofs for a sequence of tricky formulas. Acta Informatica 33, 277–280 (1996)
Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O., ed.: Seminars in Mathematics v. 8: Studies in Constructive Mathematics and Mathematical Logic, Part II. Steklov Math. Inst., Leningrad, 115–125 (English trans, Plenum.) (1968)
Zhang, H., Stickel, M.E.: Implementing the davis-putnam method. Journal of Automated Reasoning 24, 277–296 (2000)
Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: ICCAD (2001)
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
Van Gelder, A. (2005). Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning. In: Sutcliffe, G., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2005. Lecture Notes in Computer Science(), vol 3835. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11591191_40
Download citation
DOI: https://doi.org/10.1007/11591191_40
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30553-8
Online ISBN: 978-3-540-31650-3
eBook Packages: Computer ScienceComputer Science (R0)