×

HordeQBF: a modular and massively parallel QBF solver. (English) Zbl 1475.68429

Creignou, Nadia (ed.) et al., Theory and applications of satisfiability testing – SAT 2016. 19th international conference, Bordeaux, France, July 5–8, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9710, 531-538 (2016).
Summary: 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.
For the entire collection see [Zbl 1337.68009].

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: DOI arXiv

References:

[1] Balabanov, V., Jiang, J.R.: Unified QBF certification and its applications. Formal Meth. Syst. Des. 41(1), 45–65 (2012) · Zbl 1284.68516
[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) · Zbl 1423.68406
[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) · Zbl 1471.68237
[4] Biere, A.: PicoSAT essentials. JSAT 4(2–4), 75–97 (2008) · Zbl 1159.68403
[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) · Zbl 0979.68124
[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) · Zbl 1204.68191
[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)
[8] Giunchiglia, E., Marin, P., Narizzano, M.: QuBE7.0. JSAT 7(2–3), 83–88 (2010)
[9] Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause/Term resolution and learning in the evaluation of quantified boolean formulas. JAIR 26, 371–416 (2006) · Zbl 1183.68475
[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) · Zbl 0875.68206
[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) · Zbl 1336.68231
[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)
[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) · Zbl 1423.68455
[14] Kleine Büning, H., Karpinski, M., Flögel, A.: A resolution for quantified boolean formulas. Inf. Comput. 117(1), 12–18 (1995) · Zbl 0828.68045
[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) · Zbl 1015.68173
[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)
[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)
[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) · Zbl 1471.68251
[19] Lonsing, F., Biere, A.: DepQBF: A dependency-aware QBF solver. JSAT 7(2–3), 71–76 (2010)
[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) · Zbl 1306.68165
[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)
[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) · Zbl 05527216
[23] Pulina, L., Tacchella, A.: AQME’10. JSAT 7(2–3), 65–70 (2010)
[24] Vautard, J., Lallouet, A., Hamadi, Y.: A parallel solving algorithm for quantified constraints problems. In: ICTAI, pp. 271–274. IEEE Computer Society (2010)
[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) · Zbl 0863.68013
[26] Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: ICCAD, pp. 442–449. ACM / IEEE Computer Society (2002)
[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) · Zbl 05876498
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.