nach oben

Erschienen in:

2022 | OriginalPaper | Buchkapitel

Computing Smallest MUSes of Quantified Boolean Formulas

verfasst von : Andreas Niskanen, Jere Mustonen, Jeremias Berg, Matti Järvisalo

Erschienen in: Logic Programming and Nonmonotonic Reasoning

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

Computing small (subset-minimal or smallest) explanations is a computationally challenging task for various logics and non-monotonic formalisms. Arguably the most progress in practical algorithms for computing explanations has been made for propositional logic in terms of minimal unsatisfiable subsets (MUSes) of conjunctive normal form formulas. In this work, we propose an approach to computing smallest MUSes of quantified Boolean formulas (QBFs), building on the so-called implicit hitting set approach and modern QBF solving techniques. Connecting to non-monotonic formalisms, our approach finds applications in the realm of abstract argumentation in computing smallest strong explanations of acceptance and rejection. Justifying our approach, we pinpoint the complexity of deciding the existence of small MUSes for QBFs with any fixed number of quantifier alternations. We empirically evaluate the approach on computing strong explanations in abstract argumentation frameworks as well as benchmarks from recent QBF Evaluations.

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 Towards Provenance in Heterogeneous Knowledge Bases

Nächstes Kapitel Pinpointing Axioms in Ontologies via ASP

The proposition also holds when considering subset-minimal strong explanations and MUSes of the corresponding 2-QBF.

Note that by employing integer programming our approach also allows for computing weighted SMUSes, i.e., cores with smallest total weight over their elements.

Alfano, G., Calautti, M., Greco, S., Parisi, F., Trubitsyna, I.: Explainable acceptance in probabilistic abstract argumentation: complexity and approximation. In: KR, pp. 33–43 (2020)

Arieli, O., Caminada, M.W.A.: A QBF-based formalization of abstract argumentation semantics. J. Appl. Log. 11(2), 229–252 (2013)MathSciNetCrossRefMATH

Bacchus, F., Hyttinen, A., Järvisalo, M., Saikko, P.: Reduced cost fixing in MaxSAT. In: Beck, J.C. (ed.) CP 2017. LNCS, vol. 10416, pp. 641–651. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66158-2_41

Bacchus, F., Katsirelos, G.: Using minimal correction sets to more efficiently compute minimal unsatisfiable sets. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 70–86. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21668-3_5CrossRef

Baumann, R., Ulbricht, M.: Choices and their consequences - explaining acceptable sets in abstract argumentation frameworks. In: KR, pp. 110–119 (2021)

Baumeister, D., Järvisalo, M., Neugebauer, D., Niskanen, A., Rothe, J.: Acceptance in incomplete argumentation frameworks. Artif. Intell. 295, 103470 (2021)MathSciNetCrossRefMATH

Belov, A., Marques-Silva, J.: Accelerating MUS extraction with recursive model rotation. In: FMCAD, pp. 37–40. FMCAD Inc. (2011)

Bendík, J., Černá, I.: Replication-guided enumeration of minimal unsatisfiable subsets. In: Simonis, H. (ed.) CP 2020. LNCS, vol. 12333, pp. 37–54. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-58475-7_3

Besnard, P., Doutre, S.: Checking the acceptability of a set of arguments. In: NMR, pp. 59–64 (2004)

10.

Brewka, G., Thimm, M., Ulbricht, M.: Strong inconsistency. Artif. Intell. 267, 78–117 (2019)MathSciNetCrossRefMATH

11.

Brewka, G., Ulbricht, M.: Strong explanations for nonmonotonic reasoning. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, A.-Y., Wolter, F. (eds.) Description Logic, Theory Combination, and All That. LNCS, vol. 11560, pp. 135–146. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-22102-7_6

12.

Delisle, E., Bacchus, F.: Solving weighted CSPs by successive relaxations. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 273–281. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40627-0_23CrossRef

13.

Dung, P.M.: On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artif. Intell. 77(2), 321–358 (1995)MathSciNetCrossRefMATH

14.

Egly, U., Woltran, S.: Reasoning in argumentation frameworks using quantified boolean formulas. In: COMMA. FAIA, vol. 144, pp. 133–144. IOS Press (2006)

15.

Fan, X., Toni, F.: On computing explanations in argumentation. In: AAAI, pp. 1496–1502. AAAI Press (2015)

16.

Ignatiev, A., Janota, M., Marques-Silva, J.: Quantified maximum satisfiability. Constraints 21(2), 277–302 (2015). https://doi.org/10.1007/s10601-015-9195-9MathSciNetCrossRefMATH

17.

Ignatiev, A., Previti, A., Liffiton, M., Marques-Silva, J.: Smallest MUS extraction with minimal hitting set dualization. In: Pesant, G. (ed.) CP 2015. LNCS, vol. 9255, pp. 173–182. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23219-5_13CrossRef

18.

Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1–25 (2016)MathSciNetCrossRefMATH

19.

Jordan, C., Kaiser, Ł.: Experiments with reduction finding. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 192–207. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39071-5_15

20.

Liberatore, P.: Redundancy in logic I: CNF propositional formulae. Artif. Intell. 163(2), 203–232 (2005)MathSciNetCrossRefMATH

21.

Liffiton, M.H., Mneimneh, M.N., Lynce, I., Andraus, Z.S., Marques-Silva, J., Sakallah, K.A.: A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Constraints 14(4), 415–442 (2009)MathSciNetCrossRefMATH

22.

Lonsing, F., Egly, U.: Incremental QBF solving. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 514–530. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10428-7_38CrossRef

23.

Lonsing, F., Egly, U.: Incrementally computing minimal unsatisfiable cores of QBFs via a clause group solver API. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 191–198. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24318-4_14

24.

Lonsing, F., Egly, U.: DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 371–384. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_23

25.

Marques-Silva, J., Mencía, C.: Reasoning about inconsistent formulas. In: IJCAI, pp. 4899–4906. ijcai.org (2020)

26.

Mencía, C., Marques-Silva, J.: Reasoning about strong inconsistency in ASP. In: Pulina, L., Seidl, M. (eds.) SAT 2020. LNCS, vol. 12178, pp. 332–342. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51825-7_24

27.

Niskanen, A., Järvisalo, M.: Smallest explanations and diagnoses of rejection in abstract argumentation. In: KR, pp. 667–671 (2020)

28.

Papadimitriou, C.H.: Computational Complexity. Addison-Wesley (1994)

29.

Papadimitriou, C.H., Wolfe, D.: The complexity of facets resolved. J. Comput. Syst. Sci. 37(1), 2–13 (1988)MathSciNetCrossRefMATH

30.

Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57–95 (1987)MathSciNetCrossRefMATH

31.

Saikko, P., Dodaro, C., Alviano, M., Järvisalo, M.: A hybrid approach to optimization in answer set programming. In: KR, pp. 32–41. AAAI Press (2018)

32.

Saikko, P., Wallner, J.P., Järvisalo, M.: Implicit hitting set algorithms for reasoning beyond NP. In: KR, pp. 104–113. AAAI Press (2016)

33.

Sakama, C.: Abduction in argumentation frameworks. J. Appl. Non Class. Logics 28(2–3), 218–239 (2018)MathSciNetCrossRefMATH

34.

Saribatur, Z.G., Wallner, J.P., Woltran, S.: Explaining non-acceptability in abstract argumentation. In: ECAI, FAIA, vol. 325, pp. 881–888. IOS Press (2020)

35.

Ulbricht, M., Baumann, R.: If nothing is accepted - repairing argumentation frameworks. J. Artif. Intell. Res. 66, 1099–1145 (2019)MathSciNetCrossRefMATH

36.

Ulbricht, M., Thimm, M., Brewka, G.: Handling and measuring inconsistency in non-monotonic logics. Artif. Intell. 286, 103344 (2020)MathSciNetCrossRefMATH

37.

Ulbricht, M., Wallner, J.P.: Strong explanations in abstract argumentation. In: AAAI, pp. 6496–6504. AAAI Press (2021)

Titel: Computing Smallest MUSes of Quantified Boolean Formulas
verfasst von: Andreas Niskanen
Jere Mustonen
Jeremias Berg
Matti Järvisalo
Verlag: Springer International Publishing
Buch: Logic Programming and Nonmonotonic Reasoning
Print ISBN: 978-3-031-15706-6

Electronic ISBN: 978-3-031-15707-3

Copyright-Jahr: 2022
DOI: https://doi.org/10.1007/978-3-031-15707-3_23

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"

Premium Partner