{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T23:34:08Z","timestamp":1648510448002},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2005,5,1]],"date-time":"2005-05-01T00:00:00Z","timestamp":1114905600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2005,5]]},"DOI":"10.1007\/s10472-005-2369-1","type":"journal-article","created":{"date-parts":[[2005,4,15]],"date-time":"2005-04-15T10:22:01Z","timestamp":1113560521000},"page":"157-177","source":"Crossref","is-referenced-by-count":3,"title":["Correlations between Horn fractions, satisfiability and solver performance for fixed density random 3-CNF instances"],"prefix":"10.1007","volume":"44","author":[{"given":"Hans","family":"van Maaren","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Linda","family":"van Norden","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B. Aspvall","year":"1979","unstructured":"B. Aspvall, M.F. Plass and R.E. Tarjan, A linear time algorithm for testing the truth of certain quantified boolean formulas, Information Processing Letters 8 (1979) 121?123.","journal-title":"Information Processing Letters"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"H. Bennaceur and C.M. Li, Characterizing SAT problems with the row convexity property, in: Principles and Practice of Constraint Programming ? CP2002, ed. P. Van Hentenrijck (2002).","DOI":"10.1007\/3-540-46135-3_52"},{"key":"CR3","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/S0378-4371(02)00516-2","volume":"306","author":"G. Biroli","year":"2002","unstructured":"G. Biroli, S. Cocco and R. Monasson, Phase transitions and complexity in computer science: an overview of the statistical physics approach to the random satisfiability problem, Physica A 306 (2002) 381?394.","journal-title":"Physica A"},{"issue":"4","key":"CR4","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1023\/A:1009725216438","volume":"2","author":"B. Borchers","year":"1999","unstructured":"B. Borchers and J. Furman, A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems, Journal of Combinatorial Optimization 2(4) (1999) 299?306.","journal-title":"Journal of Combinatorial Optimization"},{"key":"CR5","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/S0166-218X(99)00031-1","volume":"96?97","author":"E. Boros","year":"1999","unstructured":"E. Boros, Maximum renamable Horn sub-CNFs, Discrete Applied Mathematics 96?97 (1999) 29?40.","journal-title":"Discrete Applied Mathematics"},{"key":"CR6","unstructured":"A. Braunstein, M. Mezard and R. Zecchina, SurveyPropagation: an algorithm for satisfiability, Preprint (2002)."},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"S.A. Cook, The complexity of theorem proving procedures, in: Proceedings of the 3rd Annual ACM Symposium on the Theory of Computing (1971) pp. 151?158.","DOI":"10.1145\/800157.805047"},{"key":"CR8","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/S0166-218X(96)00028-5","volume":"75","author":"Y. Crama","year":"1997","unstructured":"Y. Crama, O. Ekin and P.L. Hammer, Variable and term removal from boolean formulae, Discrete Applied Mathematics 75 (1997) 217?230.","journal-title":"Discrete Applied Mathematics"},{"key":"CR9","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"W.F. Dowling","year":"1984","unstructured":"W.F. Dowling and J.H. Gallier, Linear-time algorithms for testing the satisfiability of propositional Horn formulae, Journal of Logic Programming 1 (1984) 267?284.","journal-title":"Journal of Logic Programming"},{"key":"CR10","unstructured":"O. Dubois and G. Dequen, A backbone-search heuristic for efficient solving of hard 3-SAT formulae, in: Proceedings of IJCAI-01 (2001)."},{"issue":"4","key":"CR11","doi-asserted-by":"crossref","first-page":"1017","DOI":"10.1090\/S0894-0347-99-00305-7","volume":"12","author":"E. Friedgut","year":"1999","unstructured":"E. Friedgut, Sharp thresholds of graph proporties and the k-SAT problem, Journal of the American Mathematical Society 12(4) (1999) 1017?1054.","journal-title":"Journal of the American Mathematical Society"},{"key":"CR12","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0304-3975(76)90059-1","volume":"1","author":"M.R. Garey","year":"1976","unstructured":"M.R. Garey, D.S. Johnson and L. Stockmeyer, Some simplified NP-complete graph problems, Theory of Computer Science 1 (1976) 237?267.","journal-title":"Theory of Computer Science"},{"key":"CR13","unstructured":"E.A. Hirsch and A. Kojevnikov, UnitWalk: A new SAT solver that uses local search guided by unit clause elimination, in: Electronic Proceedings of SAT-2002 (2002)."},{"key":"CR14","unstructured":"O. Kullmann, Investigating the behaviour of a SAT solver on random formulas, Annals of Mathematics and Artificial Intelligence (2002)."},{"key":"CR15","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1038\/22055","volume":"400","author":"R. Monasson","year":"1999","unstructured":"R. Monasson, R. Zecchina, S. Kirkpatrick, B. Selman and L. Troyansky, Determining computational complexity from characteristic ?phase transitions?, Nature 400 (1999) 133?137.","journal-title":"Nature"},{"key":"CR16","unstructured":"N. Nishimura, P. Ragde and S. Szeider, Detecting backdoor sets with respect to Horn and binary clauses, in: Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing (2004)."},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"S. Porschen and E. Speckenmeyer, Worst case bounds for some $\\mathcal{NP}$ -complete modified Horn-SAT problems, in: Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing (2004).","DOI":"10.1007\/11527695_20"},{"key":"CR18","doi-asserted-by":"crossref","unstructured":"H. van Maaren and L. van Norden, Hidden threshold phenomena for fixed-density SAT-formulae, in: Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003, Selected Revised Papers, eds. E. Giunchiglia and A. Tacchella, Lecture Notes in Computer Science, Vol. 2919 (2004) pp. 135?149.","DOI":"10.1007\/978-3-540-24605-3_11"},{"key":"CR19","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1023\/A:1021200130191","volume":"37","author":"H. Maaren van","year":"2003","unstructured":"H. van Maaren and J.P. Warners, Solving satisfiability problems using elliptic approximations. A note on volumes and weights, Annals of Mathematics and Artificial Intelligence 37 (2003) 273?283.","journal-title":"Annals of Mathematics and Artificial Intelligence"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-005-2369-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-005-2369-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-005-2369-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T22:12:06Z","timestamp":1586211126000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-005-2369-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,5]]},"references-count":19,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2005,5]]}},"alternative-id":["12369"],"URL":"https:\/\/doi.org\/10.1007\/s10472-005-2369-1","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,5]]}}}