{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T07:09:10Z","timestamp":1774940950454,"version":"3.50.1"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2008,7,22]],"date-time":"2008-07-22T00:00:00Z","timestamp":1216684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2009,3]]},"DOI":"10.1007\/s10601-008-9051-2","type":"journal-article","created":{"date-parts":[[2008,7,21]],"date-time":"2008-07-21T06:56:21Z","timestamp":1216623381000},"page":"80-116","source":"Crossref","is-referenced-by-count":50,"title":["A self-adaptive multi-engine solver for quantified Boolean formulas"],"prefix":"10.1007","volume":"14","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","published-online":{"date-parts":[[2008,7,22]]},"reference":[{"key":"9051_CR1","first-page":"37","volume":"6","author":"D. Aha","year":"1991","unstructured":"Aha, D., & Kibler, D. (1991). Instance-based learning algorithms. Machine Learning, 6, 37\u201366.","journal-title":"Machine Learning"},{"key":"9051_CR2","unstructured":"Ansotegui, C., Gomes, C. P., & Selman, B. (2005). Achille\u2019s heel of QBF. In Proc. of AAAI (pp. 275\u2013281)."},{"key":"9051_CR3","doi-asserted-by":"crossref","unstructured":"Benedetti, M. (2005). sKizzo: A suite to evaluate and certify QBFs. In 20th int\u2019l. conference on automated deduction, Lecture notes in computer science (Vol. 3632, pp. 369\u2013376). Springer.","DOI":"10.1007\/11532231_27"},{"key":"9051_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A. (2005). Resolve and expand. In Seventh intl. conference on theory and applications of satisfiability testing (SAT\u201904), LNCS (Vol. 3542, pp. 59\u201370).","DOI":"10.1007\/11527695_5"},{"key":"9051_CR5","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/S0004-3702(02)00375-2","volume":"147","author":"C. Castellini","year":"2003","unstructured":"Castellini, C., Giunchiglia, E., & Tacchella, A. (2003). SAT-based planning in complex domains: Concurrency, constraints and nondeterminism. Artificial Intelligence, 147, 85\u2013117.","journal-title":"Artificial Intelligence"},{"key":"9051_CR6","doi-asserted-by":"crossref","unstructured":"Cohen, W. W. (1995). Fast effective rule induction. In Twelfth international conference on machine learning (pp. 115\u2013123).","DOI":"10.1016\/B978-1-55860-377-6.50023-2"},{"issue":"7","key":"9051_CR7","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D. (1962). A machine program for theorem proving. Communications of the ACM, 5(7), 394\u2013397.","journal-title":"Communications of the ACM"},{"key":"9051_CR8","unstructured":"Egly, U., Eiter, T., Tompits, H., & Woltran, S. (2000). Solving advanced reasoning tasks using quantified Boolean formulas. In Seventeenth national conference on artificial intelligence (AAAI 2000) (pp. 417\u2013422). The MIT Press."},{"key":"9051_CR9","doi-asserted-by":"crossref","unstructured":"Gebruers, C., Hnich, B., Bridge, D. G., & Freuder, E. C. (2005). Using CBR to select solution strategies in constraint programming. In Proceedings of the 6th int.l conf. of case-based reasoning, research and development (ICCBR 2005) (pp. 222\u2013236).","DOI":"10.1007\/11536406_19"},{"key":"9051_CR10","unstructured":"Gent, I. P., Nightingale, P., & Rowley, A. (2004). Encoding quantified CSPs as quantified Boolean formulae. In Proceedings of the 16th European conference on artificial intelligence (ECAI 2004) (pp. 176\u2013180)."},{"key":"9051_CR11","unstructured":"Gent, I. P., & Rowley, A. G. D. (2003). Encoding connect 4 using quantified Boolean formulae. Technical Report APES-68-2003, APES Research Group, July."},{"key":"9051_CR12","unstructured":"Giunchiglia, E., Narizzano, M., & Tacchella, A. (2001). Quantified Boolean formulas satisfiability library (QBFLIB). www.qbflib.org ."},{"key":"9051_CR13","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/S0004-3702(00)00081-3","volume":"126","author":"C. P. Gomes","year":"2001","unstructured":"Gomes, C. P., & Selman, B. (2001). Algorithm portfolios. Artificial Intelligence, 126, 43\u201362.","journal-title":"Artificial Intelligence"},{"key":"9051_CR14","unstructured":"Hanna, Z., Dershowitz, N., & Katz, J. (2005). Bounded model checking with QBF. In Eight international conference on theory and applications of satisfiability testing (SAT 2005), Lecture notes in computer science (Vol. 3569, pp. 408\u2013414). Springer."},{"key":"9051_CR15","doi-asserted-by":"crossref","unstructured":"Herbstritt, M., Becker, B., & Scholl, C. (2006). Advanced SAT-techniques for bounded model checking of blackbox designs. In MTV workshop (pp. 37\u201344).","DOI":"10.1109\/MTV.2006.3"},{"key":"9051_CR16","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1126\/science.275.5296.51","volume":"275","author":"B. A. Huberman","year":"1997","unstructured":"Huberman, B. A., Lukose, R. M., & Hogg, T. (1997). An economics approach to hard computational problems. Science, 275, 51\u201354.","journal-title":"Science"},{"key":"9051_CR17","unstructured":"Jussila, T., & Biere, A. (2006). Compressing BMC encodings with QBF. In Proc. 4th intl. workshop on bounded model checking (BMC\u201906)."},{"key":"9051_CR18","doi-asserted-by":"crossref","unstructured":"Kaufman, L., & Rousseeeuw, P. J. (1990). Finding groups in Data. Wiley.","DOI":"10.1002\/9780470316801"},{"issue":"1","key":"9051_CR19","doi-asserted-by":"crossref","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. (1995). Resolution for quantified Boolean formulas. Information and Computation, 117(1), 12\u201318.","journal-title":"Information and Computation"},{"key":"9051_CR20","unstructured":"Kohavi, R. (1995). A study of cross-validation and bootstrap for accuracy estimation and model selection. In Proc. of int\u2019l joint conference on artificial intelligence (IJCAI) (pp. 1137\u20131145)."},{"key":"9051_CR21","doi-asserted-by":"crossref","first-page":"191","DOI":"10.2307\/2347628","volume":"41","author":"S. Cessie Le","year":"1992","unstructured":"Le Cessie, S., & van Houwelingen, J. C. (1992). Ridge estimators in logistic regression. Applied Statistics, 41, 191\u2013201.","journal-title":"Applied Statistics"},{"key":"9051_CR22","unstructured":"Lobjois, L., & Lema\u00eetre, M. (1998). Branch and bound algorithm selection by performance prediction. In Proceedings of 15th nat\u2019l conf. on artificial intelligence (AAAI 1998) (pp. 353\u2013358)."},{"key":"9051_CR23","unstructured":"Mneimneh, M., & Sakallah, K. (2003). Computing vertex eccentricity in exponentially large graphs: QBF formulation and solution. In Sixth international conference on theory and applications of satisfiability testing (SAT 2003), Lecture notes in computer science (Vol. 2919, pp. 411\u2013425). Springer."},{"key":"9051_CR24","unstructured":"Mitchell, D. G., Selman, B., & Levesque, H. J. (1992). Hard and easy distributions for SAT problems. In Proceedings of the tenth national conference on artificial intelligence (pp. 459\u2013465). AAAI Press."},{"key":"9051_CR25","unstructured":"Narizzano, M., Pulina, L., & Taccchella, A. (2006). QBF solvers competitive evaluation (QBFEVAL). http:\/\/www.qbflib.org\/qbfeval ."},{"key":"9051_CR26","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. (2006). The third QBF solvers comparative evaluation. Journal on Satisfiability, Boolean Modeling and Computation, 2, 145\u2013164. Available on-line at http:\/\/jsat.ewi.tudelft.nl\/ .","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"9051_CR27","doi-asserted-by":"crossref","unstructured":"Narizzano, M., Pulina, L., & Tacchella, A. (2006). The QBFEVAL web portal. In 10th European conference on logics in artificial intelligence (JELIA 2006), Lecture notes in computer science (Vol. 4160, pp. 494\u2013497). Springer.","DOI":"10.1007\/11853886_45"},{"key":"9051_CR28","unstructured":"Narizzano, M., Pulina, L., & Tacchella, A. (2007). Ranking and reputation sytems in the QBF competition. In 10th conference of the Italian association for artificial intelligence (AI*IA 2007), Lecture notes in artificial intelligence (Vol. 4733, pp. 97\u2013108). Springer."},{"key":"9051_CR29","unstructured":"Narizzano, M., & Tacchella, A. (2005). QDIMACS prenex CNF standard ver. 1.1. Available online from http:\/\/www.qbflib.org\/qdimacs.html ."},{"key":"9051_CR30","doi-asserted-by":"crossref","unstructured":"Nudelman, E., Devku, A., Shoham, Y., & Leyton-Brown, K. (2004). Understanding random SAT: Beyond the clauses-to-variables ratio. In 10th intl conference on principles and practice of constraint programming (CP2004), LNCS (Vol. 3258, pp. 438\u2013452). Springer.","DOI":"10.1007\/978-3-540-30201-8_33"},{"key":"9051_CR31","unstructured":"Nudelman, E., Leyton-Brown, K., Devkar, A., Shoham, Y., & Hoos, H. (2004). SATzilla: An algorithm portfolio for SAT. In In seventh international conference on theory and applications of satisfiability testing, SAT 2004 competition: Solver descriptions (pp. 13\u201314)."},{"key":"9051_CR32","doi-asserted-by":"crossref","unstructured":"Pan, G., & Vardi, M. Y. (2003). Optimizing a BDD-based modal solver. In Proceedings of the 19th international conference on automated deduction, Lecture notes in computer science (Vol. 2741, pp. 75\u201389). Springer.","DOI":"10.1007\/978-3-540-45085-6_7"},{"key":"9051_CR33","unstructured":"Papadimitriou, C. H. (1994). Computational complexity. Addison-Wesley."},{"key":"9051_CR34","doi-asserted-by":"crossref","unstructured":"Pulina, L., & Tacchella, A. (2007). A multi-engine solver for quantified Boolean formulas. In 13th conference on principles and practice of constraint programming (CP 2007), Lecture notes in computer science (Vol. 4741, pp. 574\u2013589). Springer.","DOI":"10.1007\/978-3-540-74970-7_41"},{"key":"9051_CR35","unstructured":"Quinlan, J. R. (1993). C4.5: Programs for machine learning. Morgan Kaufmann Publishers."},{"key":"9051_CR36","doi-asserted-by":"crossref","unstructured":"Rintanen, J. (2001). Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae. In Proc. LPAR, LNCS (Vol. 2250, pp. 362\u2013376).","DOI":"10.1007\/3-540-45653-8_25"},{"key":"9051_CR37","unstructured":"Samulowitz, H., & Memisevic, R. (2007). Learning to solve QBF. In In proc. of 22nd conference on artificial intelligence (AAAI\u201907) (pp. 255\u2013260)."},{"key":"9051_CR38","unstructured":"St\u00e9phan, I. (2006). Boolean propagation based on literals for quantified Boolean formulae. In Proceedings of 17th European conf. on artificial intelligence (ECAI 2006) (pp. 452\u2013456)."},{"key":"9051_CR39","unstructured":"Stockmeyer, L. J., & Meyer, A. R. (1973). Word problems requiring exponential time. In 5th annual ACM symposium on the theory of computation (pp. 1\u20139)."},{"key":"9051_CR40","unstructured":"Streeter, M. J., Golovin, D., & Smith, S. F. (2007). Restart schedules for ensembles of problem instances. In Proceedings of 22nd AAAI conference on artificial intelligence (AAAI 2007) (pp. 1204\u20131210)."},{"key":"9051_CR41","doi-asserted-by":"crossref","unstructured":"Turner, H. (2002). Polynomial-length planning spans the polynomial hierarchy. In Proc. of eighth European conf. on logics in artificial intelligence (JELIA\u201902), Lecture notes in artificial intelligence (Vol. 2424, pp. 111\u2013124). Springer.","DOI":"10.1007\/3-540-45757-7_10"},{"key":"9051_CR42","unstructured":"Witten, I. H., & Frank, E. (2005). Data mining (2nd ed.). Morgan Kaufmann."},{"key":"9051_CR43","doi-asserted-by":"crossref","unstructured":"Xu, L., Hoos, H. H., & Leyton-Brown, K. (2007). Hierarchical hardness models for SAT. In 13th conference on principles and practice of constraint programming (CP 2007), Lecture notes in computer science (Vol. 4741, pp. 696\u2013711). Springer.","DOI":"10.1007\/978-3-540-74970-7_49"},{"key":"9051_CR44","doi-asserted-by":"crossref","unstructured":"Xu, L., Hutter, F., Hoos, H. H., & Leyton-Brown, K. (2007). The design and analysis of an algorithm portfolio for SAT. In 13th conference on principles and practice of constraint programming (CP 2007), Lecture notes in computer science (Vol. 4741, pp. 712\u2013727). Springer.","DOI":"10.1007\/978-3-540-74970-7_50"}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-008-9051-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10601-008-9051-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-008-9051-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,7]],"date-time":"2020-05-07T04:22:26Z","timestamp":1588825346000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10601-008-9051-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,7,22]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,3]]}},"alternative-id":["9051"],"URL":"https:\/\/doi.org\/10.1007\/s10601-008-9051-2","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"value":"1383-7133","type":"print"},{"value":"1572-9354","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,7,22]]}}}