Minimal Unsatisfiability and Autarkies
Kleine Büning Hans, Kullmann Oliver · Frontiers in artificial intelligence and applications · 2009
Minimal unsatisfiability describes the reduced kernel of unsatisfiable formulas. The investigation of this property is very helpful in understanding the reasons for unsatisfiability as well as the behaviour of SAT-solvers and proof calculi. Moreover, for propositional formulas and quantified Boolean formulas the computational complexity of various SAT-related problems are strongly related to the complexity of minimal unsatisfiable formulas.