{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:06:16Z","timestamp":1725512776620},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540699118"},{"type":"electronic","value":"9783540699125"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69912-5_11","type":"book-chapter","created":{"date-parts":[[2007,8,20]],"date-time":"2007-08-20T21:30:41Z","timestamp":1187645441000},"page":"128-142","source":"Crossref","is-referenced-by-count":1,"title":["Finding Models for Blocked 3-SAT Problems in Linear Time by Systematical Refinement of a Sub-model"],"prefix":"10.1007","author":[{"given":"G\u00e1bor","family":"Kusper","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"11_CR1","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B. Aspvall","year":"1979","unstructured":"Aspvall, B., Plass, M.F., Tarjan, R.E.: A Linear-Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulas. Information Processing Letters\u00a08(3), 121\u2013132 (1979)","journal-title":"Information Processing Letters"},{"key":"11_CR2","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0196-6774(80)90007-3","volume":"1","author":"B. Aspvall","year":"1980","unstructured":"Aspvall, B.: Recognizing Disguised NR(1) Instances of the Satisfiability Problem. J. of Algorithms\u00a01, 97\u2013103 (1980)","journal-title":"J. of Algorithms"},{"key":"11_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0166-218X(94)90033-7","volume":"55","author":"E. Boros","year":"1994","unstructured":"Boros, E., Hammer, P.L., Sun, X.: Recognition of q-Horn Formulae in Linear Time. Discrete Applied Mathematics\u00a055, 1\u201313 (1994)","journal-title":"Discrete Applied Mathematics"},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1137\/S0097539792228629","volume":"23","author":"E. Boros","year":"1994","unstructured":"Boros, E., et al.: A Complexity Index for Satisfiability Problems. SIAM J. on Computing\u00a023, 45\u201349 (1994)","journal-title":"SIAM J. on Computing"},{"issue":"1","key":"11_CR5","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1145\/102782.102789","volume":"38","author":"V. Chandru","year":"1991","unstructured":"Chandru, V., Hooker, J.: Extended Horn Sets in Propositional Logic. J. of the ACM\u00a038(1), 205\u2013221 (1991)","journal-title":"J. of the ACM"},{"doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The Complexity of Theorem-Proving Procedures. In: Proceedings of the 3rd ACM Symposium on Theory of Computing, pp. 151\u2013158 (1971)","key":"11_CR6","DOI":"10.1145\/800157.805047"},{"key":"11_CR7","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0020-0190(92)90081-6","volume":"44","author":"M. Dalal","year":"1992","unstructured":"Dalal, M., Etherington, D.W.: A Hierarchy of Tractable Satisfiability Problems. Information Processing Letters\u00a044, 173\u2013180 (1992)","journal-title":"Information Processing Letters"},{"issue":"3","key":"11_CR8","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"W.F. Dowling","year":"1984","unstructured":"Dowling, W.F., Gallier, J.H.: Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulae. J. of Logic Programming\u00a01(3), 267\u2013284 (1984)","journal-title":"J. of Logic Programming"},{"issue":"4","key":"11_CR9","doi-asserted-by":"publisher","first-page":"691","DOI":"10.1137\/0205048","volume":"5","author":"S. Even","year":"1976","unstructured":"Even, S., Itai, A., Shamir, A.: On the Complexity of Timetable and Multi-Commodity Flow Problems. SIAM J. on Computing\u00a05(4), 691\u2013703 (1976)","journal-title":"SIAM J. on Computing"},{"key":"11_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF02983372","volume":"28","author":"D.E. Knuth","year":"1990","unstructured":"Knuth, D.E.: Nested Satisfiability. Acta Informatica\u00a028, 1\u20136 (1990)","journal-title":"Acta Informatica"},{"issue":"1-2","key":"11_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(98)00017-6","volume":"223","author":"O. Kullmann","year":"1999","unstructured":"Kullmann, O.: New methods for 3-SAT decision and worst-case analysis. Theoretical Computer Science\u00a0223(1-2), 1\u201372 (1999)","journal-title":"Theoretical Computer Science"},{"issue":"1-3","key":"11_CR12","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"97","author":"O. Kullmann","year":"1999","unstructured":"Kullmann, O.: On a Generalization of Extended Resolution. Discrete Applied Mathematics\u00a097(1-3), 149\u2013176 (1999)","journal-title":"Discrete Applied Mathematics"},{"unstructured":"Kusper, G.: Solving the SAT Problem by Hyper-Unit Propagation. RISC Technical Report 02-02, 1\u201318, University Linz, Austria (2002)","key":"11_CR13"},{"issue":"1-4","key":"11_CR14","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/s10472-004-9423-2","volume":"43","author":"G. Kusper","year":"2005","unstructured":"Kusper, G.: Solving the Resolution-Free SAT Problem by Hyper-Unit Propagation in Linear Time. Annals of Mathematics and Artificial Intelligence\u00a043(1-4), 129\u2013136 (2005)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"11_CR15","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1145\/322047.322059","volume":"25","author":"H.R. Lewis","year":"1978","unstructured":"Lewis, H.R.: Renaming a set of clauses as a Horn set. J. of the Association for Computing Machinery\u00a025, 134\u2013135 (1978)","journal-title":"J. of the Association for Computing Machinery"},{"key":"11_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-96753-4","volume-title":"The Foundations of Program Verification","author":"J. Loeckx","year":"1987","unstructured":"Loeckx, J., Sieber, K.: The Foundations of Program Verification, 2nd edn. Wiley, Chichester (1987)","edition":"2"},{"key":"11_CR17","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/0020-0190(95)00019-9","volume":"54","author":"J.S. Schlipf","year":"1995","unstructured":"Schlipf, J.S., et al.: On finding solutions for extended Horn formulas. Information Processing Letters\u00a054, 133\u2013137 (1995)","journal-title":"Information Processing Letters"},{"issue":"3","key":"11_CR18","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0743-1066(90)90026-2","volume":"8","author":"M.G. Scutella","year":"1990","unstructured":"Scutella, M.G.: A Note on Dowling and Gallier\u2019s Top-Down Algorithm for Propositional Horn Satisfiability. J. of Logic Programming\u00a08(3), 265\u2013273 (1990)","journal-title":"J. of Logic Programming"},{"key":"11_CR19","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/0166-218X(84)90081-7","volume":"8","author":"C.A. Tovey","year":"1984","unstructured":"Tovey, C.A.: A Simplified NP-complete Satisfiability Problem. Discrete Applied Mathematics\u00a08, 85\u201389 (1984)","journal-title":"Discrete Applied Mathematics"}],"container-title":["Lecture Notes in Computer Science","KI 2006: Advances in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69912-5_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:11:54Z","timestamp":1620015114000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69912-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540699118","9783540699125"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69912-5_11","relation":{},"subject":[]}}