Abstract
In various areas of computer science, we deal with a set of constraints to be satisfied. If the constraints cannot be satisfied simultaneously, it is desirable to identify the core problems among them. Such cores are called minimal unsatisfiable subsets (MUSes). The more MUSes are identified, the more information about the conflicts among the constraints is obtained. However, a full enumeration of all MUSes is in general intractable due to the large number (even exponential) of possible conflicts. Moreover, to identify MUSes, algorithms have to test sets of constraints for their simultaneous satisfiability. The type of the test depends on the application domains. The complexity of the tests can be extremely high especially for domains like temporal logics, model checking, or SMT. In this paper, we propose a recursive algorithm that identifies MUSes in an online manner (i.e., one by one) and can be terminated at any time. The key feature of our algorithm is that it minimises the number of satisfiability tests and thus speeds up the computation. The algorithm is applicable to an arbitrary constraint domain. We benchmark our algorithm against the state-of-the-art algorithm Marco on the Boolean and SMT constraint domains and demonstrate that our algorithm really requires less satisfiability tests and consequently finds more MUSes in the given time limits.
N. Beneš—The author has been supported by the Czech Science Foundation grant No. GA18-00178S.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Zaher, S.A., Mark, HL., Karem A.S.: Cegar-based formal hardware verification: a case study. Ann Arbor (2007)
Bacchus, F., Katsirelos, G.: Using minimal correction sets to more efficiently compute minimal unsatisfiable sets. In: Kroening, Daniel, Păsăreanu, Corina S. (eds.) CAV (2). LNCS, vol. 9207, pp. 70–86. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21668-3_5
Bacchus, F., Katsirelos, G.: Finding a collection of MUSes incrementally. In: CPAIOR (2016)
Bailey, J., Stuckey, P.J.: Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2005. LNCS, vol. 3350, pp. 174–186. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30557-6_14
Barnat, J., Bauch, P., Beneš, N., Brim, L., Beran, J., Kratochvíla, T.: Analysing sanity of requirements for avionics systems. Formal Aspects of Computing (2016)
Belov, A., Heule, M., Marques-Silva, J.: MUS extraction using clausal proofs. In: SAT (2014)
Belov, A., Marques-Silva, J.: Accelerating MUS extraction with recursive model rotation. In: FMCAD (2011)
Belov, A., Marques-Silva, J.: MUSer2: An efficient MUS extractor. J. Satisf. Boolean Model. Comput. (2012)
Belov, A., Marques Silva, J.P.: Minimally unsatisfiable boolean circuits. In: SAT (2011)
Bendík, J.: Consistency checking in requirements analysis. In: ISSTA (2017)
Bendík, J., Benes, N., Cerná, I., Barnat, J: Tunable online MUS/MSS enumeration. In: FSTTCS (2016)
Bendík, J., Ghassabani, E., Whalen, M., Černá, I.: Online enumeration of all minimal inductive validity cores. In: Johnsen, E.B., Schaefer, I. (eds.) SEFM 2018. LNCS, vol. 10886, pp. 189–204. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-92970-5_12
Chen, H., Marques-Silva, J.: Improvements to satisfiability-based boolean function bi-decomposition. In: VLSI-SoC (2011)
Cimatti, A., Griggio, A., Sebastiani, R.: Computing small unsatisfiable cores in satisfiability modulo theories. J. Artif. Intell. Res. (2011)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs (1981)
Clarke, E.M., Grumberg, Jha, S., Lu, Y., Veith, H,.: Counterexample-guided abstraction refinement. In: CAV (2000)
Cohen, O., Gordon, M., Lifshits, M., Nadel, A., Ryvchin, V.: Designers work less with quality formal equivalence checking. In: Design and Verification Conference (DVCon) (2010)
de la Banda, M.G., Stuckey, P.J., Wazny, J.: Finding all minimal unsatisfiable subsets. In: Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming (2003)
de Moura, L.M., Bjørner, N..: Z3: an efficient SMT solver. In: TACAS (2008)
Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 – a framework for LTL and \(\omega \)-automata manipulation. In: ATVA (2016)
Eén, N., Sörensson, A.: An extensible sat-solver. In: SAT (2003)
Gasca, R.M., Del Valle, C., Gómez López, M.T., Ceballos, R.: NMUS: structural analysis for improving the derivation of all muses in over constrained numeric csps. In: CAEPIA (2007)
Ghassabani, E., Whalen, M.W., Gacek, A.: Efficient generation of all minimal inductive validity cores. In: FMCAD (2017)
Gleeson, J., Ryan, J.: Identifying minimally infeasible subsystems of inequalities. INFORMS J. Comput. (1990)
Han, B., Lee, S.-J.: Deriving minimal conflict sets by cs-trees with mark set in diagnosis from first principles. IEEE Trans. Syst. Man Cybern. Part B (1999)
Hou, A.: A theory of measurement in diagnosis from first principles. Artif. Intell. (1994)
Liffiton, M.H., Malik, A.: Enumerating infeasibility: finding multiple muses quickly. In: Gomes, C., Sellmann, M. (eds.) CPAIOR 2013. LNCS, vol. 7874, pp. 160–175. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38171-3_11
Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints (2015)
Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. (2008)
McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: TACAS (2003)
Nadel, A.: Boosting minimal unsatisfiable core extraction. In: FMCAD (2010)
Nadel, A., Ryvchin, V., Strichman, O.: Efficient MUS extraction with resolution. In: FMCAD (2013)
Nadel, A., Ryvchin, V., Strichman, O.: Accelerated deletion-based extraction of minimal unsatisfiable cores. In: JSAT (2014)
Pnueli, A.: The temporal logic of programs. In: FOCS (1977)
Previti, A., Marques-Silva, J.: Partial MUS enumeration. In: Proceedings of the Twenty-Seventh AAAI Conference on Artificial Intelligence, Bellevue, 14–18 July 2013
Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. (1987)
Stuckey, P.J., Sulzmann, M., Wazny, J.: Interactive type debugging in haskell. In: Haskell (2003)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Bendík, J., Černá, I., Beneš, N. (2018). Recursive Online Enumeration of All Minimal Unsatisfiable Subsets. In: Lahiri, S., Wang, C. (eds) Automated Technology for Verification and Analysis. ATVA 2018. Lecture Notes in Computer Science(), vol 11138. Springer, Cham. https://doi.org/10.1007/978-3-030-01090-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-01090-4_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-01089-8
Online ISBN: 978-3-030-01090-4
eBook Packages: Computer ScienceComputer Science (R0)