{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:25:20Z","timestamp":1740122720711,"version":"3.37.3"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,8,23]],"date-time":"2021-08-23T00:00:00Z","timestamp":1629676800000},"content-version":"vor","delay-in-days":22,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100008332","name":"Graz University of Technology","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100008332","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In recent years, expansion-based techniques have been shown to be very powerful in theory and practice for solving quantified Boolean formulas (QBF), the extension of propositional formulas with existential and universal quantifiers over Boolean variables. Such approaches partially expand one type of variable (either existential or universal) for obtaining a propositional abstraction of the QBF. If this formula is false, the truth value of the QBF is decided, otherwise further refinement steps are necessary. Classically, expansion-based solvers process the given formula quantifier-block wise and use one SAT solver per quantifier block. In this paper, we present a novel algorithm for expansion-based QBF solving that deals with the whole quantifier prefix at once. Hence recursive applications of the expansion principle are avoided and only two incremental SAT solvers are required. While our algorithm is naturally based on the <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\forall $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mo>\u2200<\/mml:mo>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>Exp+Res calculus that is the formal foundation of expansion-based solving, it is conceptually simpler than present recursive approaches. Experiments indicate that the performance of our simple approach is comparable with the state of the art of QBF solving, especially in combination with other solving techniques.<\/jats:p>","DOI":"10.1007\/s10703-021-00371-7","type":"journal-article","created":{"date-parts":[[2021,8,23]],"date-time":"2021-08-23T15:06:03Z","timestamp":1629731163000},"page":"157-177","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations"],"prefix":"10.1007","volume":"57","author":[{"given":"Roderick","family":"Bloem","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Braud-Santoni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vedad","family":"Hadzic","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uwe","family":"Egly","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Lonsing","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,8,23]]},"reference":[{"key":"371_CR1","unstructured":"Alur R, Bod\u00edk R, Dallal E, Fisman D, Garg P, Juniwal G, Kress-Gazit H, Madhusudan P, Martin MMK, Raghothaman M, Saha S, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2015) Syntax-guided synthesis. In: Dependable Software Systems Engineering, volume\u00a040 of NATO Science for Peace and Security Series, D: Information and Communication Security. IOS Press, pp 1\u201325"},{"key":"371_CR2","unstructured":"Audemard G, Simon L (2009) Predicting learnt clauses quality in modern SAT solvers. In: IJCAI, pp 399\u2013404"},{"key":"371_CR3","doi-asserted-by":"crossref","unstructured":"Ayari A, Basin DA (2002) QUBOS: deciding quantified Boolean logic using propositional satisfiability solvers. In: FMCAD, volume 2517 of LNCS. Springer, pp 187\u2013201","DOI":"10.1007\/3-540-36126-X_12"},{"key":"371_CR4","doi-asserted-by":"crossref","unstructured":"Balabanov V, Jiang J-HR, Scholl C, Mishchenko A, Brayton RK (2016) 2QBF: challenges and Solutions. In: SAT, volume 9710 of LNCS. Springer, pp 453\u2013469","DOI":"10.1007\/978-3-319-40970-2_28"},{"key":"371_CR5","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.artint.2016.08.007","volume":"241","author":"T Balyo","year":"2016","unstructured":"Balyo T, Biere A, Iser M, Sinz C (2016) SAT Race 2015. Artif Intell 241:45\u201365","journal-title":"Artif Intell"},{"key":"371_CR6","doi-asserted-by":"crossref","unstructured":"Beyersdorff O, Chew L, Janota M (2014) On unification of QBF resolution-based calculi. In: MFCS, volume 8635 of LNCS. Springer, pp 81\u201393","DOI":"10.1007\/978-3-662-44465-8_8"},{"key":"371_CR7","doi-asserted-by":"crossref","unstructured":"Beyersdorff O, Janota M, Lonsing F, Seidl M (2021) Quantified Boolean formulas. In: Handbook of satisfiability, 2nd edn. Frontiers in artificial intelligence and applications. IOS Press","DOI":"10.3233\/FAIA201015"},{"key":"371_CR8","doi-asserted-by":"crossref","unstructured":"Biere A, Lonsing F, Seidl M (2011) Blocked clause elimination for QBF. In: CADE, volume 6803 of LNCS. Springer, pp 101\u2013115","DOI":"10.1007\/978-3-642-22438-6_10"},{"key":"371_CR9","doi-asserted-by":"crossref","unstructured":"Bloem R, Braud-Santoni N, Hadzic V, Egly U, Lonsing F, Seidl M (2018)Expansion-based QBF solving without recursion. In: FMCAD. IEEE, pp 1\u201310","DOI":"10.23919\/FMCAD.2018.8603004"},{"key":"371_CR10","doi-asserted-by":"crossref","unstructured":"Bloem R, K\u00f6nighofer R, Seidl M (2014) SAT-based synthesis methods for safety specs. In: VMCAI, volume 8318 of LNCS. Springer, pp 1\u201320","DOI":"10.1007\/978-3-642-54013-4_1"},{"key":"371_CR11","unstructured":"Bogaerts B, Janhunen T, Tasharrofi S (2016) SAT-to-SAT in QBFEval 2016. In: QBF workshop, volume 1719 of CEUR workshop proceedings. CEUR-WS.org, pp 63\u201370"},{"key":"371_CR12","doi-asserted-by":"crossref","unstructured":"Bogaerts B, Janhunen T, Tasharrofi S (2016) Solving QBF instances with nested SAT solvers. In: Beyond NP, volume WS-16-05 of AAAI Workshops. AAAI Press","DOI":"10.1017\/S1471068416000387"},{"key":"371_CR13","doi-asserted-by":"crossref","unstructured":"Bubeck U, Kleine B\u00fcning H (2007) Bounded universal expansion for preprocessing QBF. In: SAT, volume 4501 of LNCS. Springer, pp 244\u2013257","DOI":"10.1007\/978-3-540-72788-0_24"},{"key":"371_CR14","unstructured":"Charwat G, Woltran S (2016) Dynamic programming-based QBF solving. In: QBF workshop, volume 1719 of CEUR workshop proceedings. CEUR-WS.org, pp 27\u201340"},{"key":"371_CR15","doi-asserted-by":"crossref","unstructured":"Cheng C-H, Hamza Y, Ruess H (2016) Structural synthesis for GXW specifications. In: CAV, volume 9779 of LNCS. Springer, pp 95\u2013117","DOI":"10.1007\/978-3-319-41528-4_6"},{"key":"371_CR16","doi-asserted-by":"crossref","unstructured":"Cheng C-H, Lee EA, Ruess H (2017) autoCode4: structural controller synthesis. In TACAS, volume 10205 of LNCS. Springer, pp 398\u2013404","DOI":"10.1007\/978-3-662-54577-5_23"},{"issue":"5","key":"371_CR17","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke EM, Grumberg O, Jha S, Yuan L, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50(5):752\u2013794","journal-title":"J ACM"},{"key":"371_CR18","doi-asserted-by":"crossref","unstructured":"Dershowitz N, Hanna Z, Katz J (2005) Bounded model checking with QBF. In: SAT, volume 3569 of LNCS. Springer, pp 408\u2013414","DOI":"10.1007\/11499107_32"},{"issue":"1","key":"371_CR19","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10472-016-9501-2","volume":"80","author":"U Egly","year":"2017","unstructured":"Egly U, Kronegger M, Lonsing F, Pfandler A (2017) Conformant planning as a case study of incremental QBF solving. Ann Math Artif Intell 80(1):21\u201345","journal-title":"Ann Math Artif Intell"},{"key":"371_CR20","doi-asserted-by":"crossref","unstructured":"Faymonville P, Finkbeiner B, Rabe MN, Tentrup L (2017) Encodings of bounded synthesis. In: TACAS, volume 10205 of LNCS. Springer, pp 354\u2013370","DOI":"10.1007\/978-3-662-54577-5_20"},{"issue":"3","key":"371_CR21","first-page":"1","volume":"11","author":"F Bernd","year":"2015","unstructured":"Bernd F, Leander T (2015) Detecting unrealizability of distributed fault-tolerant systems. Logic Methods Comput Sci 11(3):1\u201331","journal-title":"Logic Methods Comput Sci"},{"key":"371_CR22","doi-asserted-by":"crossref","unstructured":"Gasc\u00f3n A, Tiwari A (2014) A synthesized algorithm for interactive consistency. In: NASA formal methods, volume 8430 of LNCS. Springer, pp 270\u2013284","DOI":"10.1007\/978-3-319-06200-6_23"},{"key":"371_CR23","unstructured":"Giunchiglia E, Marin P, Narizzano M (2009) Reasoning with quantified Boolean formulas. In: Handbook of satisfiability, volume 185 of FAIA. IOS Press, pp 761\u2013780"},{"key":"371_CR24","doi-asserted-by":"crossref","unstructured":"Giunchiglia E, Marin P, Narizzano M (2010) sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning. In: SAT, volume 6175 of LNCS. Springer, pp 85\u201398","DOI":"10.1007\/978-3-642-14186-7_9"},{"key":"371_CR25","doi-asserted-by":"publisher","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 (2015) Clause elimination for SAT and QSAT. JAIR 53:127\u2013168","journal-title":"JAIR"},{"key":"371_CR26","doi-asserted-by":"crossref","unstructured":"Heyman T, Smith D, Mahajan Y, Leong L, Abu-Haimed H (2014) Dominant controllability check using QBF-solver and netlist optimizer. In: SAT, volume 8561 of LNCS. Springer, pp 227\u2013242","DOI":"10.1007\/978-3-319-09284-3_18"},{"key":"371_CR27","volume-title":"Towards generalization in QBF solving via machine learning","author":"M Janota","year":"2018","unstructured":"Janota M (2018) Towards generalization in QBF solving via machine learning. AAAI Press, In AAAI"},{"key":"371_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.artint.2016.01.004","volume":"234","author":"M Janota","year":"2016","unstructured":"Janota M, Klieber W, Marques-Silva J, Clarke E (2016) Solving QBF with counterexample guided refinement. Artif Intell 234:1\u201325","journal-title":"Artif Intell"},{"key":"371_CR29","doi-asserted-by":"crossref","unstructured":"Janota M, Klieber W, Marques-Silva J, Clarke EM (2012) Solving QBF with counterexample guided refinement. In: SAT, volume 7317 of LNCS. Springer, pp 114\u2013128","DOI":"10.1007\/978-3-642-31612-8_10"},{"key":"371_CR30","doi-asserted-by":"crossref","unstructured":"Janota M, Marques-Silva J (2013) On propositional QBF expansions and Q-resolution. In: SAT, volume 7962 of LNCS. Springer, pp 67\u201382","DOI":"10.1007\/978-3-642-39071-5_7"},{"key":"371_CR31","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/j.tcs.2015.01.048","volume":"577","author":"M Janota","year":"2015","unstructured":"Janota M, Marques-Silva J (2015) Expansion-based QBF solving versus Q-resolution. Theor Comput Sci 577:25\u201342","journal-title":"Theor Comput Sci"},{"key":"371_CR32","unstructured":"Janota M, Marques-Silva J (2015) Solving QBF by clause selection. In: IJCAI. AAAI Press, pp 325\u2013331"},{"key":"371_CR33","doi-asserted-by":"crossref","unstructured":"Janota M, Silva JPM (2011) Abstraction-based algorithm for 2QBF. In: SAT, volume 6695 of LNCS. Springer, pp 230\u2013244","DOI":"10.1007\/978-3-642-21581-0_19"},{"key":"371_CR34","unstructured":"B\u00fcning HK, Bubeck U (2009) Theory of quantified Boolean formulas. In: Handbook of satisfiability, volume 185 of FAIA. IOS Press, pp 735\u2013760"},{"issue":"1","key":"371_CR35","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"HK B\u00fcning","year":"1995","unstructured":"B\u00fcning HK, Karpinski M, Fl\u00f6gel A (1995) Resolution for quantified Boolean formulas. Inf Comput 117(1):12\u201318","journal-title":"Inf Comput"},{"key":"371_CR36","doi-asserted-by":"crossref","unstructured":"Klieber W, Sapra S, Gao S, Clarke EM (2010) A non-prenex, non-clausal QBF Solver with game-state learning. In: SAT, volume 6175 of LNCS. Springer, pp 128\u2013142","DOI":"10.1007\/978-3-642-14186-7_12"},{"key":"371_CR37","doi-asserted-by":"crossref","unstructured":"Letz R (2002) Lemma and model caching in decision procedures for quantified Boolean formulas. In: TABLEAUX, volume 2381 of LNCS. Springer, pp 160\u2013175","DOI":"10.1007\/3-540-45616-3_12"},{"key":"371_CR38","doi-asserted-by":"crossref","unstructured":"Lonsing F, Egly U (2017) DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL. In: CADE, volume 10395 of LNCS. Springer, pp 371\u2013384","DOI":"10.1007\/978-3-319-63046-5_23"},{"key":"371_CR39","doi-asserted-by":"crossref","unstructured":"Lonsing F, Egly U (2018) Evaluating QBF solvers: quantifier alternations matter. In: CP, volume 11008 of LNCS. Springer, pp 276\u2013294","DOI":"10.1007\/978-3-319-98334-9_19"},{"key":"371_CR40","doi-asserted-by":"crossref","unstructured":"Lonsing F, Egly U (2019) Qratpre+: effective QBF preprocessing via strong redundancy properties. In: SAT, volume 11628 of LNCS. Springer, pp 203\u2013210","DOI":"10.1007\/978-3-030-24258-9_14"},{"key":"371_CR41","doi-asserted-by":"crossref","unstructured":"Peitl T, Slivovsky F, Szeider S (2017) Dependency Learning for QBF. In: SAT, volume 10491 of LNCS. Springer, pp 298\u2013313","DOI":"10.1007\/978-3-319-66263-3_19"},{"key":"371_CR42","doi-asserted-by":"crossref","unstructured":"Rabe MN, Tentrup L (2015) CAQE: a certifying QBF solver. In: FMCAD. IEEE, pp 136\u2013143","DOI":"10.1109\/FMCAD.2015.7542263"},{"key":"371_CR43","unstructured":"Ranjan DP, Tang D, Malik S (2004) A comparative study of 2QBF algorithms. In: SAT"},{"key":"371_CR44","unstructured":"Rintanen J (2007) Asymptotically optimal encodings of conformant planning in QBF. In: AAAI. AAAI Press, pp 1045\u20131050"},{"key":"371_CR45","doi-asserted-by":"crossref","unstructured":"Shukla A, Biere A, Pulina L, Seidl M (2019) A survey on applications of quantified Boolean formulas. In: ICTAI. IEEE, pp 78\u201384","DOI":"10.1109\/ICTAI.2019.00020"},{"key":"371_CR46","doi-asserted-by":"crossref","unstructured":"Tentrup L (2016) Non-prenex QBF solving using abstraction. In: SAT, volume 9710 of LNCS. Springer, pp 393\u2013401","DOI":"10.1007\/978-3-319-40970-2_24"},{"key":"371_CR47","doi-asserted-by":"crossref","unstructured":"Tentrup L (2017) On expansion and resolution in CEGAR based QBF solving. In: CAV, volume 10427 of LNCS. Springer, pp 475\u2013494","DOI":"10.1007\/978-3-319-63390-9_25"},{"key":"371_CR48","doi-asserted-by":"crossref","unstructured":"Tu K-H, Hsu T-C, Jiang J-HR (2015) QELL: QBF reasoning with extended clause learning and levelized SAT solving. In: SAT, volume 9340 of LNCS. Springer, pp 343\u2013359","DOI":"10.1007\/978-3-319-24318-4_25"},{"issue":"11","key":"371_CR49","doi-asserted-by":"publisher","first-page":"2021","DOI":"10.1109\/JPROC.2015.2455034","volume":"103","author":"Y Vizel","year":"2015","unstructured":"Vizel Y, Weissenbacher G, Malik S (2015) Boolean satisfiability solvers and their applications in model checking. Proc IEEE 103(11):2021\u20132035","journal-title":"Proc IEEE"},{"key":"371_CR50","doi-asserted-by":"crossref","unstructured":"Wimmer R, Reimer S, Marin P, Becker B (2017) Hqspre\u2014an effective preprocessor for QBF and DQBF. In: TACAS, volume 10205 of LNCS, pp 373\u2013390","DOI":"10.1007\/978-3-662-54577-5_21"},{"key":"371_CR51","doi-asserted-by":"crossref","unstructured":"Zhang L, Malik S (2002) Towards a symmetric treatment of satisfaction and conflicts in quantified Boolean formula evaluation. In: CP, volume 2470 of LNCS. Springer, pp 200\u2013215","DOI":"10.1007\/3-540-46135-3_14"},{"key":"371_CR52","doi-asserted-by":"crossref","unstructured":"Zhang W (2014) QBF encoding of temporal properties and QBF-based verification. In: IJCAR, volume 8562 of LNCS. Springer, pp 224\u2013239","DOI":"10.1007\/978-3-319-08587-6_16"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00371-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00371-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00371-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,9]],"date-time":"2021-11-09T18:13:57Z","timestamp":1636481637000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00371-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8]]},"references-count":52,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["371"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00371-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2021,8]]},"assertion":[{"value":"16 October 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 March 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 August 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}