Tunable Online MUS/MSS Enumeration

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F16%3A00091546" target="_blank" >RIV/00216224:14330/16:00091546 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2016.50" target="_blank" >http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2016.50</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2016.50" target="_blank" >10.4230/LIPIcs.FSTTCS.2016.50</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Tunable Online MUS/MSS Enumeration

Popis výsledku v původním jazyce

In various areas of computer science, the problem of dealing with a set of constraints arises. If the set of constraints is unsatisfiable, one may ask for a minimal description of the reason for this unsatisifiability. Minimal unsatisfiable subsets (MUSes) and maximal satisfiable subsets (MSSes) are two kinds of such minimal descriptions. The goal of this work is the enumeration of MUSes and MSSes for a given constraint system. As such full enumeration may be intractable in general, we focus on building an online algorithm, which produces MUSes/MSSes in an on-the-fly manner as soon as they are discovered. The problem has been studied before even in its online version. However, our algorithm uses a novel approach that is able to outperform the current state-of-the-art algorithms for online MUS/MSS enumeration. Moreover, the performance of our algorithm can be adjusted using tunable parameters. We evaluate the algorithm on a set of benchmarks.

Název v anglickém jazyce

Tunable Online MUS/MSS Enumeration

Popis výsledku anglicky

In various areas of computer science, the problem of dealing with a set of constraints arises. If the set of constraints is unsatisfiable, one may ask for a minimal description of the reason for this unsatisifiability. Minimal unsatisfiable subsets (MUSes) and maximal satisfiable subsets (MSSes) are two kinds of such minimal descriptions. The goal of this work is the enumeration of MUSes and MSSes for a given constraint system. As such full enumeration may be intractable in general, we focus on building an online algorithm, which produces MUSes/MSSes in an on-the-fly manner as soon as they are discovered. The problem has been studied before even in its online version. However, our algorithm uses a novel approach that is able to outperform the current state-of-the-art algorithms for online MUS/MSS enumeration. Moreover, the performance of our algorithm can be adjusted using tunable parameters. We evaluate the algorithm on a set of benchmarks.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2016

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

Foundations of Software Technology and Theoretical Computer Science - 36th International Conference, FSTTCS 2016

ISBN

9783959770279

ISSN

1868-8969

e-ISSN

—

Počet stran výsledku

13

Strana od-do

661-673

Název nakladatele

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Místo vydání

Dagstuhl, Germany

Místo konání akce

Chennai, India

Datum konání akce

8. 12. 2016

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

WRD - Celosvětová akce

Kód UT WoS článku

—