Advertisement

QuBE++: An Efficient QBF Solver

  • Enrico Giunchiglia
  • Massimo Narizzano
  • Armando Tacchella
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3312)

Abstract

In this paper we describe QuBE++, an efficient solver for Quantified Boolean Formulas (QBFs). To the extent of our knowledge, QuBE++ is the first QBF reasoning engine that uses lazy data structures both for unit clauses propagation and for pure literals detection. QuBE++ also features non-chronological backtracking and a branching heuristic that leverages the information gathered during the backtracking phase. Owing to such techniques and to a careful implementation, QuBE++ turns out to be an efficient and robust solver, whose performances exceed those of other state-of-the-art QBF engines, and are comparable with the best engines currently available on SAT instances.

Keywords

Priority Queue Boolean Formula Symbolic Model Check Runtime Distribution 38th Design Automation 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Scholl, C., Becker, B.: Checking equivalence for partial implementations. In: 38th Design Automation Conference, DAC 2001 (2001)Google Scholar
  2. 2.
    Ayari, A., Basin, D.: Bounded model construction for monadic second-order logics. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 99–113. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  3. 3.
    Rintanen, J.: Constructing conditional plans by a theorem prover. Journal of Artificial Intelligence Research 10, 323–352 (1999)zbMATHGoogle Scholar
  4. 4.
    Castellini, C., Giunchiglia, E., Tacchella, A.: Sat-based planning in complex domains: Concurrency, constraints and nondeterminism. Artificial Intelligence 147(1), 85–117 (2003)zbMATHMathSciNetGoogle Scholar
  5. 5.
    Pan, G., Vardi, M.Y.: Optimizing a BDD-based modal solver. In: Proceedings of the 19th International Conference on Automated Deduction (2003)Google Scholar
  6. 6.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  7. 7.
    Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of Bounded Model Checking at an Industrial Setting. In: Proc. of CAV. LNCS, Springer, Heidelberg (2001)Google Scholar
  8. 8.
    Abdulla, P.A., Bjesse, P., Eén, N.: Symbolic Reachability Analisys Based on SAT-Solvers. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 411–425. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  9. 9.
    Le Berre, D., Simon, L., Tacchella, A.: Challenges in the QBF arena: the SAT 2003 evaluation of QBF solvers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 468–485. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  10. 10.
    Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7(3), 201–215 (1960)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5(7), 394–397 (1962)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Gent, I., Giunchiglia, E., Narizzano, M., Rowley, A., Tachella, A.: Watched data structures for QBF solvers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 348–355. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  13. 13.
    Giunchiglia, E., Narizzano, M., Tacchella, A.: Learning for quantified boolean logic satisfiability. In: Eighteenth National Conference on Artificial Intelligence (AAAI 2002), AAAI Press/MIT Press (2002)Google Scholar
  14. 14.
    Marques-Silva, J.P., Sakallah, K.A.: GRASP - A New Search Algorithm for Satisfiability. In: Proceedings of IEEE/ACM International Conference on Computer-Aided Design, November 1996, pp. 220–227 (1996)Google Scholar
  15. 15.
    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 (DAC 2001), pp. 530–535 (2001)Google Scholar
  16. 16.
    Giunchiglia, E., Maratea, M., Tacchella, A. (In)Effectiveness of Look-Ahead Techniques in a Modern SAT Solver. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 842–846. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  17. 17.
    Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: Proceedings of International Conference on Computer Aided Design, ICCAD 2002 (2002)Google Scholar
  18. 18.
    Giunchiglia, E., Narizzano, M., Tacchella, A.: Backjumping for Quantified Boolean Logic Satisfiability. In: Seventeenth International Joint Conference on Artificial Intelligence (IJCAI 2001). Morgan Kaufmann, San Francisco (2001)Google Scholar
  19. 19.
    Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: International Conference on Computer-Aided Design (ICCAD 2001), pp. 279–285 (2001)Google Scholar
  20. 20.
    Bayardo Jr., R.J., Schrag, R.C.: Using CSP Look-Back Techniques to Solve Real-World SAT instances. In: Proc. of AAAI, pp. 203–208. AAAI Press, Menlo Park (1997)Google Scholar
  21. 21.
    Giunchiglia, E., Narizzano, M., Tacchella, A.: Quantified Boolean Formulas satisfiability library, QBFLIB (2001), http://www.qbflib.org
  22. 22.
    Letz, R.: Lemma and model caching in decision procedures for quantified boolean formulas. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 160–175. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  23. 23.
    Simon, L., Le Berre, D., Hirsch, E.A.: The SAT2002 Competition (2002)Google Scholar
  24. 24.
    Simon, L., Le Berre, D.: The essentials of SAT 2003 Competition. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 452–467. Springer, Heidelberg (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Enrico Giunchiglia
    • 1
  • Massimo Narizzano
    • 1
  • Armando Tacchella
    • 1
  1. 1.DISTUniversità di GenovaGenovaItaly

Personalised recommendations