{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:32:01Z","timestamp":1766136721839},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319409696"},{"type":"electronic","value":"9783319409702"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40970-2_25","type":"book-chapter","created":{"date-parts":[[2016,6,10]],"date-time":"2016-06-10T11:14:55Z","timestamp":1465557295000},"page":"402-418","source":"Crossref","is-referenced-by-count":15,"title":["On Q-Resolution and CDCL QBF Solving"],"prefix":"10.1007","author":[{"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,11]]},"reference":[{"issue":"5","key":"25_CR1","doi-asserted-by":"crossref","first-page":"81","DOI":"10.4086\/toc.2007.v003a005","volume":"3","author":"M Alekhnovich","year":"2007","unstructured":"Alekhnovich, M., Johannsen, J., Pitassi, T., Urquhart, A.: An exponential separation between regular and general resolution. Theory Comput. 3(5), 81\u2013102 (2007)","journal-title":"Theory Comput."},{"key":"25_CR2","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1613\/jair.3152","volume":"40","author":"A Atserias","year":"2011","unstructured":"Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res. (JAIR) 40, 353\u2013373 (2011)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"issue":"1","key":"25_CR3","doi-asserted-by":"crossref","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."},{"key":"25_CR4","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P Beame","year":"2004","unstructured":"Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. (JAIR) 22, 319\u2013351 (2004)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Beame, P., Sabharwal, A.: Non-restarting SAT solvers with simple preprocessing can efficiently simulate resolution. In: Brodley, C.E., Stone, P. (eds.) Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, pp. 2608\u20132615. AAAI Press (2014)","DOI":"10.1609\/aaai.v28i1.9121"},{"key":"25_CR6","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"Handbook of Satisfiability","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Bonet, M.L., Esteban, J.L., Galesi, N., Johannsen, J.: Exponential separations between restricted resolution and cutting planes proof systems. In: 39th Annual Symposium on Foundations of Computer Science, FOCS, pp. 638\u2013647. IEEE Computer Society (1998)","DOI":"10.1109\/SFCS.1998.743514"},{"issue":"2","key":"25_CR8","doi-asserted-by":"crossref","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. Reasoning 28(2), 101\u2013142 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"25_CR9","unstructured":"Chen, H.: Proof complexity modulo the polynomial hierarchy: understanding alternation as a source of hardness. In: 43rd International Colloquium on Automata, Languages, and Programming (ICALP) (2016)"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Ehrenfeucht, A.: An application of games to the completeness problem for formalized theories. Fund. Math. 49, 129\u2013141, 13 (1961)","DOI":"10.4064\/fm-49-2-129-141"},{"issue":"1","key":"25_CR11","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(1), 371\u2013416 (2006)","journal-title":"J. Artif. Intell. Res."},{"key":"25_CR12","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: Reasoning with quantified boolean formulas. In: Biere et al. [6], pp. 761\u2013780"},{"issue":"1\u20133","key":"25_CR13","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/BF01531027","volume":"6","author":"A Goerdt","year":"1992","unstructured":"Goerdt, A.: Davis-Putnam resolution versus unrestricted resolution. Ann. Math. Artif. Intell. 6(1\u20133), 169\u2013184 (1992)","journal-title":"Ann. Math. Artif. Intell."},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Goultiaeva, A., Seidl, M., Biere, A.: Bridging the gap between dual propagation and CNF-based QBF solving. In: DATE, pp. 811\u2013814 (2013)","DOI":"10.7873\/DATE.2013.172"},{"key":"25_CR15","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theoret. Comput. Sci. 39, 297\u2013308 (1985)","journal-title":"Theoret. Comput. Sci."},{"key":"25_CR16","doi-asserted-by":"crossref","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. Theoret. Comput. Sci. 577, 25\u201342 (2015)","journal-title":"Theoret. Comput. Sci."},{"key":"25_CR17","unstructured":"Kleine B\u00fcning, H., Bubeck, U.: Theory of quantified boolean formulas. In: Biere et al. [6], pp. 735\u2013760"},{"issue":"1","key":"25_CR18","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"K B\u00fcning Kleine","year":"1995","unstructured":"B\u00fcning Kleine, K., Karpinski, M., Fl\u00f6gel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"25_CR19","unstructured":"Klieber, W.: Formal Verification Using Quantified Boolean Formulas (QBF). Ph.D. thesis, Carnegie Mellon University (2014). http:\/\/www.cs.cmu.edu\/~wklieber\/thesis.pdf"},{"key":"25_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"1","key":"25_CR21","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1016\/0890-5401(91)90059-B","volume":"90","author":"PG Kolaitis","year":"1991","unstructured":"Kolaitis, P.G.: The expressive power of stratified programs. Inf. Comput. 90(1), 50\u201366 (1991)","journal-title":"Inf. Comput."},{"key":"25_CR22","unstructured":"Lonsing, F.: Dependency Schemes and Search-Based QBF Solving: Theory and Practice. Ph.D. thesis, Johannes Kepler Universit\u00e4t (2012). http:\/\/www.kr.tuwien.ac.at\/staff\/lonsing\/diss\/"},{"issue":"2\u20133","key":"25_CR23","first-page":"71","volume":"7","author":"F Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DepQBF: a dependency-aware QBF solver. JSAT 7(2\u20133), 71\u201376 (2010)","journal-title":"JSAT"},{"key":"25_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1007\/978-3-642-39071-5_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"F Lonsing","year":"2013","unstructured":"Lonsing, F., Egly, U., Van Gelder, A.: Efficient clause learning for quantified boolean formulas via QBF pseudo unit propagation. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 100\u2013115. Springer, Heidelberg (2013)"},{"issue":"3","key":"25_CR25","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1016\/j.ipl.2015.11.017","volume":"116","author":"M Mahajan","year":"2016","unstructured":"Mahajan, M., Shukla, A.: Level-ordered Q-resolution and tree-like Q-resolution are incomparable. Inf. Process. Lett. 116(3), 256\u2013258 (2016)","journal-title":"Inf. Process. Lett."},{"issue":"5","key":"25_CR26","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques Silva","year":"1999","unstructured":"Marques Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"25_CR27","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","volume":"175","author":"K Pipatsrisawat","year":"2011","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175(2), 512\u2013525 (2011)","journal-title":"Artif. Intell."},{"key":"25_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"647","DOI":"10.1007\/978-3-642-33558-7_47","volume-title":"Principles and Practice of Constraint Programming","author":"A Gelder Van","year":"2012","unstructured":"Van Gelder, A.: Contributions to the theory of practical quantified boolean formula solving. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 647\u2013663. Springer, Heidelberg (2012)"},{"key":"25_CR29","unstructured":"Zhang, L.: Solving QBF by combining conjunctive and disjunctive normal forms. In: AAAI. AAAI Press (2006)"},{"key":"25_CR30","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: ICCAD, pp. 442\u2013449 (2002)","DOI":"10.1145\/774572.774637"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40970-2_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,1]],"date-time":"2022-07-01T12:15:15Z","timestamp":1656677715000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40970-2_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319409696","9783319409702"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40970-2_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}