DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2016.50

Tunable Online MUS/MSS Enumeration

Authors: Jaroslav Bendík, Nikola Benes, Ivana Cerná, and Jirí Barnat

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract

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.

Cite as

Jaroslav Bendík, Nikola Benes, Ivana Cerná, and Jirí Barnat. Tunable Online MUS/MSS Enumeration. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 50:1-50:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bendik_et_al:LIPIcs.FSTTCS.2016.50,
  author =	{Bend{\'\i}k, Jaroslav and Benes, Nikola and Cern\'{a}, Ivana and Barnat, Jir{\'\i}},
  title =	{{Tunable Online MUS/MSS Enumeration}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{50:1--50:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.50},
  URN =		{urn:nbn:de:0030-drops-68855},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.50},
  annote =	{Keywords: Minimal unsatisfiable subsets, Maximal satisfiable subsets, Unsatisfiab- ility analysis, Infeasibility analysis}
}

Search Results

Documents authored by Bendík, Jaroslav

Tunable Online MUS/MSS Enumeration

Abstract

Cite as

Thanks for your feedback!

Could not send message