On computing the union of MUSes

Carlos Mencía, Oliver Kullmann, Alexey Ignatiev, Joao Marques-Silva

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

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.

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing – SAT 2019
Subtitle of host publication22nd International Conference, SAT 2019 Lisbon, Portugal, July 9–12, 2019 Proceedings
EditorsMikoláš Janota, Inês Lynce
Place of PublicationCham Switzerland
PublisherSpringer
Pages211-221
Number of pages11
ISBN (Electronic)9783030242589
ISBN (Print)9783030242572
DOIs
Publication statusPublished - 2019
Externally publishedYes
EventInternational Conference on Theory and Applications of Satisfiability Testing 2019 - Lisbon, Portugal
Duration: 7 Jul 201912 Jul 2019
Conference number: 22nd
http://sat2019.tecnico.ulisboa.pt/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume11628
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Theory and Applications of Satisfiability Testing 2019
Abbreviated titleSAT 2019
CountryPortugal
CityLisbon
Period7/07/1912/07/19
Internet address

Cite this

Mencía, C., Kullmann, O., Ignatiev, A., & Marques-Silva, J. (2019). On computing the union of MUSes. In M. Janota, & I. Lynce (Eds.), Theory and Applications of Satisfiability Testing – SAT 2019: 22nd International Conference, SAT 2019 Lisbon, Portugal, July 9–12, 2019 Proceedings (pp. 211-221). (Lecture Notes in Computer Science; Vol. 11628 ). Cham Switzerland: Springer. https://doi.org/10.1007/978-3-030-24258-9_15