Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing

  • Conference paper
Theory and Applications of Satisfiability Testing - SAT 2009 (SAT 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5584))

Abstract

In this paper we present the parallel QBF Solver PaQuBE. This new solver leverages the additional computational power that can be exploited from modern computer architectures, from pervasive multicore boxes to clusters and grids, to solve more relevant instances and faster than previous generation solvers. PaQuBE extends QuBE, its sequential core, by providing a Master/Slave Message Passing Interface (MPI) based design that allows it to split the problem up over an arbitrary number of distributed processes. Furthermore, PaQuBE’s progressive parallel framework is the first to support advanced knowledge sharing in which solution cubes as well as conflict clauses can be shared. According to the last QBF Evaluation, QuBE is the most powerful state-of-the-art QBF Solver. It was able to solve more than twice as many benchmarks as the next best independent solver. Our results here, show that PaQuBE provides additional speedup, solving even more instances, faster.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Herbstritt, M., Becker, B.: On Combining 01X-Logic and QBF. In: Moreno Díaz, R., Pichler, F., Quesada Arencibia, A. (eds.) EUROCAST 2007. LNCS, vol. 4739, pp. 531–538. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  2. Dershowitz, N., Hanna, Z., Katz, J.: Bounded model checking with QBF. In: Bacchus, F., Walsh, T. (eds.) SAT 2005, vol. 3569, pp. 408–414. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  3. Rintanen, J.: Constructing conditional plans by a theorem prover. Journal of Artificial Intelligence Research 10, 323–352 (1999)

    MathSciNet  MATH  Google Scholar 

  4. Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem proving. Communication of ACM 5(7), 394–397 (1962)

    Article  MathSciNet  MATH  Google Scholar 

  5. Gent, I.P., Rowley, A.G.: Solution learning and solution directed backjumping revisited. Technical Report APES-80-2004, APES Research Group (February 2004), http://www.dcs.st-and.ac.uk/~apes/apesreports.html

  6. Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause/term resolution and learning in the evaluation of quantified Boolean formulas. Journal of Artificial Intelligence Research (JAIR) 26, 371–416 (2006)

    MathSciNet  MATH  Google Scholar 

  7. Kleine-Büning, H., Karpinski, M., Flögel, A.: Resolution for quantified Boolean formulas. Information and Computation 117(1), 12–18 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  8. Zhang, L., Malik, S.: Towards a symmetric treatment of satisfaction and conflicts in quantified Boolean formula evaluation. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 200–215. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  9. Giunchiglia, E., Marin, P., Narizzano, M.: An effective preprocessor for QBF pre-reasoning (2008)

    Google Scholar 

  10. Samulowitz, H., Davies, J., Bacchus, F.: Preprocessing QBF. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 514–529. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  11. Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE++: An efficient QBF solver. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 201–213. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  12. Giunchiglia, E., Marin, P., Narizzano, M.: 24. In: Reasoning with Quantified Boolean Formulas. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 761–780. IOS Press, Amsterdam (2009)

    Google Scholar 

  13. Zhang, H., Bonacina, M.P., Hsiang, J.: Psato: a distributed propositional prover and its application to quasigroup problems. J. Symb. Comput. 21(4-6), 543–560 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  14. Lewis, M., Schubert, T., Becker, B.: QMiraXT – A Multithreaded QBF Solver. In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (January 2009)

    Google Scholar 

  15. Yu, Y., Malik, S.: Validating the result of a quantified boolean formula (QBF) solver: theory and practice. In: Tang, T.A. (ed.) ASP-DAC, pp. 1047–1051. ACM Press, New York (2005)

    Chapter  Google Scholar 

  16. Feldmann, R., Monien, B., Schamberger, S.: A distributed algorithm to evaluate Quantified Boolean Formulae. In: Proc. AAAI (2000)

    Google Scholar 

  17. Biere, A.: Resolve and expand. In: Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  18. Lonsing, F., Biere, A.: Nenofex: Expanding nnf for QBF solving. In: Büning, H.K., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 196–210. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  19. Benedetti, M.: sKizzo: A suite to evaluate and certify QBFs. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol. 3632, pp. 369–376. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  20. Gent, I.P., Hoos, H.H., Rowley, A.G.D., Smyth, K.: Using stochastic local search to solve quantified Boolean formulae. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 348–362. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  21. Pulina, L., Tacchella, A.: A multi-engine solver for quantified Boolean formulas. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 574–589. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  22. Samulowitz, H., Memisevic, R.: Learning to solve QBF. In: Proc. AAAI, pp. 255–260 (2007)

    Google Scholar 

  23. Chrabakh, W., Wolski, R.: Gridsat: A chaff-based distributed sat solver for the grid. In: SC 2003: Proceedings of the 2003 ACM/IEEE conference on Supercomputing, Washington, DC, USA, p. 37. IEEE Computer Society, Los Alamitos (2003)

    Google Scholar 

  24. Lewis, M., Schubert, T., Becker, B.: Multithreaded SAT Solving. In: ASP Design Automation Conf., Yokohama, Japan (January 2007)

    Google Scholar 

  25. Feldmann, R., Monien, B., Schamberger, S.: A distributed algorithm to evaluate Quantified Boolean Formulae. In: Proceedings of the 7th Conference on Artificial Intelligence (AAAI 2000) and of the 12th Conference on Innovative Applications of Artificial Intelligence (IAAI 2000), July 30-3, pp. 285–290. AAAI Press, Menlo Park (2000)

    Google Scholar 

  26. Gropp, W., Lusk, E., Doss, N., Skjellum, A.: A high-performance, portable implementation of the MPI message passing interface standard. Parallel Computing 22(6), 789–828 (1996)

    Article  MATH  Google Scholar 

  27. Snir, M., Otto, S., Walker, D., Dongarra, J., Huss-Lederman, S.: MPI: The Complete Reference. MIT Press, Cambridge (1995)

    Google Scholar 

  28. Giunchiglia, E., Narizzano, M., Tacchella, A.: Quantified Boolean Formulas satisfiability library (QBFLIB) (2001), www.qbflib.org

Download references

Authors
  1. Matthew Lewis
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paolo Marin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Tobias Schubert
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Massimo Narizzano
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Bernd Becker
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Enrico Giunchiglia
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, Swansea University, Faraday Building, Singleton Park, SA2 8PP, Swansea, UK

    Oliver Kullmann

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lewis, M., Marin, P., Schubert, T., Narizzano, M., Becker, B., Giunchiglia, E. (2009). PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing. In: Kullmann, O. (eds) Theory and Applications of Satisfiability Testing - SAT 2009. SAT 2009. Lecture Notes in Computer Science, vol 5584. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02777-2_46

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02777-2_46

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02776-5

  • Online ISBN: 978-3-642-02777-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation