nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

FMUS2: An Efficient Algorithm to Compute Minimal Unsatisfiable Subsets

verfasst von : Shaofan Liu, Jie Luo

Erschienen in: Artificial Intelligence and Symbolic Computation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

In the past few years, much attention has been given to the problem of finding Minimal Unsatisfiable Subsets (MUSes), not only for its theoretical importance but also for its wide range of practical applications, including software testing, hardware verification and knowledge-based validation. In this paper, we propose an algorithm for extracting all MUSes for formulas in the field of propositional logic and the function-free and equality-free fragment of first-order logic. This algorithm extends earlier work, but some changes have been made and a number of optimization strategies have been proposed to improve its efficiency. Experimental results show that our algorithm performs well on many industrial and generated instances, and the strategies adopted can indeed improve the efficiency of our algorithm.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Machine Learning for Inductive Theorem Proving

Nächstes Kapitel Deciding Extended Modal Logics by Combining State Space Generation and SAT Solving

Bacchus, F., Katsirelos, G.: Finding a collection of MUSes incrementally. In: Quimper, C.-G. (ed.) CPAIOR 2016. LNCS, vol. 9676, pp. 35–44. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33954-2_3CrossRefMATH

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_14CrossRef

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, pp. 32–43. ACM (2003)

Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 25(2), 97–116 (2012)MathSciNetMATH

de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24CrossRef

Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3_37CrossRef

Gomes, C.P., Kautz, H., Sabharwal, A., Selman, B.: Satisfiability solvers. Found. Artifi. Intell. 3, 89–134 (2008)CrossRef

Hou, A.: A theory of measurement in diagnosis from first principles. Artif. Intell. 65(2), 281–328 (1994)MathSciNetCrossRef

Hutter, F., Hoos, H.H., Leyton-Brown, K.: Tradeoffs in the empirical evaluation of competing algorithm designs. Ann. Math. Artif. Intell. 60(1–2), 65–89 (2010)MathSciNetCrossRef

10.

Li, W., Shen, N., Wang, J.: R-calculus: a logical approach for knowledge base maintenance. Int. J. Artif. Intell. Tools 4(01n02), 177–200 (1995)CrossRef

11.

Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints 21(2), 223–250 (2016)MathSciNetCrossRef

12.

Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40(1), 1–33 (2008)MathSciNetCrossRef

13.

Luo, J., Li, W.: R-calculus without the cut rule. Sci. China Inf. Sci. 54(12), 2530–2543 (2011)MathSciNetCrossRef

14.

Previti, A., Marques-Silva, J.: Partial MUS enumeration. In: AAAI (2013)

15.

Ramsey, F.P.: On a problem of formal logic. In: Gessel, I., Rota, G.C. (eds.) Classic Papers in Combinatorics. MBC, pp. 1–24. Springer, Boston (2009). https://doi.org/10.1007/978-0-8176-4842-8_1CrossRef

16.

Ryvchin, V., Strichman, O.: Faster extraction of high-level minimal unsatisfiable cores. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 174–187. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21581-0_15CrossRefMATH

17.

Stern, R.T., Kalech, M., Feldman, A., Provan, G.M.: Exploring the duality in conflict-directed model-based diagnosis. In: AAAI, vol. 12, pp. 828–834 (2012)

18.

Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 59(4), 483–502 (2017)MathSciNetCrossRef

19.

Xiao, G., Ma, Y.: Inconsistency measurement based on variables in minimal unsatisfiable subsets. In: European Conference on Artificial Intelligence 2012 (ECAI 2012) (2012)

20.

Xie, H., Luo, J.: An algorithm to compute minimal unsatisfiable subsets for a decidable fragment of first-order formulas. In: 2016 IEEE 28th International Conference on Tools with Artificial Intelligence (ICTAI), pp. 444–451. IEEE (2016)

Titel: FMUS2: An Efficient Algorithm to Compute Minimal Unsatisfiable Subsets
verfasst von: Shaofan Liu
Jie Luo
Verlag: Springer International Publishing
Buch: Artificial Intelligence and Symbolic Computation
Print ISBN: 978-3-319-99956-2

Electronic ISBN: 978-3-319-99957-9

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-99957-9_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"