Computing Minimally Unsatisfiable Subformulas: State of the Art and Future Directions
Joao Marques-Silva
The task of modeling and reasoning about real-world problems often involves analyzing over-constrained representations, where not all constraints of a problem can be simultaneously satisfied. The need to analyze over-constrained (or unsatisfiable) problems occurs in many settings, including data and knowledge bases, artificial intelligence, applied formal methods, operations research and description logics. In most cases, the problem to solve is related with some form of minimal unsatisfiability, i.e. an irreducible set of constraints that explains unsatisfiability. This paper provides an overview of algorithms for computing minimally unsatisfiable subformulas, and conducts an experimental evaluation of these algorithms. In addition, the paper briefly overviews computational problems related with minimal unsatisfiability in Boolean logic, practical applications of minimal unsatisfiability, and extensions of minimal unsatisfiability to other domains.
Keywords: Boolean Satisfiability; Minimally Unsatisfiable Subformulas; Unsatisfiability Proofs; Extensions of Boolean Satisfiability