{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:54:28Z","timestamp":1725540868082},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642102905"},{"type":"electronic","value":"9783642102912"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10291-2_4","type":"book-chapter","created":{"date-parts":[[2009,11,16]],"date-time":"2009-11-16T08:14:47Z","timestamp":1258359287000},"page":"31-41","source":"Crossref","is-referenced-by-count":0,"title":["Hard QBF Encodings Made Easy: Dream or Reality?"],"prefix":"10.1007","author":[{"given":"Luca","family":"Pulina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"4_CR2","unstructured":"Ansotegui, C., Gomes, C.P., Selman, B.: Achille\u2019s heel of QBF. In: Proc. of AAAI (2005)"},{"key":"4_CR3","unstructured":"Peschiera, C., Pulina, L., Tacchella, A.: QBF comparative evaluation (2008), http:\/\/www.qbfeval.org\/2008"},{"key":"4_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1007\/978-3-540-89439-1_37","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"L. Pulina","year":"2008","unstructured":"Pulina, L., Tacchella, A.: Treewidth: A useful marker of empirical hardness in quantified boolean logic encodings. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 528\u2013542. Springer, Heidelberg (2008)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/11538363_17","volume-title":"Computer Science Logic","author":"H. Chen","year":"2005","unstructured":"Chen, H., Dalmau, V.: From Pebble Games to Tractability: An Ambidextrous Consistency Algorithm for Quantified Constraint Satisfaction. In: Ong, L. (ed.) CSL 2005. LNCS, vol.\u00a03634, pp. 232\u2013247. Springer, Heidelberg (2005)"},{"key":"4_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/978-3-540-45085-6_7","volume-title":"Automated Deduction \u2013 CADE-19","author":"G. Pan","year":"2003","unstructured":"Pan, G., Vardi, M.Y.: Optimizing a BDD-based modal solver. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 75\u201389. Springer, Heidelberg (2003)"},{"key":"4_CR7","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 Quantified Boolean Logic Satisfiability. Artificial Intelligence Research\u00a026, 371\u2013416 (2006)","journal-title":"Artificial Intelligence Research"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Arnborg, S., Corneil, D.G., Proskurowski, A.: Complexity of finding embeddings in a k-tree. SIAM Journal on Algebraic and Discrete Methods, 277\u2013284 (1987)","DOI":"10.1137\/0608024"},{"key":"4_CR9","unstructured":"Giunchiglia, E., Narizzano, M., Pulina, L., Tacchella, A.: Quantified Boolean Formulas satisfiability library, QBFLIB (2001), http:\/\/www.qbflib.org"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/11499107_28","volume-title":"Theory and Applications of Satisfiability Testing","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: Quantifier Trees for QBFs. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 378\u2013385. Springer, Heidelberg (2005)"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Quantifier Structure in search based procedures for QBFs. IEEE TCAD\u00a026(3) (2007)","DOI":"10.1109\/TCAD.2006.888264"},{"key":"4_CR12","unstructured":"Pulina, L., Tacchella, A.: MIND-Lab projects and related information (2008), http:\/\/www.mind-lab.it\/projects"},{"issue":"1","key":"4_CR13","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H. Kleine-B\u00fcning","year":"1995","unstructured":"Kleine-B\u00fcning, H., Karpinski, M., Fl\u00f6gel, A.: Resolution for Quantified Boolean Formulas. Information and Computation\u00a0117(1), 12\u201318 (1995)","journal-title":"Information and Computation"},{"issue":"1\/2","key":"4_CR14","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1023\/A:1006303512524","volume":"24","author":"I. Rish","year":"2000","unstructured":"Rish, I., Dechter, R.: Resolution versus search: Two strategies for sat. Journal of Automated Reasoning\u00a024(1\/2), 225\u2013275 (2000)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/11889205_37","volume-title":"Principles and Practice of Constraint Programming - CP 2006","author":"H. Samulowitz","year":"2006","unstructured":"Samulowitz, H., Davies, J., Bacchus, F.: Preprocessing QBF. In: Benhamou, F. (ed.) CP 2006. LNCS, vol.\u00a04204, pp. 514\u2013529. Springer, Heidelberg (2006)"},{"key":"4_CR16","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., B\u00fcning, H.K.: 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":"4_CR17","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1038\/30918","volume":"393","author":"D.J. Watts","year":"1998","unstructured":"Watts, D.J., Strogatz, S.H.: Collective dynamics of small-world networks. Nature\u00a0393, 440\u2013442 (1998)","journal-title":"Nature"},{"key":"4_CR18","unstructured":"Walsh, T.: Search in a Small World. In: Proc. of IJCAI (1999)"}],"container-title":["Lecture Notes in Computer Science","AI*IA 2009: Emergent Perspectives in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10291-2_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:53:31Z","timestamp":1606186411000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10291-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642102905","9783642102912"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10291-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}