Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

BENDÍK Jaroslav ČERNÁ Ivana

Rok publikování 2018
Druh Článek ve sborníku
Konference LPAR-22, 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www http://www.easychair.org/publications/paper/m8qv
Doi http://dx.doi.org/10.29007/sxzb
Klíčová slova minimal unsatisfiable subsets;mus enumeration;infeasibility analysis;unsatisfiability analysis
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.