{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:53:32Z","timestamp":1725512012757},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540797180"},{"type":"electronic","value":"9783540797197"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79719-7_22","type":"book-chapter","created":{"date-parts":[[2008,5,6]],"date-time":"2008-05-06T08:04:57Z","timestamp":1210061097000},"page":"231-245","source":"Crossref","is-referenced-by-count":1,"title":["A CNF Class Generalizing Exact Linear Formulas"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Porschen","sequence":"first","affiliation":[]},{"given":"Ewald","family":"Speckenmeyer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_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.R., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Inform. Process. Lett.\u00a08, 121\u2013123 (1979)","journal-title":"Inform. Process. Lett."},{"key":"22_CR2","doi-asserted-by":"publisher","DOI":"10.1016\/S0924-6509(08)70096-5","volume-title":"Hypergraphs","author":"C. Berge","year":"1989","unstructured":"Berge, C.: Hypergraphs. North-Holland, Amsterdam (1989)"},{"key":"22_CR3","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/BF01531068","volume":"1","author":"E. Boros","year":"1990","unstructured":"Boros, E., Crama, Y., Hammer, P.L.: Polynomial time inference of all valid implications for Horn and related formulae. Annals Math. Artif. Int.\u00a01, 21\u201332 (1990)","journal-title":"Annals Math. Artif. Int."},{"key":"22_CR4","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 Appl. Math.\u00a055, 1\u201313 (1994)","journal-title":"Discrete Appl. Math."},{"key":"22_CR5","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0166-218X(01)00358-4","volume":"125","author":"J. Franco","year":"2003","unstructured":"Franco, J., Gelder, A.v.: A perspective on certain polynomial-time solvable classes of satisfiability. Discrete Appl. Math.\u00a0125, 177\u2013214 (2003)","journal-title":"Discrete Appl. Math."},{"key":"22_CR6","volume-title":"Propositional logic, deduction and algorithms","author":"H. Kleine B\u00fcning","year":"1999","unstructured":"Kleine B\u00fcning, H., Lettman, T.: Propositional logic, deduction and algorithms. Cambridge University Press, Cambridge (1999)"},{"key":"22_CR7","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1137\/0222015","volume":"22","author":"J. Kratochvil","year":"1993","unstructured":"Kratochvil, J., Savicky, P., Tusa, Z.: One more occurrence of variables makes satisfiability jump from trivial to NP-complete. SIAM J. Comput.\u00a022, 203\u2013210 (1993)","journal-title":"SIAM J. Comput."},{"key":"22_CR8","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"},{"key":"22_CR9","doi-asserted-by":"publisher","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. ACM\u00a025, 134\u2013135 (1978)","journal-title":"J. ACM"},{"key":"22_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0020-0190(88)90124-X","volume":"29","author":"M. Minoux","year":"1988","unstructured":"Minoux, M.: LTUR: A Simplified Linear-Time Unit Resolution Algorithm for Horn Formulae and Computer Implementation. Inform. Process. Lett.\u00a029, 1\u201312 (1988)","journal-title":"Inform. Process. Lett."},{"key":"22_CR11","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0166-218X(85)90050-2","volume":"10","author":"B. Monien","year":"1985","unstructured":"Monien, B., Speckenmeyer, E.: Solving satisfiability in less than 2\n                  n\n                 steps. Discrete Appl. Math.\u00a010, 287\u2013295 (1985)","journal-title":"Discrete Appl. Math."},{"key":"22_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-540-76928-6_25","volume-title":"AI 2007: Advances in Artificial Intelligence","author":"S. Porschen","year":"2007","unstructured":"Porschen, S.: A CNF Formula Hierarchy over the Hypercube. In: Orgun, M.A., Thornton, J. (eds.) AI 2007. LNCS (LNAI), vol.\u00a04830, pp. 234\u2013243. Springer, Heidelberg (2007)"},{"key":"22_CR13","doi-asserted-by":"publisher","first-page":"1408","DOI":"10.1016\/j.dam.2007.02.010","volume":"155","author":"S. Porschen","year":"2007","unstructured":"Porschen, S., Speckenmeyer, E.: Satisfiability of Mixed Horn Formulas. Discrete Appl. Math.\u00a0155, 1408\u20131419 (2007)","journal-title":"Discrete Appl. Math."},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/11814948_22","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"S. Porschen","year":"2006","unstructured":"Porschen, S., Speckenmeyer, E., Randerath, B.: On linear CNF formulas. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 221\u2013225. Springer, Heidelberg (2006)"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Schaefer, T.J.: The complexity of satisfiability problems. In: Proc. STOC 1978. ACM, pp. 216\u2013226 (1978)","DOI":"10.1145\/800133.804350"},{"key":"22_CR16","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/0020-0190(95)00019-9","volume":"54","author":"J. Schlipf","year":"1995","unstructured":"Schlipf, J., Annexstein, F.S., Franco, J., Swaminathan, R.P.: On finding solutions for extended Horn formulas. Inform. Process. Lett.\u00a054, 133\u2013137 (1995)","journal-title":"Inform. Process. Lett."},{"key":"22_CR17","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 Appl. Math.\u00a08, 85\u201389 (1984)","journal-title":"Discrete Appl. Math."}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2008"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79719-7_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:29:13Z","timestamp":1619522953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79719-7_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540797180","9783540797197"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79719-7_22","relation":{},"subject":[]}}