Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency

We say a propositional formula F in conjunctive normal form is represented by a formula H and a homomorphism phi, if phi(H) = F. A homomorphism is a mapping consisting of a renaming and an identification of literals. The deficiency of a formula is the difference between the number of clauses and the number of variables. We show that for fixed k greater than or equal to 1 and t greater than or equal to 1 each minimal unsatisfiable formula with deficiency k can be represented by a formula H with deficiency t and a homomorphism and such a representation can be computed in polynomial time. (C) 2002 Elsevier Science B.V. All rights reserved.