Abstract
The techniques for making decisions, that is, branching, play a central role in complete methods for solving structured instances of constraint satisfaction problems (CSPs). In this work we consider branching heuristics in the context of propositional satisfiability (SAT), where CSPs are expressed as propositional formulas. In practice, there are cases when SAT solvers based on the Davis-Putnam-Logemann-Loveland procedure (DPLL) benefit from limiting the set of variables the solver is allowed to branch on to so called input variables which provide a strong unit propagation backdoor set to any SAT instance. Theoretically, however, restricting branching to input variables implies a super-polynomial increase in the length of the optimal proofs for DPLL (without clause learning), and thus input-restricted DPLL cannot polynomially simulate DPLL. In this paper we settle the case of DPLL with clause learning. Surprisingly, even with unlimited restarts, input-restricted clause learning DPLL cannot simulate DPLL (even without clause learning). The opposite also holds, and hence DPLL and input-restricted clause learning DPLL are polynomially incomparable. Additionally, we analyze the effect of input-restricted branching on clause learning solvers in practice with various structured real-world benchmarks.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Achlioptas, D., Beame, P., & Molloy, M. (2004). Exponential bounds for DPLL below the satisfiability threshold. In J. I. Munro (Ed.), Proceedings of the 15th annual ACM-SIAM symposium on discrete algorithms (SODA’04) (pp. 139–140). Philadelphia: SIAM.
Achlioptas, D., Beame, P., & Molloy, M. S. O. (2004). A sharp threshold in proof complexity yields lower bounds for satisfiability search. Journal of Computer and System Sciences, 68(2), 238–268.
Alekhnovich, M. (2004). Mutilated chessboard problem is exponentially hard for resolution. Theoretical Computer Science, 310(1–3), 513–525.
Alekhnovich, M., Hirsch, E. A., & Itsykson, D. (2005). Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas. Journal of Automated Reasoning, 35(1–3), 51–72.
Alekhnovich, M., Johannsen, J., Pitassi, T., & Urquhart, A. (2002). An exponential separation between regular and general resolution. In Proceedings on 34th annual ACM symposium on theory of computing (STOC’02) (pp. 448–456). New York: ACM.
Beame, P., Culberson, J. C., Mitchell, D. G., & Moore, C. (2005). The resolution complexity of random graph k-colorability. Discrete Applied Mathematics, 153(1–3), 25–47.
Beame, P., Impagliazzo, R., & Sabharwal, A. (2007). The resolution complexity of independent sets and vertex covers in random graphs. Computational Complexity, 16(3), 245–297.
Beame, P., Karp, R. M., Pitassi, T., & Saks, M. E. (2002). The efficiency of resolution and Davis–Putnam procedures. SIAM Journal on Computing, 31(4), 1048–1075.
Beame, P., Kautz, H. A., & Sabharwal, A. (2004). Towards understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research, 22, 319–351.
Biere, A., Cimatti, A., Clarke, E. M., Fujita, M., & Zhu, Y. (1999). Symbolic model checking using SAT procedures instead of BDDs. In Proceedings of the 36th conference on design automation (DAC’99) (pp. 317–320). New York: ACM.
Chvátal, V., & Szemerédi, E. (1988). Many hard examples for resolution. Journal of the ACM, 35(4), 759–768.
Cook, S. A. (1976). A short proof of the pigeon hole principle using extended resolution. SIGACT News, 8(4), 28–32.
Cook, S. A., & Reckhow, R. A. (1979) The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1), 36–50.
Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., et al. (2001). Benefits of bounded model checking at an industrial setting. In G. Berry, H. Comon, & A. Finkel (Eds.), Proceedings of the 13th international conference on computer aided verification (CAV’01). Lecture notes in computer science (Vol. 2102, pp. 436–453). New York: Springer.
Dantchev, S., & Riis, S. (2001). “Planar” tautologies hard for resolution. In Proceedings of the 42nd IEEE symposium on foundations of computer science (FOCS’01) (pp. 220–229). Los Alamitos: IEEE Computer Society.
Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem proving. Communications of the ACM, 5(7), 394–397.
Davis, M., & Putnam, H. (1960). A computing procedure for quantification theory. Journal of the ACM, 7(3), 201–215.
Eén, N., & Sörensson, N. (2004). An extensible SAT-solver. In E. Giunchiglia & A. Tacchella (Eds.), Revised selected papers of the 6th international conference on theory and applications of satisfiability testing (SAT’03). Lecture notes in computer science (Vol. 2919, pp. 502–518). New York: Springer.
Giunchiglia, E., Maratea, M., & Tacchella, A. (2002). Dependent and independent variables in propositional satisfiability. In S. Flesca, S. Greco, N. Leone, & G. Ianni (Eds.), Proceedings of the European conference on logics in artificial intelligence JELIA’02. Lecture notes in artificial intelligence (Vol. 2424, pp. 296–307). New York: Springer.
Giunchiglia, E., Massarotto, A., & Sebastiani, R. (1998). Act, and the rest will follow: Exploiting determinism in planning as satisfiability. In B. B. C. Rich, J. Mostow, & R. Uthurusamy (Eds.), Proceedings of the 15th national conference on artificial intelligence (AAAI’98) (pp. 948–953). Menlo Park: AAAI.
Goerdt, A. (1993). Regular resolution versus unrestricted resolution. SIAM Journal on Computing, 22(4), 661–683.
Goldberg, E., & Novikov, Y. (2002). Berkmin: A fast and robust SAT-solver. In Proceedings of the 2002 design, automation and test in Europe conference (DATE’02) (pp. 142–149). Los Alamitos: IEEE Computer Society.
Gomes, C. P., Selman, B., & Kautz, H. A. (1998). Boosting combinatorial search through randomization. In B. B. C. Rich, J. Mostow, & R. Uthurusamy (Eds.), Proceedings of the 15th national conference on artificial intelligence (AAAI’98) (pp. 431–437). Menlo Park: AAAI.
Haken, A. (1985). The intractability of resolution. Theoretical Computer Science, 39(2–3), 297–308.
Huang, J. (2007). The effect of restarts on the efficiency of clause learning. In M. M. Veloso (Ed.), Proceedings of the 20th international joint conference on artificial intelligence (IJCAI’07) (pp. 2318–2323). Menlo Park: AAAI.
Järvisalo, M. (2007). Equivalence checking multiplier designs. SAT Competition 2007 benchmark description. http://www.tcs.hut.fi/∼mjj/benchmarks/.
Järvisalo, M., & Junttila, T. (2007). Limitations of restricted branching in clause learning. In C. Bessiere (Ed.), Proceedings of the 13th international conference on principles and practice of constraint programming (CP 2007). Lecture notes in computer science (Vol. 4741, pp. 348–363). New York: Springer.
Järvisalo, M., & Junttila, T. (2008). On the power of top-down branching heuristics. In Proceedings of the 23rd AAAI conference on artificial intelligence (AAAI-08) (pp. 304–309). Menlo Park: AAAI.
Järvisalo, M., Junttila, T., & Niemelä, I. (2005). Unrestricted vs restricted cut in a tableau method for Boolean circuits. Annals of Mathematics and Artificial Intelligence, 44(4), 373–399.
Järvisalo, M., & Niemelä, I. (2008). The effect of structural branching on the efficiency of clause learning SAT solving: An experimental study. Journal of Algorithms, 63(1–3), 90–113.
Junttila, T. A., & Niemelä, I. (2000). Towards an efficient tableau method for boolean circuit satisfiability checking. In J. W. Lloyd, V. Dahl, U. Furbach, M. Kerber, K. K. Lau, C. Palamidessi, et al. (Eds.), Proceedings of the 1st international conference on computational logic (CL’00). Lecture notes in computer science (Vol. 1861, pp. 553–567). New York: Springer.
Jussila, T., Heljanko, K., & Niemelä, I. (2005). BMC via on-the-fly determinization. International Journal on Software Tools for Technology Transfer, 7(2), 89–101.
Kautz, H. A., & Selman, B. (1992). Planning as satisfiability. In B. Neumann (Ed.), Proceedings of the 10th European conference on artificial intelligence (ECAI’92) (pp. 359–363). New York: Wiley.
Krajíček, J. (1995). Bounded arithmetic, propositional logic, and complexity theory. In Encyclopedia of mathematics and its applications (Vol. 60). Cambridge: Cambridge University Press.
Kuehlmann, A., Ganai, M. K., & Paruthi, V. (2001). Circuit–based Boolean reasoning. In Proceedings of the 38th design automation conference (DAC’01) (pp. 232–237). New York: ACM.
Latvala, T., Biere, A., Heljanko, K., & Junttila, T. A. (2004). Simple bounded LTL model checking. In A. J. Hu & A. K. Martin (Eds.), Proceedings of the 5th international conference on formal methods in computer-aided design (FMCAD’04). Lecture notes in computer science (Vol. 3312, pp. 186–200). New York: Springer.
Li, C. M., & Anbulagan (1997). Heuristics based on unit propagation for satisfiability problems. In M. Pollack (Ed.), Proceedings of the 15th international joint conference on artificial intelligence (IJCAI’97) (pp. 366–371). San Francisco: Morgan Kaufmann.
Marques-Silva, J., & Guerra e Silva, L. (2003). Solving satisfiability in combinational circuits. IEEE Design & Test of Computers 20(4), 16–21.
Marques-Silva, J. P., & Sakallah, K. A. (1999). GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5), 506–521.
Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., & Malik, S. (2001). Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th design automation conference (DAC’01) (pp. 530–535). New York: ACM.
Nikolenko, S. I. (2005). Hard satisfiable instances for DPLL-type algorithms. Journal of Mathematical Sciences, 126(3), 1205–1209.
Papadimitriou, C. H. (1995). Computational complexity. Reading: Addison-Wesley.
Pyhälä, T. (2004). Factoring benchmarks for SAT-solvers. http://www.tcs.hut.fi/Software/genfacbm/.
Robinson, J. A. (1965). A machine oriented logic based on the resolution principle. Journal of the ACM, 12(1), 23–41.
Strichman, O. (2000). Tuning SAT checkers for bounded model checking. In E. A. Emerson & A. P. Sistla (Eds.), Proceedings of the 12th international conference on computer aided verification (CAV’00). Lecture notes in computer science (Vol. 1855, pp. 480–494). New York: Springer.
Thiffault, C., Bacchus, F., & Walsh, T. (2004). Solving non-clausal formulas with DPLL search. In M. Wallace (Ed.), Proceedings of the 10th international conference on principles and practice of constraint programming (CP’04). Lecture notes in computer science (Vol. 3258, pp. 663–678). New York: Springer.
Tseitin, G. S. (1983). On the complexity of derivation in propositional calculus. In A. Slisenko (Ed.), Studies in constructive mathematics and mathematical logic, part II. Seminars in mathematics, V.A. Steklov mathematical institute, Leningrad (Vol. 8, pp. 115–125). Consultants Bureau (1969). English translation appears in J. Siekmann and G. Wrightson, editors, Automation of Reasoning 2: Classical Papers on Computational Logic 1967–1970 pages 466–483. New York: Springer.
Urquhart, A. (1987). Hard examples for resolution. Journal of the ACM, 34(1), 209–219.
Urquhart, A. (1995). The complexity of propositional proofs. Bulletin of Symbolic Logic, 1(4), 425–467.
Velev, M. N., & Bryant, R. E. (1999). Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions to propositional logic. In L. Pierre & T. Kropf (Eds.), Correct hardware design and verification methods, proceedings of the 10th IFIP WG 10.5 advanced research working conference (CHARME’99). Lecture notes in computer science (Vol. 1703, pp. 37–53). New York: Springer.
Williams, R., Gomes, C. P., & Selman, B. (2003). Backdoors to typical case complexity. In G. Gottlob & T. Walsh (Eds.), Proceedings of the eighteenth international joint conference on artificial intelligence (IJCAI’03) (pp. 1173–1178). San Francisco: Morgan Kaufmann.
Zhang, L., Madigan, C. F., Moskewicz, M. W., & Malik, S. (2001). Efficient conflict driven learning in a Boolean satisfiability solver. In Proceedings of the 2001 international conference on computer-aided design (ICCAD’01) (pp. 279–285). New York: ACM.
Author information
Authors and Affiliations
Corresponding author
Additional information
This is an extended version of a paper [27] presented at the 13th International Conference on Principles and Practice of Constraint Programming (CP 2007) in Providence, RI, USA. The first author gratefully acknowledges financial support from Helsinki Graduate School in Computer Science and Engineering, Academy of Finland (grants #211025 and #122399), Emil Aaltonen Foundation, Jenny and Antti Wihuri Foundation, Finnish Foundation for Technology Promotion TES, and Nokia Foundation. The second author gratefully acknowledges the financial support from Academy of Finland (grant #112016).
Rights and permissions
About this article
Cite this article
Järvisalo, M., Junttila, T. Limitations of restricted branching in clause learning. Constraints 14, 325–356 (2009). https://doi.org/10.1007/s10601-008-9062-z
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10601-008-9062-z