Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency. (Q1853126)

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\geqslant1\) and \(t\geqslant1\) 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.