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 and Ivana ČERNÁ

Basic information

Original name

Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets

Authors

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

Edition

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

Publisher

EPiC Series in Computing

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Confidentiality degree

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

Publication form

electronic version available online

References:

URL

RIV identification code

RIV/00216224:14330/18:00104038

Organization unit

Faculty of Informatics

ISSN

DOI

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

Keywords in English

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

Abstract

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.

Links

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

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

Investor: Masaryk University, Category A

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

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

Investor: Masaryk University, Category A

Citovat

BENDÍK, Jaroslav and 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, p. 131-142. ISSN 2398-7340. Available from: 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 and 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, p.~131-142. ISSN~2398-7340. Available from: https://dx.doi.org/10.29007/sxzb.

Detailed Information on Publication Record