{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T18:45:59Z","timestamp":1769971559790,"version":"3.49.0"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2016,6,4]],"date-time":"2016-06-04T00:00:00Z","timestamp":1464998400000},"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":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2017,3]]},"DOI":"10.1007\/s10472-016-9515-9","type":"journal-article","created":{"date-parts":[[2016,6,3]],"date-time":"2016-06-03T22:43:19Z","timestamp":1464993799000},"page":"5-24","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Improving configuration checking for satisfiable random k-SAT instances"],"prefix":"10.1007","volume":"79","author":[{"given":"Andr\u00e9","family":"Abram\u00e9","sequence":"first","affiliation":[]},{"given":"Djamal","family":"Habet","sequence":"additional","affiliation":[]},{"given":"Donia","family":"Toumi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,4]]},"reference":[{"key":"9515_CR1","first-page":"49","volume-title":"Advances in Neural Information Processing Systems, vol. 17","author":"E Aurell","year":"2004","unstructured":"Aurell, E., Gordon, U., Kirkpatrick, S.: Comparing beliefs, surveys, and random walks. In: Saul, L.K., Weiss, Y., Bottou, L. (eds.) Advances in Neural Information Processing Systems, vol. 17, pp. 49\u201356. MIT Press, Cambridge (2004)"},{"key":"9515_CR2","unstructured":"Balint, A., Belov, A., Heule, M.J., J\u00e4rvisalo, M.: Generating the uniform random benchmarks for SAT competition 2013. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions, pp. 97\u201398 (2012)"},{"key":"9515_CR3","unstructured":"Balint, A., Belov, A., J\u00e4rvisalo, M., Sinz, C.: SAT challenge 2012 random sat track: Description of benchmark generation. In: Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions, pp. 72\u201373 (2012)"},{"key":"9515_CR4","doi-asserted-by":"crossref","unstructured":"Balint, A., Fr\u00f6hlich, A.: Improving stochastic local search for sat with a new probability distribution. In: Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing, SAT\u201910, pp. 10\u201315 (2010)","DOI":"10.1007\/978-3-642-14186-7_3"},{"key":"9515_CR5","unstructured":"Balint, A., Sch\u00f6ning, U.: Probsat. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions, p. 70 (2013)"},{"key":"9515_CR6","unstructured":"Cai, S., Luo, C., Su, K.: Ccasat: Solver description. In: Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions, pp. 13\u201314 (2012)"},{"key":"9515_CR7","unstructured":"Cai, S., Luo, C., Su, K.: Cscore2013. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions, pp. 18\u201319 (2013)"},{"key":"9515_CR8","doi-asserted-by":"crossref","unstructured":"Cai, S., Su, K.: Configuration checking with aspiration in local search for SAT. In: Proceedings of the 26th National Conference on Artificial intelligence, AAAI\u201912, pp. 434\u2013440 (2012)","DOI":"10.1609\/aaai.v26i1.8133"},{"key":"9515_CR9","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, IJCAI \u201913, pp. 489\u2013495 (2013)"},{"key":"9515_CR10","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. 204, 75\u201398 (2013)","journal-title":"Artif. Intell."},{"issue":"9\u201310","key":"9515_CR11","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. 175(9\u201310), 1672\u20131696 (2011)","journal-title":"Artif. Intell."},{"key":"9515_CR12","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem proving procedures. In: Proceeding of the Third Annual ACM Symp. on Theory of Computing, pp. 151\u2013158 (1971)","DOI":"10.1145\/800157.805047"},{"issue":"7","key":"9515_CR13","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 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"9515_CR14","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Proceedings of the 7th international conference on Theory and Applications of Satisfiability Testing, SAT\u201903, pp. 333\u2013336 (2004)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"9515_CR15","unstructured":"Habet, D., Toumi, D., Abram\u00e9, A.: Ncca+: Configuration checking and novelty+ like heuristic. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions, p. 62 (2013)"},{"key":"9515_CR16","unstructured":"Hoos, H.H.: On the run-time behaviour of stochastic local search algorithms for SAT. In: Proceedings of the 16th National Conference on Artificial intelligence, AAAI \u201999, pp. 661\u2013666 (1999)"},{"key":"9515_CR17","unstructured":"Hoos, H.H.: An adaptive noise mechanism for walksat. In: Proceedings of the 18th National Conference on Artificial intelligence, AAAI\u201902, pp. 655\u2013660 (2002)"},{"key":"9515_CR18","doi-asserted-by":"crossref","unstructured":"Li, C.M., Huang, W.Q.: Diversification and determinism in local search for satisfiability. In: Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing, SAT\u201905, pp. 158\u2013172 (2005)","DOI":"10.1007\/11499107_12"},{"key":"9515_CR19","unstructured":"Li, C.M., Huang, W.Q.: Switching between two adaptive noise mechanisms in local search for sat. In: SAT 2009 Competitive Events Booklet, p. 57 (2009)"},{"key":"9515_CR20","doi-asserted-by":"crossref","unstructured":"LI, C.M., LI, Y.: Satisfying versus falsifying in local search for satisfiability. In: Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing, SAT\u201912, pp. 477\u2013478 (2012)","DOI":"10.1007\/978-3-642-31612-8_43"},{"key":"9515_CR21","unstructured":"Li, C.M., Li, Y.: Description of sattime2013. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions, pp. 77\u201378 (2013)"},{"issue":"5","key":"9515_CR22","first-page":"1014","volume":"45","author":"C Luo","year":"2015","unstructured":"Luo, C., Cai, S., Su, K., Wu, W.: Clause states based configuration checking in local search for satisfiability. IEEE Trans. Cybern. 45(5), 1014\u20131027 (2015)","journal-title":"IEEE Trans. Cybern."},{"key":"9515_CR23","doi-asserted-by":"crossref","unstructured":"Luo, C., Cai, S., Wu, W., Su, K.: Focused random walk with configuration checking and break minimum for satisfiability. In: Proceedings of the 19th International Conference on Principles and Practice of Constraint Programming, CP\u201913, pp. 481\u2013496 (2013)","DOI":"10.1007\/978-3-642-40627-0_37"},{"issue":"3","key":"9515_CR24","doi-asserted-by":"crossref","first-page":"665","DOI":"10.1007\/s10489-014-0556-7","volume":"41","author":"C Luo","year":"2014","unstructured":"Luo, C., Su, K., Cai, S.: More efficient two-mode stochastic local search for random 3-satisfiability. Appl. Intell. 41(3), 665\u2013680 (2014)","journal-title":"Appl. Intell."},{"issue":"5","key":"9515_CR25","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: Grasp: A search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"9515_CR26","unstructured":"McAllester, D., Selman, B., Kautz, H.: Evidence for invariants in local search. In: Proceedings of the 14th National Conference on Artificial Intelligence, AAAI\u201997, pp. 321\u2013326 (1997)"},{"key":"9515_CR27","unstructured":"Morris, P.: The breakout method for escaping from local minima. In: Proceedings of the 11th National Conference on Artificial intelligence, AAAI\u201993, pp. 40\u201345 (1993)"},{"issue":"2-4","key":"9515_CR28","first-page":"149","volume":"4","author":"DN Pham","year":"2008","unstructured":"Pham, D.N., Thornton, J., Gretton, C., Sattar, A.: Combining adaptive and dynamic local search for satisfiability. JSAT 4(2\u20134), 149\u2013172 (2008)","journal-title":"JSAT"},{"key":"9515_CR29","unstructured":"Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: Proceedings of the 11th National Conference on Artificial Intelligence, AAAI \u201994, pp. 337\u2013343 (1994)"},{"key":"9515_CR30","unstructured":"Thornton, J., Pham, D.N., Bain, S., Ferreira, V.: Additive versus multiplicative clause weighting for SAT. In: Proceedings of the 19th National Conference on Artificial intelligence, AAAI\u201904, pp. 191\u2013196 (2004)"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-016-9515-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-016-9515-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-016-9515-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-016-9515-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,1]],"date-time":"2022-07-01T02:17:30Z","timestamp":1656641850000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-016-9515-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,4]]},"references-count":30,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["9515"],"URL":"https:\/\/doi.org\/10.1007\/s10472-016-9515-9","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,6,4]]}}}