{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:20:43Z","timestamp":1781076043777,"version":"3.54.1"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319409696","type":"print"},{"value":"9783319409702","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40970-2_33","type":"book-chapter","created":{"date-parts":[[2016,6,10]],"date-time":"2016-06-10T11:14:55Z","timestamp":1465557295000},"page":"531-538","source":"Crossref","is-referenced-by-count":5,"title":["HordeQBF: A Modular and Massively Parallel QBF Solver"],"prefix":"10.1007","author":[{"given":"Tom\u00e1\u0161","family":"Balyo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florian","family":"Lonsing","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,6,11]]},"reference":[{"issue":"1","key":"33_CR1","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/s10703-012-0152-6","volume":"41","author":"V Balabanov","year":"2012","unstructured":"Balabanov, V., Jiang, J.R.: Unified QBF certification and its applications. Formal Meth. Syst. Des. 41(1), 45\u201365 (2012)","journal-title":"Formal Meth. Syst. Des."},{"key":"33_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/978-3-319-09284-3_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"V Balabanov","year":"2014","unstructured":"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\u2013169. Springer, Heidelberg (2014)"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/978-3-319-24318-4_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"T Balyo","year":"2015","unstructured":"Balyo, T., Sanders, P., Sinz, C.: HordeSat: A massively parallel portfolio SAT solver. In: Heule, M. (ed.) SAT 2015. LNCS, vol. 9340, pp. 156\u2013172. Springer, Heidelberg (2015)"},{"issue":"2\u20134","key":"33_CR4","first-page":"75","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A.: PicoSAT essentials. JSAT 4(2\u20134), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"33_CR5","unstructured":"Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified boolean formulae. In: AAAI, pp. 262\u2013267. AAAI Press \/ The MIT Press (1998)"},{"key":"33_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"33_CR7","unstructured":"Feldmann, R., Monien, B., Schamberger, S.: A distributed algorithm to evaluate quantified boolean formulae. In: AAAI, pp. 285\u2013290. AAAI Press \/ The MIT Press (2000)"},{"issue":"2\u20133","key":"33_CR8","first-page":"83","volume":"7","author":"E Giunchiglia","year":"2010","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: QuBE7.0. JSAT 7(2\u20133), 83\u201388 (2010)","journal-title":"JSAT"},{"key":"33_CR9","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1613\/jair.1959","volume":"26","author":"E Giunchiglia","year":"2006","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause\/Term resolution and learning in the evaluation of quantified boolean formulas. JAIR 26, 371\u2013416 (2006)","journal-title":"JAIR"},{"issue":"6","key":"33_CR10","doi-asserted-by":"crossref","first-page":"789","DOI":"10.1016\/0167-8191(96)00024-5","volume":"22","author":"W Gropp","year":"1996","unstructured":"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\u2013828 (1996)","journal-title":"Parallel Comput."},{"key":"33_CR11","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1613\/jair.4694","volume":"53","author":"M Heule","year":"2015","unstructured":"Heule, M., J\u00e4rvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. J. Artif. Intell. Res. (JAIR) 53, 127\u2013168 (2015)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"33_CR12","first-page":"187","volume":"9","author":"M Janota","year":"2016","unstructured":"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\u2013206 (2016)","journal-title":"JSAT"},{"key":"33_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1007\/978-3-319-09284-3_32","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"C Jordan","year":"2014","unstructured":"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\u2013437. Springer, Heidelberg (2014)"},{"issue":"1","key":"33_CR14","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H Kleine B\u00fcning","year":"1995","unstructured":"Kleine B\u00fcning, H., Karpinski, M., Fl\u00f6gel, A.: A resolution for quantified boolean formulas. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"33_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/3-540-45616-3_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R Letz","year":"2002","unstructured":"Letz, R.: Lemma and model caching in decision procedures for quantified boolean formulas. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 160\u2013175. Springer, Heidelberg (2002)"},{"key":"33_CR16","unstructured":"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)"},{"issue":"2\u20133","key":"33_CR17","doi-asserted-by":"crossref","first-page":"139","DOI":"10.3233\/FI-2011-398","volume":"107","author":"M Lewis","year":"2011","unstructured":"Lewis, M., Schubert, T., Becker, B., Marin, P., Narizzano, M., Giunchiglia, E.: Parallel QBF solving with advanced knowledge sharing. Fundamenta Informaticae 107(2\u20133), 139\u2013166 (2011)","journal-title":"Fundamenta Informaticae"},{"key":"33_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"418","DOI":"10.1007\/978-3-662-48899-7_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F Lonsing","year":"2015","unstructured":"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\u2013433. Springer, Heidelberg (2015)"},{"issue":"2\u20133","key":"33_CR19","first-page":"71","volume":"7","author":"F Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DepQBF: A dependency-aware QBF solver. JSAT 7(2\u20133), 71\u201376 (2010)","journal-title":"JSAT"},{"key":"33_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/978-3-642-14186-7_14","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"F Lonsing","year":"2010","unstructured":"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\u2013171. Springer, Heidelberg (2010)"},{"key":"33_CR21","doi-asserted-by":"crossref","unstructured":"Mota, B.D., Nicolas, P., St\u00e9phan, I.: A new parallel architecture for QBF tools. In: Proceedings of the International Conferference on High Performance Computing and Simulation (HPCS 2010), pp. 324\u2013330. IEEE (2010)","DOI":"10.1109\/HPCS.2010.5547114"},{"key":"33_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/978-3-540-72788-0_28","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"K Pipatsrisawat","year":"2007","unstructured":"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\u2013299. Springer, Heidelberg (2007)"},{"issue":"2\u20133","key":"33_CR23","first-page":"65","volume":"7","author":"L Pulina","year":"2010","unstructured":"Pulina, L., Tacchella, A.: AQME\u201910. JSAT 7(2\u20133), 65\u201370 (2010)","journal-title":"JSAT"},{"key":"33_CR24","doi-asserted-by":"crossref","unstructured":"Vautard, J., Lallouet, A., Hamadi, Y.: A parallel solving algorithm for quantified constraints problems. In: ICTAI, pp. 271\u2013274. IEEE Computer Society (2010)","DOI":"10.1109\/ICTAI.2010.46"},{"issue":"4","key":"33_CR25","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1006\/jsco.1996.0030","volume":"21","author":"H Zhang","year":"1996","unstructured":"Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: A distributed propositional prover and its application to quasigroup problems. J. Symb. Comput. 21(4), 543\u2013560 (1996)","journal-title":"J. Symb. Comput."},{"key":"33_CR26","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: ICCAD, pp. 442\u2013449. ACM \/ IEEE Computer Society (2002)","DOI":"10.1145\/774572.774637"},{"key":"33_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-46135-3_14","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"L Zhang","year":"2002","unstructured":"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\u2013215. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40970-2_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,22]],"date-time":"2020-09-22T01:27:42Z","timestamp":1600738062000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40970-2_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319409696","9783319409702"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40970-2_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}