Back

G-2007-08

Using Meta-Heuristics to Find Minimal Unsatisfiable Subformulas in Satisfiability Problems

, , , and

BibTeX reference

In this paper, we propose efficient algorithms to extract minimal unsatisfiable subsets of clauses or variables in unsatisfiable propositional formulas. Such subsets yield unsatisfiable propositional subformulas that become satisfiable when any of their clauses or variables is removed. These subformulas have numerous applications, including proving unsatisfiability and post-infeasibility analysis. The algorithms we propose are based on meta-heuristics, and thus, can be applied to large instances. Furthermore, we show that, in some cases, the minimality of the subformulas can be proven with these algorithms. We also present an original algorithm to find minimum cardinality unsatisfiable subformulas in smaller instances. Finally, we report computational experiments on unsatisfiable instances from various sources, that demonstrate the effectiveness of our algorithms.

, 27 pages

Research Axis

Publication

Using meta-heuristics to find minimal unsatisfiable subformulas in satisfiability problems
, , , and
Journal of Combinatorial Optimization, 18, 124–150, 2009 BibTeX reference