Skip to main content
Top

2018 | OriginalPaper | Chapter

Recursive Online Enumeration of All Minimal Unsatisfiable Subsets

Authors : Jaroslav Bendík, Ivana Černá, Nikola Beneš

Published in: Automated Technology for Verification and Analysis

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literature
1.
go back to reference Zaher, S.A., Mark, HL., Karem A.S.: Cegar-based formal hardware verification: a case study. Ann Arbor (2007) Zaher, S.A., Mark, HL., Karem A.S.: Cegar-based formal hardware verification: a case study. Ann Arbor (2007)
3.
go back to reference Bacchus, F., Katsirelos, G.: Finding a collection of MUSes incrementally. In: CPAIOR (2016) Bacchus, F., Katsirelos, G.: Finding a collection of MUSes incrementally. In: CPAIOR (2016)
5.
go back to reference 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) 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)
6.
go back to reference Belov, A., Heule, M., Marques-Silva, J.: MUS extraction using clausal proofs. In: SAT (2014) Belov, A., Heule, M., Marques-Silva, J.: MUS extraction using clausal proofs. In: SAT (2014)
7.
go back to reference Belov, A., Marques-Silva, J.: Accelerating MUS extraction with recursive model rotation. In: FMCAD (2011) Belov, A., Marques-Silva, J.: Accelerating MUS extraction with recursive model rotation. In: FMCAD (2011)
8.
go back to reference Belov, A., Marques-Silva, J.: MUSer2: An efficient MUS extractor. J. Satisf. Boolean Model. Comput. (2012) Belov, A., Marques-Silva, J.: MUSer2: An efficient MUS extractor. J. Satisf. Boolean Model. Comput. (2012)
9.
go back to reference Belov, A., Marques Silva, J.P.: Minimally unsatisfiable boolean circuits. In: SAT (2011) Belov, A., Marques Silva, J.P.: Minimally unsatisfiable boolean circuits. In: SAT (2011)
10.
go back to reference Bendík, J.: Consistency checking in requirements analysis. In: ISSTA (2017) Bendík, J.: Consistency checking in requirements analysis. In: ISSTA (2017)
11.
go back to reference Bendík, J., Benes, N., Cerná, I., Barnat, J: Tunable online MUS/MSS enumeration. In: FSTTCS (2016) Bendík, J., Benes, N., Cerná, I., Barnat, J: Tunable online MUS/MSS enumeration. In: FSTTCS (2016)
13.
go back to reference Chen, H., Marques-Silva, J.: Improvements to satisfiability-based boolean function bi-decomposition. In: VLSI-SoC (2011) Chen, H., Marques-Silva, J.: Improvements to satisfiability-based boolean function bi-decomposition. In: VLSI-SoC (2011)
14.
go back to reference Cimatti, A., Griggio, A., Sebastiani, R.: Computing small unsatisfiable cores in satisfiability modulo theories. J. Artif. Intell. Res. (2011) Cimatti, A., Griggio, A., Sebastiani, R.: Computing small unsatisfiable cores in satisfiability modulo theories. J. Artif. Intell. Res. (2011)
15.
go back to reference 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., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs (1981)
16.
go back to reference Clarke, E.M., Grumberg, Jha, S., Lu, Y., Veith, H,.: Counterexample-guided abstraction refinement. In: CAV (2000) Clarke, E.M., Grumberg, Jha, S., Lu, Y., Veith, H,.: Counterexample-guided abstraction refinement. In: CAV (2000)
17.
go back to reference 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) 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)
18.
go back to reference 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 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)
19.
go back to reference de Moura, L.M., Bjørner, N..: Z3: an efficient SMT solver. In: TACAS (2008) de Moura, L.M., Bjørner, N..: Z3: an efficient SMT solver. In: TACAS (2008)
20.
go back to reference 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) 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)
21.
go back to reference Eén, N., Sörensson, A.: An extensible sat-solver. In: SAT (2003) Eén, N., Sörensson, A.: An extensible sat-solver. In: SAT (2003)
22.
go back to reference 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) 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)
23.
go back to reference Ghassabani, E., Whalen, M.W., Gacek, A.: Efficient generation of all minimal inductive validity cores. In: FMCAD (2017) Ghassabani, E., Whalen, M.W., Gacek, A.: Efficient generation of all minimal inductive validity cores. In: FMCAD (2017)
24.
go back to reference Gleeson, J., Ryan, J.: Identifying minimally infeasible subsystems of inequalities. INFORMS J. Comput. (1990) Gleeson, J., Ryan, J.: Identifying minimally infeasible subsystems of inequalities. INFORMS J. Comput. (1990)
25.
go back to reference 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) 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)
26.
go back to reference Hou, A.: A theory of measurement in diagnosis from first principles. Artif. Intell. (1994) Hou, A.: A theory of measurement in diagnosis from first principles. Artif. Intell. (1994)
28.
go back to reference Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints (2015) Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints (2015)
29.
go back to reference Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. (2008) Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. (2008)
30.
go back to reference McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: TACAS (2003) McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: TACAS (2003)
31.
go back to reference Nadel, A.: Boosting minimal unsatisfiable core extraction. In: FMCAD (2010) Nadel, A.: Boosting minimal unsatisfiable core extraction. In: FMCAD (2010)
32.
go back to reference Nadel, A., Ryvchin, V., Strichman, O.: Efficient MUS extraction with resolution. In: FMCAD (2013) Nadel, A., Ryvchin, V., Strichman, O.: Efficient MUS extraction with resolution. In: FMCAD (2013)
33.
go back to reference Nadel, A., Ryvchin, V., Strichman, O.: Accelerated deletion-based extraction of minimal unsatisfiable cores. In: JSAT (2014) Nadel, A., Ryvchin, V., Strichman, O.: Accelerated deletion-based extraction of minimal unsatisfiable cores. In: JSAT (2014)
34.
go back to reference Pnueli, A.: The temporal logic of programs. In: FOCS (1977) Pnueli, A.: The temporal logic of programs. In: FOCS (1977)
35.
go back to reference Previti, A., Marques-Silva, J.: Partial MUS enumeration. In: Proceedings of the Twenty-Seventh AAAI Conference on Artificial Intelligence, Bellevue, 14–18 July 2013 Previti, A., Marques-Silva, J.: Partial MUS enumeration. In: Proceedings of the Twenty-Seventh AAAI Conference on Artificial Intelligence, Bellevue, 14–18 July 2013
36.
go back to reference Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. (1987) Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. (1987)
37.
go back to reference Stuckey, P.J., Sulzmann, M., Wazny, J.: Interactive type debugging in haskell. In: Haskell (2003) Stuckey, P.J., Sulzmann, M., Wazny, J.: Interactive type debugging in haskell. In: Haskell (2003)
Metadata
Title
Recursive Online Enumeration of All Minimal Unsatisfiable Subsets
Authors
Jaroslav Bendík
Ivana Černá
Nikola Beneš
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-030-01090-4_9

Premium Partner