{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:08:20Z","timestamp":1748664500367,"version":"3.41.0"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243085"},{"type":"electronic","value":"9783319243092"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-24309-2_16","type":"book-chapter","created":{"date-parts":[[2015,9,8]],"date-time":"2015-09-08T06:21:33Z","timestamp":1441693293000},"page":"205-217","source":"Crossref","is-referenced-by-count":2,"title":["Abstract Solvers for Quantified Boolean Formulas and their Applications"],"prefix":"10.1007","author":[{"given":"Remi","family":"Brochenin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Maratea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,10,17]]},"reference":[{"issue":"6","key":"16_CR1","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM 53(6), 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"issue":"1\u20132","key":"16_CR2","first-page":"21","volume":"3","author":"C Barrett","year":"2007","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. JSAT 3(1\u20132), 21\u201346 (2007)","journal-title":"JSAT"},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1017\/S1471068410000578","volume":"11","author":"Y Lierler","year":"2011","unstructured":"Lierler, Y.: Abstract answer set solvers with backjumping and learning. Theory and Practice of Logic Programming 11, 135\u2013169 (2011)","journal-title":"Theory and Practice of Logic Programming"},{"issue":"4\u20135","key":"16_CR4","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1017\/S1471068411000214","volume":"11","author":"Y Lierler","year":"2011","unstructured":"Lierler, Y., Truszczynski, M.: Transition systems for model generators - a unifying approach. Theory and Practice of Logic Programming 11(4\u20135), 629\u2013646 (2011)","journal-title":"Theory and Practice of Logic Programming"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Brochenin, R., Lierler, Y., Maratea, M.: Abstract disjunctive answer set solvers. In: Schaub, T., Friedrich, G., O\u2019Sullivan, B. (eds.) Proc. of ECAI 2014, vol. 263. Frontiers in Artificial Intelligence and Applications, pp. 165\u2013170. IOS Press (2014)","DOI":"10.3233\/978-1-61499-419-0-165"},{"key":"16_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.artint.2013.10.004","volume":"207","author":"Y Lierler","year":"2014","unstructured":"Lierler, Y.: Relating constraint answer set programming languages and algorithms. Artificial Intelligence 207, 1\u201322 (2014)","journal-title":"Artificial Intelligence"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: Reasoning with quantified boolean formulas. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Volume 185 of FAIA, pp. 761\u2013780. IOS Press (2009)","DOI":"10.3233\/978-1-58603-929-5-761"},{"issue":"7","key":"16_CR8","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"16_CR9","unstructured":"Egly, U., Eiter, T., Tompits, H., Woltran, S.: Solving advanced reasoning tasks using quantified boolean formulas. In: Kautz, H.A., Porter, B.W. (eds.) Proc. of AAAI 2000, pp. 417\u2013422, AAAI Press \/ The MIT Press (2000)"},{"issue":"2","key":"16_CR10","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/j.jal.2013.03.009","volume":"11","author":"O Arieli","year":"2013","unstructured":"Arieli, O., Caminada, M.W.A.: A QBF-based formalization of abstract argumentation semantics. Journal of Applied Logic 11(2), 229\u2013252 (2013)","journal-title":"Journal of Applied Logic"},{"key":"16_CR11","unstructured":"Diller, M., Wallner, J.P., Woltran, S.: Reasoning in abstract dialectical frameworks using quantified boolean formulas. In: Parsons, S., Oren, N., Reed, C., Cerutti, F. (eds.) Proc. of COMMA 2014. Volume 266 of FAIA, pp. 241\u2013252, IOS Press (2014)"},{"key":"16_CR12","unstructured":"Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified boolean formulae. In: Mostow, J., Rich, C. (eds) Proc. of AAAI 1998, pp. 262\u2013267, AAAI Press \/ The MIT Press (1998)"},{"key":"16_CR13","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. JAIR 26, 371\u2013416 (2006)","journal-title":"JAIR"},{"key":"16_CR14","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1016\/j.artint.2014.11.008","volume":"220","author":"G Charwat","year":"2015","unstructured":"Charwat, G., Dvo\u0159\u00e1k, W., Gaggl, S.A., Wallner, J.P., Woltran, S.: Methods for Solving Reasoning Problems in Abstract Argumentation - A Survey. Artificial Intelligence 220, 28\u201363 (2015)","journal-title":"Artificial Intelligence"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-540-89982-2_35","volume-title":"Logic Programming","author":"Y Lierler","year":"2008","unstructured":"Lierler, Y.: Abstract answer set solvers. In: Garcia de la Banda, M., Pontelli, E. (eds.) ICLP 2008. LNCS, vol. 5366, pp. 377\u2013391. Springer, Heidelberg (2008)"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Cashmore, M., Fox, M., Giunchiglia, E.: Partially grounded planning as quantified boolean formula. In: Borrajo, D., Kambhampati, S., Oddi, A., Fratini, S. (eds.) Proceedings of the Twenty-Third International Conference on Automated Planning and Scheduling, ICAPS 2013, AAAI (2013)","DOI":"10.1609\/icaps.v23i1.13549"}],"container-title":["Lecture Notes in Computer Science","AI*IA 2015 Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24309-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T13:48:35Z","timestamp":1748612915000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24309-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243085","9783319243092"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24309-2_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}