{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T16:44:28Z","timestamp":1648831468477},"reference-count":11,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[1991,1,1]],"date-time":"1991-01-01T00:00:00Z","timestamp":662688000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information Processing Letters"],"published-print":{"date-parts":[[1991,1]]},"DOI":"10.1016\/0020-0190(91)90139-9","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T23:38:59Z","timestamp":1027640339000},"page":"85-89","source":"Crossref","is-referenced-by-count":5,"title":["A dual algorithm for the satisfiability problem"],"prefix":"10.1016","volume":"37","author":[{"given":"Yoshihiro","family":"Tanaka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0020-0190(91)90139-9_BIB1","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1016\/0305-0548(86)90056-0","article-title":"Some results and experiments in programming techniques for propositional logic","volume":"13","author":"Blair","year":"1986","journal-title":"Comput. Oper. Res."},{"key":"10.1016\/0020-0190(91)90139-9_BIB2","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/800157.805047","article-title":"The complexity of theorem-proving procedures","author":"Cook","year":"1971","journal-title":"Proc. Third Annual ACM Symposium Theory of Computing"},{"key":"10.1016\/0020-0190(91)90139-9_BIB3","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. ACM"},{"key":"10.1016\/0020-0190(91)90139-9_BIB4","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","article-title":"Linear-time algorithms for testing the satisfiability of propositional Horn formulae","volume":"3","author":"Dowling","year":"1984","journal-title":"J. Logic Programming"},{"key":"10.1016\/0020-0190(91)90139-9_BIB5","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/0020-0190(86)90051-7","article-title":"On the probabilistic performance of algorithms for the satisfiability problem","volume":"23","author":"Franco","year":"1986","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/0020-0190(91)90139-9_BIB6","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\/0020-0190(91)90139-9_BIB7","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0167-9236(88)90097-8","article-title":"A quantitative approach to logical inference","volume":"4","author":"Hooker","year":"1988","journal-title":"Decis. Support Syst."},{"key":"10.1016\/0020-0190(91)90139-9_BIB8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0167-6377(88)90044-2","article-title":"Resolution vs. cutting plane solution of inference problems, some computational experiments","volume":"7","author":"Hooker","year":"1988","journal-title":"Oper. Res. Lett."},{"key":"10.1016\/0020-0190(91)90139-9_BIB9","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1137\/0218026","article-title":"CNF satisfiability test by counting and polynomial average time","volume":"18","author":"Iwama","year":"1989","journal-title":"SIAM J. Comput."},{"key":"10.1016\/0020-0190(91)90139-9_BIB10","series-title":"Solving propositional satisfiability problems","author":"Jeroslow","year":"1987"},{"key":"10.1016\/0020-0190(91)90139-9_BIB11","series-title":"International Workshop on Discrete Algorithms and Complexity, 89-AL-12","first-page":"253","article-title":"Random satisfiability problems","author":"Purdom","year":"1989"}],"container-title":["Information Processing Letters"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0020019091901399?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0020019091901399?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,13]],"date-time":"2019-04-13T04:23:29Z","timestamp":1555129409000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0020019091901399"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,1]]},"references-count":11,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1991,1]]}},"alternative-id":["0020019091901399"],"URL":"https:\/\/doi.org\/10.1016\/0020-0190(91)90139-9","relation":{},"ISSN":["0020-0190"],"issn-type":[{"value":"0020-0190","type":"print"}],"subject":[],"published":{"date-parts":[[1991,1]]}}}