{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T16:58:53Z","timestamp":1743008333751,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031308222"},{"type":"electronic","value":"9783031308239"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Over the last years, innovative parallel and distributed SAT solving techniques were presented that could impressively exploit the power of modern hardware and cloud systems. Two approaches were particularly successful: (1) search-space splitting in a Divide-and-Conquer (D &amp;C) manner and (2) portfolio-based solving. The latter executes different solvers or configurations of solvers in parallel. For quantified Boolean formulas (QBFs), the extension of propositional logic with quantifiers, there is surprisingly little recent work in this direction compared to SAT.<\/jats:p><jats:p>In this paper, we present <jats:sc>ParaQooba<\/jats:sc>, a novel framework for parallel and distributed QBF solving which combines D &amp;C parallelization and distribution with portfolio-based solving. Our framework is designed in such a way that it can be easily extended and arbitrary sequential QBF solvers can be integrated out of the box, without any programming effort. We show how <jats:sc>ParaQooba<\/jats:sc> orchestrates the collaboration of different solvers for joint problem solving by performing an extensive evaluation on benchmarks from QBFEval\u201922, the most recent QBF competition.<\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_22","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T20:19:12Z","timestamp":1682108352000},"page":"426-447","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7297-6000","authenticated-orcid":false,"given":"Maximilian","family":"Heisinger","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3267-4494","authenticated-orcid":false,"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7170-9242","authenticated-orcid":false,"given":"Armin","family":"Biere","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"22_CR1","doi-asserted-by":"publisher","unstructured":"Balyo, T., Lonsing, F.: HordeQBF: A modular and massively parallel QBF solver. In: Creignou, N., Berre, D.L. (eds.) Proc. of the 19th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT). Lecture Notes in Computer Science, vol.\u00a09710, pp. 531\u2013538. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_33","DOI":"10.1007\/978-3-319-40970-2_33"},{"key":"22_CR2","doi-asserted-by":"publisher","unstructured":"Beyersdorff, O., Janota, M., Lonsing, F., Seidl, M.: Quantified boolean formulas. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 1177\u20131221. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA201015","DOI":"10.3233\/FAIA201015"},{"key":"22_CR3","doi-asserted-by":"publisher","unstructured":"Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bj\u00f8rner, N.S., Sofronie-Stokkermans, V. (eds.) Proc. of the 23rd Int.\u00a0Conf.\u00a0on Automated Deduction (CADE). Lecture Notes in Computer Science, vol.\u00a06803, pp. 101\u2013115. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_10","DOI":"10.1007\/978-3-642-22438-6_10"},{"key":"22_CR4","unstructured":"Feldmann, R., Monien, B., Schamberger, S.: A distributed algorithm to evaluate quantified boolean formulae. In: Kautz, H.A., Porter, B.W. (eds.) Proc.\u00a0of the 17th Nat.\u00a0Conf.\u00a0on Artificial Intelligence and 12th Conf.\u00a0on on Innovative Applications of Artificial Intelligence (AAAI\/IAAI). pp. 285\u2013290. AAAI Press \/ The MIT Press (2000), http:\/\/www.aaai.org\/Library\/AAAI\/2000\/aaai00-044.php"},{"key":"22_CR5","doi-asserted-by":"publisher","unstructured":"Frioux, L.L., Baarir, S., Sopena, J., Kordon, F.: Modular and efficient divide-and-conquer SAT solver on top of the painless framework. In: Vojnar, T., Zhang, L. (eds.) Proc. of the 25th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 11427, pp. 135\u2013151. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_8","DOI":"10.1007\/978-3-030-17462-0_8"},{"key":"22_CR6","unstructured":"Heisinger, M.: Distributed SAT & QBF solving: The paracooba framework. Master Thesis, JKU Linz (2021)"},{"key":"22_CR7","doi-asserted-by":"publisher","unstructured":"Heisinger, M., Fleury, M., Biere, A.: Distributed cube and conquer with paracooba. In: Pulina, L., Seidl, M. (eds.) Proc. of the 23rd Int. Conf. on Theory and Applications of Satisfiability Testing (SAT). Lecture Notes in Computer Science, vol. 12178, pp. 114\u2013122. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_9","DOI":"10.1007\/978-3-030-51825-7_9"},{"key":"22_CR8","doi-asserted-by":"publisher","unstructured":"Heisinger, M., Seidl, M., Biere, A.: Artifact for Paper ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving (Nov 2022). https:\/\/doi.org\/10.5281\/zenodo.7554207","DOI":"10.5281\/zenodo.7554207"},{"key":"22_CR9","unstructured":"Heisinger, M., Seidl, M., Biere, A.: QuAPI: Adding assumptions to non-assuming SAT & QBF solvers. In: Konev, B., Schon, C., Steen, A. (eds.) Proc.\u00a0of the Workshop on Practical Aspects of Automated Reasoning (FLoC\/IJCAR). CEUR Workshop Proceedings, vol.\u00a03201. CEUR-WS.org (2022), http:\/\/ceur-ws.org\/Vol-3201\/paper1.pdf"},{"key":"22_CR10","doi-asserted-by":"publisher","unstructured":"Heule, M., J\u00e4rvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. J. Artif. Intell. Res. 53, 127\u2013168 (2015). https:\/\/doi.org\/10.1613\/jair.4694","DOI":"10.1613\/jair.4694"},{"key":"22_CR11","doi-asserted-by":"publisher","unstructured":"Heule, M., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: Guiding CDCL SAT solvers by lookaheads. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) Proc. of the 7th Int. Conf. on Hardware and Software: Verification and Testing (HVC). Lecture Notes in Computer Science, vol.\u00a07261, pp. 50\u201365. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-34188-5_8","DOI":"10.1007\/978-3-642-34188-5_8"},{"key":"22_CR12","doi-asserted-by":"publisher","unstructured":"Hoos, H.H., Peitl, T., Slivovsky, F., Szeider, S.: Portfolio-based algorithm selection for circuit QBFs. In: Hooker, J.N. (ed.) Proc. of the 24th Int. Conf. on Principles and Practice of Constraint Programming (CP). Lecture Notes in Computer Science, vol. 11008, pp. 195\u2013209. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-98334-9_13","DOI":"10.1007\/978-3-319-98334-9_13"},{"key":"22_CR13","doi-asserted-by":"publisher","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) Proc. of the 15th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT). Lecture Notes in Computer Science, vol.\u00a07317, pp. 114\u2013128. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_10","DOI":"10.1007\/978-3-642-31612-8_10"},{"key":"22_CR14","doi-asserted-by":"publisher","unstructured":"Jordan, C., Kaiser, L., Lonsing, F., Seidl, M.: MPIDepQBF: Towards parallel QBF solving without knowledge sharing. In: Sinz, C., Egly, U. (eds.) Proc. of the 17th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT). Lecture Notes in Computer Science, vol.\u00a08561, pp. 430\u2013437. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_32","DOI":"10.1007\/978-3-319-09284-3_32"},{"key":"22_CR15","unstructured":"Kaufmann, D., Kauers, M., Biere, A., Cok, D.: Arithmetic verification problems submitted to the SAT Race 2019. In: Heule, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proc.\u00a0of SAT Race 2019 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2019-1, p.\u00a049. University of Helsinki (2019)"},{"key":"22_CR16","doi-asserted-by":"publisher","unstructured":"Lewis, M., Schubert, T., Becker, B., Marin, P., Narizzano, M., Giunchiglia, E.: Parallel QBF solving with advanced knowledge sharing. Fundam. Informaticae 107(2-3), 139\u2013166 (2011). https:\/\/doi.org\/10.3233\/FI-2011-398","DOI":"10.3233\/FI-2011-398"},{"key":"22_CR17","doi-asserted-by":"publisher","unstructured":"Lonsing, F., Egly, U.: DepQBF 6.0: A search-based QBF solver beyond traditional QCDCL. In: de\u00a0Moura, L. (ed.) Proc. of the 26th Int.\u00a0Conf.\u00a0on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 10395, pp. 371\u2013384. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_23","DOI":"10.1007\/978-3-319-63046-5_23"},{"key":"22_CR18","doi-asserted-by":"publisher","unstructured":"Lonsing, F., Seidl, M.: Parallel solving of quantified boolean formulas. In: Hamadi, Y., Sais, L. (eds.) Handbook of Parallel Constraint Reasoning, pp. 101\u2013139. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-63516-3_4","DOI":"10.1007\/978-3-319-63516-3_4"},{"key":"22_CR19","doi-asserted-by":"publisher","unstructured":"Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 133\u2013182. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA200987","DOI":"10.3233\/FAIA200987"},{"key":"22_CR20","doi-asserted-by":"publisher","unstructured":"Mayer-Eichberger, V., Saffidine, A.: Positional games and QBF: The corrective encoding. In: Pulina, L., Seidl, M. (eds.) Proc. of the 23rd Int. Conf. on Theory and Applications of Satisfiability Testing (SAT). Lecture Notes in Computer Science, vol. 12178, pp. 447\u2013463. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_31","DOI":"10.1007\/978-3-030-51825-7_31"},{"key":"22_CR21","doi-asserted-by":"publisher","unstructured":"Pulina, L., Seidl, M.: The 2016 and 2017 QBF solvers evaluations (QBFEVAL\u201916 and QBFEVAL\u201917). Artif. Intell. 274, 224\u2013248 (2019). https:\/\/doi.org\/10.1016\/j.artint.2019.04.002","DOI":"10.1016\/j.artint.2019.04.002"},{"key":"22_CR22","unstructured":"Pulina, L., Seidl, M., Shukla, A.: QBFEval 2022. http:\/\/www.qbflib.org\/qbfeval22.php (2022)"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Rabe, M.N., Tentrup, L.: CAQE: A certifying QBF solver. In: Kaivola, R., Wahl, T. (eds.) Proc. of the Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD). pp. 136\u2013143. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542263"},{"key":"22_CR24","doi-asserted-by":"publisher","unstructured":"Sanders, P., Schreiber, D.: Mallob: Scalable SAT solving on demand with decentralized job scheduling. J. Open Source Softw. 7(77), \u00a04591 (2022). https:\/\/doi.org\/10.21105\/joss.04591","DOI":"10.21105\/joss.04591"},{"key":"22_CR25","doi-asserted-by":"publisher","unstructured":"Shaik, I., Mayer-Eichberger, V., van\u00a0de Pol, J., Saffidine, A.: Implicit state and goals in QBF encodings for positional games (extended version) (2023). https:\/\/doi.org\/10.48550\/ARXIV.2301.07345","DOI":"10.48550\/ARXIV.2301.07345"},{"key":"22_CR26","doi-asserted-by":"publisher","unstructured":"Shukla, A., Biere, A., Pulina, L., Seidl, M.: A survey on applications of quantified boolean formulas. In: Proc. of the 31st IEEE Int.\u00a0Conf.\u00a0on Tools with Artificial Intelligence (ICTAI). pp. 78\u201384. IEEE (2019). https:\/\/doi.org\/10.1109\/ICTAI.2019.00020","DOI":"10.1109\/ICTAI.2019.00020"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,4]],"date-time":"2023-08-04T10:05:19Z","timestamp":1691143519000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"169","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"56","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}