{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T15:48:00Z","timestamp":1649173680708},"reference-count":33,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":3766,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Discrete Applied Mathematics"],"published-print":{"date-parts":[[2003,5]]},"DOI":"10.1016\/s0166-218x(02)00385-2","type":"journal-article","created":{"date-parts":[[2003,5,12]],"date-time":"2003-05-12T23:10:20Z","timestamp":1052781020000},"page":"523-534","source":"Crossref","is-referenced-by-count":0,"title":["A complete adaptive algorithm for propositional satisfiability"],"prefix":"10.1016","volume":"127","author":[{"given":"Renato","family":"Bruni","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antonio","family":"Sassano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0166-218X(02)00385-2_BIB1","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1090\/dimacs\/026\/18","article-title":"Random generation of test instances with controlled attributes","volume":"26","author":"Asahiro","year":"1996","journal-title":"DIMACS Ser. Discrete Math. Theoret. Comput. Sci."},{"key":"10.1016\/S0166-218X(02)00385-2_BIB2","doi-asserted-by":"crossref","unstructured":"R.J. Bayardo, R.C. Schrag, Using CSP look-back techniques to solve real-world SAT instances, in: Proceedings AAAI-97, 1997.","DOI":"10.1007\/3-540-61551-2_65"},{"key":"10.1016\/S0166-218X(02)00385-2_BIB3","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1137\/S0097539792228629","article-title":"A complexity index for satisfiability problems","volume":"23","author":"Boros","year":"1994","journal-title":"SIAM J. Comput."},{"key":"10.1016\/S0166-218X(02)00385-2_BIB4","doi-asserted-by":"crossref","unstructured":"R. Bruni, A. Sassano, Finding minimal unsatisfiable subformulae in satisfiability instances, in: Proceedings of the Sixth International Conference on Principles and Practice of Constraint Programming, Lecture Notes in Computer Science, Vol. 1894, Springer, Berlin, 2000, pp. 500\u2013505.","DOI":"10.1007\/3-540-45349-0_37"},{"issue":"8","key":"10.1016\/S0166-218X(02)00385-2_BIB5","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for Boolean function manipulation","volume":"C35","author":"Bryant","year":"1986","journal-title":"IEEE Trans. Comput."},{"key":"10.1016\/S0166-218X(02)00385-2_BIB6","unstructured":"K.M. Bugrara, P.W. Purdom, Clause order backtracking, Technical Report 311, Indiana University, 1990."},{"key":"10.1016\/S0166-218X(02)00385-2_BIB7","series-title":"Optimization Methods for Logical Inference","author":"Chandru","year":"1999"},{"key":"10.1016\/S0166-218X(02)00385-2_BIB8","unstructured":"J. Crawford, L. Auton, Experimental results on the crossover point in satisfiability problems, in: Proceedings AAAI-93, 1993, pp. 22\u201328."},{"key":"10.1016\/S0166-218X(02)00385-2_BIB9","first-page":"394","article-title":"A machine program for theorem-proving","volume":"5","author":"Davis","year":"1962","journal-title":"Commun. Assoc. Comput. Mach."},{"key":"10.1016\/S0166-218X(02)00385-2_BIB10","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","article-title":"A computing procedure for quantification theory","volume":"7","author":"Davis","year":"1960","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/S0166-218X(02)00385-2_BIB11","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1090\/dimacs\/026\/20","article-title":"SAT versus UNSAT","volume":"26","author":"Dubois","year":"1996","journal-title":"DIMACS Ser. Discrete Math. Theoret. Comput. Sci."},{"key":"10.1016\/S0166-218X(02)00385-2_BIB12","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0166-218X(83)90017-3","article-title":"Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem","volume":"5","author":"Franco","year":"1983","journal-title":"Discrete Appl. Math."},{"key":"10.1016\/S0166-218X(02)00385-2_BIB13","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1090\/dimacs\/026\/27","article-title":"Satisfiability testing with more reasoning and less guessing","volume":"26","author":"Van Gelder","year":"1996","journal-title":"DIMACS Ser. Discrete Math. Theoret. Comput. Sci."},{"key":"10.1016\/S0166-218X(02)00385-2_BIB14","unstructured":"I.P. Gent, H. van Maaren, T. Walsh (Eds.), SAT 2000, IOS Press, Amsterdam, 2000."},{"key":"10.1016\/S0166-218X(02)00385-2_BIB15","series-title":"SAT 2000","article-title":"The propositional formula checker HeerHugo","author":"Groote","year":"2000"},{"key":"10.1016\/S0166-218X(02)00385-2_BIB16","series-title":"Advances in Optimization and Approximation","first-page":"72","article-title":"Optimization algorithms for the satisfiability (SAT) problem","author":"Gu","year":"1994"},{"key":"10.1016\/S0166-218X(02)00385-2_BIB17","doi-asserted-by":"crossref","unstructured":"J. Gu, P.W. Purdom, J. Franco, B.W. Wah, Algorithms for the satisfiability (SAT) problem: a survey, DIMACS Ser. Discrete Math., American Mathematical Society, 1999.","DOI":"10.1007\/978-1-4757-3023-4_7"},{"key":"10.1016\/S0166-218X(02)00385-2_BIB18","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1287\/ijoc.6.4.423","article-title":"A computational study of satisfiability algorithms for propositional logic","volume":"6","author":"Harche","year":"1994","journal-title":"ORSA J. Comput."},{"key":"10.1016\/S0166-218X(02)00385-2_BIB19","first-page":"123","article-title":"Branch and cut solution of inference problems in propositional logic","volume":"1","author":"Hooker","year":"1990","journal-title":"Ann. Math. AI"},{"key":"10.1016\/S0166-218X(02)00385-2_BIB20","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/BF00881805","article-title":"Branching rules for satisfiability","volume":"15","author":"Hooker","year":"1995","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/S0166-218X(02)00385-2_BIB21","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1090\/dimacs\/026\/22","article-title":"Tabu search and a quadratic relaxation for the satisfiability problem","volume":"26","author":"Jaumard","year":"1996","journal-title":"DIMACS Ser. Discrete Math. Theoret. Comput. Sci."},{"key":"10.1016\/S0166-218X(02)00385-2_BIB22","first-page":"167","article-title":"Solving propositional satisfiability problems","volume":"1","author":"Jeroslow","year":"1990","journal-title":"Ann. Math. AI"},{"key":"10.1016\/S0166-218X(02)00385-2_BIB23","doi-asserted-by":"crossref","unstructured":"D.S. Johnson, M.A. Trick (Eds.), Cliques, Coloring, and Satisfiability, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 26, American Mathematical Society, Providence, RI, 1996.","DOI":"10.1090\/dimacs\/026"},{"key":"10.1016\/S0166-218X(02)00385-2_BIB24","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/BF01581082","article-title":"A continuous approach to inductive inference","volume":"57","author":"Kamath","year":"1992","journal-title":"Mathematical Programming"},{"key":"10.1016\/S0166-218X(02)00385-2_BIB25","series-title":"SAT 2000","article-title":"Relaxations of the satisfiability problem using semidefinite programming","author":"de Klerk","year":"2000"},{"key":"10.1016\/S0166-218X(02)00385-2_BIB26","series-title":"Automated Theorem Proving: a Logical Basis","author":"Loveland","year":"1978"},{"key":"10.1016\/S0166-218X(02)00385-2_BIB27","first-page":"34","article-title":"Augmentation, local search and learning","volume":"XIII","author":"Mannino","year":"2000","journal-title":"AI-IA Notizie"},{"issue":"5","key":"10.1016\/S0166-218X(02)00385-2_BIB28","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","article-title":"GRASP","volume":"48","author":"Marques-Silva","year":"1999","journal-title":"IEEE Trans. Comput."},{"key":"10.1016\/S0166-218X(02)00385-2_BIB29","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1090\/dimacs\/026\/23","article-title":"Efficiency and stability of hypergraph SAT algorithms","volume":"26","author":"Pretolani","year":"1996","journal-title":"DIMACS Ser. Discrete Math. Theoret. Comput. Sci."},{"key":"10.1016\/S0166-218X(02)00385-2_BIB30","doi-asserted-by":"crossref","unstructured":"G. St\u00e5lmarck, M. S\u00e4flund, Modeling and verifying systems and software in propositional logic, in: Proceedings of the International Conference on Safety of Computer Control Systems, Pergamon Press, Oxford, 1990, pp. 31\u201336.","DOI":"10.1016\/B978-0-08-040953-5.50011-8"},{"key":"10.1016\/S0166-218X(02)00385-2_BIB31","series-title":"Effective Logic Computation","author":"Truemper","year":"1998"},{"key":"10.1016\/S0166-218X(02)00385-2_BIB32","doi-asserted-by":"crossref","unstructured":"H. Zhang, SATO: an efficient propositional prover, in: Proceedings of the International Conference on Automated Deduction (CADE-97), Lecture Notes in Artificial Intelligence, Vol. 1104, Springer, Berlin, 1997, pp. 308\u2013312.","DOI":"10.1007\/3-540-63104-6_28"},{"key":"10.1016\/S0166-218X(02)00385-2_BIB33","series-title":"SAT 2000","article-title":"Implementing the Davis\u2013Putnam method","author":"Zhang","year":"2000"}],"container-title":["Discrete Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0166218X02003852?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0166218X02003852?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,19]],"date-time":"2020-03-19T19:03:54Z","timestamp":1584644634000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0166218X02003852"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["S0166218X02003852"],"URL":"https:\/\/doi.org\/10.1016\/s0166-218x(02)00385-2","relation":{},"ISSN":["0166-218X"],"issn-type":[{"value":"0166-218X","type":"print"}],"subject":[],"published":{"date-parts":[[2003,5]]}}}