{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,16]],"date-time":"2024-03-16T12:25:55Z","timestamp":1710591955170},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"9","license":[{"start":{"date-parts":[[2017,5,11]],"date-time":"2017-05-11T00:00:00Z","timestamp":1494460800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Sci. China Inf. Sci."],"published-print":{"date-parts":[[2017,9]]},"DOI":"10.1007\/s11432-016-0258-4","type":"journal-article","created":{"date-parts":[[2017,5,15]],"date-time":"2017-05-15T05:38:16Z","timestamp":1494826696000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A randomized diversification strategy for solving satisfiability problem with long clauses"],"prefix":"10.1007","volume":"60","author":[{"given":"Jian","family":"Gao","sequence":"first","affiliation":[]},{"given":"Ruizhi","family":"Li","sequence":"additional","affiliation":[]},{"given":"Minghao","family":"Yin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,5,11]]},"reference":[{"key":"258_CR1","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis M, Putnam H. A computing procedure for quantification theory. J ACM, 1960, 7: 201\u2013215","journal-title":"J ACM"},{"key":"258_CR2","doi-asserted-by":"crossref","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. Commun ACM, 1962, 5: 394\u2013397","journal-title":"Commun ACM"},{"key":"258_CR3","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: 506\u2013521","journal-title":"IEEE Trans Comput"},{"key":"258_CR4","first-page":"279","volume-title":"Proceedings of the 2001 IEEE\/ACM International Conference on Computer-Aided Design","author":"L Zhang","year":"2001","unstructured":"Zhang L, Madigan C F, Moskewicz M H, et al. Efficient conflict driven learning in a Booleansatisfiability solver. In: Proceedings of the 2001 IEEE\/ACM International Conference on Computer-Aided Design. Piscataway: IEEE Press, 2001. 279\u2013285"},{"key":"258_CR5","first-page":"521","volume":"26","author":"B Selman","year":"1996","unstructured":"Selman B, Kautz H A, Cohen B. Local search strategies for satisfiability testing. Discrete Math Theor, 1996, 26: 521\u2013532","journal-title":"Discrete Math Theor"},{"key":"258_CR6","first-page":"337","volume-title":"Proceedings of the 12th National Conference on Artificial Intelligence (AAAI-94)","author":"B Selma","year":"1994","unstructured":"Selma B, Kautz H A, Cohen B. Noise strategies for improving local search. In: Proceedings of the 12th National Conference on Artificial Intelligence (AAAI-94). San Francisco: AAAI Press, 1994. 337\u2013343"},{"key":"258_CR7","doi-asserted-by":"crossref","first-page":"759","DOI":"10.1038\/nature03602","volume":"435","author":"D Achlioptas","year":"2005","unstructured":"Achlioptas D, Naor A, Peres Y. Rigorous location of phase transitions in hard optimization problems. Nature, 2005, 435: 759\u2013764","journal-title":"Nature"},{"key":"258_CR8","first-page":"331","volume-title":"Proceedings of the International Joint Conference on Artificial Intelligence. San Francisco: Morgan Kaufmann Publishers","author":"P Cheeseman","year":"1991","unstructured":"Cheeseman P, Kanefsky B, Taylor W M. Where the really hard problems are. In: Proceedings of the International Joint Conference on Artificial Intelligence. San Francisco: Morgan Kaufmann Publishers, 1991. 331\u2013340"},{"key":"258_CR9","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1613\/jair.696","volume":"12","author":"K Xu","year":"2000","unstructured":"Xu K, Li W. Exact phase transitions in random constraint satisfaction problems. J Artif Intell Res, 2000, 12: 93\u2013103","journal-title":"J Artif Intell Res"},{"key":"258_CR10","doi-asserted-by":"crossref","first-page":"514","DOI":"10.1016\/j.artint.2007.04.001","volume":"171","author":"K Xu","year":"2007","unstructured":"Xu K, Boussemart F, Hemery F, et al. Random constraint satisfaction: easy generation of hard (satisfiable) instances. Artif Intell, 2007, 171: 514\u2013534","journal-title":"Artif Intell"},{"key":"258_CR11","first-page":"459","volume-title":"Proceedings of the 10th National Conference on Artificial Intelligence (AAAI-92)","author":"D G Mitchell","year":"1992","unstructured":"Mitchell D G, Selman B, Levesque H J. Hard and easy distributions of SAT problems. In: Proceedings of the 10th National Conference on Artificial Intelligence (AAAI-92). San Jose: AAAI Press, 1992. 459\u2013465"},{"key":"258_CR12","first-page":"440","volume-title":"Proceedings of the 10th National Conference on Artificial Intelligence (AAAI-92)","author":"B Selman","year":"1992","unstructured":"Selman B, Levesque H, Mitchell D. A new method for solving hard satisfiability problems. In: Proceedings of the 10th National Conference on Artificial Intelligence (AAAI-92). San Jose: AAAI Press, 1992. 440\u2013446"},{"key":"258_CR13","first-page":"233","volume-title":"Proceedings of the 8th International Conference on the Principles and Practice of Constraint Programming","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: Proceedings of the 8th International Conference on the Principles and Practice of Constraint Programming. Berlin: Springer, 2002. 233\u2013248"},{"key":"258_CR14","first-page":"191","volume-title":"Proceedings of the 19th National Conference on Artificial Intelligence (AAAI-04)","author":"J Thornton","year":"2004","unstructured":"Thornton J, Pham D N, Bain S, et al. Additive versus multiplicative clause weighting for SAT. In: Proceedings of the 19th National Conference on Artificial Intelligence (AAAI-04). San Jose: AAAI Press, 2004. 191\u2013196"},{"key":"258_CR15","first-page":"16","volume-title":"Proceedings of the International Conference on Theory and Applications of Satisfiability Testing","author":"A Balint","year":"2012","unstructured":"Balint A, Sch\u00f6ning U. Choosing probability distributions for stochastic local search and the role of make versus break. In: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing. Berlin: Springer, 2012. 16\u201329"},{"key":"258_CR16","first-page":"477","volume-title":"Proceedings of the International Conference on Theory and Applications of Satisfiability Testing","author":"CM Li","year":"2012","unstructured":"Li CM, Li Y. Satisfying versus falsifying in local search for satisfiability. In: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing. Berlin: Springer, 2012. 477\u2013478"},{"key":"258_CR17","first-page":"219","volume":"4","author":"W Wei","year":"2008","unstructured":"Wei W, Li C M, Zhang H. A switching criterion for intensification and diversification in local search for SAT. J Satisfiab Bool Model Comput, 2008, 4: 219\u2013237","journal-title":"J Satisfiab Bool Model Comput"},{"key":"258_CR18","volume-title":"Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing","author":"T T Duong","year":"2013","unstructured":"Duong T T, Pham D N, Sattar A, et al. Weight-enhanced diversification in stochastic local search for satisfiability. In: Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, 2013"},{"key":"258_CR19","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/j.artint.2013.09.001","volume":"204","author":"S Cai","year":"2013","unstructured":"Cai S, Su K. Local search for Boolean Satisfiability with configuration checking and subscore. Artif Intell, 2013, 204: 75\u201398","journal-title":"Artif Intell"},{"key":"258_CR20","first-page":"367","volume-title":"Proceedings of the International Conference on Theory and Applications of Satisfiability Testing","author":"O Gableske","year":"2011","unstructured":"Gableske O, Heule M. EagleUP: solving random 3-SAT using SLS with unit propagation. In: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing. Berlin: Springer, 2011. 367\u2013368"},{"key":"258_CR21","volume-title":"Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing","author":"S Cai","year":"2013","unstructured":"Cai S, Su K. Comprehensive Score: towards efficient local search for SAT with long clauses. In: Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, 2013"},{"key":"258_CR22","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1613\/jair.4480","volume":"51","author":"S Cai","year":"2014","unstructured":"Cai S, Luo C, Su K. Scoring functions based on second level score for k-SAT with long clauses. J Artif Intell Res, 2014, 51: 413\u2013441","journal-title":"J Artif Intell Res"},{"key":"258_CR23","first-page":"302","volume-title":"Proceedings of the International Conference on Theory and Applications of Satisfiability Testing","author":"A Balint","year":"2014","unstructured":"Balint A, Biere A, Fr\u00f6hlich A, et al. Improving implementation of SLS solvers for SAT and new heuristics for k-SAT with long clauses. In: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing. Berlin: Springer, 2014. 302\u2013316"},{"key":"258_CR24","volume-title":"Proceedings of the 26th AAAI Conference on Artificial Intelligence, Phoenix","author":"S Liu","year":"2016","unstructured":"Liu S, Papakonstantinou P A. Local search for hard SAT formulas: The strength of the polynomial law. In: Proceedings of the 26th AAAI Conference on Artificial Intelligence, Phoenix, 2016"},{"key":"258_CR25","doi-asserted-by":"crossref","first-page":"092101","DOI":"10.1007\/s11432-016-5526-8","volume":"59","author":"J Liu","year":"2016","unstructured":"Liu J, Xu K. A novel weighting scheme for random k-SAT. Sci China Inf Sci, 2016, 59: 092101","journal-title":"Sci China Inf Sci"},{"key":"258_CR26","volume-title":"Proceedings of the 26th AAAI Conference on Artificial Intelligence","author":"S Cai","year":"2016","unstructured":"Cai S, Su K. Configuration checking with aspiration in local search for SAT. In: Proceedings of the 26th AAAI Conference on Artificial Intelligence. Phoenix: AAAI Press, 2016"},{"key":"258_CR27","doi-asserted-by":"crossref","first-page":"1672","DOI":"10.1016\/j.artint.2011.03.003","volume":"175","author":"S Cai","year":"2011","unstructured":"Cai S, Su K, Sattar A. Local search with edge weighting and configuration checking heuristics for minimum vertex cover. Artif Intell, 2011, 175: 1672\u20131696","journal-title":"Artif Intell"},{"key":"258_CR28","first-page":"2703","volume-title":"Proceedings of the 28th AAAI Conference on Artificial Intelligence","author":"C Luo","year":"2014","unstructured":"Luo C, Cai S, Wu W, et al. Double configuration checking in stochastic local search for satisfiability. In: Proceedings of the 28th AAAI Conference on Artificial Intelligence. Quebec City: AAAI Press, 2014. 2703\u20132709"},{"key":"258_CR29","doi-asserted-by":"crossref","first-page":"062103","DOI":"10.1007\/s11432-015-5377-8","volume":"60","author":"Y Y Wang","year":"2017","unstructured":"Wang Y Y, Ouyang D T, Zhang L M, et al. A novel local search for unicost set covering problem using hyperedge configuration checking and weight diversity. Sci China Inf Sci, 2017, 60: 062103","journal-title":"Sci China Inf Sci"},{"key":"258_CR30","first-page":"1014","volume":"45","author":"C Luo","year":"2015","unstructured":"Luo C, Cai S, Su K, et al. Clause states based configuration checking in local search for satisfiability. IEEE Trans Cybernetics, 2015, 45: 1014\u20131027","journal-title":"IEEE Trans Cybernetics"}],"container-title":["Science China Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-016-0258-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-016-0258-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-016-0258-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,24]],"date-time":"2019-09-24T16:53:15Z","timestamp":1569343995000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-016-0258-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5,11]]},"references-count":30,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2017,9]]}},"alternative-id":["258"],"URL":"https:\/\/doi.org\/10.1007\/s11432-016-0258-4","relation":{},"ISSN":["1674-733X","1869-1919"],"issn-type":[{"value":"1674-733X","type":"print"},{"value":"1869-1919","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,5,11]]},"article-number":"092109"}}