Polynomial-Time Recognition of Minimal Unsatisfiable Formulas with Fixed Clause-Variable Difference
Theoretical Computer Science 289 no. 1, pp. 503-516, 2002.
Download:   [paper ps] [paper pdf]
Abstract:A formula (in conjunctive normal form) is said to be minimal unsatisfiable if it is unsatisfiable and deleting any clause makes it satisfiable. The deficiency of a formula is the difference of the number of clauses and the number of variables. It is known that every minimal unsatisfiable formula has positive deficiency.
Until recently, polynomial-time algorithms were known to recognize minimal unsatisfiable formulas with deficiency 1 and 2. We state an algorithm which recognizes minimal unsatisfiable formulas with any fixed deficiency in polynomial time.