Abstract
In many areas of computer science, we are given an unsatisfiable set of constraints with the goal to provide an insight into the unsatisfiability. One of common approaches is to identify minimal unsatisfiable subsets (MUSes) of the constraint set. The more MUSes are identified, the better insight is obtained. However, since there can be up to exponentially many MUSes, their complete enumeration might be intractable. Therefore, we focus on algorithms that enumerate MUSes online, i.e. one by one, and thus can find at least some MUSes even in the intractable cases. Since MUSes find applications in different constraint domains and new applications still arise, there have been proposed several domain agnostic algorithms. Such algorithms can be applied in any constraint domain and thus theoretically serve as ready-to-use solutions for all the emerging applications. However, there are almost no domain agnostic tools, i.e. tools that both implement domain agnostic algorithms and can be easily extended to support any constraint domain. In this work, we close this gap by introducing a domain agnostic tool called MUST. Our tool outperforms other existing domain agnostic tools and moreover, it is even competitive to fully domain specific solutions.
This research was supported by ERDF “CyberSecurity, CyberCrime and Critical Information Infrastructures Center of Excellence” (No. CZ.\(02.1.01/0.0/0.0/16\_019/0000822\)).
Chapter PDF
Similar content being viewed by others
References
Fahiem Bacchus and George Katsirelos. Using minimal correction sets to more efficiently compute minimal unsatisfiable sets. In CAV (2), volume 9207 of LNCS, pages 70–86. Springer, 2015.
Fahiem Bacchus and George Katsirelos. Finding a collection of MUSes incrementally. In CPAIOR, volume 9676 of LNCS, pages 35–44. Springer, 2016.
James Bailey and Peter J. Stuckey. Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In PADL, pages 174–186. Springer, 2005.
Jiří Barnat, Petr Bauch, Nikola Beneš, Luboš Brim, JanBeran, and Tomáš Kratochvíla. Analysing sanity of requirements for avionics systems.FAoC, 2016.
Anton Belov and João Marques-Silva.MUSer2: An efficient MUS extractor. JSAT, 8:123–128, 2012.
Jaroslav Bendík. Consistency checking in requirements analysis. In ISSTA, pages 408–411. ACM, 2017.
Jaroslav Bendík, Nikola Beneš, Ivana Černá, andJiří Barnat. Tunable online MUS/MSS enumeration. In FSTTCS, volume 65 of LIPIcs, pages 50:1–50:13. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
Jaroslav Bendík and Ivana Černá. Evaluation of domain agnostic approaches for enumeration of minimal unsatisfiable subsets. In LPAR, volume 57 of EPiC Series in Computing, pages 131–142. EasyChair, 2018.
Jaroslav Bendík, Ivana Černá, and Nikola Beneš. Recursive online enumeration of all minimal unsatisfiable subsets. In ATVA, volume 11138 of LNCS, pages 143–159. Springer, 2018.
Jaroslav Bendík, Elaheh Ghassabani, Michael W. Whalen, and IvanaČerná. Online enumeration of all minimal inductive validity cores. In SEFM, volume 10886 of LNCS, pages 189–204. Springer, 2018.
Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. The nuxmv symbolic model checker. In CAV, volume 8559 of LNCS, pages 334–342. Springer, 2014.
Huan Chen and João Marques-Silva. Improvements to satisfiability-based boolean function bi-decomposition. In VLSI-SoC, pages 142–147. IEEE, 2011.
Alessandro Cimatti, Alberto Griggio, and Roberto Sebastiani. Computing small unsatisfiable cores in satisfiability modulotheories.JAIR, 40:701–728, 2011.
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In CAV, volume 1855 of LNCS, pages 154–169. Springer, 2000.
Orly Cohen, Moran Gordon, Michael Lifshits, Alexander Nadel, and Vadim Ryvchin. Designers work less with quality formal equivalence checking. In Design and Verification Conference (DVCon). Citeseer, 2010.
Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In TACAS, volume 4963 of LNCS, pages 337–340. Springer, 2008.
Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud,Etienne Renault, and Laurent Xu. Spot 2.0 - A framework for LTL and \(\omega \)-automata manipulation. In ATVA, volume 9938 of LNCS, pages 122–129, 2016.
Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In SAT, volume 2919 of LNCS, pages 502–518. Springer,2003.
Elaheh Ghassabani, Andrew Gacek, and Michael W. Whalen. Efficient generation of inductive validity cores for safety properties. In SIGSOFT FSE, pages 314–325. ACM, 2016.
Elaheh Ghassabani, Michael W. Whalen, and Andrew Gacek. Efficient generation of all minimal inductive validity cores. In FMCAD, pages 31–38. IEEE, 2017.
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.
Mark H. Liffiton, Alessandro Previti, Ammar Malik, and JoãoMarques-Silva. Fast, flexible MUS enumeration.Constraints, pages 1–28, 2015.
Kenneth L. McMillan and Nina Amla. Automatic abstraction without counterexamples. In TACAS, volume 2619 of LNCS, pages 2–17. Springer, 2003.
Alexander Nadel, Vadim Ryvchin, and Ofer Strichman. Accelerated deletion-based extraction of minimal unsatisfiable cores.JSAT, 9:27–51, 2014.
Nina Narodytska, Nikolaj Bjørner, Maria-Cristina Marinescu, and MoolySagiv. Core-guided minimal correction set and core enumeration. In IJCAI, pages 1353–1361. ijcai.org, 2018.
AMASS project partners. Project AMASS (Architecture-driven, Multi-concern and Seamless Assurance and Certification of Cyber-Physical Systems). https://amass-ecsel.eu/. [Online; Accessed: 2019-22-10].
AMASS project partners. Project AMASS, deliverable D3.6: Prototype for Architecture-DrivenAssurance (c). https://amass-ecsel.eu/content/deliverables. [Online; Accessed: 2019-22-10].
Emanuel Sperner. Ein satz über untermengen einer endlichen menge. Mathematische Zeitschrift, 27(1):544–548, 1928.
Roni Tzvi Stern, Meir Kalech, Alexander Feldman, and Gregory M. Provan. Exploring the duality in conflict-directed model-based diagnosis. In AAAI. AAAI Press, 2012.
Peter J. Stuckey, Martin Sulzmann, and Jeremy Wazny. Interactive type debugging in haskell. In Haskell, pages 72–83. ACM, 2003.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Bendík, J., Černá, I. (2020). MUST: Minimal Unsatisfiable Subsets Enumeration Tool. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science(), vol 12078. Springer, Cham. https://doi.org/10.1007/978-3-030-45190-5_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-45190-5_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45189-9
Online ISBN: 978-3-030-45190-5
eBook Packages: Computer ScienceComputer Science (R0)