Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems |
| |
Authors: | Christian Desrosiers Philippe Galinier Alain Hertz Sandrine Paroz |
| |
Institution: | (1) Ecole Polytechnique and GERAD, Montreal, Canada;(2) Ecole Polytechnique and CRT, Montreal, Canada |
| |
Abstract: | 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 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. |
| |
Keywords: | Satisfiability Heuristics Minimal unsatisfiable subformulas (MUS) |
本文献已被 SpringerLink 等数据库收录! |
|