{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T08:52:20Z","timestamp":1672476740449},"reference-count":25,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2003,8,1]],"date-time":"2003-08-01T00:00:00Z","timestamp":1059696000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":3674,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Discrete Applied Mathematics"],"published-print":{"date-parts":[[2003,8]]},"DOI":"10.1016\/s0166-218x(02)00411-0","type":"journal-article","created":{"date-parts":[[2003,7,31]],"date-time":"2003-07-31T22:28:16Z","timestamp":1059690496000},"page":"351-365","source":"Crossref","is-referenced-by-count":10,"title":["Homomorphisms of conjunctive normal forms"],"prefix":"10.1016","volume":"130","author":[{"given":"Stefan","family":"Szeider","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0166-218X(02)00411-0_BIB1","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1016\/0097-3165(86)90060-9","article-title":"Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas","volume":"43","author":"Aharoni","year":"1986","journal-title":"J. Combin. Theory, Ser. A"},{"key":"10.1016\/S0166-218X(02)00411-0_BIB2","series-title":"Automated Reasoning with Analytic Tableaux and Related Methods (Proc. TABLEAUX 2000)","first-page":"40","article-title":"Local symmetries in propositional logic","volume":"Vol. 1847","author":"Arai","year":"2000"},{"key":"10.1016\/S0166-218X(02)00411-0_BIB3","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/BF00881844","article-title":"Tractability through symmetries in propositional calculus","volume":"12","author":"Benhamou","year":"1994","journal-title":"J. Automat. Reason."},{"issue":"1","key":"10.1016\/S0166-218X(02)00411-0_BIB4","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","article-title":"The relative efficiency of propositional proof systems","volume":"44","author":"Cook","year":"1979","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0166-218X(02)00411-0_BIB5","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1023\/A:1018924526592","article-title":"An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF","volume":"23","author":"Davydov","year":"1998","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1","key":"10.1016\/S0166-218X(02)00411-0_BIB6","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1016\/S0304-3975(01)00337-1","article-title":"Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference","volume":"289","author":"Fleischner","year":"2002","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0166-218X(02)00411-0_BIB7","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0166-218X(01)00358-4","article-title":"A perspective on certain polynomial time solvable classes of satisfiability","volume":"125","author":"Franco","year":"2003","journal-title":"Discrete Appl. Math."},{"key":"10.1016\/S0166-218X(02)00411-0_BIB8","unstructured":"M. Goldstern, Personal communication."},{"key":"10.1016\/S0166-218X(02)00411-0_BIB9","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","article-title":"The intractability of resolution","volume":"39","author":"Haken","year":"1985","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0166-218X(02)00411-0_BIB10","series-title":"CSL\u201998","first-page":"171","article-title":"An upper bound for minimal resolution refutations","volume":"Vol. 1584","author":"Kleine B\u00fcning","year":"1999"},{"key":"10.1016\/S0166-218X(02)00411-0_BIB11","series-title":"Propositional Logic: Deduction and Algorithms","author":"Kleine B\u00fcning","year":"1999"},{"key":"10.1016\/S0166-218X(02)00411-0_BIB12","unstructured":"H. Kleine B\u00fcning, X. Zhao, Homomorphisms and MU(k), March 2001, unpublished manuscript."},{"key":"10.1016\/S0166-218X(02)00411-0_BIB13","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/BF00265682","article-title":"Short proofs for tricky formulas","volume":"22","author":"Krishnamurthy","year":"1985","journal-title":"Acta Inform."},{"key":"10.1016\/S0166-218X(02)00411-0_BIB14","doi-asserted-by":"crossref","unstructured":"O. Kullmann, An application of matroid theory to the SAT problem, Fifteenth Annual IEEE Conference on Computational Complexity, 2000, pp. 116\u2013124.","DOI":"10.1109\/CCC.2000.856741"},{"issue":"1\u20133","key":"10.1016\/S0166-218X(02)00411-0_BIB15","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/S0166-218X(00)00262-6","article-title":"Investigations on autark assignments","volume":"107","author":"Kullmann","year":"2000","journal-title":"Discrete Appl. Math."},{"key":"10.1016\/S0166-218X(02)00411-0_BIB16","unstructured":"O. Kullmann, Personal communication."},{"key":"10.1016\/S0166-218X(02)00411-0_BIB17","doi-asserted-by":"crossref","unstructured":"O. Kullmann, Lean clause-sets: generalizations of minimally unsatisfiable clause-sets, Discrete Appl. Math., to appear.","DOI":"10.1016\/S0166-218X(02)00406-7"},{"key":"10.1016\/S0166-218X(02)00411-0_BIB18","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1093\/comjnl\/8.4.341","article-title":"Theorem-proving for computers","volume":"8","author":"Meltzer","year":"1966","journal-title":"Comput. J."},{"key":"10.1016\/S0166-218X(02)00411-0_BIB19","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0166-218X(85)90050-2","article-title":"Solving satisfiability in less than 2n steps","volume":"10","author":"Monien","year":"1985","journal-title":"Discrete Appl. Math."},{"issue":"1","key":"10.1016\/S0166-218X(02)00411-0_BIB20","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/0022-0000(88)90042-6","article-title":"The complexity of facets resolved","volume":"37","author":"Papadimitriou","year":"1988","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/S0166-218X(02)00411-0_BIB21","unstructured":"S. Szeider, Conjunctive normal forms with bounded deficiency, Ph.D. Thesis, University of Vienna, September 2001."},{"key":"10.1016\/S0166-218X(02)00411-0_BIB22","series-title":"IJCAR 2001, Proceedings of the First International Joint Conference on Automated Reasoning","first-page":"168","article-title":"NP-completeness of refutability by literal-once resolution","volume":"Vol. 2083","author":"Szeider","year":"2001"},{"key":"10.1016\/S0166-218X(02)00411-0_BIB23","unstructured":"S. Szeider, The universality of refutation by homomorphism, 2001, in preparation."},{"issue":"4","key":"10.1016\/S0166-218X(02)00411-0_BIB24","doi-asserted-by":"crossref","first-page":"425","DOI":"10.2178\/bsl\/1203350879","article-title":"The complexity of propositional proofs","volume":"1","author":"Urquhart","year":"1995","journal-title":"Bull. Symbolic Logic"},{"key":"10.1016\/S0166-218X(02)00411-0_BIB25","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0166-218X(99)00039-6","article-title":"The symmetry rule in propositional logic","volume":"96\/97","author":"Urquhart","year":"1999","journal-title":"Discrete Appl. Math."}],"container-title":["Discrete Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0166218X02004110?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0166218X02004110?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,17]],"date-time":"2019-03-17T07:58:54Z","timestamp":1552809534000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0166218X02004110"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,8]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,8]]}},"alternative-id":["S0166218X02004110"],"URL":"https:\/\/doi.org\/10.1016\/s0166-218x(02)00411-0","relation":{},"ISSN":["0166-218X"],"issn-type":[{"value":"0166-218X","type":"print"}],"subject":[],"published":{"date-parts":[[2003,8]]}}}