{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:34:54Z","timestamp":1740123294803,"version":"3.37.3"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,11,12]],"date-time":"2015-11-12T00:00:00Z","timestamp":1447286400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council (BE)","doi-asserted-by":"publisher","award":["239962"],"award-info":[{"award-number":["239962"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2016,4]]},"DOI":"10.1007\/s10817-015-9353-1","type":"journal-article","created":{"date-parts":[[2015,11,12]],"date-time":"2015-11-12T05:07:03Z","timestamp":1447304823000},"page":"459-477","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Quantifier Reordering for QBF"],"prefix":"10.1007","volume":"56","author":[{"given":"Friedrich","family":"Slivovsky","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"key":"9353_CR1","unstructured":"Atserias, A., Oliva, S.: Bounded-width QBF is PSPACE-complete. In: Portier, N., Wilke, T. (eds.) 30th International Symposium on Theoretical Aspects of Computer Science, STACS 2013, February 27\u2013March 2, Kiel, Germany, Volume 20 of LIPIcs, pp. 44\u201354. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)"},{"key":"9353_CR2","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without bdds. In: Cleaveland, R. (eds.) 5th International Conference in Tools and Algorithms for Construction and Analysis of Systems (TACAS \u201999), Held as Part of the European Joint Conferences on the Theory and Practice of Software (ETAPS \u201999), Amsterdam, The Netherlands, March 22\u201328, Proceedings, Volume 1579 of Lecture Notes in Computer Science, pp. 193\u2013207. Springer, Berlin (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"9353_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Lonsing, F.: Integrating dependency schemes in search-based QBF solvers. In: Strichman, O., Szeider, S. (eds.) Theory and Applications of Satisfiability Testing\u2014(SAT 2010), Volume 6175 of Lecture Notes in Computer Science, pp. 158\u2013171. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14186-7_14"},{"key":"9353_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) International Conference on Automated Deduction\u2014(CADE 23), Volume 6803 of Lecture Notes in Computer Science, pp. 101\u2013115. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22438-6_10"},{"key":"9353_CR5","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an alpha microprocessor using satisfiability solvers. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer Aided Verification: Proceedings of the 13th International Conference (CAV 2001), Paris, France, July 18\u201322, pp. 454\u2013464 (2001)","DOI":"10.1007\/3-540-44585-4_44"},{"issue":"1","key":"9353_CR6","doi-asserted-by":"crossref","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. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"9353_CR7","unstructured":"Kautz, H., Selman, B.: Pushing the envelope: planning, propositional logic, and stochastic search. In: Proceedings of the Thirteenth AAAI Conference on Artificial Intelligence (AAAI \u201996), pp. 1194\u20131201. AAAI Press, Palo Alto (1996)"},{"key":"9353_CR8","volume-title":"Propositional Logic: Deduction and Algorithms","author":"H Kleine B\u00fcning","year":"1999","unstructured":"Kleine B\u00fcning, H., Lettman, T.: Propositional Logic: Deduction and Algorithms. Cambridge University Press, Cambridge (1999)"},{"key":"9353_CR9","unstructured":"Lonsing, F.: Dependency Schemes and Search-Based QBF Solving: Theory and Practice. Ph.D. thesis, Johannes Kepler University, Linz, Austria (2012)"},{"issue":"2","key":"9353_CR10","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"AGM Prasad","year":"2005","unstructured":"Prasad, A.G.M., Biere, A.: A survey of recent advances in SAT-based formal verification. Softw. Tools Technol. Transf. 7(2), 156\u2013173 (2005)","journal-title":"Softw. Tools Technol. Transf."},{"key":"9353_CR11","unstructured":"Pan, G., Vardi, M.Y.: Fixed-parameter hierarchies inside PSPACE. In: Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12\u201315 August, Seattle, WA, USA, pp. 27\u201336. IEEE Computer Society, Los Alamitos (2006)"},{"issue":"1","key":"9353_CR12","doi-asserted-by":"crossref","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)","journal-title":"J. Autom. Reason."},{"key":"9353_CR13","doi-asserted-by":"crossref","unstructured":"Slivovsky, F., Szeider, S.: Computing resolution-path dependencies in linear time. In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of Satisfiability Testing\u2014SAT 2012, Volume 7317 of Lecture Notes in Computer Science, pp. 58\u201371. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-31612-8_6"},{"key":"9353_CR14","doi-asserted-by":"crossref","unstructured":"Slivovsky, F., Szeider, S.: Variable dependencies and Q-resolution. In: Sinz, C., Egly, U. (eds.) Theory and Applications of Satisfiability Testing\u2014SAT 2014, Volume 8561 of Lecture Notes in Computer Science, pp. 269\u2013284. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-09284-3_21"},{"issue":"1","key":"9353_CR15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"LJ Stockmeyer","year":"1976","unstructured":"Stockmeyer, L.J.: The polynomial-time hierarchy. Theor. Comput. Sci. 3(1), 1\u201322 (1976)","journal-title":"Theor. Comput. Sci."},{"key":"9353_CR16","doi-asserted-by":"crossref","unstructured":"Van Gelder, A.: Variable independence and resolution paths for quantified Boolean formulas. In: Lee, J. (eds.) Principles and Practice of Constraint Programming\u2014CP 2011, Volume 6876 of Lecture Notes in Computer Science, pp. 789\u2013803. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-23786-7_59"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9353-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9353-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9353-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,1]],"date-time":"2019-09-01T09:21:05Z","timestamp":1567329665000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9353-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11,12]]},"references-count":16,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,4]]}},"alternative-id":["9353"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9353-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2015,11,12]]}}}