Tunable Online MUS/MSS Enumeration

D 2016

Tunable Online MUS/MSS Enumeration

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

Basic information

Original name

Tunable Online MUS/MSS Enumeration

Authors

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

Country of publisher

Germany

Confidentiality degree

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

Publication form

printed version "print"

RIV identification code

RIV/00216224:14330/16:00091546

Organization unit

Faculty of Informatics

ISBN

978-3-95977-027-9

ISSN

DOI

http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2016.50

Keywords in English

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

Abstract

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.

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)

Investor: European Union, ECSEL

Citovat

BENDÍK, Jaroslav, Nikola BENEŠ, Ivana ČERNÁ and Jiří BARNAT. Tunable Online MUS/MSS Enumeration. In Akash Lal, S. Akshay, Saket Saurabh, Sandeep Sen. Foundations of Software Technology and Theoretical Computer Science - 36th International Conference, FSTTCS 2016. 65th ed. Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2016, p. 661-673. ISBN 978-3-95977-027-9. Available from: https://dx.doi.org/10.4230/LIPIcs.FSTTCS.2016.50.

@inproceedings{1359581,
   author = {Bendík, Jaroslav and Beneš, Nikola and Černá, Ivana and Barnat, Jiří},
   address = {Dagstuhl, Germany},
   booktitle = {Foundations of Software Technology and Theoretical Computer Science - 36th International Conference, FSTTCS 2016},
   doi = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2016.50},
   edition = {65},
   editor = {Akash Lal, S. Akshay, Saket Saurabh, Sandeep Sen},
   keywords = {Minimal unsatisfiable subsets; Maximal satisfiable subsets; Unsatisfiability analysis; Infeasibility analysis},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Dagstuhl, Germany},
   isbn = {978-3-95977-027-9},
   pages = {661-673},
   publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
   title = {Tunable Online MUS/MSS Enumeration},
   year = {2016}
}

TY  - JOUR
ID  - 1359581
AU  - Bendík, Jaroslav - Beneš, Nikola - Černá, Ivana - Barnat, Jiří
PY  - 2016
TI  - Tunable Online MUS/MSS Enumeration
PB  - Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
CY  - Dagstuhl, Germany
SN  - 9783959770279
KW  - Minimal unsatisfiable subsets
KW  - Maximal satisfiable subsets
KW  - Unsatisfiability analysis
KW  - Infeasibility analysis
N2  - 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.
ER  -

BENDÍK, Jaroslav, Nikola BENEŠ, Ivana ČERNÁ and Jiří BARNAT. Tunable Online MUS/MSS Enumeration. In Akash Lal, S. Akshay, Saket Saurabh, Sandeep Sen. \textit{Foundations of Software Technology and Theoretical Computer Science - 36th International Conference, FSTTCS 2016}. 65th ed. Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2016, p.~661-673. ISBN~978-3-95977-027-9. Available from: https://dx.doi.org/10.4230/LIPIcs.FSTTCS.2016.50.

Detailed Information on Publication Record