×

zbMATH — the first resource for mathematics

Anytime answer set optimization via unsatisfiable core shrinking. (English) Zbl 1379.68033
Summary: Unsatisfiable core analysis can boost the computation of optimum stable models for logic programs with weak constraints. However, current solvers employing unsatisfiable core analysis either run to completion, or provide no suboptimal stable models but the one resulting from the preliminary disjoint cores analysis. This drawback is circumvented here by introducing a progression based shrinking of the analyzed unsatisfiable cores. In fact, suboptimal stable models are possibly found while shrinking unsatisfiable cores, hence resulting into an anytime algorithm. Moreover, as confirmed empirically, unsatisfiable core analysis also benefits from the shrinking process in terms of solved instances.

MSC:
68N17 Logic programming
Software:
clasp; Cmodels; DLV; maxino; WASP
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alviano, M.; Dodaro, C.; Faber, W.; Leone, N.; Ricca, F.; Cabalar, P.; Son, T. C., Logic Programming and Nonmonotonic Reasoning, 12th International Conference, LPNMR 2013, Corunna, Spain, September 15-19, 2013, WASP: A native ASP solver based on constraint learning, 54-66, (2013), Springer · Zbl 06214646
[2] Alviano, M.; Dodaro, C.; Leone, N.; Ricca, F.; Calimeri, F.; Ianni, G.; Truszczynski, M., Proceedings of Logic Programming and Nonmonotonic Reasoning - 13th International Conference, LPNMR 2015, Advances in WASP, 40-54, (2015), Springer
[3] Alviano, M.; Dodaro, C.; Marques-Silva, J.; Ricca, F., pp., (2015)
[4] Alviano, M.; Dodaro, C.; Ricca, F., Anytime computation of cautious consequences in answer set programming., Theory and Practice of Logic Programming, 14, 4-5, 755-770, (2014) · Zbl 1307.68012
[5] Alviano, M.; Dodaro, C.; Ricca, F.; Yang, Q.; Wooldridge, M., Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, A MaxSAT Algorithm Using Cardinality Constraints of Bounded Size, 2677-2683, (2015), AAAI Press
[6] Alviano, M.; Faber, W.; Cabalar, P.; Son, T. C., Logic Programming and Nonmonotonic Reasoning, 12th International Conference, LPNMR 2013, Corunna, Spain, September 15-19, 2013, The complexity boundary of answer set programming with generalized atoms under the FLP semantics, 67-72, (2013), Springer · Zbl 1405.68036
[7] Alviano, M.; Faber, W.; Gebser, M., Rewriting recursive aggregates in answer set programming: back to monotonicity., Theory and Practice of Logic Programming, 15, 4-5, 559-573, (2015) · Zbl 1379.68034
[8] Alviano, M.; Faber, W.; Leone, N.; Perri, S.; Pfeifer, G.; Terracina, G.; de Moor, O.; Gottlob, G.; Furche, T.; Sellers, A. J., Datalog Reloaded - First International Workshop, Datalog 2010, Oxford, UK, March 16-19, 2010, The disjunctive datalog system DLV, 282-301, (2010), Springer
[9] Alviano, M.; Faber, W.; Strass, H.; Schuurmans, D.; Wellman, M. P., Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, February 12-17, 2016, Phoenix, Arizona, USA., Boolean functions with ordered domains in answer set programming, 879-885, (2016), AAAI Press
[10] Alviano, M.; Leone, N., Complexity and compilation of gz-aggregates in answer set programming., Theory and Practice of Logic Programming, 15, 4-5, 574-587, (2015) · Zbl 1379.68035
[11] Andres, B.; Kaufmann, B.; Matheis, O.; Schaub, T.; Dovier, A.; Costa, V. S., pp., (2012)
[12] Ansótegui, C.; Bonet, M. L.; Levy, J.; Kullmann, O., Proceedings of Theory and Applications of Satisfiability Testing, SAT 2009, Solving (weighted) partial maxsat through satisfiability testing, pp., (2009), Springer · Zbl 1165.68014
[13] Argelich, J.; Lynce, I.; Silva, J. P. M.; Boutilier, C., pp., (2009)
[14] Bartholomew, M.; Lee, J.; Meng, Y., Logical Formalizations of Commonsense Reasoning, Papers from the 2011 AAAI Spring Symposium, Technical Report SS-11-06, Stanford, California, USA, March 21-23, 2011, First-order semantics of aggregates in answer set programming via modified circumscription, pp., (2011), AAAI
[15] Bliem, B.; Kaufmann, B.; Schaub, T.; Woltran, S., Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, ASP for Anytime Dynamic Programming on Tree Decompositions, pp., (2016), AAAI Press
[16] Brewka, G.; Eiter, T.; Truszczynski, M., Answer set programming at a glance., Commun. ACM, 54, 12, 92-103, (2011)
[17] Buccafurri, F.; Leone, N.; Rullo, P., Enhancing disjunctive Datalog by constraints., IEEE Trans. Knowl. Data Eng., 12, 5, 845-860, (2000)
[18] Cha, B.; Iwama, K.; Kambayashi, Y.; Miyazaki, S., Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, Local search algorithms for partial MAXSAT, 263-268, (1997), AAAI Press / The MIT Press
[19] Dodaro, C.; Alviano, M.; Faber, W.; Leone, N.; Ricca, F.; Sirianni, M.; Fioravanti, F., pp., (2011)
[20] Eiter, T.; Ianni, G.; Krennwallner, T.; Tessaris, S.; Franconi, E.; Eiter, T.; Gutierrez, C.; Handschuh, S.; Rousset, M.; Schmidt, R. A., Reasoning Web. Semantic Technologies for Information Systems, 5th International Summer School 2009, Tutorial Lectures, Answer Set Programming: A Primer, 40-110, (2009), Springer
[21] Faber, W.; Pfeifer, G.; Leone, N., Semantics and complexity of recursive aggregates in answer set programming., Artif. Intell., 175, 1, 278-298, (2011) · Zbl 1216.68263
[22] Ferraris, P., Logic programs with propositional connectives and aggregates, ACM Trans. Comput. Log., 12, 4, pp., (2011) · Zbl 1351.68053
[23] Fu, Z.; Malik, S.; Biere, A.; Gomes, C. P., Proceedings of Theory and Applications of Satisfiability Testing, SAT 2006, On Solving the Partial MAX-SAT Problem, 252-265, (2006), Springer · Zbl 1114.68003
[24] Gebser, M.; Kaminski, R.; Kaufmann, B.; Romero, J.; Schaub, T.; Calimeri, F.; Ianni, G.; Truszczynski, M., LPNMR 2015, Progress in clasp Series 3, 368-383, (2015), Springer · Zbl 06504246
[25] Gebser, M.; Kaminski, R.; Kaufmann, B.; Schaub, T.; Gallagher, J. P.; Gelfond, M., pp., (2011)
[26] Gebser, M.; Kaminski, R.; Schaub, T., Complex optimization in answer set programming., Theory and Practice of Logic Programming, 11, 4-5, 821-839, (2011) · Zbl 1222.68059
[27] Gebser, M.; Maratea, M.; Ricca, F.; Calimeri, F.; Ianni, G.; Truszczynski, M., Proceedings of Logic Programming and Nonmonotonic Reasoning - 13th International Conference, LPNMR 2015, The Design of the Sixth Answer Set Programming Competition, 531-544, (2015), Springer · Zbl 1418.68028
[28] Gelfond, M.; Lifschitz, V., Classical negation in logic programs and disjunctive databases., New Generation Comput., 9, 3/4, 365-386, (1991) · Zbl 0735.68012
[29] Gelfond, M.; Zhang, Y., Vicious circle principle and logic programs with aggregates., Theory and Practice of Logic Programming, 14, 4-5, 587-601, (2014) · Zbl 1309.68032
[30] Giunchiglia, E.; Lierler, Y.; Maratea, M., Answer set programming based on propositional satisfiability., J. Autom. Reasoning, 36, 4, 345-377, (2006) · Zbl 1107.68029
[31] Lierler, Y.; Maratea, M.; Lifschitz, V.; Niemelä, I., Logic Programming and Nonmonotonic Reasoning, 7th International Conference, LPNMR 2004, Fort Lauderdale, FL, USA, January 6-8, 2004, Proceedings, Cmodels-2: Sat-based answer set solver enhanced to non-tight programs, 346-350, (2004), Springer · Zbl 1122.68377
[32] Lifschitz, V.; Fox, D.; Gomes, C. P., Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, AAAI 2008, What Is Answer Set Programming?, 1594-1597, (2008), AAAI Press
[33] Liu, G.; Janhunen, T.; Niemelä, I.; Brewka, G.; Eiter, T.; McIlraith, S. A., Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth International Conference, KR 2012, Answer Set Programming via Mixed Integer Programming, pp., (2012), AAAI Press
[34] Liu, L.; Pontelli, E.; Son, T. C.; Truszczynski, M., Logic programs with abstract constraint atoms: the role of computations., Artif. Intell., 174, 3-4, 295-315, (2010) · Zbl 1207.68119
[35] Manquinho, V. M.; Silva, J. P. M.; Planes, J.; Kullmann, O., Proceedings of Theory and Applications of Satisfiability Testing, SAT 2009, Algorithms for weighted boolean optimization, 495-508, (2009), Springer · Zbl 1165.68014
[36] Marek, V. W.; Niemelä, I.; Truszczynski, M., Logic programs with monotone abstract constraint atoms., Theory and Practice of Logic Programming, 8, 2, 167-199, (2008) · Zbl 1142.68018
[37] Marques-Silva, J.; Manquinho, V. M.; Büning, H. K.; Zhao, X., Proceedings of Theory and Applications of Satisfiability Testing, SAT 2008, Towards more effective unsatisfiability-based maximum satisfiability algorithms, 225-230, (2008), Springer · Zbl 1136.68007
[38] Marques-Silva, J.; Planes, J., Design, Automation and Test in Europe, DATE 2008, Algorithms for Maximum Satisfiability using Unsatisfiable Cores, 408-413, (2008), IEEE, Munich, Germany
[39] Morgado, A.; Dodaro, C.; Marques-Silva, J., Proceedings of Principles and Practice of Constraint Programming - 20th International Conference, CP 2014, Core-Guided MaxSAT with Soft Cardinality Constraints, 564-573, (2014), Springer, Lyon, France
[40] Nadel, A.; Bloem, R.; Sharygina, N., Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Boosting minimal unsatisfiable core extraction, 221-229, (2010), IEEE
[41] Nadel, A.; Ryvchin, V.; Strichman, O., Accelerated deletion-based extraction of minimal unsatisfiable cores, JSAT, 9, 27-51, (2014)
[42] Narodytska, N.; Bacchus, F., Twenty-Eighth AAAI Conference on Artificial Intelligence, Maximum Satisfiability Using Core-Guided MaxSAT Resolution, 2717-2723, (2014), AAAI Press, Québec City, Canada
[43] Niemelä, I., Logic programs with stable model semantics as a constraint programming paradigm., Ann. Math. Artif. Intell., 25, 3-4, 241-273, (1999) · Zbl 0940.68018
[44] Simons, P.; Niemelä, I.; Soininen, T., Extending and implementing the stable model semantics., Artif. Intell., 138, 1-2, 181-234, (2002) · Zbl 0995.68021
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.