Abstract
This paper considers unsatisfiable CNF formulas and addresses the problem of computing the union of the clauses included in some minimally unsatisfiable subformula (MUS). The union of MUSes represents a useful notion in infeasibility analysis since it summarizes all the causes for the unsatisfiability of a given formula. The paper proposes a novel algorithm for this problem, developing a refined recursive enumeration of MUSes based on powerful pruning techniques. Experimental results indicate the practical suitability of the approach.
Cite
CITATION STYLE
Mencía, C., Kullmann, O., Ignatiev, A., & Marques-Silva, J. (2019). On Computing the Union of MUSes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11628 LNCS, pp. 211–221). Springer Verlag. https://doi.org/10.1007/978-3-030-24258-9_15
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
