An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF

    loading  Checking for direct PDF access through Ovid

Abstract

We consider the minimal unsatisfiability problem for propositional formulas over n variables with n+k clauses for fixed k. We will show that in case of at most n clauses no formula is minimal unsatisfiable. For n+1 clauses the minimal unsatisfiability problem is solvable in quadratic time. Further, we present a characterization of minimal unsatisfiable formulas with n+1 clauses in terms of a certain form of matrices.

Related Topics

    loading  Loading Related Articles