{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:08Z","timestamp":1760202608242},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642033667"},{"type":"electronic","value":"9783642033674"}],"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-03367-4_13","type":"book-chapter","created":{"date-parts":[[2009,7,20]],"date-time":"2009-07-20T03:56:42Z","timestamp":1248062202000},"page":"144-155","source":"Crossref","is-referenced-by-count":3,"title":["An Improved SAT Algorithm in Terms of Formula Length"],"prefix":"10.1007","author":[{"given":"Jianer","family":"Chen","sequence":"first","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1006\/jagm.2001.1186","volume":"41","author":"J. Chen","year":"2001","unstructured":"Chen, J., Kanj, I., Jia, W.: Vertex cover: further observations and further improvements. Journal of Algorithms\u00a041, 280\u2013301 (2001)","journal-title":"Journal of Algorithms"},{"key":"13_CR2","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07, 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Fomin, F.V., Grandoni, F., Kratsch, D.: Measure and conquer: a simple O(20.288n) independent set algorithm. In: Proc. 17th Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 18\u201325 (2006)","DOI":"10.1145\/1109557.1109560"},{"key":"13_CR4","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"M. Garey","year":"1979","unstructured":"Garey, M., Johnson, D.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H.Freeman and Company, New York (1979)"},{"key":"13_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(88)90014-4","volume":"79","author":"A. Gelder Van","year":"1988","unstructured":"Van Gelder, A.: A satisfiability tester for non-clausal propositional claculus. Information and Computation\u00a079, 1\u201321 (1988)","journal-title":"Information and Computation"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Gu, J., Purdom, P., Wah, W.: Algorithms for the satisfiability (SAT) problem: A survey. In: Satisfiability Problem: Theory and Applications, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, AMS, pp. 19\u2013152 (1997)","DOI":"10.1090\/dimacs\/035\/02"},{"key":"13_CR7","unstructured":"Hirsh, E.: Two new upper bounds for SAT. In: Proc. 9th Annual ACM-SIAM Symp. on Discrete Algorithms, pp. 521\u2013530 (1998)"},{"key":"13_CR8","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1023\/A:1006340920104","volume":"24","author":"E. Hirsh","year":"2000","unstructured":"Hirsh, E.: New Worst-Case Upper Bounds for SAT. Journal of Automated Reasoning\u00a024, 397\u2013420 (2000)","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR9","unstructured":"Kullmann, O., Luckhardt, H.: Deciding propositional tautologies: Algorithms and their complexity (manuscript) (1997)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-540-31856-9_3","volume-title":"STACS 2005","author":"U. Sch\u00f6ning","year":"2005","unstructured":"Sch\u00f6ning, U.: Algorithmics in exponential time. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol.\u00a03404, pp. 36\u201343. Springer, Heidelberg (2005)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/11561071_12","volume-title":"Algorithms \u2013 ESA 2005","author":"M. Wahlstr\u00f6m","year":"2005","unstructured":"Wahlstr\u00f6m, M.: An algorithm for the SAT problem for formulae of linear length. In: Brodal, G.S., Leonardi, S. (eds.) ESA 2005. LNCS, vol.\u00a03669, pp. 107\u2013118. Springer, Heidelberg (2005)"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/11499107_23","volume-title":"Theory and Applications of Satisfiability Testing","author":"M. Wahlst\u00f6m","year":"2005","unstructured":"Wahlst\u00f6m, M.: Faster Exact Solving of SAT Formulae with a Low Number of Occurrences per Variable. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 309\u2013323. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Algorithms and Data Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03367-4_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T11:28:51Z","timestamp":1558438131000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03367-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033667","9783642033674"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03367-4_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}