Страница публикации

On Computing the Union of MUSes

Авторы: Mencía C., Kullmann O., Ignatiev A., Marques-Silva J.

Журнал: Lecture Notes in Computer Science: Proc. of 22nd Intern. Conf. on Theory and Applications of Satisfiability Testing (SAT'2019; Lisbon; Portugal)

Том: 11628

Номер:

Год: 2019

Отчётный год: 2019

Издательство:

Местоположение издательства:

URL:

Проекты:

DOI: 10.1007/978-3-030-24258-9_15

Аннотация: 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.

Индексируется WOS: Q4

Индексируется Scopus: Нет

Индексируется УБС: Нет

Индексируется РИНЦ: Да

Индексируется ВАК: Нет

Индексируется CORE: Нет

Публикация в печати: 0