Other formats:
BibTeX
LaTeX
RIS
@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.
|
