{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T16:18:27Z","timestamp":1783009107449,"version":"3.54.5"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,3,24]],"date-time":"2016-03-24T00:00:00Z","timestamp":1458777600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund (AT)","doi-asserted-by":"publisher","award":["S11409-N23"],"award-info":[{"award-number":["S11409-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund (AT)","doi-asserted-by":"publisher","award":["P25518-N23"],"award-info":[{"award-number":["P25518-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft (DE)","doi-asserted-by":"publisher","award":["ER 738\/2-1"],"award-info":[{"award-number":["ER 738\/2-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2017,5]]},"DOI":"10.1007\/s10472-016-9501-2","type":"journal-article","created":{"date-parts":[[2016,3,24]],"date-time":"2016-03-24T01:16:14Z","timestamp":1458782174000},"page":"21-45","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Conformant planning as a case study of incremental QBF solving"],"prefix":"10.1007","volume":"80","author":[{"given":"Uwe","family":"Egly","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Kronegger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florian","family":"Lonsing","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andreas","family":"Pfandler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,3,24]]},"reference":[{"key":"9501_CR1","doi-asserted-by":"crossref","unstructured":"Audemard, G., Lagniez, J.M., Simon, L.: Improving Glucose for incremental SAT solving with assumptions: Application to MUS extraction. In: Proc. SAT 2013, LNCS, vol. 7962, pp. 309\u2013317. Springer (2013)","DOI":"10.1007\/978-3-642-39071-5_23"},{"issue":"1","key":"9501_CR2","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s10703-012-0152-6","volume":"41","author":"V Balabanov","year":"2012","unstructured":"Balabanov, V., Jiang, J.H.R.: Unified QBF certification and its applications. Formal Methods Syst. Des. 41(1), 45\u201365 (2012)","journal-title":"Formal Methods Syst. Des."},{"issue":"1-2","key":"9501_CR3","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/S0004-3702(00)00043-6","volume":"122","author":"C Baral","year":"2000","unstructured":"Baral, C., Kreinovich, V., Trejo, R.: Computational complexity of planning and approximate planning in the presence of incompleteness. Artif. Intell. 122(1-2), 241\u2013267 (2000)","journal-title":"Artif. Intell."},{"key":"9501_CR4","unstructured":"Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: Proc. STACS 2015, LIPIcs, vol. 30, pp. 76\u201389. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)"},{"key":"9501_CR5","doi-asserted-by":"crossref","unstructured":"Biere, A.: Resolve and expand. In: Proc. SAT 2004, LNCS, vol. 3542, pp. 59\u201370. Springer (2004)","DOI":"10.1007\/11527695_5"},{"key":"9501_CR6","doi-asserted-by":"publisher","unstructured":"Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Proc. CADE 2011, LNCS, vol. 6803, pp. 101\u2013115. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_10"},{"issue":"1-2","key":"9501_CR7","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/S0004-3702(96)00047-1","volume":"90","author":"A Blum","year":"1997","unstructured":"Blum, A., Furst, M.L.: Fast planning through planning graph analysis. Artif. Intell. 90(1-2), 281\u2013300 (1997)","journal-title":"Artif. Intell."},{"key":"9501_CR8","doi-asserted-by":"publisher","unstructured":"Bubeck, U., Kleine Buning\u0308, H.: Bounded universal expansion for preprocessing QBF. In: Proc. SAT 2007, LNCS, vol. 4501, pp. 244\u2013257. Springer (2007)","DOI":"10.1007\/978-3-540-72788-0_24"},{"issue":"2","key":"9501_CR9","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/A:1015019416843","volume":"28","author":"M Cadoli","year":"2002","unstructured":"Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An algorithm to evaluate quantified Boolean formulae and its experimental evaluation. J. Autom. Reas. 28(2), 101\u2013142 (2002)","journal-title":"J. Autom. Reas."},{"key":"9501_CR10","unstructured":"Cashmore, M., Fox, M., Giunchiglia, E.: Planning as quantified Boolean formula. In: Proc. ECAI, FAIA, vol. 242, pp. 217\u2013222. IOS Press (2012)"},{"issue":"7","key":"9501_CR11","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"4","key":"9501_CR12","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electron. Notes Theor. Comput. Sci. 89(4), 543\u2013560 (2003)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9501_CR13","doi-asserted-by":"publisher","unstructured":"Egly, U., Kronegger, M., Lonsing, F., Pfandler, A.: Conformant planning as a case study of incremental QBF solving. In: Proc. AISC 2014, LNCS, pp. 120\u2013131. Springer (2014)","DOI":"10.1007\/978-3-319-13770-4_11"},{"key":"9501_CR14","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Marin, P.: Narizzano, M.: sQueezeBF: An effective preprocessor for QBFs based on equivalence reasoning. In: Proc. SAT 2010, LNCS, vol. 6175, pp. 85\u201398. Springer (2010)","DOI":"10.1007\/978-3-642-14186-7_9"},{"key":"9501_CR15","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. J. Artif. Intell. Res. 26, 371\u2013416 (2006)","journal-title":"J. Artif. Intell. Res."},{"key":"9501_CR16","unstructured":"Goultiaeva, A., Van Gelder, A., Bacchus, F.: A uniform approach for generating proofs and strategies for both true and false QBF formulas. In: Proc. IJCAI 2011, pp. 546\u2013553. AAAI Press (2011)"},{"key":"9501_CR17","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1613\/jair.4694","volume":"53","author":"M Heule","year":"2015","unstructured":"Heule, M., Ja\u0307rvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. J. Artif. Intell. Res. 53, 127\u2013168 (2015)","journal-title":"J. Artif. Intell. Res."},{"key":"9501_CR18","doi-asserted-by":"publisher","unstructured":"Heule, M., Seidl, M., Biere, A.: Efficient extraction of skolem functions from QRAT proofs. In: Proc. FMCAD 2014, pp. 107\u2013114. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987602"},{"key":"9501_CR19","doi-asserted-by":"publisher","unstructured":"Heule, M., Seidl, M., Biere, A.: A unified proof system for QBF preprocessing. In: Proc. IJCAR 2014, LNCS, vol. 8562, pp. 91\u2013106. Springer (2014)","DOI":"10.1007\/978-3-319-08587-6_7"},{"key":"9501_CR20","doi-asserted-by":"crossref","unstructured":"Heyman, T., Smith, D., Mahajan, Y., Leong, L.: Abu-Haimed, H.: Dominant controllability check using QBF-solver and netlist optimizer. In: Proc. SAT 2014, LNCS, vol. 8561, pp. 227\u2013242. Springer (2014)","DOI":"10.1007\/978-3-319-09284-3_18"},{"issue":"6\u20137","key":"9501_CR21","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1016\/j.artint.2006.01.003","volume":"170","author":"J Hoffmann","year":"2006","unstructured":"Hoffmann, J., Brafman, R.I.: Conformant planning via heuristic forward search: A new approach. Artif. Intell 170(6\u20137), 507\u2013541 (2006)","journal-title":"Artif. Intell"},{"key":"9501_CR22","doi-asserted-by":"crossref","unstructured":"Janota, M., Grigore, R.: Marques-Silva, J.: On QBF proofs and preprocessing. In: Proc. LPAR 2013, LNCS, vol. 8312, pp. 473\u2013489. Springer (2013)","DOI":"10.1007\/978-3-642-45221-5_32"},{"key":"9501_CR23","doi-asserted-by":"publisher","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample guided refinement. In: Proc. SAT 2012, LNCS, vol. 7317, pp. 114\u2013128. Springer (2012)","DOI":"10.1007\/978-3-642-31612-8_10"},{"key":"9501_CR24","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.: Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci. 577, 25\u201342 (2015)","journal-title":"Theor. Comput. Sci."},{"key":"9501_CR25","doi-asserted-by":"publisher","unstructured":"Ja\u0307rvisalo, M., Biere, A.: Reconstructing solutions after blocked clause elimination. In: Proc. SAT 2010, LNCS, vol. 6175, pp. 340\u2013345. Springer (2010)","DOI":"10.1007\/978-3-642-14186-7_30"},{"key":"9501_CR26","doi-asserted-by":"publisher","unstructured":"Ja\u0307rvisalo, M., Heule, M., Biere, A.: Inprocessing rules. In: Proc. IJCAR 2012, LNCS, vol. 7364, pp. 355\u2013370. Springer (2012)","DOI":"10.1007\/978-3-642-31365-3_28"},{"issue":"1","key":"9501_CR27","doi-asserted-by":"publisher","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.: Resolution for quantified Boolean formulas. Inform. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inform. Comput."},{"key":"9501_CR28","unstructured":"Kronegger, M., Pfandler, A., Pichler, R.: Conformant planning as a benchmark for QBF-solvers. In: Proc. QBF 2013, pp. 1\u20135. http:\/\/fmv.jku.at\/qbf2013\/reportQBFWS13.pdf (2013)"},{"key":"9501_CR29","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96\u201397","author":"O Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Appl. Math. 96\u201397, 149\u2013176 (1999)","journal-title":"Discrete Appl. Math."},{"key":"9501_CR30","doi-asserted-by":"publisher","unstructured":"Lagniez, J.M., Biere, A.: Factoring out assumptions to speed up MUS extraction. In: Proc. SAT 2013, LNCS, vol. 7962, pp. 276\u2013292. Springer (2013)","DOI":"10.1007\/978-3-642-39071-5_21"},{"key":"9501_CR31","doi-asserted-by":"publisher","unstructured":"Letz, R.: Lemma and model caching in decision procedures for quantified Boolean formulas. In: Proc. TABLEAUX 2002, LNCS, vol. 2381, pp. 160\u2013175. Springer (2002)","DOI":"10.1007\/3-540-45616-3_12"},{"key":"9501_CR32","doi-asserted-by":"publisher","unstructured":"Lonsing, F., Bacchus, F., Biere, A., Egly, U., Seidl, M.: Enhancing search-based QBF solving by dynamic blocked clause elimination. In: Proc. LPAR 2015, LNCS, vol. 9450, pp. 418\u2013433. Springer (2015)","DOI":"10.1007\/978-3-662-48899-7_29"},{"key":"9501_CR33","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Biere, A.: Nenofex: Expanding NNF for QBF solving. In: Proc. SAT 2008, LNCS, vol. 4996, pp. 196\u2013210. Springer (2008)","DOI":"10.1007\/978-3-540-79719-7_19"},{"key":"9501_CR34","doi-asserted-by":"publisher","unstructured":"Lonsing, F., Egly, U.: Incremental QBF solving. In: Proc. CP 2014, LNCS, vol. 8656, pp. 514\u2013530. Springer (2014)","DOI":"10.1007\/978-3-319-10428-7_38"},{"key":"9501_CR35","doi-asserted-by":"publisher","unstructured":"Lonsing, F., Egly, U.: Incremental QBF solving by DepQBF. In: Proc. ICMS 2014, LNCS, vol. 8592, pp. 307\u2013314. Springer (2014)","DOI":"10.1007\/978-3-662-44199-2_48"},{"key":"9501_CR36","doi-asserted-by":"publisher","unstructured":"Lonsing, F., Egly, U., Van Gelder, A.: Efficient clause learning for quantified Boolean formulas via QBF pseudo unit propagation. In: Proc. SAT 2013, LNCS, vol. 7962, pp. 100\u2013115. Springer (2013)","DOI":"10.1007\/978-3-642-39071-5_9"},{"key":"9501_CR37","doi-asserted-by":"crossref","unstructured":"Marin, P., Miller, C., Becker, B.: Incremental QBF preprocessing for partial design verification - (poster presentation). In: Proc. SAT 2012, LNCS, vol. 7317, pp. 473\u2013474. Springer (2012)","DOI":"10.1007\/978-3-642-31612-8_41"},{"key":"9501_CR38","doi-asserted-by":"publisher","unstructured":"Marin, P., Miller, C., Lewis, M.D.T., Becker, B.: Verification of partial designs using incremental QBF solving. In: Proc. DATE 2012, pp. 623\u2013628. IEEE (2012)","DOI":"10.1109\/DATE.2012.6176547"},{"issue":"2","key":"9501_CR39","doi-asserted-by":"crossref","first-page":"283","DOI":"10.3233\/AIC-140633","volume":"28","author":"C Miller","year":"2015","unstructured":"Miller, C., Marin, P., Becker, B.: Verification of partial designs using incremental QBF. AI Commun. 28(2), 283\u2013307 (2015)","journal-title":"AI Commun."},{"key":"9501_CR40","doi-asserted-by":"publisher","unstructured":"Nadel, A., Ryvchin, V., Strichman, O.: Ultimately incremental SAT. In: Proc. SAT 2014, LNCS, vol. 8561, pp. 206\u2013218. Springer (2014)","DOI":"10.1007\/978-3-319-09284-3_16"},{"key":"9501_CR41","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF - (tool presentation). In: Proc. SAT 2012, LNCS, vol. 7317, pp. 430\u2013435. Springer (2012)","DOI":"10.1007\/978-3-642-31612-8_33"},{"key":"9501_CR42","doi-asserted-by":"crossref","first-page":"623","DOI":"10.1613\/jair.2708","volume":"35","author":"H Palacios","year":"2009","unstructured":"Palacios, H., Geffner, H.: Compiling uncertainty away in conformant planning problems with bounded width. J. Artif. Intell. Res. 35, 623\u2013675 (2009)","journal-title":"J. Artif. Intell. Res."},{"key":"9501_CR43","unstructured":"Rintanen, J.: Asymptotically optimal encodings of conformant planning in QBF. In: Proc. AAAI 2007, pp. 1045\u20131050. AAAI Press (2007)"},{"issue":"1","key":"9501_CR44","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. Reas. 42(1), 77\u201397 (2009)","journal-title":"J. Autom. Reas."},{"key":"9501_CR45","doi-asserted-by":"crossref","unstructured":"Samulowitz, H., Davies, J., Bacchus, F.: Preprocessing QBF. In: Proc. CP 2006, LNCS, vol. 4204, pp. 514\u2013529. Springer (2006)","DOI":"10.1007\/11889205_37"},{"key":"9501_CR46","doi-asserted-by":"crossref","unstructured":"Seidl, M., K\u00f6nighofer, R.: Partial witnesses from preprocessed quantified Boolean formulas. In: Proc. DATE 2014, pp. 1\u20136. IEEE (2014)","DOI":"10.7873\/DATE.2014.162"},{"key":"9501_CR47","unstructured":"Smith, D.E., Weld, D.S.: Conformant graphplan. In: Proc. AAAI\/IAAI 1998, pp. 889\u2013896. AAAI Press \/ The MIT Press (1998)"},{"key":"9501_CR48","doi-asserted-by":"publisher","unstructured":"Van Gelder, A., Wood, S.B., Lonsing, F.: Extended failed-literal preprocessing for quantified Boolean formulas. In: Proc. SAT 2012, LNCS, vol. 7317, pp. 86\u201399. Springer (2012)","DOI":"10.1007\/978-3-642-31612-8_8"},{"key":"9501_CR49","doi-asserted-by":"publisher","unstructured":"Yu, Y., Malik, S.: Validating the result of a quantified Boolean formula (QBF) solver: theory and practice. In: Proc. ASP-DAC 2005, pp. 1047\u20131051. ACM Press (2005)","DOI":"10.1145\/1120725.1120821"},{"key":"9501_CR50","doi-asserted-by":"publisher","unstructured":"Zhang, L., Malik, S.: Towards a symmetric treatment of satisfaction and conflicts in quantified Boolean formula evaluation. In: Proc. CP 2002, LNCS, vol. 2470, pp. 200\u2013215. Springer (2002)","DOI":"10.1007\/3-540-46135-3_14"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-016-9501-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-016-9501-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-016-9501-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-016-9501-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,17]],"date-time":"2020-09-17T18:20:00Z","timestamp":1600366800000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-016-9501-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3,24]]},"references-count":50,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,5]]}},"alternative-id":["9501"],"URL":"https:\/\/doi.org\/10.1007\/s10472-016-9501-2","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,3,24]]}}}