{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,6]],"date-time":"2025-04-06T02:26:36Z","timestamp":1743906396864},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642215803"},{"type":"electronic","value":"9783642215810"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-21581-0_19","type":"book-chapter","created":{"date-parts":[[2011,6,10]],"date-time":"2011-06-10T13:30:19Z","timestamp":1307712619000},"page":"230-244","source":"Crossref","is-referenced-by-count":32,"title":["Abstraction-Based Algorithm for 2QBF"],"prefix":"10.1007","author":[{"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"first","affiliation":[]},{"given":"Joao","family":"Marques-Silva","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","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)"},{"volume-title":"Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications","year":"2009","key":"19_CR2","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press, Amsterdam (2009)"},{"key":"19_CR3","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1145\/1185448.1185456","volume-title":"ACM Southeast Regional Conference","author":"B. Browning","year":"2006","unstructured":"Browning, B., Remshagen, A.: A SAT-based solver for Q-ALL SAT. In: Menezes, R. (ed.) ACM Southeast Regional Conference, pp. 30\u201333. ACM, New York (2006)"},{"key":"19_CR4","unstructured":"Castellini, C., Giunchiglia, E., Tacchella, A.: Improvements to SAT-based conformant planning. In: European Conference on Planning (2001)"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/3-540-36126-X_3","volume-title":"Formal Methods in Computer-Aided Design","author":"P. Chauhan","year":"2002","unstructured":"Chauhan, P., Clarke, E.M., Kukula, J.H., Sapra, S., Veith, H., Wang, D.: Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 33\u201351. Springer, Heidelberg (2002)"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"issue":"5","key":"19_CR7","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"issue":"7","key":"19_CR8","doi-asserted-by":"publisher","first-page":"1113","DOI":"10.1109\/TCAD.2004.829807","volume":"23","author":"E.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Gupta, A., Strichman, O.: SAT-based counterexample-guided abstraction refinement. IEEE Trans. on CAD of Integrated Circuits and Systems\u00a023(7), 1113\u20131123 (2004)","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/11499107_32","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Dershowitz","year":"2005","unstructured":"Dershowitz, N., Hanna, Z., Katz, J.: Bounded model checking with QBF. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 408\u2013414. Springer, Heidelberg (2005)"},{"key":"19_CR10","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) [18]"},{"issue":"2","key":"19_CR11","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0304-3975(93)90073-3","volume":"114","author":"T. Eiter","year":"1993","unstructured":"Eiter, T., Gottlob, G.: Propositional circumscription and extended closed-world reasoning are \u03a0 P 2-complete. Theor. Comput. Sci.\u00a0114(2), 231\u2013245 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-45069-6_34","volume-title":"Computer Aided Verification","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 355\u2013367. Springer, Heidelberg (2003)"},{"key":"19_CR13","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: An effective preprocessor for QBF pre-reasoning. In: 2nd International Workshop on Quantification in Constraint Programming, QiCP (2008)"},{"key":"19_CR14","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: Reasoning with quantified boolean formulas. In: Biere, et al (eds.) [2], pp. 761\u2013780"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: sQueezeBF: An effective preprocessor for QBFs based on equivalence reasoning. In: Strichman, O., Szeider, A. (eds.) [36], pp. 85\u201398","DOI":"10.1007\/978-3-642-14186-7_9"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-30494-4_15","volume-title":"Formal Methods in Computer-Aided Design","author":"E. Giunchiglia","year":"2004","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE++: An Efficient QBF Solver. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 201\u2013213. Springer, Heidelberg (2004)"},{"key":"19_CR17","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 (JAIR)\u00a026, 371\u2013416 (2006)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","year":"2004","unstructured":"Giunchiglia, E., Tacchella, A. (eds.): SAT 2003. LNCS, vol.\u00a02919. Springer, Heidelberg (2004)"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1007\/978-3-642-11266-9_44","volume-title":"SOFSEM 2010: Theory and Practice of Computer Science","author":"M. Janota","year":"2010","unstructured":"Janota, M., Botterweck, G., Grigore, R., Marques-Silva, J.: How to complete an interactive configuration process? In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorn\u00fd, J., Rumpe, B. (eds.) SOFSEM 2010. LNCS, vol.\u00a05901, pp. 528\u2013539. Springer, Heidelberg (2010)"},{"key":"19_CR20","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":"19_CR21","unstructured":"Kleine-B\u00fcning, H., Bubeck, U.: Theory of quantified boolean formulas. In: Biere, et al (eds.) [2]"},{"key":"19_CR22","unstructured":"Li, C.M., Many\u00e0, F.: Maxsat, hard and soft constraints. In: Biere, et al (eds.) [2], pp. 613\u2013631"},{"key":"19_CR23","unstructured":"Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, et al (eds.) [2], pp. 131\u2013153"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Meyer, A.R., Stockmeyer, L.J.: The equivalence problem for regular expressions with squaring requires exponential space. In: Symposium Switching and Automata Theory (October 1972)","DOI":"10.1109\/SWAT.1972.29"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Mneimneh, M.N., Sakallah, K.A.: Computing vertex eccentricity in exponentially large graphs: QBF formulation and solution. In: Giunchiglia, E., Tacchella, A. (eds.) [18], pp. 411\u2013425","DOI":"10.1007\/978-3-540-24605-3_31"},{"key":"19_CR26","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":"19_CR27","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/3-540-45620-1_35","volume-title":"Automated Deduction - CADE-18","author":"L.M. Moura de","year":"2002","unstructured":"de Moura, L.M., 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":"19_CR28","doi-asserted-by":"crossref","unstructured":"Peschiera, C., Pulina, L., Tacchella, A., Bubeck, U., Kullmann, O., Lynce, I.: The seventh QBF solvers evaluation (QBFEVAL\u201910). In: Strichman, O., Szeider, S. (eds.) [36], pp. 237\u2013250","DOI":"10.1007\/978-3-642-14186-7_20"},{"issue":"2","key":"19_CR29","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/S0166-218X(02)00409-2","volume":"130","author":"D.A. Plaisted","year":"2003","unstructured":"Plaisted, D.A., Biere, A., Zhu, Y.: A satisfiability procedure for quantified boolean formulae. Discrete Applied Mathematics\u00a0130(2), 291\u2013328 (2003)","journal-title":"Discrete Applied Mathematics"},{"issue":"3","key":"19_CR30","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput.\u00a02(3), 293\u2013304 (1986)","journal-title":"J. Symb. Comput."},{"key":"19_CR31","unstructured":"QBF solver evaluation portal, http:\/\/www.qbflib.org\/index_eval.php"},{"key":"19_CR32","unstructured":"The Quantified Boolean Formulas satisfiability library, http:\/\/www.qbflib.org\/"},{"key":"19_CR33","unstructured":"Ranjan, D.P., Tang, D., Malik, S.: A comparative study of 2QBF algorithms. In: SAT (2004)"},{"key":"19_CR34","first-page":"1192","volume-title":"IJCAI","author":"J. Rintanen","year":"1999","unstructured":"Rintanen, J.: Improvements to the evaluation of quantified Boolean formulae. In: Dean, T. (ed.) IJCAI, pp. 1192\u20131197. Morgan Kaufmann, San Francisco (1999)"},{"issue":"4","key":"19_CR35","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/s10601-010-9095-y","volume":"15","author":"E.D. Rosa","year":"2010","unstructured":"Rosa, E.D., Giunchiglia, E., Maratea, M.: Solving satisfiability problems with preferences. Constraints\u00a015(4), 485\u2013515 (2010)","journal-title":"Constraints"},{"key":"19_CR36","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","year":"2010","unstructured":"Strichman, O., Szeider, S. (eds.): SAT 2010. LNCS, vol.\u00a06175. Springer, Heidelberg (2010)"},{"key":"19_CR37","unstructured":"STRUQS: A Structural QBF Solver, www.qbflib.org\/DESCRIPTIONS\/struqs.pdf"},{"issue":"115-125","key":"19_CR38","first-page":"10","volume":"2","author":"G.S. Tseitin","year":"1968","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic\u00a02(115-125), 10\u201313 (1968)","journal-title":"Studies in Constructive Mathematics and Mathematical Logic"},{"issue":"4","key":"19_CR39","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1006\/jcss.2001.1775","volume":"63","author":"C. Umans","year":"2001","unstructured":"Umans, C.: The minimum equivalent DNF problem and shortest implicants. J. Comput. Syst. Sci.\u00a063(4), 597\u2013611 (2001)","journal-title":"J. Comput. Syst. Sci."},{"key":"19_CR40","unstructured":"Wintersteiger, C.M., Hamadi, Y., de Moura, L.: Efficiently solving quantified bit-vector formulas. In: Proceedings of Formal Methods in Computer Aided Design FMCAD (October 2010)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2011"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21581-0_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,24]],"date-time":"2021-11-24T23:14:32Z","timestamp":1637795672000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21581-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642215803","9783642215810"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21581-0_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}