{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T05:14:07Z","timestamp":1737090847659,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540441205"},{"type":"electronic","value":"9783540461357"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46135-3_12","type":"book-chapter","created":{"date-parts":[[2007,5,15]],"date-time":"2007-05-15T05:59:47Z","timestamp":1179208787000},"page":"172-184","source":"Crossref","is-referenced-by-count":18,"title":["A Hybrid Approach for SAT"],"prefix":"10.1007","author":[{"given":"Djamal","family":"Habet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chu Min","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laure","family":"Devendeville","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michel","family":"Vasquez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,2]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Y. Asahiro, K. Iwama, and E. Miyano. Random Generation of Test Instances with Controlled Attributes. In D. S. Johnson and M. A. Trick, editors, Cliques, Coloring, and Satisfiability; The Second DIMACS Implementation Challenge, volume 26, pages 377\u2013394, 1996.","key":"12_CR1","DOI":"10.1090\/dimacs\/026\/18"},{"unstructured":"L. Brisoux Devendeville, L. Sa\u00efs, and E. Gr\u00e9goire. Recherche locale: vers une exploitation des propri\u00e9t\u00e9s structurelles. In proceedings of JNPC\u20192000, pages 243\u2013244, Marseille, France, 2000.","key":"12_CR2"},{"doi-asserted-by":"crossref","unstructured":"S. Cook. The Complexity of Theorem Proving Procedures. In Proceeding oh the Third Annual ACM Symp. on Theory of Computing, pages 151\u2013158, 1971.","key":"12_CR3","DOI":"10.1145\/800157.805047"},{"issue":"1\u20132","key":"12_CR4","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/0004-3702(95)00046-1","volume":"81","author":"J. M. Crawford","year":"1996","unstructured":"J. M. Crawford and L. D. Auton. Experimental Results on the Crosover Point in Random 3-SAT. Artificial Intelligence Journal, 81(1\u20132):31\u201357, 1996.","journal-title":"Artificial Intelligence Journal"},{"doi-asserted-by":"crossref","unstructured":"M. Davis, G. Logemann, and D. Loveland. A Machine Program for Theorem Proving. In Communication of ACM Journal, volume 5(7), pages 394\u2013397, July 1962.","key":"12_CR5","DOI":"10.1145\/368273.368557"},{"doi-asserted-by":"crossref","unstructured":"F. J. Ferguson and T. Larrabee. Test Pattern Generation for Realistic Bridging Faults in CMOS ICS. In Proceedings of the International Testing Conference, pages 492\u2013499, 1991.","key":"12_CR6","DOI":"10.1109\/TEST.1991.519711"},{"key":"12_CR7","series-title":"PhD thesis","volume-title":"Improvements to Propostional Satisfiability Search Algorithms","author":"J. W. Freeman","year":"1995","unstructured":"J. W. Freeman. Improvements to Propostional Satisfiability Search Algorithms. PhD thesis, Departement of Computer and Information Science, University of Pennsylvania, Philadelphia, PA, 1995."},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0004-3702(95)00051-8","volume":"81","author":"J. W. Freeman","year":"1996","unstructured":"J. W. Freeman. Hard Random 3-SAT Problems and the Davis-Putnam Procedure. In Artificial Intelligence Journal, pages 81:183\u2013198, 1996.","journal-title":"Artificial Intelligence Journal"},{"key":"12_CR9","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1613\/jair.1","volume":"1","author":"M. L. Ginsberg","year":"1993","unstructured":"M. L. Ginsberg. Dynamic backtracking. Journal of Artificial Intelligence Research, 1:25\u201346, 1993.","journal-title":"Journal of Artificial Intelligence Research"},{"doi-asserted-by":"crossref","unstructured":"M. L. Ginsberg and D. A. McAllester. GSAT and Dynamic Backtracking. In P. Torasso, J. Doyle, and E. Sandewall, editors, Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning KR\u201994, pages 226\u2013237. Morgan Kaufmann, 1994.","key":"12_CR10","DOI":"10.1016\/B978-1-4832-1452-8.50117-2"},{"doi-asserted-by":"crossref","unstructured":"F. Glover and M. Laguna. Tabu Search. Kluwer Academic Publishers, 1997.","key":"12_CR11","DOI":"10.1007\/978-1-4615-6089-0"},{"issue":"1","key":"12_CR12","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/130836.130837","volume":"3","author":"J. Gu","year":"1992","unstructured":"J. Gu. Efficient Local Search for Very Large-Scale Satisfiability problems. In ACM SIGART Bulletin, pages 3(1):8\u201312, 1992.","journal-title":"ACM SIGART Bulletin"},{"issue":"4","key":"12_CR13","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1023\/A:1006350622830","volume":"24","author":"H. H. Hoos","year":"2000","unstructured":"H. H. Hoos and T. Stutzle. Local search algorithms for SAT: An empirical evaluation. Journal of Automated Reasoning, 24(4):421\u2013481, 2000.","journal-title":"Journal of Automated Reasoning"},{"unstructured":"N. Jussien and O. Lhomme. Local search with constraint propagation and conflict-based heuristics. In Proceedings of the Seventh National Conference on Artificial Intelligence (AAAI\u20192000), pages 169\u2013174, Austin, TX, USA, August 2000.","key":"12_CR14"},{"unstructured":"H. Kautz, D. McAllester, and B. Selman. Encoding Plans in Propositional Logic. In Proceedings of the 4th International Conference on the Principle of Knowledge Representation and Reasoning, KR\u201996, pages 374\u2013384, 1996.","key":"12_CR15"},{"unstructured":"H. Kautz and B. Selman. Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search. In Howard Shrobe and Ted Senator, editors, Proceedings of the 13th National Conference on Artificial Intelligence and the 8th Innovative Applications of Artificial Intelligence Conference, pages 1194\u20131201, Menlo Park, California, 1996.","key":"12_CR16"},{"unstructured":"J. Lang and P. Marquis. Complexity Results for Independence and Definability in Propositional Logic. In A. G. Cohn, L. K. Schubert, and S. C. Shapiro, editors, Proceedings of the Sixth International Conference on Principles of Knowledge Representataion and Reasoning, KR\u201998, pages 356\u2013367, 1998.","key":"12_CR17"},{"issue":"1","key":"12_CR18","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1109\/43.108614","volume":"11","author":"T. Larrabee","year":"1992","unstructured":"T. Larrabee. Test Pattern Generation Using Boolean Satisfiability. In IEEE Transactions on Computer-Aided Design, pages 11(1):6\u201322, 1992.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"unstructured":"C. M. Li. Exploiting Yet More the Power of Unit Clause Propagation to solve 3-SAT Problem. In ECAI\u201996 Workshop on Advances in Propositional Deduction, pages 11\u201316, Budapest, Hungray, 1996.","key":"12_CR19"},{"key":"12_CR20","series-title":"Lect Notes Comput Sci","first-page":"342","volume-title":"Proceedings of CP\u201997","author":"C. M. Li","year":"1997","unstructured":"C. M. Li and Anbulagan. Heuristic Based on Unit Propagation for Satisfiability. In Proceedings of CP\u201997, Springer-Verlag, LNCS 1330, pages 342\u2013356, Austria, 1997."},{"issue":"3\u20134","key":"12_CR21","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1023\/A:1018999721141","volume":"22","author":"B. Mazure","year":"1998","unstructured":"B. Mazure, L. Sa\u00efs, and E. Gr\u00e9goire. Boosting Complete Techniques Thanks to Local Search. Annals of Mathematics and Artificial Intelligence, 22(3\u20134):319\u2013331, 1998.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"unstructured":"D. McAllester, B. Selman, and H. Kautz. Evidence for Invariants in Local Search. In Proceedings of the 14th National Conference on Artificial Intelligence, AAAI\u201997, pages 321\u2013326, Providence, Rhode Island, 1997. MIT Press.","key":"12_CR22"},{"unstructured":"B. Selman, H. Kautz, and B. Cohen. Noise Strategies for Improving Local Search. In MIT press, editor, Proceedings of the 12th National Conference on Artificial Intelligence AAAI\u201994, volume 1, pages 337\u2013343, 1994.","key":"12_CR23"},{"unstructured":"B. Selman, H. Kautz, and D. McAllester. Ten Challenges in Propositional Reasoning and Search. In Proceedings of IJCAI\u201997, pages 50\u201354, Nagoya, Aichi, Japan, August 1997.","key":"12_CR24"},{"unstructured":"B. Selman, H. J. Levesque, and D. Mitchell. A New Method for Solving Hard Satisfiability Problems. In Paul Rosenbloom and Peter Szolovits, editors, Proceedings of the 10th National Conference on Artificial Intelligence, AAAI\u201992, pages 440\u2013446, Menlo Park, California, 1992.","key":"12_CR25"},{"unstructured":"M. N. Velev and R. E. Bryant. Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions to propositional logic. In Correct Hardware Design and Verification Methods, CHARME\u201999, 1999.","key":"12_CR26"},{"issue":"1","key":"12_CR27","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1023\/A:1006351428454","volume":"24","author":"H. Zhang","year":"2000","unstructured":"H. Zhang and M. E. Stickel. Implementing the davis-putnam method. Journal of Automated Reasoning, 24(1):277\u2013296, 2000.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming - CP 2002"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46135-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T08:24:20Z","timestamp":1737015860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46135-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441205","9783540461357"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-46135-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2002]]}}}