Document Open Access Logo

Tunable Online MUS/MSS Enumeration

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

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2016.50.pdf
  • Filesize: 493 kB
  • 13 pages

Document Identifiers

Author Details

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

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.FSTTCS.2016.50

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.

Subject Classification

Keywords
  • Minimal unsatisfiable subsets
  • Maximal satisfiable subsets
  • Unsatisfiab- ility analysis
  • Infeasibility analysis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Zaher S. Andraus, Mark H. Liffiton, and Karem A. Sakallah. Reveal: A formal verification tool for verilog designs. In LPAR, volume 5330 of Lecture Notes in Computer Science, pages 343-352. Springer, 2008. Google Scholar
  2. James Bailey and Peter J. Stuckey. Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In Practical Aspects of Declarative Languages, pages 174-186. Springer, 2005. Google Scholar
  3. Jiri Barnat, Petr Bauch, and Lubos Brim. Checking sanity of software requirements. In SEFM 2012 Proceedings, volume 7504 of LNCS, pages 48-62. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-33826-7_4.
  4. Anton Belov and Joao Marques-Silva. MUSer2: An efficient MUS extractor. Journal on Satisfiability, Boolean Modeling and Computation, 8:123-128, 2012. Google Scholar
  5. Elazar Birnbaum and Eliezer L. Lozinskii. Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell., 15(1):25-46, 2003. Google Scholar
  6. Renato Bruni and Antonio Sassano. Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae. Electronic Notes in Discrete Mathematics, 9:162-173, 2001. Google Scholar
  7. Maria Garcia de la Banda, Peter J. Stuckey, and Jeremy Wazny. Finding all minimal unsatisfiable subsets. In Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, pages 32-43. ACM, 2003. Google Scholar
  8. Niklas Eén and Niklas Sörensson. An extensible sat-solver. In SAT, volume 2919 of Lecture Notes in Computer Science, pages 502-518. Springer, 2003. Google Scholar
  9. Benjamin Han and Shie-Jue Lee. Deriving minimal conflict sets by cs-trees with mark set in diagnosis from first principles. IEEE Trans. Systems, Man, and Cybernetics, Part B, 29(2):281-286, 1999. Google Scholar
  10. Aimin Hou. A theory of measurement in diagnosis from first principles. Artif. Intell., 65(2):281-328, 1994. Google Scholar
  11. Ulrich Junker. QUICKXPLAIN: preferred explanations and relaxations for over-constrained problems. In AAAI, pages 167-172. AAAI Press / The MIT Press, 2004. Google Scholar
  12. Mark H. Liffiton and Ammar Malik. Enumerating infeasibility: Finding multiple muses quickly. In Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 10th International Conference, CPAIOR 2013, Yorktown Heights, NY, USA, May 18-22, 2013. Proceedings, volume 7874 of Lecture Notes in Computer Science, pages 160-175. Springer, 2013. Google Scholar
  13. Mark H. Liffiton, Michael D. Moffitt, Martha E. Pollack, and Karem A. Sakallah. Identifying conflicts in overconstrained temporal problems. In IJCAI, pages 205-211. Professional Book Center, 2005. Google Scholar
  14. Mark H. Liffiton, Alessandro Previti, Ammar Malik, and Joao Marques-Silva. Fast, flexible MUS enumeration. Constraints, pages 1-28, 2015. Google Scholar
  15. Mark H. Liffiton and Karem A. Sakallah. Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning, 40(1):1-33, 2008. Google Scholar
  16. MUS track of the 2011 SAT competition. URL: http://www.cril.univ-artois.fr/SAT11/.
  17. Yoonna Oh, Maher N. Mneimneh, Zaher S. Andraus, Karem A. Sakallah, and Igor L. Markov. AMUSE: a minimally-unsatisfiable subformula extractor. In DAC, pages 518-523. ACM, 2004. Google Scholar
  18. Alessandro Previti and João Marques-Silva. Partial MUS enumeration. In Proceedings of the Twenty-Seventh AAAI Conference on Artificial Intelligence, July 14-18, 2013, Bellevue, Washington, USA. Press, 2013. Google Scholar
  19. Lintao Zhang and Sharad Malik. Extracting small unsatisfiable cores from unsatisfiable boolean formula. SAT, 3, 2003. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact