{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:20:41Z","timestamp":1781076041443,"version":"3.54.1"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319092836","type":"print"},{"value":"9783319092843","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09284-3_32","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T09:43:21Z","timestamp":1404294201000},"page":"430-437","source":"Crossref","is-referenced-by-count":4,"title":["MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing"],"prefix":"10.1007","author":[{"given":"Charles","family":"Jordan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lukasz","family":"Kaiser","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florian","family":"Lonsing","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"1-4","key":"32_CR1","doi-asserted-by":"crossref","first-page":"133","DOI":"10.3233\/SAT190055","volume":"5","author":"M. Benedetti","year":"2008","unstructured":"Benedetti, M., Mangassarian, H.: QBF-based formal verification: Experience and perspectives. Journal on Satisfiability, Boolean Modeling and Computation\u00a05(1-4), 133\u2013191 (2008)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"32_CR2","unstructured":"Biere, A.: Lingeling, Plingeling and Treengeling Entering the SAT Competition 2013. In: Proc. of the SAT Competition 2013. Dep. of Computer Science Series of Publications B, University of Helsinki, vol. B-2013-1, pp. 51\u201352 (2013)"},{"key":"32_CR3","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-642-22438-6_10","volume-title":"Automated Deduction \u2013 CADE-23","author":"A. Biere","year":"2011","unstructured":"Biere, A., Lonsing, F., Seidl, M.: Blocked Clause Elimination for QBF. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol.\u00a06803, pp. 101\u2013115. Springer, Heidelberg (2011)"},{"key":"32_CR4","unstructured":"B\u00fcning, H.K., Bubeck, U.: Theory of Quantified Boolean Formulas. In: Handbook of Satisfiability, pp. 735\u2013760. IOS Press (2009)"},{"issue":"1","key":"32_CR5","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H.K. B\u00fcning","year":"1995","unstructured":"B\u00fcning, H.K., Karpinski, M., Fl\u00f6gel, A.: Resolution for Quantified Boolean Formulas. Information and Computation\u00a0117(1), 12\u201318 (1995)","journal-title":"Information and Computation"},{"key":"32_CR6","unstructured":"Feldmann, R., Monien, B., Schamberger, S.: A Distributed Algorithm to Evaluate Quantified Boolean Formulae. In: Proc. of the 17th Nat. Conference on Artificial Intelligence (AAAI 2000), pp. 285\u2013290. AAAI (2000)"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: Reasoning with Quantified Boolean Formulas. In: Handbook of Satisfiability, pp. 761\u2013780. IOS Press (2009)","DOI":"10.3233\/978-1-58603-929-5-761"},{"issue":"2-3","key":"32_CR8","doi-asserted-by":"crossref","first-page":"83","DOI":"10.3233\/SAT190079","volume":"7","author":"E. Giunchiglia","year":"2010","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: QuBE7.0. Journal on Satisfiability, Boolean Modeling and Computation\u00a07(2-3), 83\u201388 (2010)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"issue":"1","key":"32_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. Journal of Artificial Intelligence Research\u00a026(1), 371\u2013416 (2006)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-39071-5_8","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"A. Goultiaeva","year":"2013","unstructured":"Goultiaeva, A., Bacchus, F.: Recovering and Utilizing Partial Duality in QBF. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol.\u00a07962, pp. 83\u201399. Springer, Heidelberg (2013)"},{"key":"32_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-31612-8_10","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"M. Janota","year":"2012","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with Counterexample Guided Refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 114\u2013128. Springer, Heidelberg (2012)"},{"key":"32_CR12","unstructured":"Lewis, M., Schubert, T., Becker, B.: QMiraXT \u2013 a multithreaded QBF solver. In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, MBMV (2009)"},{"issue":"2-3","key":"32_CR13","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\u00a0107(2-3), 139\u2013166 (2011)","journal-title":"Fundamenta Informaticae"},{"key":"32_CR14","doi-asserted-by":"crossref","first-page":"71","DOI":"10.3233\/SAT190077","volume":"7","author":"F. Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DepQBF: A dependency-aware QBF solver. Journal on Satisfiability, Boolean Modeling and Computation\u00a07, 71\u201376 (2010)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"32_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-39071-5_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"F. Lonsing","year":"2013","unstructured":"Lonsing, F., Egly, U., Van Gelder, A.: Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol.\u00a07962, pp. 100\u2013115. Springer, Heidelberg (2013)"},{"key":"32_CR16","doi-asserted-by":"crossref","unstructured":"Marin, P., Miller, C., Lewis, M., Becker, B.: Verification of partial designs using incremental QBF solving. In: Proc. of the Int. Conf on Design, Automation & Test in Europe (DATE 2012), pp. 623\u2013628. IEEE (2012)","DOI":"10.1109\/DATE.2012.6176547"},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"Marin, P., Narizzano, M., Giunchiglia, E., Lewis, M.D.T., Schubert, T., Becker, B.: Comparison of knowledge sharing strategies in a parallel QBF solver. In: Proc. of the Int. Conf. on High Performance Computing & Simulation (HPCS 2009), pp. 161\u2013167. IEEE (2009)","DOI":"10.1109\/HPCSIM.2009.5195312"},{"key":"32_CR18","doi-asserted-by":"crossref","unstructured":"Mota, B.D., Nicolas, P., St\u00e9phan, I.: A new parallel architecture for QBF tools. In: Proc. of the Int. Conf. on High Performance Computing and Simulation (HPCS 2010), pp. 324\u2013330. IEEE (2010)","DOI":"10.1109\/HPCS.2010.5547114"},{"key":"32_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-31612-8_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A. Nadel","year":"2012","unstructured":"Nadel, A., Ryvchin, V.: Efficient SAT solving under assumptions. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 242\u2013255. Springer, Heidelberg (2012)"},{"key":"32_CR20","doi-asserted-by":"crossref","unstructured":"Vautard, J., Lallouet, A., Hamadi, Y.: A parallel solving algorithm for quantified constraints problems. In: Proc. of the 22nd IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2010), pp. 271\u2013274. IEEE Computer Society (2010)","DOI":"10.1109\/ICTAI.2010.46"},{"key":"32_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a02470, pp. 200\u2013215. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09284-3_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:52:05Z","timestamp":1746291125000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09284-3_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319092836","9783319092843"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09284-3_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}