Polynomial-Time Recognition of Minimal Unsatisfiable Formulas with Fixed Clause-Variable DifferenceTheoretical 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. [back to Stefan Szeider's homepage] |