nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Reasoning About Strong Inconsistency in ASP

verfasst von : Carlos Mencía, Joao Marques-Silva

Erschienen in: Theory and Applications of Satisfiability Testing – SAT 2020

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

The last decade has witnessed remarkable improvements in the analysis of inconsistent formulas, namely in the case of Boolean Satisfiability (SAT) formulas. However, these successes have been restricted to monotonic logics. Recent work proposed the notion of strong inconsistency for a number of non-monotonic logics, including Answer Set Programming (ASP). This paper shows how algorithms for reasoning about inconsistency in monotonic logics can be extended to the case of ASP programs, in the concrete case of strong inconsistency. Initial experimental results illustrate the potential of the proposed approach.

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 On Weakening Strategies for PB Solvers

Nächstes Kapitel Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology

MSMP was proposed in [37, 38], but it was inspired by earlier work [12, 13].

This notion was defined for arbitrary non-monotonic logics. We show it for ASP.

Computing a minimal/maximal model can be reduced to computing an MCS. For this purpose, several alternatives can be used (e.g. [3, 36, 39, 40]).

Ansótegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial maxSAT through satisfiability testing. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 427–440. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02777-2_39MATHCrossRef

Ansótegui, C., Bonet, M.L., Levy, J.: SAT-based MaxSAT algorithms. Artif. Intell. 196, 77–105 (2013)MathSciNetMATHCrossRef

Bacchus, F., Davies, J., Tsimpoukelli, M., Katsirelos, G.: Relaxation search: a simple way of managing optional clauses. In: AAAI, pp. 835–841 (2014)

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

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_3MATHCrossRef

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

Bakker, R.R., Dikker, F., Tempelman, F., Wognum, P.M.: Diagnosing and solving over-determined constraint satisfaction problems. In: IJCAI, pp. 276–281 (1993)

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

Bendík, J., Černá, I., Beneš, N.: Recursive online enumeration of all minimal unsatisfiable subsets. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 143–159. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01090-4_9CrossRef

10.

Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)

11.

Birnbaum, E., Lozinskii, E.L.: Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell. 15(1), 25–46 (2003)MATHCrossRef

12.

Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: FMCAD, pp. 173–180 (2007)

13.

Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Formal Aspects of Comput. 20(4–5), 379–405 (2008). https://doi.org/10.1007/s00165-008-0080-9MATHCrossRef

14.

Brewka, G., Eiter, T., Truszczynski, M.: Answer set programming at a glance. Commun. ACM 54(12), 92–103 (2011)CrossRef

15.

Brewka, G., Thimm, M., Ulbricht, M.: Strong inconsistency in nonmonotonic reasoning. In: IJCAI, pp. 901–907 (2017)

16.

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

17.

Chinneck, J.W., Dravnieks, E.W.: Locating minimal infeasible constraint sets in linear programs. ORSA J. Comput. 3(2), 157–168 (1991)MATHCrossRef

18.

Davies, J., Bacchus, F.: Solving MAXSAT by solving a sequence of simpler SAT instances. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 225–239. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23786-7_19CrossRef

19.

Dodaro, C., Gasteiger, P., Musitsch, B., Ricca, F., Shchekotykhin, K.: Interactive debugging of non-ground ASP programs. In: Calimeri, F., Ianni, G., Truszczynski, M. (eds.) LPNMR 2015. LNCS (LNAI), vol. 9345, pp. 279–293. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23264-5_24MATHCrossRef

20.

Fandinno, J., Schulz, C.: Answering the “why” in answer set programming - a survey of explanation approaches. Theory Pract. Log. Program. 19(2), 114–203 (2019)MathSciNetMATHCrossRef

21.

Felfernig, A., Schubert, M., Zehentner, C.: An efficient diagnosis algorithm for inconsistent constraint sets. AI EDAM 26(1), 53–62 (2012)

22.

Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T.: Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers, San Rafael (2012)

23.

Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T.: Clingo = ASP + control: extended report. Technical report, University of Potsdam (2014)

24.

Gebser, M., Pührer, J., Schaub, T., Tompits, H.: A meta-programming technique for debugging answer-set programs. In: AAAI, pp. 448–453 (2008)

25.

Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: ICLP/SLP, pp. 1070–1080 (1988)

26.

Grégoire, É., Izza, Y., Lagniez, J.: Boosting MCSes enumeration. In: IJCAI, pp. 1309–1315 (2018)

27.

Grégoire, É., Lagniez, J., Mazure, B.: An experimentally efficient method for (MSS, CoMSS) partitioning. In: AAAI, pp. 2666–2673 (2014)

28.

Grégoire, É., Mazure, B., Piette, C.: Extracting MUSes. In: ECAI, pp. 387–391 (2006)

29.

Hemery, F., Lecoutre, C., Sais, L., Boussemart, F.: Extracting MUCs from constraint networks. In: ECAI, pp. 113–117 (2006)

30.

Janota, M., Marques-Silva, J.: On minimal corrections in ASP. CoRR abs/1406.7838 (2014). http://arxiv.org/abs/1406.7838

31.

Janota, M., Marques-Silva, J.: On minimal corrections in ASP. In: RCRA, pp. 45–54 (2017). http://ceur-ws.org/Vol-2011/paper5.pdf

32.

Junker, U.: QUICKXPLAIN: preferred explanations and relaxations for over-constrained problems. In: AAAI, pp. 167–172 (2004)

33.

Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints 21(2), 223–250 (2015). https://doi.org/10.1007/s10601-015-9183-0MathSciNetMATHCrossRef

34.

Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning 40(1), 1–33 (2008). https://doi.org/10.1007/s10817-007-9084-zMathSciNetMATHCrossRef

35.

Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for weighted Boolean optimization. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 495–508. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02777-2_45CrossRef

36.

Marques-Silva, J., Heras, F., Janota, M., Previti, A., Belov, A.: On computing minimal correction subsets. In: IJCAI, pp. 615–622 (2013)

37.

Marques-Silva, J., Janota, M., Belov, A.: Minimal sets over monotone predicates in Boolean formulae. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 592–607. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_39CrossRef

38.

Marques-Silva, J., Janota, M., Mencía, C.: Minimal sets on propositional formulae. Problems and reductions. Artif. Intell. 252, 22–50 (2017)MathSciNetMATHCrossRef

39.

Mencía, C., Ignatiev, A., Previti, A., Marques-Silva, J.: MCS extraction with sublinear oracle queries. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 342–360. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_21CrossRef

40.

Mencía, C., Previti, A., Marques-Silva, J.: Literal-based MCS extraction. In: IJCAI, pp. 1973–1979 (2015)

41.

Morgado, A., Heras, F., Liffiton, M.H., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints 18(4), 478–534 (2013). https://doi.org/10.1007/s10601-013-9146-2MathSciNetMATHCrossRef

42.

Narodytska, N., Bjørner, N., Marinescu, M.V., Sagiv, M.: Core-guided minimal correction set and core enumeration. In: IJCAI, pp. 1353–1361 (2018)

43.

Oetsch, J., Pührer, J., Tompits, H.: Catching the ouroboros: on debugging non-ground answer-set programs. Theory Pract. Log. Program. 10(4–6), 513–529 (2010)MathSciNetMATHCrossRef

44.

Polleres, A., Frühstück, M., Schenner, G., Friedrich, G.: Debugging non-ground ASP programs with choice rules, cardinality and weight constraints. In: Cabalar, P., Son, T.C. (eds.) LPNMR 2013. LNCS (LNAI), vol. 8148, pp. 452–464. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40564-8_45MATHCrossRef

45.

Previti, A., Mencía, C., Järvisalo, M., Marques-Silva, J.: Premise set caching for enumerating minimal correction subsets. In: AAAI, pp. 6633–6640 (2018)

46.

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

47.

Simons, P., Niemelä, I., Soininen, T.: Extending and implementing the stable model semantics. Artif. Intell. 138(1–2), 181–234 (2002)MathSciNetMATHCrossRef

48.

de Siqueira N., J.L., Puget, J.: Explanation-based generalisation of failures. In: ECAI, pp. 339–344 (1988)

Titel: Reasoning About Strong Inconsistency in ASP
verfasst von: Carlos Mencía
Joao Marques-Silva
Verlag: Springer International Publishing
Buch: Theory and Applications of Satisfiability Testing – SAT 2020
Print ISBN: 978-3-030-51824-0

Electronic ISBN: 978-3-030-51825-7

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-51825-7_24

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"