D 2016

Tunable Online MUS/MSS Enumeration

BENDÍK, Jaroslav, Nikola BENEŠ, Ivana ČERNÁ a Jiří BARNAT

Základní údaje

Originální název

Tunable Online MUS/MSS Enumeration

Autoři

BENDÍK, Jaroslav (203 Česká republika, garant), Nikola BENEŠ (203 Česká republika, domácí), Ivana ČERNÁ (203 Česká republika, domácí) a Jiří BARNAT (203 Česká republika, domácí)

Vydání

65. vyd. Dagstuhl, Germany, Foundations of Software Technology and Theoretical Computer Science - 36th International Conference, FSTTCS 2016, od s. 661-673, 13 s. 2016

Nakladatel

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Kód RIV

RIV/00216224:14330/16:00091546

Organizační jednotka

Fakulta informatiky

ISBN

978-3-95977-027-9

ISSN

DOI

Klíčová slova anglicky

Minimal unsatisfiable subsets; Maximal satisfiable subsets; Unsatisfiability analysis; Infeasibility analysis

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 13. 10. 2020 09:44, prof. RNDr. Ivana Černá, CSc.

Anotace

V originále

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

MUNI/A/0935/2015, interní kód MU
Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0945/2015, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
692474, interní kód MU
Název: AMASS - Architecture-driven, Multi-concern and Seamless Assurance and Certification of Cyber-Physical Systems (Akronym: AMASS)
Investor: Evropská unie, AMASS - Architecture-driven, Multi-concern and Seamless Assurance and Certification of Cyber-Physical Systems, ECSEL