Polynomial-Time Recognition of Minimal Unsatisfiable Formulas with Fixed Clause-Variable Difference

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

• Type: Journal
• Year: 2000
• Where: ECCC
• Authors: Herbert Fleischner, Stefan Szeider
• Keywords: Conjunctive Normal Form, ECCC 2000, Minimal Unsatisfiable Formulas, Unsatisfiable