Extracting MUSes

Minimally unsatisfiable subformulas (in short, MUSes) represent the smallest explanations for the inconsistency of SAT instances in terms of the number of involved clauses. Extracting MUSes can thus prove valuable because it circumscribes the sources of contradiction in an instance. In this paper, a new heuristic-based approach to approximate or compute MUSes is presented. It is shown that it often outperforms current competing ones.

• Type: Conference
• Year: 2006
• Where: ECAI
• Authors: Éric Grégoire, Bertrand Mazure, Cédric Piette
• Keywords: Artificial Intelligence, ECAI 2006, MUSes, Sat Instances, Smallest Explanations