Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F18%3A00104038" target="_blank" >RIV/00216224:14330/18:00104038 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.29007/sxzb" target="_blank" >http://dx.doi.org/10.29007/sxzb</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.29007/sxzb" target="_blank" >10.29007/sxzb</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2018

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

LPAR-22, 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning

ISBN

—

ISSN

2398-7340

e-ISSN

—

Počet stran výsledku

12

Strana od-do

131-142

Název nakladatele

EPiC Series in Computing

Místo vydání

Awassa, Etiopie

Místo konání akce

Awassa, Etiopie

Datum konání akce

1. 1. 2018

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—