Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets

Result code in 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>

Result on the web

<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>

Result language

angličtina

Original language name

Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

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

Project

—

Continuities

S - Specificky vyzkum na vysokych skolach

Publication year

2018

Confidentiality

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

Article name in the collection

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

ISBN

—

ISSN

2398-7340

e-ISSN

—

Number of pages

12

Pages from-to

131-142

Publisher name

EPiC Series in Computing

Place of publication

Awassa, Etiopie

Event location

Awassa, Etiopie

Event date

Jan 1, 2018

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—