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

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)

Язык публикации: english

Серия книг: Lecture Notes in Computer Science

Том: 11628

Номера страниц: 211-221

Количество страниц: 11

Год публикации: 2019

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

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: Нет