Evaluation of Domain Agnostic Approaches for Enumeration of
Minimal Unsatisfiable Subsets

D 2018

Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets

BENDÍK, Jaroslav a Ivana ČERNÁ

Základní údaje

Originální název

Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets

Autoři

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

Vydání

Awassa, Etiopie, LPAR-22, 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, od s. 131-142, 12 s. 2018

Nakladatel

EPiC Series in Computing

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Utajení

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

Forma vydání

elektronická verze "online"

Odkazy

URL

Kód RIV

RIV/00216224:14330/18:00104038

Organizační jednotka

Fakulta informatiky

ISSN

DOI

http://dx.doi.org/10.29007/sxzb

Klíčová slova anglicky

minimal unsatisfiable subsets;mus enumeration;infeasibility analysis;unsatisfiability analysis

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 31. 5. 2022 14:21, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

In many different applications we are given a set of constraints with the goal to decide whether the set is satisfiable. If the set is determined to be unsatisfiable, one might be interested in analysing this unsatisfiability. Identification of minimal unsatisfiable subsets (MUSes) is a kind of such analysis. The more MUSes are identified, the better insight into the unsatisfiability is obtained. However, the full enumeration of all MUSes is often intractable. Therefore, algorithms that identify MUSes in an online fashion, i.e., one by one, are needed. Moreover, since MUSes find applications in various constraint domains, and new applications still arise, there is a desire for domain agnostic MUS enumeration approaches. In this paper, we present an experimental evaluation of four state-of-the-art domain agnostic MUS enumeration algorithms: MARCO, TOME, ReMUS, and DAA. The evaluation is conducted in the SAT, SMT, and LTL constraint domains. The results evidence that there is no silver-bullet algorithm that would beat all the others in all the domains.

Návaznosti

MUNI/A/0854/2017, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII.

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

MUNI/A/1038/2017, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

BENDÍK, Jaroslav a Ivana ČERNÁ. Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets. Online. In Gilles Barthe and Geoff Sutcliffe and Margus Veanes. LPAR-22, 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Awassa, Etiopie: EPiC Series in Computing, 2018, s. 131-142. ISSN 2398-7340. Dostupné z: https://dx.doi.org/10.29007/sxzb.

@inproceedings{1449236,
   author = {Bendík, Jaroslav and Černá, Ivana},
   address = {Awassa, Etiopie},
   booktitle = {LPAR-22, 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
   doi = {http://dx.doi.org/10.29007/sxzb},
   editor = {Gilles Barthe and Geoff Sutcliffe and Margus Veanes},
   keywords = {minimal unsatisfiable subsets;mus enumeration;infeasibility analysis;unsatisfiability analysis},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Awassa, Etiopie},
   pages = {131-142},
   publisher = {EPiC Series in Computing},
   title = {Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets},
   url = {http://www.easychair.org/publications/paper/m8qv},
   year = {2018}
}

TY  - JOUR
ID  - 1449236
AU  - Bendík, Jaroslav - Černá, Ivana
PY  - 2018
TI  - Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets
PB  - EPiC Series in Computing
CY  - Awassa, Etiopie
KW  - minimal unsatisfiable subsets;mus enumeration;infeasibility analysis;unsatisfiability analysis
UR  - http://www.easychair.org/publications/paper/m8qv
N2  - In many different applications we are given a set of constraints with the goal to decide whether the set is satisfiable. If the set is determined to be unsatisfiable, one might be interested in analysing this unsatisfiability. Identification of minimal unsatisfiable subsets (MUSes) is a kind of such analysis. The more MUSes are identified, the better insight into the unsatisfiability is obtained. However, the full enumeration of all MUSes is often intractable. Therefore, algorithms that identify MUSes in an online fashion, i.e., one by one, are needed. Moreover, since MUSes find applications in various constraint domains, and new applications still arise, there is a desire for domain agnostic MUS enumeration approaches. In this paper, we present an experimental evaluation of four state-of-the-art domain agnostic MUS enumeration algorithms: MARCO, TOME, ReMUS, and DAA. The evaluation is conducted in the SAT, SMT, and LTL constraint domains. The results evidence that there is no silver-bullet algorithm that would beat all the others in all the domains.
ER  -

BENDÍK, Jaroslav a Ivana ČERNÁ. Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets. Online. In Gilles Barthe and Geoff Sutcliffe and Margus Veanes. \textit{LPAR-22, 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning}. Awassa, Etiopie: EPiC Series in Computing, 2018, s.~131-142. ISSN~2398-7340. Dostupné z: https://dx.doi.org/10.29007/sxzb.

Podrobný výpis o publikaci