{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:40:07Z","timestamp":1747593607553,"version":"3.40.5"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031634970"},{"type":"electronic","value":"9783031634987"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T00:00:00Z","timestamp":1719792000000},"content-version":"vor","delay-in-days":182,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Modern solvers for quantified Boolean formulas (QBFs) process formulas in prenex form, which divides each QBF into two parts: the quantifier prefix and the propositional matrix. While this representation does not cover the full language of QBF, every non-prenex formula can be transformed to an equivalent formula in prenex form. This transformation offers several degrees of freedom and blurs structural information that might be useful for the solvers. In a case study conducted 20 years back, it has been shown that the applied transformation strategy heavily impacts solving time. We revisit this work and investigate how sensitive recent QBF solvers perform w.r.t. various prenexing strategies.<\/jats:p>","DOI":"10.1007\/978-3-031-63498-7_20","type":"book-chapter","created":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T19:01:44Z","timestamp":1719774104000},"page":"325-343","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Quantifier Shifting for\u00a0Quantified Boolean Formulas Revisited"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-7630-2791","authenticated-orcid":false,"given":"Simone","family":"Heisinger","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7297-6000","authenticated-orcid":false,"given":"Maximilian","family":"Heisinger","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9234-4377","authenticated-orcid":false,"given":"Adrian","family":"Rebola-Pardo","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3267-4494","authenticated-orcid":false,"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,1]]},"reference":[{"key":"20_CR1","doi-asserted-by":"publisher","unstructured":"Beyersdorff, O., Hinde, L., Pich, J.: Reasons for hardness in QBF proof systems. ACM Trans. Comput. Theory 12(2), 10:1\u201310:27 (2020). https:\/\/doi.org\/10.1145\/3378665","DOI":"10.1145\/3378665"},{"key":"20_CR2","doi-asserted-by":"publisher","unstructured":"Beyersdorff, O., Janota, M., Lonsing, F., Seidl, M.: Quantified Boolean formulas. In: Handbook of Satisfiability \u2013 Second Edition, 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":"20_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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. 6803, pp. 101\u2013115. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_10"},{"key":"20_CR4","unstructured":"Charwat, G., Woltran, S.: BDD-based dynamic programming on tree decompositions. Technical report, Technische Universit\u00e4t Wien, Institut f\u00fcr Informationssysteme, Technical report (2016)"},{"key":"20_CR5","unstructured":"Charwat, G., Woltran, S.: Dynamic programming-based QBF solving. In: Proceedings of the 4th International Workshop on Quantified Boolean Formulas (QBF 2016) co-located with 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016), Bordeaux, France, July 4, 2016. CEUR Workshop Proceedings, vol.\u00a01719, pp. 27\u201340. CEUR-WS.org (2016)"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-540-24605-3_17","volume-title":"Theory and Applications of Satisfiability Testing","author":"U Egly","year":"2004","unstructured":"Egly, U., Seidl, M., Tompits, H., Woltran, S., Zolda, M.: Comparing different prenexing strategies for quantified Boolean formulas. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 214\u2013228. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_17"},{"key":"20_CR7","unstructured":"Egly, U., Seidl, M., Woltran, S.: A solver for QBFS in nonprenex form. In: ECAI 2006, 17th European Conference on Artificial Intelligence, August 29 - September 1, 2006, Riva del Garda, Italy, Including Prestigious Applications of Intelligent Systems (PAIS 2006), Proceedings. Frontiers in Artificial Intelligence and Applications, vol.\u00a0141, pp. 477\u2013481. IOS Press (2006)"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-642-14186-7_29","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"A Goultiaeva","year":"2010","unstructured":"Goultiaeva, A., Bacchus, F.: Exploiting circuit representations in QBF solving. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 333\u2013339. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14186-7_29"},{"key":"20_CR9","doi-asserted-by":"publisher","unstructured":"Hecking-Harbusch, J., Tentrup, L.: Solving QBF by abstraction. In: Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2018, Saarbr\u00fccken, Germany, 26-28th September 2018. EPTCS, vol.\u00a0277, pp. 88\u2013102 (2018). https:\/\/doi.org\/10.4204\/EPTCS.277.7","DOI":"10.4204\/EPTCS.277.7"},{"key":"20_CR10","doi-asserted-by":"publisher","unstructured":"Heisinger, M., Heisinger, S., Seidl, M.: Booleguru, the propositional polyglot. In: Benzm\u00fcller, C., Heule, M., Schmidt, R. (eds.) Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings. LNCS, vol. 14739, p. 315\u2013324. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_19","DOI":"10.1007\/978-3-031-63498-7_19"},{"key":"20_CR11","doi-asserted-by":"publisher","unstructured":"Heisinger, S., Heisinger, M., Rebola-Pardo, A., Seidl, M.: Artifact for \u201cquantifier shifting for quantified Boolean formulas revisited\u201d (2024). https:\/\/doi.org\/10.5281\/zenodo.10634925","DOI":"10.5281\/zenodo.10634925"},{"key":"20_CR12","unstructured":"Janota, M.: QFUN: towards machine learning in QBF. CoRR abs\/1710.02198 (2017)"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-319-94144-8_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"M Janota","year":"2018","unstructured":"Janota, M.: Circuit-based search space pruning in QBF. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 187\u2013198. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_12"},{"key":"20_CR14","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. 7317, pp. 114\u2013128. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_10"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-14186-7_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"W Klieber","year":"2010","unstructured":"Klieber, W., Sapra, S., Gao, S., Clarke, E.: A non-prenex, non-clausal QBF Solver with game-state learning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 128\u2013142. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14186-7_12"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-642-14186-7_14"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-3-319-63046-5_23","volume-title":"Automated Deduction \u2013 CADE 26","author":"F Lonsing","year":"2017","unstructured":"Lonsing, F., Egly, U.: DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 371\u2013384. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_23"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-319-98334-9_19","volume-title":"Principles and Practice of Constraint Programming","author":"F Lonsing","year":"2018","unstructured":"Lonsing, F., Egly, U.: Evaluating QBF solvers: quantifier alternations matter. In: Hooker, J. (ed.) CP 2018. LNCS, vol. 11008, pp. 276\u2013294. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98334-9_19"},{"issue":"1\u20132","key":"20_CR19","doi-asserted-by":"publisher","first-page":"133","DOI":"10.3233\/FI-2016-1445","volume":"149","author":"P Marin","year":"2016","unstructured":"Marin, P., Narizzano, M., Pulina, L., Tacchella, A., Giunchiglia, E.: Twelve years of QBF evaluations: QSAT is PSPACE-Hard and it shows. Fundam. Informaticae 149(1\u20132), 133\u2013158 (2016). https:\/\/doi.org\/10.3233\/FI-2016-1445","journal-title":"Fundam. Informaticae"},{"key":"20_CR20","doi-asserted-by":"publisher","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Handbook of Automated Reasoning (in 2 volumes), pp. 335\u2013367. Elsevier and MIT Press (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50008-4","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-319-66263-3_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"T Peitl","year":"2017","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Dependency learning for QBF. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 298\u2013313. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_19"},{"key":"20_CR22","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1613\/jair.1.11529","volume":"65","author":"T Peitl","year":"2019","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Dependency learning for QBF. J. Artif. Intell. Res. 65, 180\u2013208 (2019). https:\/\/doi.org\/10.1613\/jair.1.11529","journal-title":"J. Artif. Intell. Res."},{"issue":"7\u20138","key":"20_CR23","first-page":"957","volume":"41","author":"G Peterson","year":"2001","unstructured":"Peterson, G., Reif, J., Azhar, S.: Lower bounds for multiplayer noncooperative games of incomplete information. Comput. Math. App. 41(7\u20138), 957\u2013992 (2001)","journal-title":"Comput. Math. App."},{"issue":"3","key":"20_CR24","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"DA Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3), 293\u2013304 (1986). https:\/\/doi.org\/10.1016\/S0747-7171(86)80028-1","journal-title":"J. Symb. Comput."},{"key":"20_CR25","doi-asserted-by":"publisher","unstructured":"Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, September 27-30, 2015. pp. 136\u2013143. IEEE (2015). https:\/\/doi.org\/10.1109\/FMCAD.2015.7542263","DOI":"10.1109\/FMCAD.2015.7542263"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-030-99524-9_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JE Reeves","year":"2022","unstructured":"Reeves, J.E., Heule, M.J.H., Bryant, R.E.: Moving definition variables in quantified Boolean formulas. In: TACAS 2022. LNCS, vol. 13243, pp. 462\u2013479. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_26"},{"issue":"1","key":"20_CR27","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10817-008-9114-5","volume":"42","author":"M Samer","year":"2009","unstructured":"Samer, M., Szeider, S.: Backdoor sets of quantified Boolean formulas. J. Autom. Reason. 42(1), 77\u201397 (2009). https:\/\/doi.org\/10.1007\/s10817-008-9114-5","journal-title":"J. Autom. Reason."},{"key":"20_CR28","doi-asserted-by":"publisher","unstructured":"Shukla, A., Biere, A., Pulina, L., Seidl, M.: A survey on applications of quantified Boolean formulas. In: 31st IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2019, Portland, OR, USA, November 4-6, 2019, pp. 78\u201384. IEEE (2019). https:\/\/doi.org\/10.1109\/ICTAI.2019.00020","DOI":"10.1109\/ICTAI.2019.00020"},{"key":"20_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-319-40970-2_24","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"L Tentrup","year":"2016","unstructured":"Tentrup, L.: Non-prenex QBF solving using abstraction. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 393\u2013401. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_24"},{"key":"20_CR30","doi-asserted-by":"publisher","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning. Symbolic Computation, pp. 466\u2013483. Springer, Berlin, Heidelberg (1983). https:\/\/doi.org\/10.1007\/978-3-642-81955-1_28","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"20_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-662-54577-5_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Wimmer","year":"2017","unstructured":"Wimmer, R., Reimer, S., Marin, P., Becker, B.: HQSpre \u2013 an effective preprocessor for QBF and DQBF. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 373\u2013390. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_21"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63498-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:17:38Z","timestamp":1747592258000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63498-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031634970","9783031634987"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63498-7_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}