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 φ, if φ(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?1 and t?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.