MUST: Minimal Unsatisfiable Subsets Enumeration Tool

D 2020

MUST: Minimal Unsatisfiable Subsets Enumeration Tool

BENDÍK, Jaroslav and Ivana ČERNÁ

Basic information

Original name

MUST: Minimal Unsatisfiable Subsets Enumeration Tool

Authors

BENDÍK, Jaroslav (203 Czech Republic, guarantor, belonging to the institution) and Ivana ČERNÁ (203 Czech Republic, belonging to the institution)

Edition

Neuveden, Tools and Algorithms for the Construction and Analysis of Systems, p. 135-152, 18 pp. 2020

Publisher

Springer International Publishing

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10200 1.2 Computer and information sciences

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/20:00115396

Organization unit

Faculty of Informatics

ISBN

978-3-030-45189-9

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-45190-5_8

Keywords in English

Minimal unsatisfiable subsets;Unsatisfiability analysis;Infeasibility analysis;MUS;Diagnosis

Abstract

V originále

In many areas of computer science, we are given an unsatisfiable set of constraints with the goal to provide an insight into the unsatisfiability. One of common approaches is to identify minimal unsatisfiable subsets (MUSes) of the constraint set. The more MUSes are identified, the better insight is obtained. However, since there can be up to exponentially many MUSes, their complete enumeration might be intractable. Therefore, we focus on algorithms that enumerate MUSes online, i.e. one by one, and thus can find at least some MUSes even in the intractable cases. Since MUSes find applications in different constraint domains and new applications still arise, there have been proposed several domain agnostic algorithms. Such algorithms can be applied in any constraint domain and thus theoretically serve as ready-to-use solutions for all the emerging applications. However, there are almost no domain agnostic tools, i.e. tools that both implement domain agnostic algorithms and can be easily extended to support any constraint domain. In this work, we close this gap by introducing a domain agnostic tool called MUST. Our tool outperforms other existing domain agnostic tools and moreover, it is even competitive to fully domain specific solutions.

Links

EF16_019/0000822, research and development project

Name: Centrum excelence pro kyberkriminalitu, kyberbezpečnost a ochranu kritických informačních infrastruktur

MUNI/A/1050/2019, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX (Acronym: SV-FI MAV IX)

Investor: Masaryk University, Category A

MUNI/A/1076/2019, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 20 (Acronym: SKOMU)

Investor: Masaryk University, Category A

Citovat

BENDÍK, Jaroslav and Ivana ČERNÁ. MUST: Minimal Unsatisfiable Subsets Enumeration Tool. In Armin Biere and David Parker. Tools and Algorithms for the Construction and Analysis of Systems. Neuveden: Springer International Publishing, 2020, p. 135-152. ISBN 978-3-030-45189-9. Available from: https://dx.doi.org/10.1007/978-3-030-45190-5_8.

@inproceedings{1633241,
   author = {Bendík, Jaroslav and Černá, Ivana},
   address = {Neuveden},
   booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
   doi = {http://dx.doi.org/10.1007/978-3-030-45190-5_8},
   editor = {Armin Biere and David Parker},
   keywords = {Minimal unsatisfiable subsets;Unsatisfiability analysis;Infeasibility analysis;MUS;Diagnosis},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-030-45189-9},
   pages = {135-152},
   publisher = {Springer International Publishing},
   title = {MUST: Minimal Unsatisfiable Subsets Enumeration Tool},
   year = {2020}
}

TY  - JOUR
ID  - 1633241
AU  - Bendík, Jaroslav - Černá, Ivana
PY  - 2020
TI  - MUST: Minimal Unsatisfiable Subsets Enumeration Tool
PB  - Springer International Publishing
CY  - Neuveden
SN  - 9783030451899
KW  - Minimal unsatisfiable subsets;Unsatisfiability analysis;Infeasibility analysis;MUS;Diagnosis
N2  - In many areas of computer science, we are given an unsatisfiable set of constraints with the goal to provide an insight into the unsatisfiability. One of common approaches is to identify minimal unsatisfiable subsets (MUSes) of the constraint set. The more MUSes are identified, the better insight is obtained. However, since there can be up to exponentially many MUSes, their complete enumeration might be intractable. Therefore, we focus on algorithms that enumerate MUSes online, i.e. one by one, and thus can find at least some MUSes even in the intractable cases. Since MUSes find applications in different constraint domains and new applications still arise, there have been proposed several domain agnostic algorithms. Such algorithms can be applied in any constraint domain and thus theoretically serve as ready-to-use solutions for all the emerging applications. However, there are almost no domain agnostic tools, i.e. tools that both implement domain agnostic algorithms and can be easily extended to support any constraint domain. In this work, we close this gap by introducing a domain agnostic tool called MUST. Our tool outperforms other existing domain agnostic tools and moreover, it is even competitive to fully domain specific solutions.
ER  -

BENDÍK, Jaroslav and Ivana ČERNÁ. MUST: Minimal Unsatisfiable Subsets Enumeration Tool. In Armin Biere and David Parker. \textit{Tools and Algorithms for the Construction and Analysis of Systems}. Neuveden: Springer International Publishing, 2020, p.~135-152. ISBN~978-3-030-45189-9. Available from: https://dx.doi.org/10.1007/978-3-030-45190-5\_{}8.

Detailed Information on Publication Record