{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T07:17:46Z","timestamp":1725520666281},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540894384"},{"type":"electronic","value":"9783540894391"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-89439-1_37","type":"book-chapter","created":{"date-parts":[[2008,11,15]],"date-time":"2008-11-15T03:03:10Z","timestamp":1226718190000},"page":"528-542","source":"Crossref","is-referenced-by-count":6,"title":["Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic Encodings"],"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":"37_CR1","doi-asserted-by":"crossref","unstructured":"Bodlaender, H.L.: Treewidth: Characterizations, applications, and computations. Technical report, Utrecht University (2006)","DOI":"10.1007\/11917496_1"},{"key":"37_CR2","unstructured":"Freuder, E.: Complexity of k-tree structured constraint satisfation problem. In: Proc. of AAAI 1990 (1990)"},{"key":"37_CR3","doi-asserted-by":"crossref","unstructured":"Dechter, R., Pearl, J.: Tree Clustering for constraint networks. Artificial Intelligence, 61\u201395 (1989)","DOI":"10.1016\/0004-3702(89)90037-4"},{"key":"37_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. Springer, Heidelberg (2005)"},{"key":"37_CR5","unstructured":"Gottlob, G., Greco, G., Scarcello, F.: The Complexity of Quantified Constraint Satisfaction Problems under Structural Restrictions. In: IJCAI 2005, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, pp. 150\u2013155. Professional Book Center (2005)"},{"key":"37_CR6","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1109\/LICS.2006.25","volume-title":"21th IEEE Symposium on Logic in Computer Science (LICS 2006)","author":"G. Pan","year":"2006","unstructured":"Pan, G., Vardi, M.Y.: Fixed-Parameter Hierarchies inside PSPACE. In: 21th IEEE Symposium on Logic in Computer Science (LICS 2006), pp. 27\u201336. IEEE Computer Society, Los Alamitos (2006)"},{"key":"37_CR7","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time. In: 5th Annual ACM Symposium on the Theory of Computation, pp. 1\u20139 (1973)","DOI":"10.1145\/800125.804029"},{"key":"37_CR8","unstructured":"Giunchiglia, E., Narizzano, M., Pulina, L., Tacchella, A.: Quantified Boolean Formulas satisfiability library, QBFLIB (2001), www.qbflib.org"},{"key":"37_CR9","unstructured":"Narizzano, M., Pulina, L., Taccchella, A.: QBF solvers competitive evaluation (QBFEVAL) (2006), http:\/\/www.qbflib.org\/qbfeval"},{"key":"37_CR10","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":"37_CR11","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), http:\/\/www.jair.org\/vol\/vol26.html","journal-title":"Artificial Intelligence Research"},{"key":"37_CR12","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: Proceedings of International Conference on Computer Aided Design (ICCAD 2002) (2002)","DOI":"10.1145\/774572.774637"},{"key":"37_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/11532231_27","volume-title":"Automated Deduction \u2013 CADE-20","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: sKizzo: A suite to evaluate and certify QBFS. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol.\u00a03632, pp. 369\u2013376. Springer, Heidelberg (2005)"},{"key":"37_CR14","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., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"key":"37_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-540-30201-8_34","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","author":"G. Pan","year":"2004","unstructured":"Pan, G., Y. Vardi, M.: Symbolic decision procedures for QBF. In: Wallace, M. (ed.) CP 2004. LNCS, vol.\u00a03258, pp. 453\u2013467. Springer, Heidelberg (2004)"},{"issue":"1\/2","key":"37_CR16","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"},{"issue":"1","key":"37_CR17","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1137\/0214020","volume":"14","author":"R.E. Tarjan","year":"1985","unstructured":"Tarjan, R.E., Yannakakis, M.: Addendum: Simple linear-time algorithms to test chordality of graphs, test acyclicity of hypergraphs, and selectively reduce acyclic hypergraphs. SIAM J. Comput.\u00a014(1), 254\u2013255 (1985)","journal-title":"SIAM J. Comput."},{"key":"37_CR18","unstructured":"Gogate, V., Dechter, R.: A Complete Anytime Algorithm for Treewidth. In: UAI 2004, Proceedings of the 20th Conference in Uncertainty in Artificial Intelligence, pp. 201\u2013208. AUAI Press (2004)"},{"key":"37_CR19","unstructured":"Subbarayan, S., Andersen, H.R.: Backtracking Procedures for Hypertree, HyperSpread and Connected Hypertree Decomposition of CSPs. In: IJCAI, pp. 180\u2013185 (2007)"},{"key":"37_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. Springer, Heidelberg (2005)"},{"key":"37_CR21","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Quantifier Structure in search based procedures for QBFs. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems\u00a026(3) (2007)","DOI":"10.1109\/TCAD.2006.888264"},{"key":"37_CR22","unstructured":"Pulina, L., Taccchella, A.: MIND-Lab projects and related information (2008), http:\/\/www.mind-lab.it\/projects"},{"key":"37_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1007\/978-3-540-74970-7_41","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"L. Pulina","year":"2007","unstructured":"Pulina, L., Tacchella, A.: A multi-engine solver for quantified boolean formulas. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol.\u00a04741, pp. 574\u2013589. Springer, Heidelberg (2007)"},{"key":"37_CR24","volume-title":"Data Mining","author":"I.H. Witten","year":"2005","unstructured":"Witten, I.H., Frank, E.: Data Mining, 2nd edn. Morgan Kaufmann, San Francisco (2005)","edition":"2"},{"issue":"1","key":"37_CR25","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":"3","key":"37_CR26","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1023\/A:1025627211942","volume":"8","author":"J. Larrosa","year":"2003","unstructured":"Larrosa, J., Dechter, R.: Boosting Search with Variable Elimination in Constraint Optimization and Constraint Satisfaction Problems. Constraints\u00a08(3), 303\u2013326 (2003)","journal-title":"Constraints"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-89439-1_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T13:12:51Z","timestamp":1557925971000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-89439-1_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540894384","9783540894391"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-89439-1_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}