{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T17:58:57Z","timestamp":1743098337823,"version":"3.40.3"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319559100"},{"type":"electronic","value":"9783319559117"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-55911-7_26","type":"book-chapter","created":{"date-parts":[[2017,3,20]],"date-time":"2017-03-20T10:23:37Z","timestamp":1490005417000},"page":"362-372","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On the Computational Complexity of Read once Resolution Decidability in 2CNF Formulas"],"prefix":"10.1007","author":[{"given":"Hans","family":"Kleine B\u00fcning","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Wojciechowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K.","family":"Subramani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,21]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1016\/0097-3165(86)90060-9","volume":"43","author":"R Aharoni","year":"1986","unstructured":"Aharoni, R., Linial, N.: Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas. J. Combin. Theor. Ser. A 43, 196\u2013204 (1986)","journal-title":"J. Combin. Theor. Ser. A"},{"key":"26_CR2","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1023\/A:1018924526592","volume":"23","author":"G Davidov","year":"1998","unstructured":"Davidov, G., Davydova, I., Kleine B\u00fcning, H.: An efficient algorithm for the minimal unsatisability problem for a subclass of CNF. Ann. Math. Artif. Intell. 23, 229\u2013245 (1998)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1","key":"26_CR3","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1016\/S0304-3975(01)00337-1","volume":"289","author":"H Fleischer","year":"2002","unstructured":"Fleischer, H., Kullmann, O., Szeider, S.: Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference. Theor. Comput. Sci. 289(1), 503\u2013516 (2002)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"26_CR4","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/0304-3975(80)90009-2","volume":"10","author":"S Fortune","year":"1980","unstructured":"Fortune, S., Hopcroft, J.E., Wyllie, J.: The directed subgraph homeomorphism problem. Theor. Comput. Sci. 10(2), 111\u2013121 (1980)","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Iwama, K., Miyano, E.: Intractability of read-once resolution. In: Proceedings of the 10th Annual Conference on Structure in Complexity Theory, pp. 29\u201336. IEEE (1995)","key":"26_CR5","DOI":"10.1109\/SCT.1995.514725"},{"issue":"4","key":"26_CR6","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1023\/A:1016339119669","volume":"36","author":"H Kleine B\u00fcning","year":"2002","unstructured":"Kleine B\u00fcning, H., Zhao, X.: The complexity of read-once resolution. Ann. Math. Artif. Intell. 36(4), 419\u2013435 (2002)","journal-title":"Ann. Math. Artif. Intell."},{"key":"26_CR7","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/S0166-218X(02)00405-5","volume":"130","author":"H Kleine B\u00fcning","year":"2003","unstructured":"Kleine B\u00fcning, H., Zhao, X.: On the structure of some classes of minimal unsatisfiable formulas. Discrete Appl. Math. 130, 185\u2013207 (2003)","journal-title":"Discrete Appl. Math."},{"key":"26_CR8","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/0022-0000(88)90042-6","volume":"37","author":"CH Papadimitriou","year":"1988","unstructured":"Papadimitriou, C.H., Wolfe, D.: The complexity of facets resolved. J. Comput. Syst. Sci. 37, 2\u201313 (1988)","journal-title":"J. Comput. Syst. Sci."},{"key":"26_CR9","doi-asserted-by":"crossref","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 multicommodity flow problems. SIAM J. Comput. 5, 691\u2013703 (1976)","journal-title":"SIAM J. Comput."},{"key":"26_CR10","first-page":"66","volume":"65","author":"P Beame","year":"1998","unstructured":"Beame, P., Pitassi, T.: Propositional proof complexity: past, present, future. Bull. EATCS 65, 66\u201389 (1998)","journal-title":"Bull. EATCS"},{"issue":"1","key":"26_CR11","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J Robinson","year":"1965","unstructured":"Robinson, J.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H., McAllester, D., Lynch, C.: Bachmair, L., Ganzinger, H., McAllester, D., Lynch, C.: Chapter 2 - Resolution theorem proving. Handbook of Automated Reasoning, Issue. 1, pp. 19\u201399 (2001)","key":"26_CR12","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"doi-asserted-by":"crossref","unstructured":"Szeider, S.: NP-Completeness of refutability by literal-once resolution. In: Automated Reasoning: First International Joint Conference, pp. 168\u2013181 (2001)","key":"26_CR13","DOI":"10.1007\/3-540-45744-5_13"},{"issue":"4","key":"26_CR14","doi-asserted-by":"crossref","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"1","author":"A Urquhart","year":"1995","unstructured":"Urquhart, A.: The complexity of propositional proofs. Bull. Symbolic Logic 1(4), 425\u2013467 (1995)","journal-title":"Bull. Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Models of Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-55911-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,19]],"date-time":"2019-09-19T20:20:04Z","timestamp":1568924404000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-55911-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319559100","9783319559117"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-55911-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}