{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:04:21Z","timestamp":1725487461065},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540426011"},{"type":"electronic","value":"9783540454113"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45411-x_13","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:17:28Z","timestamp":1184588248000},"page":"111-122","source":"Crossref","is-referenced-by-count":4,"title":["An Analysis of Backjumping and Trivial Truth in 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,9,7]]},"reference":[{"key":"13_CR1","unstructured":"M. Cadoli, A. Giovanardi, and M. Schaerf. An algorithm to evaluate quantified boolean formulae. In Proc. of AAAI, 1998."},{"key":"13_CR2","unstructured":"M. Cadoli, M. Schaerf, A. Giovanardi, and M. Giovanardi. An Algorithm to Evaluate Quantified Boolean Formulae and its Experimental Evaluation. In Highlights of Satisfiability Research in the Year 2000. IOS Press, 2000."},{"key":"13_CR3","unstructured":"E. Giunchiglia, M. Narizzano, and A. Tacchella. Backjumping for Quantified Boolean Logic Satisfiability. In Proc. of IJCAI, 2001. To appear."},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"E. Giunchiglia, M. Narizzano, and A. Tacchella. QuBE: a system for Deciding Quantified Boolean Formulas Satisfiability. In Proc. of IJCAR, 2001.","DOI":"10.1007\/3-540-45744-5_27"},{"key":"13_CR5","unstructured":"R. Feldmann, B. Monien, and S. Schamberger. A Distributed Algorithm to Evaluate Quantified Boolean Formulae. In Proc. of AAAI, 2000."},{"key":"13_CR6","unstructured":"Ian Gent and Toby Walsh. Beyond NP: the QSAT phase transition. In Proc. of AAAI, pages 648\u2013653, 1999."},{"key":"13_CR7","unstructured":"J. T. Rintanen. Improvements to the Evaluation of Quantified Boolean Formulae. In Proc. of IJCAI, pages 1192\u20131197, 1999."},{"issue":"1","key":"13_CR8","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H. Kleine-B\u00fcning","year":"1995","unstructured":"H. Kleine-B\u00fcning and M. Karpinski and A. Fl\u00f6gel. Resolution for quantified boolean formulas. Information and Computation, 117(1):12\u201318, 1995.","journal-title":"Information and Computation"},{"key":"13_CR9","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":"13_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of IJCAR","author":"E. Giunchiglia","year":"2001","unstructured":"E. Giunchiglia, M. Maratea, A. Tacchella, and D. Zambonin. Evaluating search heuristics and optimization techniques in propositional satisfiability. In Proc. of IJCAR, LNCS. Springer Verlag, 2001. To appear."},{"key":"13_CR11","unstructured":"M. Buro and H. Kleine-B\u00fcning. Report on a SAT competition. Technical Report 110, University of Paderborn, November 1992."},{"key":"13_CR12","unstructured":"D. S. Moore and G. P. McCabe. Introduction to the Practice of Statistics. W. H. Freeman and Co., 1993."}],"container-title":["Lecture Notes in Computer Science","AI*IA 2001: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45411-X_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T18:42:11Z","timestamp":1550428931000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45411-X_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540426011","9783540454113"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-45411-x_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}