The Complexity of Some Subclasses of Minimal Unsatisfiable Formulas

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