The deficiency of a propositional formula F in CNF with n variables
and m clauses is defined as m-n. It is known that minimal
unsatisfiable formulas (unsatisfiable formulas which become
satisfiable by removing any clause) have positive deficiency.
Recognition of minimal unsatisfiable formulas is NP-hard, and it was
shown recently ... more >>>