{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:56Z","timestamp":1761611216319},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540422549"},{"type":"electronic","value":"9783540457442"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45744-5_27","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T21:02:07Z","timestamp":1193432527000},"page":"364-369","source":"Crossref","is-referenced-by-count":59,"title":["QuBE: A System for Deciding Quantified Boolean Formulas Satisfiability"],"prefix":"10.1007","author":[{"given":"Enrico","family":"Giunchiglia","sequence":"first","affiliation":[]},{"given":"Massimo","family":"Narizzano","sequence":"additional","affiliation":[]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,8]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1613\/jair.591","volume":"10","author":"J. Rintanen","year":"1999","unstructured":"Jussi Rintanen. Constructing conditional plans by a theorem prover. Journal of Artificial Intelligence Research, 10:323\u2013352, 1999.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"27_CR2","unstructured":"U. Egly, T. Eiter, H. Tompits, and S. Woltran. Solving advanced reasoning tasks using quantified boolean formulas. In Proc. AAAI, 2000."},{"key":"27_CR3","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"D.A. Plaisted and S. Greenbaum. A Structure-preserving Clause Form Translation. Journal of Symbolic Computation, 2:293\u2013304, 1986.","journal-title":"Journal of Symbolic Computation"},{"key":"27_CR4","unstructured":"M. Cadoli, M. Schaerf, A. Giovanardi, and M. Giovanardi. An algorithm to evaluate quantified boolean formulae and its experimental evaluation. Journal of Automated Reasoning, 2000. To appear. Reprinted in [13]."},{"key":"27_CR5","first-page":"1192","volume-title":"Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI-99-2)","author":"J. T. Rintanen","year":"1999","unstructured":"Jussi T. Rintanen. Improvements to the evaluation of quantified boolean formulae. In Dean Thomas, editor, Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI-99-Vol2), pages 1192\u20131197, S.F., July 31-August 6 1999. Morgan Kaufmann Publishers."},{"key":"27_CR6","unstructured":"R. Feldmann, B. Monien, and S. Schamberger. A distributed algorithm to evaluate quantified boolean formulae. In Proc. AAAI, 2000."},{"key":"27_CR7","unstructured":"Enrico Giunchiglia, Massimo Narizzano, and Armando Tacchella. Back jumping for quantified boolean logic satisfiability. In Proc. of the International Joint Conference on Artificial Intelligence (IJCAI\u20192001), 2001."},{"key":"27_CR8","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/BF02127976","volume":"17","author":"M. B\u00f6hm","year":"1996","unstructured":"M. B\u00f6hm and E Speckenmeyer. A fast parallel SAT-solver-efficient workload balancing. Annals of Mathematics and Artificial Intelligence, 17:381\u2013400, 1996.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"27_CR9","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF01531077","volume":"1","author":"R. G. Jeroslow","year":"1990","unstructured":"Robert G. Jeroslow and Jinchang Wang. Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence, 1:167\u2013187, 1990.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"27_CR10","first-page":"366","volume-title":"Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI-97)","author":"C. M. Li","year":"1997","unstructured":"Chu Min Li and Anbulagan. Heuristics based on unit propagation for satisfiability problems. In Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI-97), pages 366\u2013371, San Francisco, August 23-29 1997. Morgan Kaufmann Publishers."},{"issue":"1","key":"27_CR11","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. and Karpinski, M. and Fl\u00f6gel, A. Resolution for quantified boolean formulas. Information and computation, 117(1):12\u201318, 1995.","journal-title":"Information and computation"},{"key":"27_CR12","unstructured":"Ian Gent and Toby Walsh. Beyond NP: the QSAT phase transition. In Proc. AAAI, pages 648\u2013653, 1999."},{"key":"27_CR13","unstructured":".Ian P. Gent, Hans Van Maaren, and Toby Walsh, editors. SAT2000. Highlights Of Satisfiability Research in the Year 2000. IOS Press, 2000."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45744-5_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,24]],"date-time":"2019-02-24T16:12:40Z","timestamp":1551024760000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45744-5_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422549","9783540457442"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-45744-5_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]}}}