{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T05:25:19Z","timestamp":1737609919001,"version":"3.33.0"},"reference-count":11,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T00:00:00Z","timestamp":1196467200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Sci. China Ser. F-Inf. Sci."],"published-print":{"date-parts":[[2007,12]]},"DOI":"10.1007\/s11432-007-0070-1","type":"journal-article","created":{"date-parts":[[2007,11,17]],"date-time":"2007-11-17T09:41:41Z","timestamp":1195292501000},"page":"915-925","source":"Crossref","is-referenced-by-count":1,"title":["Solving SAT problem by heuristic polarity decision-making algorithm"],"prefix":"10.1007","volume":"50","author":[{"given":"MingE","family":"Jing","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dian","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"PuShan","family":"Tang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"XiaoFang","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hua","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"70_CR1","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1023\/A:1008287028851","volume":"12","author":"Y. Shang","year":"1998","unstructured":"Shang Y, Wah B W. A discrete lagrangian-based global-search method for solving satisfiability problems. J Global Optimiz, 1998, 12(1): 61\u201399","journal-title":"J Global Optimiz"},{"issue":"3","key":"70_CR2","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1360\/04yf0171","volume":"48","author":"M. Ding","year":"2005","unstructured":"Ding M, Tang P S, Zhou D. Integrating advanced reasoning into a SAT solver. Sci China Ser F-Inf, 2005, 48(3): 366\u2013378","journal-title":"Sci China Ser F-Inf"},{"key":"70_CR3","doi-asserted-by":"crossref","unstructured":"Jin H S, Somenzi F. Strong conflict analysis for propositional satisfiability. In: Proceedings of Design, Automation and Test in Europe(DATE), 2006, 06-10, March 2006, (1): 1\u20136","DOI":"10.1109\/DATE.2006.244149"},{"key":"70_CR4","doi-asserted-by":"crossref","unstructured":"Moskewicz M W, Madigan C F, Zhao Y, et al. Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC), 2001. 530\u2013535","DOI":"10.1145\/378239.379017"},{"key":"70_CR5","doi-asserted-by":"crossref","unstructured":"Goldberg E, Novikov Y. BerkMin: A fast and robust SAT-solver. In: Proceedings of Design Automation and Test in Europe (DATE), 2002. 142\u2013149","DOI":"10.1109\/DATE.2002.998262"},{"key":"70_CR6","doi-asserted-by":"crossref","unstructured":"E\u00e9n N, S\u00f6rensson N. An extensible SAT-solver. In: SAT Competition, 2003. 1\u201323","DOI":"10.1007\/978-3-540-24605-3_37"},{"issue":"5","key":"70_CR7","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J. P. Marques-Silva","year":"1999","unstructured":"Marques-Silva J P, Sakallah K A. GRASP: A search algorithm for propositional satisfiability. IEEE Trans Comput, 1999, 48(5): 506\u2013521","journal-title":"IEEE Trans Comput"},{"key":"70_CR8","doi-asserted-by":"crossref","unstructured":"Zhang H. SATO: an efficient propositional prover. In: Proceedings of the International Conference on Automated Deduction. July 1997, 272\u2013275","DOI":"10.1007\/3-540-63104-6_28"},{"key":"70_CR9","unstructured":"Freeman J W. Improvements to propositional satisfiability search algorithms. Ph.D. Thesis. University of Pennsylvania: Department of Computer and Information Science, 1995"},{"key":"70_CR10","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BF01531077","volume":"1","author":"R. J. Jeroslow","year":"1990","unstructured":"Jeroslow R J, Wang J. Solving propositional satisfiability problems. Annal Math Artif Intell, 1990, 1: 167\u2013187","journal-title":"Annal Math Artif Intell"},{"key":"70_CR11","doi-asserted-by":"crossref","unstructured":"Marques-Silva J P. The impact of branching heuristics in propositional satisfiability algorithms. In: 9th Portuguese Conference on Artificial Intelligence (EPIA), 1999, 62\u201374","DOI":"10.1007\/3-540-48159-1_5"}],"container-title":["Science in China Series F: Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-007-0070-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-007-0070-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-007-0070-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T14:20:20Z","timestamp":1737555620000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-007-0070-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,12]]},"references-count":11,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2007,12]]}},"alternative-id":["70"],"URL":"https:\/\/doi.org\/10.1007\/s11432-007-0070-1","relation":{},"ISSN":["1009-2757","1862-2836"],"issn-type":[{"type":"print","value":"1009-2757"},{"type":"electronic","value":"1862-2836"}],"subject":[],"published":{"date-parts":[[2007,12]]}}}