Unsatisfiable Core Analysis and Aggregates for Optimum Stable Model Search

• Autorzy: Alviano Mario , Dodaro Carmine

Identyfikatory

DOI

10.3233/FI-2020-1974

• Języki publikacji: EN

Abstrakty

EN

Many efficient algorithms for the computation of optimum stable models in the context of Answer Set Programming (ASP) are based on unsatisfiable core analysis. Among them, algorithm OLL was the first introduced in the context of ASP, whereas algorithms ONE and PMRES were first introduced for solving the Maximum Satisfiability problem (MaxSAT) and later on adapted to ASP. In this paper, we present the porting to ASP of another state-of-the-art algorithm introduced for MaxSAT, namely K, which generalizes ONE and PMRES. Moreover, we present a new algorithm called OLL-IN-ONE that compactly encodes all aggregates of OLL by taking advantage of shared aggregate sets propagators. The performance of the algorithms have been empirically compared on instances taken from the latest ASP Competition.

Słowa kluczowe

EN

answer set programming; ASP; weak constraints; unsatisfiable core analysis

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 176, nr 3/4
• Strony: 271--297
• Opis fizyczny: Bibliogr. 59 poz., tab., wykr.

Twórcy

autor

Alviano Mario

• Department of Mathematics and Computer Science, University of Calabria, Arcavacata di Rende, Italy

autor

Dodaro Carmine

• Department of Informatics, Bioengineering, Robotics and Systems Engineering, University of Genova, Genova, Italy

Bibliografia

• [1] Gelfond M, Lifschitz V. Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing, 1991. 9(3/4):365-386. doi:10.1007/BF03037169.
• [2] Niemelä I. Logic Programming with Stable Model Semantics as Constraint Programming Paradigm. Annals of Mathematics and Artificial Intelligence, 1999. 25(3-4):241-273. doi:10.1023/A:1018930122475.
• [3] Marek VW, Truszczyński M. Stable Models and an Alternative Logic Programming Paradigm. In: The Logic Programming Paradigm - A 25-Year Perspective, pp. 375-398. Springer Verlag, 1999. doi:10.1007/978-3-642-60085-2_17.
• [4] Lifschitz V. Answer Set Programming and Plan Generation. Artificial Intelligence, 2002. 138:39-54. doi:10.1016/S0004-3702(02)00186-8.
• [5] Gelfond M, Kahl Y. Knowledge Representation, Reasoning, and the Design of Intelligent Agents: The Answer-Set Programming Approach. Cambridge University Press, 2014. ISBN 978-1107029569.
• [6] Faber W, Pfeifer G, Leone N. Semantics and complexity of recursive aggregates in answer set programming. Artificial Intelligence, 2011. 175(1):278-298. doi:10.1016/j.artint.2010.04.002.
• [7] Ferraris P. Logic programs with propositional connectives and aggregates. ACM Transactions on Computational Logic, 2011. 12(4):25. doi:10.1145/1970398.1970401.
• [8] Pelov N, Denecker M, Bruynooghe M. Well-founded and stable semantics of logic programs with aggregates. Theory and Practice of Logic Programming, 2007. 7(3):301-353. doi:10.1017/S1471068406002973.
• [9] Son TC, Pontelli E. A Constructive semantic characterization of aggregates in answer set programming. Theory and Practice of Logic Programming, 2007. 7(3):355-375. doi:10.1017/S1471068406002936.
• [10] Alviano M, Faber W. The Complexity Boundary of Answer Set Programming with Generalized Atoms under the FLP Semantics. In: Cabalar P, Son TC (eds.), International Conference on Logic Programming and Nonmonotonic Reasoning, volume 8148 of Lecture Notes in Computer Science. Springer, 2013 pp. 67-72. doi:10.1007/978-3-642-40564-8_7.
• [11] Alviano M, Faber W, Gebser M. Rewriting recursive aggregates in answer set programming: back to monotonicity. Theory and Practice of Logic Programming, 2015. 15(4-5):559-573. doi:10.1017/S1471068415000228.
• [12] Alviano M. Evaluating Answer Set Programming with Non-Convex Recursive Aggregates. Fundamenta Informaticae, 2016. 149(1-2):1-34. doi:10.3233/FI-2016-1441.
• [13] Balduccini M, Gelfond M, Watson R, Nogueira M. The USA-Advisor: A Case Study in Answer Set Planning. In: Eiter T, Faber W, Truszczynski M (eds.), International Conference on Logic Programming and Nonmonotonic Reasoning, volume 2173 of Lecture Notes in Computer Science. Springer, 2001 pp. 439-442. doi:10.1007/3-540-45402-0_39.
• [14] Alviano M, Dodaro C, Maratea M. An Advanced Answer Set Programming Encoding for Nurse Scheduling. In: Esposito F, Basili R, Ferilli S, Lisi FA (eds.), International Conference of the Italian Association for Artificial Intelligence (AI*IA), volume 10640 of Lecture Notes in Computer Science. Springer, 2017 pp. 468-482. doi:10.1007/978-3-319-70169-1_35.
• [15] Ricca F, Grasso G, Alviano M, Manna M, Lio V, Iiritano S, Leone N. Team-building with answer set programming in the Gioia-Tauro seaport. Theory and Practice of Logic Programming, 2012. 12(3):361-381. doi:10.1017/S147106841100007X.
• [16] Baral C, Uyan C. Declarative Specification and Solution of Combinatorial Auctions Using Logic Programming. In: Eiter T, Faber W, Truszczynski M (eds.), International Conference on Logic Programming and Nonmonotonic Reasoning, volume 2173 of Lecture Notes in Computer Science. Springer, 2001 pp. 186-199. doi:10.1007/3-540-45402-0\_14.
• [17] Koponen L, Oikarinen E, Janhunen T, Säilä L. Optimizing phylogenetic supertrees using answer set programming. Theory and Practice of Logic Programming, 2015. 15(4-5):604-619. doi:10.1017/S1471068415000265.
• [18] Dodaro C, Leone N, Nardi B, Ricca F. Allotment Problem in Travel Industry: A Solution Based on ASP. In: ten Cate B, Mileo A (eds.), International Conference on Web Reasoning and Rule Systems, volume 9209 of Lecture Notes in Computer Science. Springer, 2015 pp. 77-92. doi:10.1007/978-3-319-22002-4_7.
• [19] Marileo MC, Bertossi LE. The consistency extractor system: Answer set programs for consistent query answering in databases. Data & Knowledge Engineering, 2010. 69(6):545-572. doi:10.1016/j.datak.2010.01.005.
• [20] Gebser M, Ryabokon A, Schenner G. Combining Heuristics for Configuration Problems Using Answer Set Programming. In: Calimeri F, Ianni G, Truszczynski M (eds.), International Conference on Logic Programming and Nonmonotonic Reasoning, volume 9345 of Lecture Notes in Computer Science. Springer, 2015 pp. 384-397. doi:10.1007/978-3-319-23264-5_32.
• [21] Gebser M, Kaminski R, Kaufmann B, Romero J, Schaub T. Progress in clasp Series 3. In: Calimeri F, Ianni G, Truszczynski M (eds.), International Conference on Logic Programming and Nonmonotonic Reasoning, volume 9345 of Lecture Notes in Computer Science. Springer, 2015 pp. 368-383. doi:10.1007/978-3-319-23264-5_31.
• [22] Alviano M, Calimeri F, Dodaro C, Fuscà D, Leone N, Perri S, Ricca F, Veltri P, Zangari J. The ASP System DLV2. In: Balduccini M, Janhunen T (eds.), International Conference on Logic Programming and Nonmonotonic Reasoning, volume 10377 of Lecture Notes in Computer Science. Springer, 2017 pp. 215-221. doi:10.1007/978-3-319-61660-5_19.
• [23] Lierler Y, Maratea M. Cmodels-2: SAT-based Answer Set Solver Enhanced to Non-tight Programs. In: Lifschitz V, Niemelä I (eds.), International Conference on Logic Programming and Nonmonotonic Reasoning, volume 2923 of Lecture Notes in Computer Science. Springer, 2004 pp. 346-350. doi:10.1007/978-3-540-24609-1_32.
• [24] Bruynooghe M, Blockeel H, Bogaerts B, Cat BD, Pooter SD, Jansen J, Labarre A, Ramon J, Denecker M, Verwer S. Predicate logic as a modeling language: modeling and solving some machine learning and data mining problems with IDP3. TPLP, 2015. 15(6):783-817. doi:10.1017/S147106841400009X.
• [25] Alviano M, Dodaro C, Marques-Silva J, Ricca F. Optimum stable model search: algorithms and implementation. Journal of Logic and Computation, 2015. doi:10.1093/logcom/exv061.
• [26] Andres B, Kaufmann B, Matheis O, Schaub T. Unsatisfiability-based optimization in clasp. In: Dovier A, Costa VS (eds.), Technical Communications of the 28th International Conference on Logic Programming, ICLP 2012, volume 17 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012 pp. 211-221.
• [27] Narodytska N, Bacchus F. Maximum Satisfiability Using Core-Guided MaxSAT Resolution. In: Brodley CE, Stone P (eds.), AAAI Conference on Artificial Intelligence. AAAI Press, 2014 pp. 2717-2723. URL http://www.aaai.org/ocs/index.php/AAAI/AAAI14/paper/view/8513.
• [28] Alviano M, Dodaro C. Anytime answer set optimization via unsatisfiable core shrinking. Theory and Practice of Logic Programming, 2016. 16(5-6):533-551. doi:10.1017/S147106841600020X.
• [29] Alviano M, Dodaro C, Ricca F. A MaxSAT Algorithm Using Cardinality Constraints of Bounded Size. In: Yang Q, Wooldridge M (eds.), International Joint Conference on Artificial Intelligence. AAAI Press, 2015 pp. 2677-2683. URL http://ijcai.org/Abstract/15/379.
• [30] Alviano M, Dodaro C, Maratea M. Shared aggregate sets in answer set programming. TPLP, 2018. 18(3-4):301-318. doi:10.1017/S1471068418000133.
• [31] Alviano M, Amendola G, Dodaro C, Leone N, Maratea M, Ricca F. Evaluation of Disjunctive Programs in WASP. In: International Conference on Logic Programming and Nonmonotonic Reasoning, volume 11481 of Lecture Notes in Computer Science. Springer, 2019 pp. 241-255. doi:10.1007/978-3-030-20528-7\_18.
• [32] Gebser M, Maratea M, Ricca F. The Design of the Seventh Answer Set Programming Competition. In: Balduccini M, Janhunen T (eds.), International Conference on Logic Programming and Nonmonotonic Reasoning, volume 10377 of Lecture Notes in Computer Science. Springer, 2017 pp. 3-9. doi:10.1007/978-3-319-61660-5_1.
• [33] Gebser M, Kaufmann B, Schaub T. Conflict-driven answer set solving: From theory to practice. Artificial Intelligence, 2012. 187:52-89. doi:10.1016/j.artint.2012.04.001.
• [34] Alviano M, Dodaro C. Completion of Disjunctive Logic Programs. In: Kambhampati S (ed.), International Joint Conference on Artificial Intelligence. IJCAI/AAAI Press, 2016 pp. 886-892. URL http://www.ijcai.org/Abstract/16/130.
• [35] Bacchus F, Narodytska N. Cores in Core Based MaxSat Algorithms: An Analysis. In: Sinz C, Egly U (eds.), International Conference on Theory and Applications of Satisfiability Testing, volume 8561 of Lecture Notes in Computer Science. Springer, 2014 pp. 7-15. doi:10.1007/978-3-319-09284-3\_2.
• [36] Alviano M, Dodaro C, Leone N, Ricca F. Advances in WASP. In: Calimeri F, Ianni G, Truszczynski M (eds.), International Conference on Logic Programming and Nonmonotonic Reasoning, volume 9345 of Lecture Notes in Computer Science. Springer, 2015 pp. 40-54. doi:10.1007/978-3-319-23264-5_5.
• [37] Eén N, Sörensson N. An Extensible SAT-solver. In: Giunchiglia E, Tacchella A (eds.), International Conference on Theory and Applications of Satisfiability Testing, volume 2919 of Lecture Notes in Computer Science. Springer, 2003 pp. 502-518. doi:10.1007/978-3-540-24605-3_37.
• [38] Gebser M, Kaminski R, König A, Schaub T. Advances in gringo Series 3. In: Delgrande JP, Faber W (eds.), International Conference on Logic Programming and Nonmonotonic Reasoning, volume 6645 of Lecture Notes in Computer Science. Springer, 2011 pp. 345-351. doi:10.1007/978-3-642-20895-9_39.
• [39] Calimeri F, Fuscà D, Perri S, Zangari J. I-DLV: The new intelligent grounder of DLV. Intelligenza Artificiale, 2017. 11(1):5-20. doi:10.3233/IA-170104.
• [40] Calimeri F, Faber W, Gebser M, Ianni G, Kaminski R, Krennwallner T, Leone N, Ricca F, Schaub T. ASP-Core-2 Input Language Format, 2013. URL https://www.mat.unical.it/aspcomp2013/files/ASP-CORE-2.01c.pdf.
• [41] Buccafurri F, Leone N, Rullo P. Enhancing Disjunctive Datalog by Constraints. IEEE Transactions on Knowledge and Data Engineering, 2000. 12(5):845-860. doi:10.1109/69.877512.
• [42] Alviano M, Dodaro C. Unsatisfiable Core Shrinking for Anytime Answer Set Optimization. In: Sierra C (ed.), International Joint Conference on Artificial Intelligence. ijcai.org, 2017 pp. 4781-4785. doi:10.24963/ijcai.2017/666.
• [43] Fu Z, Malik S. On Solving the Partial MAX-SAT Problem. In: Biere A, Gomes CP (eds.), Proceedings of Theory and Applications of Satisfiability Testing, SAT 2006, volume 4121 of Lecture Notes in Computer Science. Springer, 2006 pp. 252-265.
• [44] Marques-Silva J, Manquinho VM. Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms. In: Büning HK, Zhao X (eds.), Proceedings of Theory and Applications of Satisfiability Testing, SAT 2008, volume 4996 of Lecture Notes in Computer Science. Springer, 2008 pp. 225-230.
• [45] Marques-Silva J, Planes J. Algorithms for Maximum Satisfiability using Unsatisfiable Cores. In: Sciuto D (ed.), Design, Automation and Test in Europe. ACM, 2008 pp. 408-413. doi:10.1109/DATE.2008.4484715.
• [46] Manquinho VM, Marques-Silva JP, Planes J. Algorithms for Weighted Boolean Optimization. In: Kullmann O (ed.), Proceedings of Theory and Applications of Satisfiability Testing, SAT 2009, volume 5584 of Lecture Notes in Computer Science. Springer, 2009 pp. 495-508. doi:10.1007/978-3-642-02777-2\_45.
• [47] Ansótegui C, Bonet ML, Levy J. Solving (Weighted) Partial MaxSAT through Satisfiability Testing. In: Kullmann O (ed.), Proceedings of Theory and Applications of Satisfiability Testing, SAT 2009, volume 5584 of Lecture Notes in Computer Science. Springer, 2009 pp. 427-440. doi:10.1007/978-3-642-02777-2\_39.
• [48] Morgado A, Dodaro C, Marques-Silva J. Core-Guided MaxSAT with Soft Cardinality Constraints. In: O’Sullivan B (ed.), International Conference on Principles and Practice of Constraint Programming, volume 8656 of Lecture Notes in Computer Science. Springer, 2014 pp. 564-573. doi:10.1007/978-3-319-10428-7_41.
• [49] Bomanson J, Gebser M, Janhunen T. Improving the Normalization of Weight Rules in Answer Set Programs. In: Fermé E, Leite J (eds.), European Conference on Logics in Artificial Intelligence, volume 8761 of Lecture Notes in Computer Science. Springer, 2014 pp. 166-180. doi:10.1007/978-3-319-11558-0\_12.
• [50] Bomanson J, Janhunen T. Normalizing Cardinality Rules Using Merging and Sorting Constructions. In: Cabalar P, Son TC (eds.), International Conference on Logic Programming and Nonmonotonic Reasoning, volume 8148 of Lecture Notes in Computer Science. Springer, 2013 pp. 187-199. doi:10.1007/978-3-642-40564-8_19.
• [51] Giunchiglia E, Lierler Y, Maratea M. Answer Set Programming Based on Propositional Satisfiability. Journal of Automated Reasoning, 2006. 36(4):345-377. doi:10.1007/s10817-006-9033-2.
• [52] Giunchiglia E, Leone N, Maratea M. On the relation among answer set solvers. Annals of Mathematics and Artificial Intelligence, 2008. 53(1-4):169-204. doi:10.1007/s10472-009-9113-1.
• [53] Ferraris P, Lifschitz V. Weight constraints as nested expressions. Theory and Practice of Logic Programming, 2005. 5(1-2):45-74. doi:10.1017/S1471068403001923.
• [54] Nieuwenhuis R, Oliveras A, Tinelli C. Solving SAT and SAT Modulo Theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM, 2006. 53(6):937-977. doi:10.1145/1217856.1217859.
• [55] Abío I, Stuckey PJ. Conflict Directed Lazy Decomposition. In: Milano M (ed.), International Conference on Principles and Practice of Constraint Programming, volume 7514 of Lecture Notes in Computer Science. Springer, 2012 pp. 70-85. doi:10.1007/978-3-642-33558-7\_8.
• [56] Bomanson J, Gebser M, Janhunen T, Kaufmann B, Schaub T. Answer Set Programming Modulo Acyclicity. In: Calimeri F, Ianni G, Truszczynski M (eds.), International Conference on Logic Programming and Nonmonotonic Reasoning, volume 9345 of Lecture Notes in Computer Science. Springer, 2015 pp.143-150. doi:10.1007/978-3-319-23264-5_13.
• [57] Cuteri B, Dodaro C, Ricca F, Schüller P. Constraints, lazy constraints, or propagators in ASP solving: An empirical analysis. Theory and Practice of Logic Programming, 2017. 17(5-6):780-799. doi:10.1017/S1471068417000254.
• [58] Saikko P, Berg J, Järvisalo M. LMHS: A SAT-IP Hybrid MaxSAT Solver. In: International Conference on Theory and Applications of Satisfiability Testing, volume 9710 of Lecture Notes in Computer Science. Springer, 2016 pp. 539-546. doi:10.1007/978-3-319-40970-2\_34.
• [59] Alviano M, Dodaro C, Järvisalo M, Maratea M, Previti A. Cautious reasoning in ASP via minimal models and unsatisfiable cores. TPLP, 2018. 18(3-4):319-336. doi:10.1017/S1471068418000145.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).