D 2020

MUST: Minimal Unsatisfiable Subsets Enumeration Tool

BENDÍK, Jaroslav a Ivana ČERNÁ

Základní údaje

Originální název

MUST: Minimal Unsatisfiable Subsets Enumeration Tool

Autoři

BENDÍK, Jaroslav (203 Česká republika, garant, domácí) a Ivana ČERNÁ (203 Česká republika, domácí)

Vydání

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

Nakladatel

Springer International Publishing

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Utajení

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

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/20:00115396

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-45189-9

ISSN

DOI

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

Klíčová slova anglicky

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

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 10. 5. 2021 05:40, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

Návaznosti

EF16_019/0000822, projekt VaV
Název: Centrum excelence pro kyberkriminalitu, kyberbezpečnost a ochranu kritických informačních infrastruktur
MUNI/A/1050/2019, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX (Akronym: SV-FI MAV IX)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/1076/2019, interní kód MU
Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 20 (Akronym: SKOMU)
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 20, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
Zobrazeno: 5. 11. 2024 10:47