{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T01:40:01Z","timestamp":1750556401470,"version":"3.41.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319633893"},{"type":"electronic","value":"9783319633909"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63390-9_25","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:50Z","timestamp":1499849630000},"page":"475-494","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["On Expansion and Resolution in CEGAR Based QBF Solving"],"prefix":"10.1007","author":[{"given":"Leander","family":"Tentrup","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-662-44465-8_8","volume-title":"Mathematical Foundations of Computer Science 2014","author":"O Beyersdorff","year":"2014","unstructured":"Beyersdorff, O., Chew, L., Janota, M.: On unification of QBF resolution-based calculi. In: Csuhaj-Varj\u00fa, E., Dietzfelbinger, M., \u00c9sik, Z. (eds.) MFCS 2014. LNCS, vol. 8635, pp. 81\u201393. Springer, Heidelberg (2014). doi:10.1007\/978-3-662-44465-8_8"},{"key":"25_CR2","unstructured":"Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: Proceedings of STACS. LIPIcs, vol. 30, pp. 76\u201389. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)"},{"issue":"2\u20134","key":"25_CR3","first-page":"75","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A.: PicoSAT essentials. JSAT 4(2\u20134), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A.: Lingeling essentials, a tutorial on design and implementation aspects of the the SAT solver lingeling. In: Proceedings of POS@SAT. EPiC Series in Computing, vol. 27, p. 88. EasyChair (2014)","DOI":"10.29007\/jhd7"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","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, vol. 6803, pp. 101\u2013115. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-22438-6_10"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Bloem, R., Egly, U., Klampfl, P., K\u00f6nighofer, R., Lonsing, F.: SAT-based methods for circuit synthesis. In: Proceedings of FMCAD, pp. 31\u201334. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987592"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-54013-4_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Bloem","year":"2014","unstructured":"Bloem, R., K\u00f6nighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 1\u201320. Springer, Heidelberg (2014). doi:10.1007\/978-3-642-54013-4_1"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). doi:10.1007\/978-3-540-24605-3_37"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-319-40970-2_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"U Egly","year":"2016","unstructured":"Egly, U.: On stronger calculi for QBFs. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 419\u2013434. Springer, Cham (2016). doi:10.1007\/978-3-319-40970-2_26"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-662-54577-5_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 354\u2013370. Springer, Heidelberg (2017). doi:10.1007\/978-3-662-54577-5_20"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-319-23506-6_15","volume-title":"Correct System Design","author":"B Finkbeiner","year":"2015","unstructured":"Finkbeiner, B.: Bounded synthesis for petri games. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 223\u2013237. Springer, Cham (2015). doi:10.1007\/978-3-319-23506-6_15"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Tentrup, L.: Detecting unrealizability of distributed fault-tolerant systems. Logical Methods Comput. Sci. 11(3) (2015)","DOI":"10.2168\/LMCS-11(3:12)2015"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/978-3-642-33558-7_47","volume-title":"Principles and Practice of Constraint Programming","author":"A Gelder","year":"2012","unstructured":"Gelder, A.: Contributions to the theory of practical quantified boolean formula solving. In: Milano, M. (ed.) CP 2012. LNCS, pp. 647\u2013663. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-33558-7_47"},{"issue":"1\u20133","key":"25_CR14","doi-asserted-by":"publisher","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_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-319-40970-2_25","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"M Janota","year":"2016","unstructured":"Janota, M.: On Q-resolution and CDCL QBF solving. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 402\u2013418. Springer, Cham (2016). doi:10.1007\/978-3-319-40970-2_25"},{"key":"25_CR16","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.M.: Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1\u201325 (2016)","journal-title":"Artif. Intell."},{"key":"25_CR17","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":"25_CR18","unstructured":"Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: Proceedings of IJCAI, pp. 325\u2013331. AAAI Press (2015)"},{"issue":"1","key":"25_CR19","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"HK B\u00fcning","year":"1995","unstructured":"B\u00fcning, H.K., Karpinski, M., Fl\u00f6gel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"25_CR20","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). doi:10.1007\/978-3-642-14186-7_12"},{"issue":"2\u20133","key":"25_CR21","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_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-319-40970-2_27","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"F Lonsing","year":"2016","unstructured":"Lonsing, F., Egly, U., Seidl, M.: Q-resolution with generalized axioms. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 435\u2013452. Springer, Cham (2016). doi:10.1007\/978-3-319-40970-2_27"},{"issue":"3","key":"25_CR23","doi-asserted-by":"publisher","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."},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Miller, C., Scholl, C., Becker, B.: Proving QBF-hardness in bounded model checking for incomplete designs. In: Proceedings of MTV, pp. 23\u201328. IEEE Computer Society (2013)","DOI":"10.1109\/MTV.2013.11"},{"key":"25_CR25","doi-asserted-by":"crossref","unstructured":"Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: Proceedings of FMCAD, pp. 136\u2013143. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542263"},{"key":"25_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-02777-2_24","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M Soos","year":"2009","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244\u2013257. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-02777-2_24"},{"key":"25_CR27","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: Proceedings of ICCAD, pp. 442\u2013449. ACM\/IEEE Computer Society (2002)","DOI":"10.1145\/774572.774637"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63390-9_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T01:10:26Z","timestamp":1750554626000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63390-9_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633893","9783319633909"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63390-9_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}