{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,14]],"date-time":"2026-05-14T09:33:37Z","timestamp":1778751217917,"version":"3.51.4"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2006,10,20]],"date-time":"2006-10-20T00:00:00Z","timestamp":1161302400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2007,2,14]]},"DOI":"10.1007\/s10817-006-9025-2","type":"journal-article","created":{"date-parts":[[2006,10,19]],"date-time":"2006-10-19T13:26:17Z","timestamp":1161264377000},"page":"261-276","source":"Crossref","is-referenced-by-count":7,"title":["An Efficient Approach to Solving Random k-sat Problems"],"prefix":"10.1007","volume":"37","author":[{"given":"Gilles","family":"Dequen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olivier","family":"Dubois","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,10,20]]},"reference":[{"key":"9025_CR1","doi-asserted-by":"crossref","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of Boolean cardinality constraints. In: Principles and Practice of Constraint Programming\u2013CP2003: 9th Internatioanl Conference, LNCS, vol. 2833, pp. 108\u2013122 (2003)","DOI":"10.1007\/978-3-540-45193-8_8"},{"issue":"4","key":"9025_CR2","doi-asserted-by":"crossref","first-page":"1048","DOI":"10.1137\/S0097539700369156","volume":"31","author":"P. Beame","year":"2002","unstructured":"Beame, P., Karp, R., Pitassi, T., Saks, M.: The efficiency of resolution and Davis\u2013Putnam procedures. SIAM 31(4), 1048\u20131075 (2002)","journal-title":"SIAM"},{"issue":"1\u20132","key":"9025_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(95)00184-0","volume":"215","author":"Y. Boufkhad","year":"1999","unstructured":"Boufkhad, Y., Dubois, O.: Length of prime implicants and number of solutions of random CNF formulae. Theor. Comp. Sci. 215(1\u20132), 1\u201330 (1999)","journal-title":"Theor. Comp. Sci."},{"key":"9025_CR4","unstructured":"Braunstein, A., Mezard, M., Zecchina, R.: Survey propagation: an algorithm for satisfiability. arXiv-cond-mat\/0207194 (2002)"},{"issue":"2-3","key":"9025_CR5","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1016\/j.tcs.2004.02.034","volume":"320","author":"S. Cocco","year":"2004","unstructured":"Cocco, S., Monasson, R.: Heuristic average-case analysis of the backtrack resolution of random 3-satisfiability instances. Theor. Comp. Sci. 320(2\u20133), 345\u2013372 (2004)","journal-title":"Theor. Comp. Sci."},{"key":"9025_CR6","unstructured":"Crawford, J.M., Auton, L.D.: Experimental results on the crossover point in satisfiability problems. In: Proceedings of the 11th National Conference on Artificial Intelligence, pp. 21\u201327 (1993)"},{"key":"9025_CR7","first-page":"394","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. J. Assoc. Comput. Mach. 5, 394\u2013397 (1962)","journal-title":"J. Assoc. Comput. Mach."},{"key":"9025_CR8","doi-asserted-by":"crossref","unstructured":"Dequen, G., Dubois, O.: kcnfs: An efficient solver for random k-SAT formulae. In: International Conference on Theory and Applications of Satisfiability Testing (SAT), Selected Revised Papers, LNCS, vol. 6, pp. 486\u2013501 (2003)","DOI":"10.1007\/978-3-540-24605-3_36"},{"key":"9025_CR9","doi-asserted-by":"crossref","unstructured":"Dubois, O., Andre, P., Boufkhad, Y., Carlier, J.: SAT versus UNSAT. In: DIMACS Series in Discr. Math. and Theor. Computer Science, pp. 415\u2013436 (1993)","DOI":"10.1090\/dimacs\/026\/20"},{"issue":"2","key":"9025_CR10","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1006\/jagm.1997.0867","volume":"24","author":"O. Dubois","year":"1997","unstructured":"Dubois, O., Boufkhad, Y.: A general upper bound for the satisfiability threshold of random r-SAT formulae. J. Algorithms 24(2), 395\u2013420 (1997)","journal-title":"J. Algorithms"},{"key":"9025_CR11","unstructured":"Dubois, O., Dequen, G.: A backbone search heuristic for efficient solving of hard 3-SAT Formulae. In: Proceedings of the 17th International Joint Conference on Artificial Intelligence. Seattle, pp. 248\u2013253 (2001a)"},{"key":"9025_CR12","doi-asserted-by":"crossref","unstructured":"Dubois, O., Dequen, G.: The non-existence of (3,1,2)-conjugate orthogonal idempotent Latin square of order 10. In: Proceedings of CP'2001, pp 108\u2013120 (2001b)","DOI":"10.1007\/3-540-45578-7_8"},{"key":"9025_CR13","doi-asserted-by":"crossref","unstructured":"Dubois, O., Mandler, J.: The 3-XORSAT threshold. In: Proceedings of the 43rd Symposium on Foundations of Computer Science, pp. 769\u2013778 (2002)","DOI":"10.1109\/SFCS.2002.1182002"},{"key":"9025_CR14","doi-asserted-by":"crossref","unstructured":"Feige, U.: Relations between average case complexity and approximation complexity. In: Proceedings of the Thirty-fourth Annual ACM Symposium on Theory of Computing, Montreal, Quebec, Canada, pp. 534\u2013543 (2002)","DOI":"10.1145\/509907.509985"},{"key":"9025_CR15","unstructured":"Freeman, J.W.: Improvements to propositional satisfiability search Algorithms. PhD thesis, Department of Computer and Information Science, University of Pennsylvania, Philadelphia (1995)"},{"issue":"1\u20132","key":"9025_CR16","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0004-3702(95)00051-8","volume":"81","author":"J.W. Freeman","year":"1996","unstructured":"Freeman, J.W.: Hard random 3-SAT problems and the Davis\u2013Putnam procedure. Artif. Intell. 81(1\u20132), 183\u2013198 (1996)","journal-title":"Artif. Intell."},{"issue":"3","key":"9025_CR17","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1017\/S0963548303005637","volume":"12","author":"A. Goerdt","year":"2003","unstructured":"Goerdt, A., Jurdzinski, T.: Some results on random unsatisfiable k-Sat instances and approximation algorithms applied to random structures. Comb. Probab. Comput. 12(3), 245\u2013267 (2003)","journal-title":"Comb. Probab. Comput."},{"key":"9025_CR18","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, E., Ostrowski, R., Mazure, B., Sais, L.: Automatic extraction of functional dependencies. In: Testing: 7th International Conference (SAT\u201904), Revised Selected Papers, LNCS, vol. 3542, Springer, pp. 122\u2013132 (2005)","DOI":"10.1007\/11527695_10"},{"key":"9025_CR19","unstructured":"Hoos, H.H.: An adaptive noise mechanism for walkSAT. In: Eighteenth National Conference on Artificial Intelligence, pp. 655\u2013660 (2002)"},{"issue":"4","key":"9025_CR20","doi-asserted-by":"crossref","first-page":"421","DOI":"10.1023\/A:1006350622830","volume":"24","author":"H.H. Hoos","year":"2000","unstructured":"Hoos, H.H., Stutzle, T.: Local search algorithms for SAT: An empirical evaluation. J. Autom. Reason. 24(4), 421\u2013481 (2000)","journal-title":"J. Autom. Reason."},{"key":"9025_CR21","unstructured":"Kullman, O.: Heuristics for SAT algorithms: A systematic study. In: Extended abstract for the Second Workshop on the Satisfiability Problem (SAT'98) (1998)"},{"key":"9025_CR22","doi-asserted-by":"crossref","unstructured":"Leberre, D., Simon, L.: The essentials of the SAT 2003 competition. In: International Conference on Theory and Applications of Satisfiability Testing (SAT), Revised Selected Papers, LNCS, vol. 6 (2003)","DOI":"10.1007\/978-3-540-24605-3_34"},{"key":"9025_CR23","doi-asserted-by":"crossref","unstructured":"Leberre, D., Simon, L.: Fifty-five solvers in Vancouver: The SAT 2004 Competition. In: Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing, SAT 2004, Revised Selected Papers, LNCS, vol. 3542, Springer, pp 321\u2013344 (2005)","DOI":"10.1007\/11527695_25"},{"key":"9025_CR24","unstructured":"Li, C.M.: Exploiting yet more the power of unit clause propagation to solve the 3-SAT problem. In: Proceedings of European Conference on Artificial Intelligence. pp. 11\u201316 (1996)"},{"key":"9025_CR25","unstructured":"Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of the 15th International Joint Conference on Artificial Intelligence. Nagoya, Japan, pp. 366\u2013371 (1997a)"},{"key":"9025_CR26","doi-asserted-by":"crossref","unstructured":"Li, C.M., Anbulagan: Look-ahead versus look-back for satisfiability problems. In: Lecture Notes in Computer Science 1330, pp. 341\u2013355 (1997b)","DOI":"10.1007\/BFb0017450"},{"key":"9025_CR27","doi-asserted-by":"crossref","unstructured":"Mezard, M., Parisi, G., Zecchina, R.: Analytic and algorithmic solutions of random satisfiability problems. Science 297, 812\u2013815 (2002)","DOI":"10.1126\/science.1073287"},{"key":"9025_CR28","unstructured":"Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B., Troyansky, L.: 2+p-SAT: Relation of typical-case complexity to the nature of the phase transition. RSA: Random Struct. Algorithms 15, 414\u2013440 (1999)"},{"key":"9025_CR29","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of 9th Design Automation Conference. Las Vegas (2001)","DOI":"10.1145\/378239.379017"},{"issue":"4","key":"9025_CR30","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1093\/logcom\/9.4.501","volume":"9","author":"J.W. Rosenthal","year":"1999","unstructured":"Rosenthal, J.W., Plotkin, J.W., Franco, J.: The probability of pure literals. J. Log. Comput. 9(4), 501\u2013513 (1999)","journal-title":"J. Log. Comput."},{"key":"9025_CR31","unstructured":"Selman, B., Kautz, H.A.: Ten challenges redux: Recent progress in propositional reasoning and search. Invited paper, Ninth International Conference on Principles and Practice of Constraint Programming (CP 2003). Cork (Ireland) (2003)"},{"key":"9025_CR32","unstructured":"Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: Proceedings of the 12th National Conference on Artificial Intelligence, vol. 1, pp. 337\u2013343. Menlo Park, California (1994)"},{"key":"9025_CR33","unstructured":"Selman, B., Kautz, H.A., McAllester, D.A.: Ten challenges in propositional reasoning and search. In: Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97), pp. 50\u201354 (1997)"},{"key":"9025_CR34","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1613\/jair.711","volume":"12","author":"J. Singer","year":"2000","unstructured":"Singer, J., Gent, I., Smail, A.: Backbone fragility and the local search cost peak. J. Artif. Intell. Res. 12, 235\u2013270 (2000)","journal-title":"J. Artif. Intell. Res."},{"key":"9025_CR35","unstructured":"Slaney, J., Walsh, T.: Backbones in optimization and approximation. In: Proceedings of the 17th International Joint Conference on Artificial Intelligence. Seattle, pp. 254\u2013259 (2001)"},{"key":"9025_CR36","unstructured":"Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: Proceedings of ICCAD, 279\u2013285, IEEE Press, Piscataway, NJ"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9025-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-006-9025-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9025-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T16:38:56Z","timestamp":1736613536000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-006-9025-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10,20]]},"references-count":36,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2007,2,14]]}},"alternative-id":["9025"],"URL":"https:\/\/doi.org\/10.1007\/s10817-006-9025-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,10,20]]}}}