Hostname: page-component-cd9895bd7-lnqnp Total loading time: 0 Render date: 2024-12-23T11:20:59.314Z Has data issue: false hasContentIssue false
  • English
  • Français

Model enumeration in propositional circumscription via unsatisfiable core analysis*

Published online by Cambridge University Press:  22 August 2017

MARIO ALVIANO
MARIO ALVIANO*
Affiliation:
Department of Mathematics and Computer Science, University of Calabria, Rende, Italy (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

Many practical problems are characterized by a preference relation over admissible solutions, where preferred solutions are minimal in some sense. For example, a preferred diagnosis usually comprises a minimal set of reasons that is sufficient to cause the observed anomaly. Alternatively, a minimal correction subset comprises a minimal set of reasons whose deletion is sufficient to eliminate the observed anomaly. Circumscription formalizes such preference relations by associating propositional theories with minimal models. The resulting enumeration problem is addressed here by means of a new algorithm taking advantage of unsatisfiable core analysis. Empirical evidence of the efficiency of the algorithm is given by comparing the performance of the resulting solver, circumscriptino, with hclasp, camus_mcs, lbx and mcsls on the enumeration of minimal models for problems originating from practical applications.

Keywords

Circumscriptionminimal model enumerationminimal correction subsetsminimal intervention strategiesunsatisfiable core analysis
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 17 , Special Issue 5-6: 33rd International Conference on Logic Programming , September 2017 , pp. 708 - 725
Copyright
Copyright © Cambridge University Press 2017 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

*

This research has been partially supported by the Italian Ministry for Economic Development (MISE) under project “PIUCultura – Paradigmi Innovativi per l'Utilizzo della Cultura” (no. F/020016/01-02/X27), and under project “Smarter Solutions in the Big Data World (S2BDW)” (no. F/050389/01-03/X32) funded within the call “HORIZON2020” PON I&C 2014-2020, and by Gruppo Nazionale per il Calcolo Scientifico (GNCS-INdAM).

References

Alviano, M. 2016. Evaluating answer set programming with non-convex recursive aggregates. Fundamenta Informaticae 149, 1–2, 1–34.CrossRefGoogle Scholar
Alviano, M., Calimeri, F., Dodaro, C., Fuscà, D., Leone, N., Perri, S., Ricca, F., Veltri, P. and Zangari, J. 2017. The ASP system DLV2. In Proc. of 14th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR '17), July 3–6, Espoo, Finland, Balduccini, M. and Janhunen, T., Eds., Lecture Notes in Computer Science, vol. 10377. Springer, 215–221.Google Scholar
Alviano, M. and Dodaro, C. 2016a. Answer set enumeration via assumption literals. In Proc. of 25th International Conference of the Italian Association for Artificial Intelligence on Advances in Artificial Intelligence (AI*IA '16), November 29–December 1, Genova, Italy, Adorni, G., Cagnoni, S., Gori, M. and Maratea, M., Eds., Lecture Notes in Computer Science, vol. 10037. Springer, 149–163.Google Scholar
Alviano, M. and Dodaro, C. 2016b. Anytime answer set optimization via unsatisfiable core shrinking. Theory and Practice of Logic Programming 16, 5–6, 533–551.CrossRefGoogle Scholar
Alviano, M. and Dodaro, C. 2016c. Completion of disjunctive logic programs. In Proc. of 25th International Joint Conference on Artificial Intelligence (IJCAI '16), July 9–15, New York, NY, USA, Kambhampati, S., Ed., IJCAI/AAAI Press, 886–892.Google Scholar
Alviano, M., Dodaro, C., Leone, N. and Ricca, F. 2015. Advances in WASP. In Proc. of 13th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR '15), September 27–30, Lexington, KY, USA, Calimeri, F., Ianni, G. and Truszczynski, M., Eds., Lecture Notes in Computer Science, vol. 9345. Springer, 40–54.Google Scholar
Alviano, M., Dodaro, C. and Ricca, F. 2015. A maxsat algorithm using cardinality constraints of bounded size. In Proc. of 24th International Joint Conference on Artificial Intelligenc (IJCAI '15), July 25–31, Buenos Aires, Argentina, Yang, Q. and Wooldridge, M., Eds., AAAI Press, 2677–2683.Google Scholar
Alviano, M. and Faber, W. 2013. The complexity boundary of answer set programming with generalized atoms under the FLP semantics. In Proc. of 12th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR '13), September 15–19, Corunna, Spain, Cabalar, P. and Son, T. C., Eds., Lecture Notes in Computer Science, vol. 8148. Springer, 67–72.Google Scholar
Alviano, M., Faber, W. and Gebser, M. 2015. Rewriting recursive aggregates in answer set programming: Back to monotonicity. Theory and Practice of Logic Programming 15, 4–5, 559–573.CrossRefGoogle Scholar
Alviano, M. and Leone, N. 2015. Complexity and compilation of GZ-aggregates in answer set programming. Theory and Practice of Logic Programming 15, 4–5, 574–587.CrossRefGoogle Scholar
Andres, B., Kaufmann, B., Matheis, O. and Schaub, T. 2012. Unsatisfiability-based optimization in clasp. In Proc. of Technical Communications of the 28th International Conference on Logic Programming (ICLP '12), September 4–8, Budapest, Hungary, Dovier, A. and Costa, V. S., Eds., LIPIcs, vol. 17, Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 211–221.Google Scholar
Audemard, G. and Simon, L. 2009. Predicting learnt clauses quality in modern SAT solvers. In Proc. of 21st International Joint Conference on Artificial Intelligence (IJCAI '09), July 11–17, Pasadena, CA, USA, Boutilier, C., Ed., 399–404.Google Scholar
Bacchus, F. and Narodytska, N. 2014. Cores in core based maxsat algorithms: An analysis. In Proc. of 17th International Conference on Theory and Applications of Satisfiability Testing (SAT '14), Held as Part of the Vienna Summer of Logic (VSL '04), July 14–17, Vienna, Austria, Sinz, C. and Egly, U., Eds., Lecture Notes in Computer Science, vol. 8561. Springer, 7–15.Google Scholar
Brewka, G., Delgrande, J. P., Romero, J. and Schaub, T. 2015a. asprin: Customizing answer set preferences without a headache. In Proc. of 29th AAAI Conference on Artificial Intelligence, January 25–30, Austin, TX, USA, Bonet, B. and Koenig, S., Eds. AAAI Press, 1467–1474.Google Scholar
Brewka, G., Delgrande, J. P., Romero, J. and Schaub, T. 2015b. Implementing preferences with asprin. In Proc. of 13th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR '15), September 27–30, Lexington, KY, USA, Calimeri, F., Ianni, G. and Truszczynski, M., Eds., Lecture Notes in Computer Science, vol. 9345. Springer, 158–172.Google Scholar
Dodaro, C., Alviano, M., Faber, W., Leone, N., Ricca, F. and Sirianni, M. 2011. The birth of a WASP: preliminary report on a new ASP solver. In Proc. of 26th Italian Conference on Computational Logic, August 31–September 2, Pescara, Italy, Fioravanti, F. (Ed.), CEUR Workshop Proceedings, vol. 810. CEUR-WS.org, 99–113.Google Scholar
Faber, W., Vallati, M., Cerutti, F. and Giacomin, M. 2016. Solving set optimization problems by cardinality optimization with an application to argumentation. In Proc. of 22nd European Conference on Artificial Intelligence (ECAI '16) – Including Prestigious Applications of Artificial Intelligence (PAIS '16), 29 August–2 September, The Hague, The Netherlands, Kaminka, G. A., Fox, M., Bouquet, P., Hüllermeier, E., Dignum, V., Dignum, F. and van Harmelen, F., Eds., Frontiers in Artificial Intelligence and Applications, vol. 285. IOS Press, 966–973.Google Scholar
Gebser, M., Kaminski, R., Kaufmann, B., Romero, J., and Schaub, T. 2015. Progress in clasp series 3. In Proc. of 13th International Conference Logic Programming and Nonmonotonic Reasoning (LPNMR '05), September 27–30, Lexington, KY, USA, Calimeri, F., Ianni, G. and Truszczynski, M., Eds., Lecture Notes in Computer Science, vol. 9345, 2015. Springer, 368–383.Google Scholar
Gebser, M., Kaminski, R., Kaufmann, B. and Schaub, T. 2009. On the implementation of weight constraint rules in conflict-driven ASP solvers. In Proc. of 25th International Conference on Logic Programming (ICLP '09), July 14–17, Pasadena, CA, USA, Hill, P. M. and Warren, D. S., Eds., Lecture Notes in Computer Science, vol. 5649. Springer, 250–264.Google Scholar
Gebser, M., Kaminski, R., Kaufmann, B. and Schaub, T. 2017. Multi-shot ASP solving with clingo. CoRR abs/1705.09811.Google Scholar
Gebser, M., Kaufmann, B., Neumann, A. and Schaub, T. 2007. Conflict-driven answer set enumeration. In Proc. of 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR '07), May 15–17, Tempe, AZ, USA, Baral, C., Brewka, G. and Schlipf, J. S., Eds., Lecture Notes in Computer Science, vol. 4483. Springer, 136–148.Google Scholar
Gebser, M., Kaufmann, B., Romero, J., Otero, R., Schaub, T. and Wanko, P. 2013. Domain-specific heuristics in answer set programming. In Proc. of 27th AAAI Conference on Artificial Intelligence, July 14–18, Bellevue, Washington, USA, desJardins, M. and Littman, M. L., Eds. AAAI Press.CrossRefGoogle Scholar
Gebser, M., Kaufmann, B. and Schaub, T. 2012. Conflict-driven answer set solving: From theory to practice. Artificial Intelligence 187, 52–89.CrossRefGoogle Scholar
Giunchiglia, E., Lierler, Y. and Maratea, M. 2004. Sat-based answer set programming. In Proc. of 19th National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence, July 25–29, San Jose, CA, USA, McGuinness, D. L. and Ferguson, G., Eds. AAAI Press/MIT Press, 61–66.Google Scholar
Giunchiglia, E., Lierler, Y. and Maratea, M. 2006. Answer set programming based on propositional satisfiability. Journal of Automated Reasoning 36, 4, 345–377.CrossRefGoogle Scholar
Giunchiglia, E. and Maratea, M. 2006. optsat: A tool for solving SAT related optimization problems. In Proc. of 10th European Conference on Logics in Artificial Intelligence (JELIA '06), September 13–15, Liverpool, UK, Fisher, M., van der Hoek, W., Konev, B. and Lisitsa, A., Eds. Lecture Notes in Computer Science, vol. 4160. Springer, 485–489.Google Scholar
Janhunen, T. and Niemelä, I. 2011. Compact translations of non-disjunctive answer set programs to propositional clauses. In Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning – Essays Dedicated to Michael Gelfond on the Occasion of His 65th Birthday, Balduccini, M. and Son, T. C., Eds., Lecture Notes in Computer Science, vol. 6565. Springer, 111–130.CrossRefGoogle Scholar
Jannach, D., Schmitz, T. and Shchekotykhin, K. M. 2016. Parallel model-based diagnosis on multi-core computers. Journal of Artificial Intelligence Research 55, 835–887.CrossRefGoogle Scholar
Järvisalo, M., Berre, D. L., Roussel, O. and Simon, L. 2012. The international SAT solver competitions. AI Magazine 33, 1, 89–94.CrossRefGoogle Scholar
Junker, U. 2004. QUICKXPLAIN: Preferred explanations and relaxations for over-constrained problems. In Proc. of 19th National Conference on Artificial Intelligence, 16th Conference on Innovative Applications of Artificial Intelligence, July 25–29, San Jose, CA, USA, McGuinness, D. L. and Ferguson, G., Eds. AAAI Press/MIT Press, 167–172.Google Scholar
Kaminski, R., Schaub, T., Siegel, A. and Videla, S. 2013. Minimal intervention strategies in logical signaling networks with ASP. Theory and Practice of Logic Programming 13, 4–5, 675–690.CrossRefGoogle Scholar
Lee, J. and Lifschitz, V. 2003. Loop formulas for disjunctive logic programs. In Proc. of 19th International Conference on Logic Programming (ICLP '03), December 9–13, Mumbai, India, Palamidessi, C., Ed. Lecture Notes in Computer Science, vol. 2916. Springer, 451–465.Google Scholar
Lee, J. and Lin, F. 2006. Loop formulas for circumscription. Artificial Intelligence 170, 2, 160–185.CrossRefGoogle Scholar
Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S. and Scarcello, F. 2006. The DLV system for knowledge representation and reasoning. ACM Transactions on Computational Logic 7, 3, 499–562.CrossRefGoogle Scholar
Liffiton, M. H. and Sakallah, K. A. 2008. Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning 40, 1, 1–33.CrossRefGoogle Scholar
Lifschitz, V. 1986. On the satisfiability of circumscription. Artificial Intelligence 28, 1, 17–27.CrossRefGoogle Scholar
Lin, F. and Zhao, Y. 2004. ASSAT: Computing answer sets of a logic program by SAT solvers. Artificial Intelligence 157, 1–2, 115–137.CrossRefGoogle Scholar
Marques-Silva, J., Heras, F., Janota, M., Previti, A. and Belov, A. 2013. On computing minimal correction subsets. In Proc. of 23rd International Joint Conference on Artificial Intelligence (IJCAI '13), August 3–9, Beijing, China, Rossi, F., Ed. IJCAI/AAAI, 615–622.Google Scholar
Marques-Silva, J. and Previti, A. 2014. On computing preferred MUSes and MCSes. In Proc. of 17th International Conference on Theory and Applications of Satisfiability Testing (SAT '14), Held as Part of the Vienna Summer of Logic (VSL '14), July 14–17, Vienna, Austria, Sinz, C. and Egly, U., Eds. Lecture Notes in Computer Science, vol. 8561. Springer, 58–74.Google Scholar
McCarthy, J. 1980. Circumscription – A form of non-monotonic reasoning. Artificial Intelligence 13, 1–2, 27–39.CrossRefGoogle Scholar
Mencía, C., Ignatiev, A., Previti, A. and Marques-Silva, J. 2016. MCS extraction with sublinear oracle queries. In Proc. of 19th International Conference on Theory and Applications of Satisfiability Testing (SAT '16), July 5–8, Bordeaux, France, Creignou, N. and Berre, D. L., Eds. Lecture Notes in Computer Science, vol. 9710. Springer, 342–360.Google Scholar
Mencía, C., Previti, A. and Marques-Silva, J. 2015. Literal-based MCS extraction. In Proc. of 24th International Joint Conference on Artificial Intelligence (IJCAI '15), July 25–31, Buenos Aires, Argentina, Yang, Q. and Wooldridge, M., Eds. AAAI Press.Google Scholar
Morgado, A., Heras, F., Liffiton, M. H., Planes, J. and Marques-Silva, J. 2013. Iterative and core-guided maxsat solving: A survey and assessment. Constraints 18, 4, 478–534.CrossRefGoogle Scholar
Narodytska, N. and Bacchus, F. 2014. Maximum satisfiability using core-guided maxsat resolution. In Proc. of 28th AAAI Conference on Artificial Intelligence, July 27–31, Québec City, Québec, Canada, Brodley, C. E. and Stone, P., Eds., AAAI Press, 2717–2723.Google Scholar
Pereira, L. M., Damásio, C. V. and Alferes, J. J. 1993. Debugging by diagnosing assumptions. In Proc. of 1st International Workshop Automated and Algorithmic Debugging (AADEBUG '93), May 3–5, Linköping, Sweden, Fritszon, P. (Ed.), Lecture Notes in Computer Science, vol. 749. Springer, 58–74.Google Scholar
Romero, J., Schaub, T. and Wanko, P. 2016. Computing diverse optimal stable models. In Proc. of Technical Communications of the 32nd International Conference on Logic Programming, (ICLP-TC '16), October 16–21, New York, NY, USA, Carro, M., King, A., Saeedloei, N. and Vos, M. D., Eds. OASICS, vol. 52, Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 3:1–3:14.Google Scholar