The beta version of DROPS 2 is now publicly available! Check this page out at DROPS 2 now!


License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2016.50
URN: urn:nbn:de:0030-drops-68855
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6885/
Go to the corresponding LIPIcs Volume Portal

Bendík, Jaroslav ; Benes, Nikola ; Cerná, Ivana ; Barnat, Jirí

Tunable Online MUS/MSS Enumeration

pdf-format:
LIPIcs-FSTTCS-2016-50.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{bendk_et_al:LIPIcs:2016:6885,
  author =	{Jaroslav Bend{\'i}k and Nikola Benes and Ivana Cern{\'a} and Jir{\'i} Barnat},
  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 =	{Akash Lal and S. Akshay and Saket Saurabh and Sandeep Sen},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6885},
  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}
}

Keywords: Minimal unsatisfiable subsets, Maximal satisfiable subsets, Unsatisfiab- ility analysis, Infeasibility analysis
Collection: 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)
Issue Date: 2016
Date of publication: 10.12.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI