Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theory and Applications of Satisfiability Testing

SAT 2003: Theory and Applications of Satisfiability Testing pp 242–256Cite as

Using Problem Structure for Efficient Clause Learning

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2919))

Abstract

DPLL based clause learning algorithms for satisfiability testing are known to work very well in practice. However, like most branch-and-bound techniques, their performance depends heavily on the variable order used in making branching decisions. We propose a novel way of exploiting the underlying problem structure to guide clause learning algorithms toward faster solutions. The key idea is to use a higher level problem description, such as a graph or a PDDL specification, to generate a good branching sequence as an aid to SAT solvers. The sequence captures hierarchical structure that is lost in the CNF translation. We show that this leads to exponential speedups on grid and randomized pebbling problems. The ideas we use originate from the analysis of problem structure recently used in [1] to study clause learning from a theoretical perspective.

Research supported by NSF Grant ITR-0219468

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Beame, P., Kautz, H., Sabharwal, A.: Understanding the power of clause learning. In: Proceedings of the 18th International Joint Conference on Artificial Intelligence, Acapulco, Mexico (2003) (to appear)

    Google Scholar 

  2. Velev, M., Bryant, R.: Effective use of boolean satisfiability procedures in the formal verification of superscalar and vliw microprocessors. In: Proceedings of the 38th Design Automation Conference, pp. 226–231 (2001)

    Google Scholar 

  3. Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of the 36th Design Automation Conference, New Orleans, LA, pp. 317–320 (1999)

    Google Scholar 

  4. Zhang, H., Hsiang, J.: Solving open quasigroup problems by propositional reasoning. In: Proceedings of the International Computer Symp., Hsinchu, Taiwan (1994)

    Google Scholar 

  5. Konuk, H., Larrabee, T.: Explorations of sequential ATPG using boolean satisfiability. In: 11th VLSI Test Symposium, pp. 85–90 (1993)

    Google Scholar 

  6. Gomes, C.P., Selman, B., McAloon, K., Tretkoff, C.: Randomization in backtrack search: Exploiting heavy-tailed profiles for solving hard scheduling problems. In: Proceedings of the 4th International Conference on Artificial Intelligence Planning Systems, Pittsburgh, PA (1998)

    Google Scholar 

  7. Davis, M., Putnam, H.: A computing procedure for quantification theory. Communications of the ACM 7, 201–215 (1960)

    MATH  MathSciNet  Google Scholar 

  8. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5, 394–397 (1962)

    Article  MATH  MathSciNet  Google Scholar 

  9. Li, C.M.: Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: IJCAI (1), pp. 366–371 (1997)

    Google Scholar 

  10. Gomes, C.P., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: Proceedings, AAAI 1998: 15th National Conference on Artificial Intelligence, Madison, WI, pp. 431–437 (1998)

    Google Scholar 

  11. Bayardo Jr., R.J., Schrag, R.C.: Using CST look-back techniques to solve real-world SAT instances. In: Proceedings, AAAI 1997: 14th National Conference on Artificial Intelligence, pp. 203–208 (1997)

    Google Scholar 

  12. Marques-Silva, J.P., Sakallah, K.A.: GRASP – a new search algorithm for satisfiability. In: Proceedings of the International Conference on Computer Aided Design, San Jose, CA, pp. 220–227. ACM/IEEE (1996)

    Google Scholar 

  13. Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 272–275. Springer, Heidelberg (1997)

    Google Scholar 

  14. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, Las Vegas, NV, pp. 530–535. ACM/IEEE (2001)

    Google Scholar 

  15. Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: Proceedings of the International Conference on Computer Aided Design, San Jose, CA, pp. 279–285, ACM/IEEE (2001)

    Google Scholar 

  16. de Kleer, J., Williams, B.C.: Diagnosing multiple faults. Artificial Intelligence 32, 97–130 (1987)

    Article  MATH  Google Scholar 

  17. Stallman, R., Sussman, G.J.: Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artificial Intelligence 9, 135–196 (1977)

    Article  MATH  Google Scholar 

  18. Genesereth, R.: The use of design descriptions in automated diagnosis. Artificial Intelligence 24, 411–436 (1984)

    Article  Google Scholar 

  19. Davis, R.: Diagnostic reasoning based on structure and behavior. Artificial Intelligence 24, 347–410 (1984)

    Article  Google Scholar 

  20. Li, C.M.: Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of the 15th International Joint Conference on Artificial Intelligence, Nagoya, Japan, pp. 366–371 (1997)

    Google Scholar 

  21. Mézard, M., Zecchina, R.: Random k-satisfiability problem: From an analytic solution to an efficient algorithm. Physical Review E 66, 056126 (2002)

    Article  Google Scholar 

  22. Ghallab, M., Howe, A., Knoblock, C., McDermott, D., Ram, A., Veloso, M., Weld, D., Wilkins, D.: PDDL – the planning domain definition language. Technical report, Yale University, New Haven, CT (1998)

    Google Scholar 

  23. 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, Providence (1996)

    MATH  Google Scholar 

  24. Giunchiglia, E., Maratea, M., Tacchella, A.: Dependent and independent variables in propositional satisfiability. In: Flesca, S., Greco, S., Leone, N., Ianni, G. (eds.) JELIA 2002. LNCS (LNAI), vol. 2424, pp. 296–307. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  25. Ostrowski, R., Grégoire, E., Mazure, B., Sais, L.: Recovering and exploiting structural knowledge from cnf formulas. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 185–199. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  26. Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Solving difficult SAT instances in presence of symmetry. In: Proceedings of the 39th Design Automation Conference, New Orleans, LA, pp. 731–736 (2002)

    Google Scholar 

  27. Brafman, R.I.: A simplifier for propositional formulas with many binary clauses. In: Proceedings of the 17th International Joint Conference on Artificial Intelligence, Seattle, WA, pp. 515–522 (2001)

    Google Scholar 

  28. Amir, E., McIlraith, S.A.: Partition-based logical reasoning. In: Proceedings of the 7th International Conference on Principles of Knowledge Representation and Reasoning, Breckenridge, CO, pp. 389–400 (2000)

    Google Scholar 

  29. Shtrichman, O.: Tuning SAT checkers for bounded model checking. In: Proceedings of the 12th International Conference on Computer Aided Verification, Chicago, IL, pp. 480–494 (2000)

    Google Scholar 

  30. Kautz, H.A., Selman, B.: Pushing the envelope: Planning, propositional logic, and stochastic search. In: Proceedings, AAAI 1996: 13th National Conference on Artificial Intelligence, Portland, OR, pp. 1194–1201 (1996)

    Google Scholar 

  31. Bonet, M.L., Esteban, J.L., Galesi, N., Johansen, J.: On the relative complexity of resolution refinements and cutting planes proof systems. SIAM Journal on Computing 30, 1462–1484 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  32. Bonet, M.L., Galesi, N.: A study of proof search algorithms for resolution and polynomial calculus. In: Proceedings 40th Annual Symposium on Foundations of Computer Science, New York, NY, pp. 422–432. IEEE, Los Alamitos (1999)

    Google Scholar 

  33. Ben-Sasson, E., Impagliazzo, R., Wigderson, A.: Near-optimal separation of treelike and general resolution. Technical Report TR00-005, Electronic Colloquium in Computation Complexity (2000), http://www.eccc.uni-trier.de/eccc/

  34. Beame, P., Impagliazzo, R., Pitassi, T., Segerlind, N.: Memoization and DPLL: Formula caching proof systems. In: Proceedings 18th Annual IEEE Conference on Computational Complexity, Aarhus, Denmark (2003) (to appear)

    Google Scholar 

  35. Kautz, H.A., Selman, B.: Planning as satisfiability. In: Proceedings of the 10th European Conference on Artificial Intelligence, Vienna, Austria, pp. 359–363 (1992)

    Google Scholar 

  36. Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, Amsterdam, The Netherlands, pp. 193–207 (1999)

    Google Scholar 

  37. Aziz, A., Tasiran, S., Brayton, R.K.: BDD variable orderings for interacting finite state machines. In: Proceedings of the 31th Design Automation Conference, San Diego, CA, pp. 283–288 (1994)

    Google Scholar 

  38. Harlow, J.E., Brglez, F.: Design of experiments in BDD variable ordering: Lessons learned. In: Proceedings of the International Conference on Computer Aided Design, San Jose, CA, pp. 646–652 (1998)

    Google Scholar 

  39. Hulgaard, H., Williams, P.F., Andersen, H.R.: Equivalence checking of combinational circuits using boolean expression diagrams. IEEE Transactions on Computer-Aided Design of Integrated Circuits 18, 903–917 (1999)

    Article  Google Scholar 

  40. Reda, S., Drechsler, R., Orailoglu, A.: On the relation between SAT and BDDs for equivalence checking. In: Proceedings of the International Symposium on Quality Electronic Design, San Jose, CA, pp. 394–399 (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science and Engineering, University of Washington, Seattle, WA, 98195-2350, USA

    Ashish Sabharwal, Paul Beame & Henry Kautz

Authors
  1. Ashish Sabharwal
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paul Beame
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Henry Kautz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. DIST, Università di Genova, Viale Causa, 13, 16145, Genova, Italy

    Enrico Giunchiglia  & Armando Tacchella  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sabharwal, A., Beame, P., Kautz, H. (2004). Using Problem Structure for Efficient Clause Learning. In: Giunchiglia, E., Tacchella, A. (eds) Theory and Applications of Satisfiability Testing. SAT 2003. Lecture Notes in Computer Science, vol 2919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24605-3_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24605-3_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20851-8

  • Online ISBN: 978-3-540-24605-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation