{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T07:02:58Z","timestamp":1725519778220},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540886358"},{"type":"electronic","value":"9783540886365"}],"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-88636-5_3","type":"book-chapter","created":{"date-parts":[[2008,10,16]],"date-time":"2008-10-16T22:19:04Z","timestamp":1224195544000},"page":"34-43","source":"Crossref","is-referenced-by-count":0,"title":["QuBIS: An (In)complete 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":"3_CR1","unstructured":"Ansotegui, C., Gomes, C.P., Selman, B.: Achille\u2019s heel of QBF. In: Proc. of AAAI, pp. 275\u2013281 (2005)"},{"key":"3_CR2","series-title":"Lecture Notes in Artificial Intelligence","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 (LNAI), vol.\u00a03632, pp. 369\u2013376. Springer, Heidelberg (2005)"},{"key":"3_CR3","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.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"key":"3_CR4","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)"},{"issue":"3","key":"3_CR5","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"3_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. The MIT Press, Cambridge (2000)"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Van Gelder, A., Tsuji, Y.K.: Satisfiability testing with more reasoning and less guessing. Technical Report UCSC-CRL-95-34 (1995)","DOI":"10.1090\/dimacs\/026\/27"},{"key":"3_CR8","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Quantified Boolean Formulas satisfiability library (QBFLIB) (2001), www.qbflib.org"},{"key":"3_CR9","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":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-540-45193-8_24","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"A.G.D. Rowley","year":"2003","unstructured":"Rowley, A.G.D., Gent, I.P., Hoos, H.H., Smyth, K.: Using Stochastic Local Search to Solve Quantified Boolean Formulae. In: Rossi, F. (ed.) CP 2003. LNCS, vol.\u00a02833, pp. 348\u2013362. Springer, Heidelberg (2003)"},{"key":"3_CR11","unstructured":"Jussila, T., Biere, A.: Compressing BMC Encodings with QBF. In: Proc. 4th Intl. Workshop on Bounded Model Checking (BMC 2006) (2006)"},{"issue":"1","key":"3_CR12","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":"3_CR13","unstructured":"Narizzano, M., Pulina, L., Taccchella, A.: QBF solvers competitive evaluation (QBFEVAL) (2006), http:\/\/www.qbflib.org\/qbfeval"},{"key":"3_CR14","unstructured":"Narizzano, M., Pulina, L., Tacchella, A.: QBF competition 2006 (qbfeval 2006), www.qbfeval.org\/2006"},{"key":"3_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., Vardi, M.Y.: Symbolic Decision Procedures for QBF. In: Wallace, M. (ed.) CP 2004. LNCS, vol.\u00a03258, pp. 453\u2013467. Springer, Heidelberg (2004)"},{"key":"3_CR16","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)"},{"issue":"1\/2","key":"3_CR17","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":"3_CR18","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":"3_CR19","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"}],"container-title":["Lecture Notes in Computer Science","MICAI 2008: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88636-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,18]],"date-time":"2021-09-18T19:10:20Z","timestamp":1631992220000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88636-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540886358","9783540886365"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88636-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}