{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:35:24Z","timestamp":1725564924029},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540202028"},{"type":"electronic","value":"9783540451938"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45193-8_24","type":"book-chapter","created":{"date-parts":[[2010,9,8]],"date-time":"2010-09-08T23:35:03Z","timestamp":1283988903000},"page":"348-362","source":"Crossref","is-referenced-by-count":10,"title":["Using Stochastic Local Search to Solve Quantified Boolean Formulae"],"prefix":"10.1007","author":[{"given":"Ian P.","family":"Gent","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger H.","family":"Hoos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew G. D.","family":"Rowley","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kevin","family":"Smyth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","unstructured":"Guinchiglia, E., Narizzano, M., Tacchella, A.: Backjumping for quantified Boolean logic satisfiability. In: IJCAI 2001, pp. 275\u2013281 (2001)"},{"key":"24_CR2","unstructured":"Selman, B., Kautz, H.: Domain-independent extensions to GSAT: solving large structured satisfiability problems. In: IJCAI 1993, pp. 290\u2013295 (1993)"},{"key":"24_CR3","unstructured":"McAllester, D., Selman, B., Kautz, H.: Evidence for invariants in local search. In: AAAI 1997, pp. 321\u2013326 (1997)"},{"key":"24_CR4","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/3-540-45411-X_13","volume-title":"AI*IA- 2001","author":"E. Guinchiglia","year":"2001","unstructured":"Guinchiglia, E., Narizzano, M., Tacchella, A.: An analysis of backjumping and trivial truth in quantified Boolean formulas satisfiability. In: AI*IA- 2001, pp. 111\u2013122. Springer, Heidelberg (2001)"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-46135-3_14","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: Towards a symmetric treatment of satisfaction and conflicts in quantified boolean formula evaluation. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, pp. 200\u2013215. Springer, Heidelberg (2002)"},{"key":"24_CR6","unstructured":"Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified Boolean formulae. In: AAAI 1998, pp. 262\u2013267 (1998)"},{"key":"24_CR7","unstructured":"Hoos, H.: Stochastic Local Search - Methods, Models, Applications. PhD thesis (1998)"},{"key":"24_CR8","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1023\/A:1006350622830","volume":"24","author":"H. Hoos","year":"2000","unstructured":"Hoos, H., St\u00fctzle, T.: Local search algorithms for SAT: An empirical evaluation. J. of Automated Reasoning\u00a024, 421\u2013481 (2000)","journal-title":"J. of Automated Reasoning"},{"key":"24_CR9","unstructured":"Gent, I., Walsh, T.: Beyond NP: the QSAT phase transition. In: AAAI 1999, pp. 648\u2013653 (1999)"},{"key":"24_CR10","unstructured":"Rintanen, J.: Improvements to the evaluation of quantified boolean formulae. In: IJCAI 1999, pp. 1192\u20131197 (1999)"},{"key":"24_CR11","unstructured":"Guinchiglia, E., Narizzano, M., Tacchella, A.: Learning for quantified boolean logic satisfiability. In: AAAI 2002, pp. 649\u2013654 (2002)"},{"key":"24_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-45616-3_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Letz","year":"2002","unstructured":"Letz, R.: Lemma and model caching in decision procedures for quantified boolean formulas. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 160\u2013175. Springer, Heidelberg (2002)"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Plaisted, D., Biere, A., Zhu, Y.: A satisfiability procedure for quantified boolean formulae. Discrete Applied Mathematics (2003) (to appear)","DOI":"10.1016\/S0166-218X(02)00409-2"},{"key":"24_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/3-540-45653-8_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Rintanen","year":"2001","unstructured":"Rintanen, J.: Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 362\u2013376. Springer, Heidelberg (2001)"},{"key":"24_CR15","unstructured":"Schiex, T., Verfaillie, G.: Stubbornness: a possible enhancement for backjumping and no-good recording. In: ECAI 1994, pp. 165\u2013169 (1994)"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming \u2013 CP 2003"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45193-8_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,18]],"date-time":"2019-01-18T03:11:48Z","timestamp":1547781108000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45193-8_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540202028","9783540451938"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45193-8_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}