{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:56:54Z","timestamp":1762459014655,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642316111"},{"type":"electronic","value":"9783642316128"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31612-8_10","type":"book-chapter","created":{"date-parts":[[2012,6,18]],"date-time":"2012-06-18T09:14:42Z","timestamp":1340010882000},"page":"114-128","source":"Crossref","is-referenced-by-count":74,"title":["Solving QBF with Counterexample Guided Refinement"],"prefix":"10.1007","author":[{"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"first","affiliation":[]},{"given":"William","family":"Klieber","sequence":"additional","affiliation":[]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-36126-X_12","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Ayari","year":"2002","unstructured":"Ayari, A., Basin, D.A.: QUBOS: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 187\u2013201. Springer, Heidelberg (2002)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-45657-0_18","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2002","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 236\u2013249. Springer, Heidelberg (2002)"},{"key":"10_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-540-32275-7_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: Evaluating QBFs via Symbolic Skolemization. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 285\u2013300. Springer, Heidelberg (2005)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/11527695_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Biere","year":"2005","unstructured":"Biere, A.: Resolve and Expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"key":"10_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.\u00a06803, pp. 101\u2013115. Springer, Heidelberg (2011)"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Browning, B., Remshagen, A.: A SAT-based solver for Q-ALL SAT. In: ACM Southeast Regional Conference (2006)","DOI":"10.1145\/1185448.1185456"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-540-72788-0_24","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"U. Bubeck","year":"2007","unstructured":"Bubeck, U., Kleine B\u00fcning, H.: Bounded Universal Expansion for Preprocessing QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 244\u2013257. Springer, Heidelberg (2007)"},{"key":"10_CR8","unstructured":"B\u00fcning, H.K., Bubeck, U.: Theory of quantified boolean formulas. In: Handbook of Satisfiability. IOS Press (2009)"},{"key":"10_CR9","unstructured":"Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate Quantified Boolean Formulae. In: National Conference on Artificial Intelligence (1998)"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5) (2003)","DOI":"10.1145\/876638.876643"},{"key":"10_CR11","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.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: QuBE 7.0 system description. Journal on Satisfiability, Boolean Modeling and Computation 7 (2010)","DOI":"10.3233\/SAT190079"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: Reasoning with quantified boolean formulas. In: Handbook of Satisfiability. IOS Press (2009)","DOI":"10.3233\/978-1-58603-929-5-761"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-642-14186-7_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"E. Giunchiglia","year":"2010","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 85\u201398. Springer, Heidelberg (2010)"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Goultiaeva, A., Bacchus, F.: Exploiting QBF duality on a circuit representation. In: AAAI (2010)","DOI":"10.1609\/aaai.v24i1.7548"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-15675-5_18","volume-title":"Logics in Artificial Intelligence","author":"M. Janota","year":"2010","unstructured":"Janota, M., Grigore, R., Marques-Silva, J.: Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription. In: Janhunen, T., Niemel\u00e4, I. (eds.) JELIA 2010. LNCS, vol.\u00a06341, pp. 195\u2013207. Springer, Heidelberg (2010)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-21581-0_19","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"M. Janota","year":"2011","unstructured":"Janota, M., Marques-Silva, J.: Abstraction-Based Algorithm for 2QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 230\u2013244. Springer, Heidelberg (2011)"},{"key":"10_CR18","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.M.: A Non-prenex, Non-clausal QBF Solver with Game-State Learning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 128\u2013142. Springer, Heidelberg (2010)"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-540-79719-7_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"F. Lonsing","year":"2008","unstructured":"Lonsing, F., Biere, A.: Nenofex: Expanding NNF for QBF Solving. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 196\u2013210. Springer, Heidelberg (2008)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Biere, A.: DepQBF: A dependency-aware QBF solver. JSAT (2010)","DOI":"10.3233\/SAT190077"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-642-21581-0_21","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"F. Lonsing","year":"2011","unstructured":"Lonsing, F., Biere, A.: Failed Literal Detection for QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 259\u2013272. Springer, Heidelberg (2011)"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/978-3-540-24605-3_31","volume-title":"Theory and Applications of Satisfiability Testing","author":"M. Mneimneh","year":"2004","unstructured":"Mneimneh, M., Sakallah, K.: Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 411\u2013425. Springer, Heidelberg (2004)"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-14295-6_51","volume-title":"Computer Aided Verification","author":"D. Monniaux","year":"2010","unstructured":"Monniaux, D.: Quantifier Elimination by Lazy Model Enumeration. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 585\u2013599. Springer, Heidelberg (2010)"},{"key":"10_CR24","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/3-540-45620-1_35","volume-title":"Automated Deduction - CADE-18","author":"L. Moura de","year":"2002","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Lazy Theorem Proving for Bounded Model Checking over Infinite Domains. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 438\u2013455. Springer, Heidelberg (2002)"},{"key":"10_CR25","unstructured":"The Quantified Boolean Formulas satisfiability library, http:\/\/www.qbflib.org\/"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1007\/11564751_43","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"H. Samulowitz","year":"2005","unstructured":"Samulowitz, H., Bacchus, F.: Using SAT in QBF. In: van Beek, P. (ed.) CP 2005. LNCS, vol.\u00a03709, pp. 578\u2013592. Springer, Heidelberg (2005)"},{"key":"10_CR27","unstructured":"Wintersteiger, C.M., Hamadi, Y., de Moura, L.: Efficiently Solving Quantified Bit-Vector Formulas. In: FMCAD (2010)"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: ICCAD (2002)","DOI":"10.1145\/774572.774637"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2012"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31612-8_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,1]],"date-time":"2025-04-01T15:39:43Z","timestamp":1743521983000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31612-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642316111","9783642316128"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31612-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}