Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theory and Applications of Satisfiability Testing

SAT 2016: Theory and Applications of Satisfiability Testing – SAT 2016 pp 531–538Cite as

HordeQBF: A Modular and Massively Parallel QBF Solver

  • Conference paper
  • First Online:

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

Abstract

The recently developed massively parallel satisfiability (SAT) solver HordeSAT was designed in a modular way to allow the integration of any sequential CDCL-based SAT solver in its core. We integrated the QCDCL-based quantified Boolean formula (QBF) solver DepQBF in HordeSAT to obtain a massively parallel QBF solver—HordeQBF. In this paper we describe the details of this integration and report on results of the experimental evaluation of HordeQBF’s performance. HordeQBF achieves superlinear average and median speedup on the hard application instances of the 2014 QBF Gallery.

T. Balyo—Supported by DFG project SA 933/11-1.

F. Lonsing—Supported by the Austrian Science Fund (FWF) under grant S11409-N23.

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 EPUB and 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

Notes

  1. 1.

    http://lonsing.github.io/depqbf/.

References

  1. Balabanov, V., Jiang, J.R.: Unified QBF certification and its applications. Formal Meth. Syst. Des. 41(1), 45–65 (2012)

    Article  MATH  Google Scholar 

  2. Balabanov, V., Widl, M., Jiang, J.H.R.: QBF resolution systems and their proof complexities. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 154–169. Springer, Heidelberg (2014)

    Google Scholar 

  3. Balyo, T., Sanders, P., Sinz, C.: HordeSat: A massively parallel portfolio SAT solver. In: Heule, M. (ed.) SAT 2015. LNCS, vol. 9340, pp. 156–172. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  4. Biere, A.: PicoSAT essentials. JSAT 4(2–4), 75–97 (2008)

    MATH  Google Scholar 

  5. Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified boolean formulae. In: AAAI, pp. 262–267. AAAI Press / The MIT Press (1998)

    Google Scholar 

  6. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  7. Feldmann, R., Monien, B., Schamberger, S.: A distributed algorithm to evaluate quantified boolean formulae. In: AAAI, pp. 285–290. AAAI Press / The MIT Press (2000)

    Google Scholar 

  8. Giunchiglia, E., Marin, P., Narizzano, M.: QuBE7.0. JSAT 7(2–3), 83–88 (2010)

    Google Scholar 

  9. Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause/Term resolution and learning in the evaluation of quantified boolean formulas. JAIR 26, 371–416 (2006)

    MathSciNet  MATH  Google Scholar 

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

    Article  MATH  Google Scholar 

  11. Heule, M., Järvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. J. Artif. Intell. Res. (JAIR) 53, 127–168 (2015)

    MathSciNet  MATH  Google Scholar 

  12. Janota, M., Jordan, C., Klieber, W., Lonsing, F., Seidl, M., Van Gelder, A.: The QBF Gallery 2014: The QBF competition at the FLoC olympic games. JSAT 9, 187–206 (2016)

    Google Scholar 

  13. Jordan, C., Kaiser, L., Lonsing, F., Seidl, M.: MPIDepQBF: Towards parallel QBF solving without knowledge sharing. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 430–437. Springer, Heidelberg (2014)

    Google Scholar 

  14. Kleine Büning, H., Karpinski, M., Flögel, A.: A resolution for quantified boolean formulas. Inf. Comput. 117(1), 12–18 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  15. 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)

    Chapter  Google Scholar 

  16. Lewis, M., Schubert, T., Becker, B.: QMiraXT - a multithreaded QBF solver. In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV) (2009)

    Google Scholar 

  17. Lewis, M., Schubert, T., Becker, B., Marin, P., Narizzano, M., Giunchiglia, E.: Parallel QBF solving with advanced knowledge sharing. Fundamenta Informaticae 107(2–3), 139–166 (2011)

    MathSciNet  Google Scholar 

  18. Lonsing, F., Bacchus, F., Biere, A., Egly, U., Seidl, M.: Enhancing search-based QBF solving by dynamic blocked clause elimination. In: Davis, M. (ed.) LPAR-20 2015. LNCS, vol. 9450, pp. 418–433. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  19. Lonsing, F., Biere, A.: DepQBF: A dependency-aware QBF solver. JSAT 7(2–3), 71–76 (2010)

    Google Scholar 

  20. Lonsing, F., Biere, A.: Integrating dependency schemes in search-based QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 158–171. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  21. Mota, B.D., Nicolas, P., Stéphan, I.: A new parallel architecture for QBF tools. In: Proceedings of the International Conferference on High Performance Computing and Simulation (HPCS 2010), pp. 324–330. IEEE (2010)

    Google Scholar 

  22. Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 294–299. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  23. Pulina, L., Tacchella, A.: AQME’10. JSAT 7(2–3), 65–70 (2010)

    Google Scholar 

  24. Vautard, J., Lallouet, A., Hamadi, Y.: A parallel solving algorithm for quantified constraints problems. In: ICTAI, pp. 271–274. IEEE Computer Society (2010)

    Google Scholar 

  25. Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: A distributed propositional prover and its application to quasigroup problems. J. Symb. Comput. 21(4), 543–560 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  26. Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: ICCAD, pp. 442–449. ACM / IEEE Computer Society (2002)

    Google Scholar 

  27. 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 

Download references

Author information

Authors and Affiliations

  1. Karlsruhe Institute of Technology (KIT), Karlsruhe, Germany

    Tomáš Balyo

  2. Knowledge-Based Systems Group, Vienna University of Technology, Vienna, Austria

    Florian Lonsing

Authors
  1. Tomáš Balyo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Florian Lonsing
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Florian Lonsing .

Editor information

Editors and Affiliations

  1. Aix-Marseille Université, Marseille, France

    Nadia Creignou

  2. Université d'Artois, Lens, France

    Daniel Le Berre

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Balyo, T., Lonsing, F. (2016). HordeQBF: A Modular and Massively Parallel QBF Solver. In: Creignou, N., Le Berre, D. (eds) Theory and Applications of Satisfiability Testing – SAT 2016. SAT 2016. Lecture Notes in Computer Science(), vol 9710. Springer, Cham. https://doi.org/10.1007/978-3-319-40970-2_33

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-40970-2_33

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-40969-6

  • Online ISBN: 978-3-319-40970-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation