{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:58:17Z","timestamp":1725533897950},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642027765"},{"type":"electronic","value":"9783642027772"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02777-2_11","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T06:58:18Z","timestamp":1245999498000},"page":"86-100","source":"Crossref","is-referenced-by-count":1,"title":["On Some Aspects of Mixed Horn Formulas"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Porschen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tatjana","family":"Schmidt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ewald","family":"Speckenmeyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"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.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":"11_CR2","doi-asserted-by":"crossref","unstructured":"Dantsin, E., Wolpert, A.: Algorithms for SAT based on search in Hamming balls, ECCC Report No. 17 (2004)","DOI":"10.1007\/978-3-540-24749-4_13"},{"key":"11_CR3","doi-asserted-by":"crossref","first-page":"49","DOI":"10.3233\/SAT190002","volume":"1","author":"E. Dantsin","year":"2005","unstructured":"Dantsin, E., Wolpert, A.: A faster clause-shortening algorithm for SAT with no restriction on clause length. J. Satisfiability, Boolean Modeling and Computation\u00a01, 49\u201360 (2005)","journal-title":"J. Satisfiability, Boolean Modeling and Computation"},{"key":"11_CR4","first-page":"85","volume-title":"Proc. Sympos. IBM Thomas J. Watson Res. Center, Yorktown Heights","author":"R.M. Karp","year":"1972","unstructured":"Karp, R.M.: Reducibility Among Combinatorial Problems. In Complexity of Computer Computations. In: Proc. Sympos. IBM Thomas J. Watson Res. Center, Yorktown Heights, pp. 85\u2013103. Plenum, New York (1972)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-540-79719-7_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"S. Kottler","year":"2008","unstructured":"Kottler, S., Kaufmann, M., Sinz, C.: A New Bound for an NP-Hard Subclass of 3-SAT Using Backdoors. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 161\u2013167. Springer, Heidelberg (2008)"},{"key":"11_CR6","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":"11_CR7","unstructured":"Porschen, S., Schmidt, T., Speckenmeyer, E.: MHF \u2013 a central subclass of CNF, working paper, Universit\u00e4t zu K\u00f6ln (2009)"},{"key":"11_CR8","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":"11_CR9","doi-asserted-by":"publisher","first-page":"1046","DOI":"10.1016\/j.dam.2008.03.031","volume":"157","author":"S. Porschen","year":"2009","unstructured":"Porschen, S., Speckenmeyer, E., Zhao, X.: Linear CNF formulas and satisfiability. Discrete Appl. Math.\u00a0157, 1046\u20131068 (2009)","journal-title":"Discrete Appl. Math."},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Randerath, B., Speckenmeyer, E., Boros, E., Hammer, P., Kogan, A., Makino, K., Simeone, B., Cepek, O.: A Satisfiability Formulation of Problems on Level Graphs. In: ENDM, vol.\u00a09 (2001)","DOI":"10.1016\/S1571-0653(04)00327-0"},{"key":"11_CR11","first-page":"216","volume-title":"Proc. STOC 1978","author":"T.J. Schaefer","year":"1978","unstructured":"Schaefer, T.J.: The complexity of satisfiability problems. In: Proc. STOC 1978, pp. 216\u2013226. ACM Press, New York (1978)"},{"key":"11_CR12","unstructured":"Stamm-Wilbrandt, H.: Programming in propositional Logic or Reductions: Back to the Roots (Satisfiability), Technical Report, Universit\u00e4t Bonn (1991)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02777-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,20]],"date-time":"2020-05-20T01:25:58Z","timestamp":1589937958000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02777-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027765","9783642027772"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02777-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}