BENDÍK, Jaroslav (203 Czech Republic, guarantor), Nikola BENEŠ (203 Czech Republic, belonging to the institution), Ivana ČERNÁ (203 Czech Republic, belonging to the institution) and Jiří BARNAT (203 Czech Republic, belonging to the institution)
Edition
65. vyd. Dagstuhl, Germany, Foundations of Software Technology and Theoretical Computer Science - 36th International Conference, FSTTCS 2016, p. 661-673, 13 pp. 2016
Publisher
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Other information
Language
English
Type of outcome
Stať ve sborníku
Field of Study
10201 Computer sciences, information science, bioinformatics
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.
Links
MUNI/A/0935/2015, interní kód MU
Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Category A
MUNI/A/0945/2015, interní kód MU
Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.
Investor: Masaryk University, Category A
692474, interní kód MU
Name: AMASS - Architecture-driven, Multi-concern and Seamless Assurance and Certification of Cyber-Physical Systems (Acronym: AMASS)