{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T06:50:55Z","timestamp":1760597455883,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642162411"},{"type":"electronic","value":"9783642162428"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16242-8_34","type":"book-chapter","created":{"date-parts":[[2010,10,4]],"date-time":"2010-10-04T12:51:59Z","timestamp":1286196719000},"page":"474-488","source":"Crossref","is-referenced-by-count":9,"title":["Boosting Local Search Thanks to cdcl"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Audemard","sequence":"first","affiliation":[]},{"given":"Jean-Marie","family":"Lagniez","sequence":"additional","affiliation":[]},{"given":"Bertrand","family":"Mazure","sequence":"additional","affiliation":[]},{"given":"Lakhdar","family":"Sa\u00efs","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"34_CR1","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of International Joint Conference on Artificial Intelligence, pp. 399\u2013404 (2009)"},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/978-3-642-02777-2_28","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"A. Balint","year":"2009","unstructured":"Balint, A., Henn, M., Gableske, O.: A novel approach to combine a SLS- and DPLL-solver for the satisfiability problem. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 284\u2013297. Springer, Heidelberg (2009)"},{"key":"34_CR3","first-page":"75","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere, A.: PicoSAT essentials. Journal on Satisfiability\u00a04, 75\u201397 (2008)","journal-title":"Journal on Satisfiability"},{"key":"34_CR4","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"Handbook of Satisfiability","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, February 2009. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press, Amsterdam (2009)"},{"key":"34_CR5","unstructured":"Crawford, J.: Solving satisfiability problems using a combination of systematic and local search. In: Second Challenge on Satisfiability Testing organized by Center for Discrete Mathematics and Computer Science of Rutgers University (1996)"},{"key":"34_CR6","doi-asserted-by":"crossref","unstructured":"Darwiche, A., Pipatsrisawat, K.: Complete Algorithms, ch.\u00a03, pp. 99\u2013130. IOS Press, Amsterdam (2009)","DOI":"10.3233\/978-1-58603-929-5-99"},{"issue":"7","key":"34_CR7","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communication of ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communication of ACM"},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 61\u201375. Springer, Heidelberg (2005)"},{"key":"34_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Een","year":"2004","unstructured":"Een, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"34_CR10","doi-asserted-by":"crossref","unstructured":"Fang, L., Hsiao, M.: A new hybrid solution to boost SAT solver performance. In: Proceedings of DATE, pp. 1307\u20131313 (2007)","DOI":"10.1109\/DATE.2007.364478"},{"key":"34_CR11","unstructured":"Ferris, B., Fr\u00f6hlich, J.: Walksat as an informed heuristic to DPLL in SAT solving. Technical report, CSE 573: Artificial Intelligence (2004)"},{"key":"34_CR12","unstructured":"Gableske, O., R\u00fcth, J.: Satun: A complete hybrid sat solver. SAT2010 paper draft (2010)"},{"key":"34_CR13","unstructured":"Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Conflict-driven answer set solving. In: Proceedings IJCAI 2007, pp. 386\u2013392 (2007)"},{"key":"34_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-02777-2_16","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"E. Goldberg","year":"2009","unstructured":"Goldberg, E.: Boundary points and resolution. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 147\u2013160. Springer, Heidelberg (2009)"},{"key":"34_CR15","unstructured":"Gomes, C., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: AAAI\/IAAI, pp. 431\u2013437 (1998)"},{"key":"34_CR16","unstructured":"Gregoire, E., Mazure, B., Piette, C.: Extracting MUSes. In: proceedings of ECAI, pp. 387\u2013391 (2006)"},{"issue":"3","key":"34_CR17","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s10601-007-9019-7","volume":"12","author":"E. Gregoire","year":"2007","unstructured":"Gregoire, E., Mazure, B., Piette, C.: Local-search extraction of muses. Constraints\u00a012(3), 325\u2013344 (2007)","journal-title":"Constraints"},{"key":"34_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-46135-3_12","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"D. Habet","year":"2002","unstructured":"Habet, D., Li, C.M., Devendeville, L., Vasquez, M.: A hybrid approach for sat. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, pp. 172\u2013184. Springer, Heidelberg (2002)"},{"key":"34_CR19","doi-asserted-by":"crossref","unstructured":"Havens, W., Dilkina, B.: A hybrid schema for systematic local search. In: Canadian Conference on AI, pp. 248\u2013260 (2004)","DOI":"10.1007\/978-3-540-24840-8_18"},{"issue":"1","key":"34_CR20","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s10472-005-0421-9","volume":"43","author":"E. Hirsch","year":"2005","unstructured":"Hirsch, E., Kojevnikov, A.: Unitwalk: A new SAT solver that uses local search guided by unit clause elimination. Annals of Mathematical and Artificial Intelligence\u00a043(1), 91\u2013111 (2005)","journal-title":"Annals of Mathematical and Artificial Intelligence"},{"key":"34_CR21","unstructured":"Hoos, H.: An adaptive noise mechanism for walksat. In: proceedings of AAAI, pp. 655\u2013660 (2002)"},{"key":"34_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/3-540-46135-3_16","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"F. Hutter","year":"2002","unstructured":"Hutter, F., Tompkins, D.A.D., Hoos, H.H.: Scaling and probabilistic smoothing: Efficient dynamic local search for SAT. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, pp. 233\u2013248. Springer, Heidelberg (2002)"},{"key":"34_CR23","unstructured":"Jussien, N., Lhomme, O.: Local search with constraint propagation and conflict-based heuristics. In: AAAI\/IAAI, pp. 169\u2013174 (2000)"},{"key":"34_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45193-8_1","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"H. Kautz","year":"2003","unstructured":"Kautz, H., Selman, B.: Ten challenges redux: Recent progress in propositional reasoning and search. In: Rossi, F. (ed.) CP 2003. LNCS, vol.\u00a02833, pp. 1\u201318. Springer, Heidelberg (2003)"},{"key":"34_CR25","unstructured":"Kroc, L., Sabharwal, A., Gomes, C.P., Selman, B.: Integrating systematic and local search paradigms: A new strategy for maxsat. In: IJCAI, pp. 544\u2013551 (2009)"},{"key":"34_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-79719-7_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"F. Letombe","year":"2008","unstructured":"Letombe, F., Marques-Silva, J.: Improvements to hybrid incremental sat algorithms. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 168\u2013181. Springer, Heidelberg (2008)"},{"key":"34_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-72788-0_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"C.M. Li","year":"2007","unstructured":"Li, C.M., Wei, W., Zhang, H.: Combining adaptive noise and look-ahead in local search for sat. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 121\u2013133. Springer, Heidelberg (2007)"},{"issue":"3-4","key":"34_CR28","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1023\/A:1018999721141","volume":"22","author":"B. Mazure","year":"1998","unstructured":"Mazure, B., Sa\u00efs, L., Gr\u00e9goire, E.: Boosting complete techniques thanks to local search methods. Ann. Math. Artif. Intell.\u00a022(3-4), 319\u2013331 (1998)","journal-title":"Ann. Math. Artif. Intell."},{"key":"34_CR29","unstructured":"McAllester, D., Selman, B., Kautz, H.: Evidence for invariants in local search. In: Proceedings of AAAI, pp. 321\u2013326 (1997)"},{"key":"34_CR30","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of DAC, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"34_CR31","unstructured":"Pham, D.N., Thornton, J., Sattar, A.: Building structure into local search for sat. In: proceedings of IJCAI, pp. 2359\u20132364 (2007)"},{"key":"34_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-72788-0_28","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"K. Pipatsrisawat","year":"2007","unstructured":"Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 294\u2013299. Springer, Heidelberg (2007)"},{"key":"34_CR33","unstructured":"Selman, B., Kautz, H.: An empirical study of greedy local search for satisfiability testing. In: Proceedings of AAAI, pp. 46\u201351 (1993)"},{"key":"34_CR34","unstructured":"Selman, B., Kautz, H., Cohen, B.: Noise strategies for improving local search. In: proceedings of AAAI, pp. 337\u2013343 (1994)"},{"key":"34_CR35","unstructured":"Selman, B., Kautz, H., McAllester, D.: Ten challenges in propositional reasoning and search. In: Proceedings of IJCAI, pp. 50\u201354 (1997)"},{"key":"34_CR36","doi-asserted-by":"crossref","unstructured":"Marques Silva, J., Sakallah, K.: Grasp - a new search algorithm for satisfiability. In: ICCAD, pp. 220\u2013227 (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"34_CR37","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"L. Xu","year":"2008","unstructured":"Xu, L., Hutter, F., Hoos, H.: K\u00a0Leyton-Brown. Satzilla: Portfolio-based algorithm selection for sat. Journal of Artificial Intelligence Research\u00a032, 565\u2013606 (2008)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"34_CR38","unstructured":"Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: proceedings of ICCAD, pp. 279\u2013285 (2001)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16242-8_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,26]],"date-time":"2025-02-26T05:33:54Z","timestamp":1740548034000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16242-8_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642162411","9783642162428"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16242-8_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}