{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:36:17Z","timestamp":1725492977666},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540749691"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74970-7_41","type":"book-chapter","created":{"date-parts":[[2007,10,9]],"date-time":"2007-10-09T23:49:08Z","timestamp":1191973748000},"page":"574-589","source":"Crossref","is-referenced-by-count":22,"title":["A Multi-engine Solver for Quantified Boolean Formulas"],"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":"41_CR1","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 (1973)","DOI":"10.1145\/800125.804029"},{"key":"41_CR2","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)"},{"key":"41_CR3","unstructured":"Gent, I.P., Nightingale, P., Rowley, A.: Encoding Quantified CSPs as Quantified Boolean Formulae. In: Proceedings of the 16th European Conference on Artificial Intelligence (ECAI 2004) (2004)"},{"key":"41_CR4","unstructured":"Jussila, T., Biere, A.: Compressing BMC encodings with QBF. In: Proc. 4th Intl. Workshop on Bounded Model Checking (BMC 2006) (2006)"},{"key":"41_CR5","unstructured":"Ansotegui, C., Gomes, C.P., Selman, B.: Achille\u2019s heel of QBF. In: Proc. of AAAI (2005)"},{"key":"41_CR6","first-page":"417","volume-title":"Seventeenth National Conference on Artificial Intelligence (AAAI 2000)","author":"U. Egly","year":"2000","unstructured":"Egly, U., Eiter, T., Tompits, H., Woltran, S.: Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas. In: Seventeenth National Conference on Artificial Intelligence (AAAI 2000), pp. 417\u2013422. MIT Press, Cambridge (2000)"},{"key":"41_CR7","unstructured":"Narizzano, M., Pulina, L., Taccchella, A.: QBF solvers competitive evaluation (QBFEVAL) (2003-2007), http:\/\/www.qbflib.org\/qbfeval"},{"key":"41_CR8","doi-asserted-by":"crossref","unstructured":"Huberman, B.A., Lukose, R.M., Hogg, T.: An economics approach to hard computational problems. Science\u00a03 (1997)","DOI":"10.1126\/science.275.5296.51"},{"key":"41_CR9","doi-asserted-by":"crossref","unstructured":"Gomes, C.P., Selman, B.: Algorithm portfolios. Artificial Intelligence\u00a0126 (2001)","DOI":"10.1016\/S0004-3702(00)00081-3"},{"key":"41_CR10","series-title":"Lecture Notes in Computer Science","first-page":"13","volume-title":"Theory and Applications of Satisfiability Testing","author":"E. Nudelman","year":"2005","unstructured":"Nudelman, E., Leyton-Brown, K., Devkar, A., Shoham, Y., Hoos, H.: SATzilla: An Algorithm Portfolio for SAT. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 13\u201314. Springer, Heidelberg (2005)"},{"key":"41_CR11","unstructured":"Samulowitz, H., Memisevic, R.: Learning to Solve QBF. In: AAAI 2007. Proc. of 22nd Conference on Artificial Intelligence (2007)"},{"issue":"7","key":"41_CR12","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\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"issue":"1","key":"41_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"},{"key":"41_CR14","series-title":"Lecture Notes in Artificial Intelligence","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.) Automated Deduction \u2013 CADE-20. LNCS (LNAI), vol.\u00a03632. Springer, Heidelberg (2005)"},{"key":"41_CR15","series-title":"Lecture Notes in Computer Science","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. Springer, Heidelberg (2005)"},{"key":"41_CR16","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Quantified Boolean Formulas satisfiability library (QBFLIB) (2001), www.qbflib.org"},{"key":"41_CR17","doi-asserted-by":"crossref","first-page":"145","DOI":"10.3233\/SAT190019","volume":"2","author":"M. Narizzano","year":"2006","unstructured":"Narizzano, M., Pulina, L., Tacchella, A.: The third QBF solvers comparative evaluation. Journal on Satisfiability, Boolean Modeling and Computation\u00a02, 145\u2013164 (2006), http:\/\/jsat.ewi.tudelft.nl\/","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"41_CR18","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316801","volume-title":"Finding Groups in Data","author":"L. Kaufman","year":"1990","unstructured":"Kaufman, L., Rousseeeuw, P.J.: Finding Groups in Data. Wiley, Chichester (1990)"},{"key":"41_CR19","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"},{"key":"41_CR20","volume-title":"C4.5: Programs for Machine Learning","author":"J.R. Quinlan","year":"1993","unstructured":"Quinlan, J.R.: C4.5: Programs for Machine Learning. Morgan Kaufmann, San Francisco (1993)"},{"key":"41_CR21","doi-asserted-by":"crossref","unstructured":"Cohen, W.W.: Fast effective rule induction. In: Twelfth International Conference on Machine Learning, pp. 115\u2013123 (1995)","DOI":"10.1016\/B978-1-55860-377-6.50023-2"},{"key":"41_CR22","doi-asserted-by":"publisher","first-page":"191","DOI":"10.2307\/2347628","volume":"41","author":"S. Cessie Le","year":"1992","unstructured":"Le Cessie, S., van Houwelingen, J.C.: Ridge estimators in logistic regression. Applied Statistics\u00a041, 191\u2013201 (1992)","journal-title":"Applied Statistics"},{"key":"41_CR23","doi-asserted-by":"crossref","unstructured":"Aha, D., Kibler, D.: Instance-based learning algorithms. Machine Learning, 37\u201366 (1991)","DOI":"10.1007\/BF00153759"},{"key":"41_CR24","unstructured":"Kohavi, R.: A study of cross-validation and bootstrap for accuracy estimation and model selection. In: Proc. of Intl. Joint Conference on Artificial Intelligence (IJCAI) (2005)"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming \u2013 CP 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74970-7_41.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:25:18Z","timestamp":1605763518000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74970-7_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540749691"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74970-7_41","relation":{},"subject":[]}}