{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:56:09Z","timestamp":1725663369834},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540542339"},{"type":"electronic","value":"9783540475163"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54233-7_131","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:36:49Z","timestamp":1330209409000},"page":"151-162","source":"Crossref","is-referenced-by-count":0,"title":["General resolution of tseitin formulas is hard"],"prefix":"10.1007","author":[{"given":"Jean-Denis","family":"Fouks","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"unstructured":"C. BERGE, Theorie des graphes et ses applications, DUNOD PARIS (1958).","key":"11_CR1"},{"issue":"4","key":"11_CR2","doi-asserted-by":"crossref","first-page":"759","DOI":"10.1145\/48014.48016","volume":"35","author":"V. Chvatal","year":"1988","unstructured":"V. CHVATAL et E. SZEMEREDI, Many hard examples for resolution, J. ACM 35, 4 (1988) 759\u2013768","journal-title":"J. ACM"},{"key":"11_CR3","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"1","author":"M. Davis","year":"1960","unstructured":"M. DAVIS and H. PUTNAM, A computing procedure for quantification theory, J. ACM 1 (1960) 201\u2013215","journal-title":"J. ACM"},{"unstructured":"J.D. FOUKS, Tseitin's formulas revisited, Publ. no 52, UHA, Mulhouse (1990).","key":"11_CR4"},{"unstructured":"J.D. FOUKS and J.C. SPEHNER, Meta-resolution, An algorithmic formalisation Publ. no54 UHA 68093 Mulhouse Cedex (1991)","key":"11_CR5"},{"unstructured":"J.D. FOUKS, Sur la r\u00e9solution du probl\u00e8me de satisfiabilit\u00e9, Doctoral Thesis UHA Mulhouse (1991).","key":"11_CR6"},{"issue":"3","key":"11_CR7","doi-asserted-by":"crossref","first-page":"444","DOI":"10.1137\/0206031","volume":"6","author":"Z. Galil","year":"1977","unstructured":"Z. GALIL, On resolution with clauses of bounded size, SIAM J. Comput. vol 6 No3 (1977), 444\u2013459","journal-title":"SIAM J. Comput."},{"key":"11_CR8","first-page":"297","volume":"39","author":"A. Haken","year":"1985","unstructured":"A. HAKEN, The intractibility of resolution, T.C.S. 39 (1985), 297\u2013308","journal-title":"T.C.S."},{"key":"11_CR9","first-page":"325","volume":"9","author":"G.A. Margulis","year":"1973","unstructured":"G.A. MARGULIS,explicit construction of concentrators, Problems of information transmission 9, (1973), 325\u2013332.","journal-title":"Problems of information transmission"},{"key":"11_CR10","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"J.A. ROBINSON,A machine oriented logic based on the resolution principle, J. ACM 12 (1965), 23\u201341","journal-title":"J. ACM"},{"doi-asserted-by":"crossref","unstructured":"G.S.TSEITIN, On the complexity of derivations in the propositional calculus, Structures in constructive mathematics and mathematical logic,Part II, A.O.Slisenko,ed.,consultants bureau, N.Y., (1970), 115\u2013125","key":"11_CR11","DOI":"10.1007\/978-1-4899-5327-8_25"},{"issue":"1","key":"11_CR12","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A. Urquhart","year":"1987","unstructured":"A. URQUHART, Hard examples for resolution, J. ACM 34, 1 (1987), 209\u2013219","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54233-7_131.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:53:08Z","timestamp":1605646388000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54233-7_131"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540542339","9783540475163"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-54233-7_131","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}