The Complexity of Some Subclasses of Minimal Unsatisfiable Formulas

This paper is concerned with the complexity of some natural subclasses of minimal unsatisable formulas. We show the D P {completeness of the classes of maximal and marginal minimal unsatisable formulas. Then we consider the class Unique{MU of minimal unsatisable formulas which have after removing a clause exactly one satisfying truth assignment. We show that Unique{MU has the same complexity as the unique satisabilit y problem with respect to polynomial reduction. However, a slight modication of this class leads to the D P {completeness. Finally we show that the class of minimal unsatisable formulas which can be divided for every variable into two separate minimal unsatisable formulas is at least as hard as the unique satisabilit y problem.