{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T09:22:04Z","timestamp":1649064124302},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2004,12,31]],"date-time":"2004-12-31T00:00:00Z","timestamp":1104451200000},"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,1]]},"DOI":"10.1007\/s10472-005-0423-7","type":"journal-article","created":{"date-parts":[[2005,3,2]],"date-time":"2005-03-02T19:19:42Z","timestamp":1109791182000},"page":"129-136","source":"Crossref","is-referenced-by-count":1,"title":["Solving the resolution-free SAT problem by submodel propagation in linear time"],"prefix":"10.1007","volume":"43","author":[{"given":"G\u00e1bor","family":"Kusper","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2004,12,31]]},"reference":[{"key":"423_CR1","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0196-6774(80)90007-3","volume":"1","author":"B. Aspvall","year":"1980","unstructured":"B. Aspvall, Recognizing disguised NR(1) instances of the satisfiability problem, Journal of Algorithms 1 (1980) 97\u2013103.","journal-title":"Journal of Algorithms"},{"issue":"3","key":"423_CR2","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(3) (1979) 121\u2013123.","journal-title":"Information Processing Letters"},{"key":"423_CR3","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1137\/S0097539792228629","volume":"23","author":"E. Boros","year":"1994","unstructured":"E. Boros, Y. Crama, P.L. Hammer and M. Saks, A complexity index for satisfiability problems, SIAM Journal on Computing 23 (1994) 45\u201349.","journal-title":"SIAM Journal on Computing"},{"key":"423_CR4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0166-218X(94)90033-7","volume":"55","author":"E. Boros","year":"1994","unstructured":"E. Boros, P.L. Hammer and X. Sun, Recognition of q-Horn formulae in linear time, Discrete Applied Mathematics 55 (1994) 1\u201313.","journal-title":"Discrete Applied Mathematics"},{"issue":"1","key":"423_CR5","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1145\/102782.102789","volume":"38","author":"V. Chandru","year":"1991","unstructured":"V. Chandru and J. Hooker, Extended Horn sets in propositional logic, Journal of the ACM 38(1) (1991) 205\u2013221.","journal-title":"Journal of the ACM"},{"key":"423_CR6","doi-asserted-by":"crossref","unstructured":"S.A. Cook, The complexity of theorem proving procedures, in: Proc. 3rd Ann. ACM Symp. on Theory of Computing (1971) pp. 151\u2013158.","DOI":"10.1145\/800157.805047"},{"key":"423_CR7","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0020-0190(92)90081-6","volume":"44","author":"M. Dalal","year":"1992","unstructured":"M. Dalal and D.W. Etherington, A hierarchy of tractable satisfiability problems, Information Processing Letters 44 (1992) 173\u2013180.","journal-title":"Information Processing Letters"},{"issue":"3","key":"423_CR8","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 formulas, Journal of Logic Programming 1(3) (1984) 267\u2013284.","journal-title":"Journal of Logic Programming"},{"key":"423_CR9","doi-asserted-by":"crossref","unstructured":"S. Even, A. Itai and A. Shamir, On the complexity of timetable and multicommodity flow problems, SIAM Journal on Computing 5(4) (1976).","DOI":"10.1137\/0205048"},{"key":"423_CR10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF02983372","volume":"28","author":"D.E. Knuth","year":"1990","unstructured":"D.E. Knuth, Nested satisfiability, Acta Informatica 28 (1990) 1\u20136.","journal-title":"Acta Informatica"},{"issue":"1\u20132","key":"423_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(98)00017-6","volume":"223","author":"O. Kullmann","year":"1999","unstructured":"O. Kullmann, New methods for 3-SAT decision and worst-case analysis, Theoretical Computer Science 223(1\u20132) (1999) 1\u201372.","journal-title":"Theoretical Computer Science"},{"key":"423_CR12","series-title":"RISC Technical Report","first-page":"18","volume-title":"Solving the SAT problem by hyper-unit propagation","author":"G. Kusper","year":"2002","unstructured":"G. Kusper, Solving the SAT problem by hyper-unit propagation, RISC Technical Report 2002-02, RISC-Linz, Johannes Kepler University, Linz, Austria (2002) 18."},{"issue":"3","key":"423_CR13","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/0743-1066(90)90026-2","volume":"8","author":"M.G. Scutella","year":"1990","unstructured":"M.G. Scutella, A note on Dowling and Gallier\u2019s top-down algorithm for propositional Horn satisfiability, Journal of Logic Programming 8(3) (1990) 265\u2013273.","journal-title":"Journal of Logic Programming"},{"key":"423_CR14","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0166-218X(84)90081-7","volume":"8","author":"C.A. Tovey","year":"1984","unstructured":"C.A. Tovey, A simplified NP-complete satisfiability problem, Discrete Applied Mathematics 8 (1984) 85\u201389.","journal-title":"Discrete Applied Mathematics"},{"key":"423_CR15","unstructured":"H. Zhang and M.E. Stickel, An efficient algorithm for unit propagation, in: Proc. of Fourth International Symposium on Artificial Intelligence and Mathematics (1996) pp. 166\u2013169."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-005-0423-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-005-0423-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-005-0423-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T17:51:48Z","timestamp":1559152308000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-005-0423-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,12,31]]},"references-count":15,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2005,1]]}},"alternative-id":["423"],"URL":"https:\/\/doi.org\/10.1007\/s10472-005-0423-7","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,12,31]]}}}