×

zbMATH — the first resource for mathematics

Design and results of the Fifth Answer Set Programming Competition. (English) Zbl 1344.68042
Summary: Answer Set Programming (ASP) is a well-established paradigm of declarative programming that has been developed in the field of logic programming and non-monotonic reasoning. Advances in ASP solving technology are customarily assessed in competition events, as it happens for other closely related problem solving areas such as Boolean Satisfiability, Satisfiability Modulo Theories, Quantified Boolean Formulas, Planning, etc. This paper reports about the fifth edition of the ASP Competition by covering all aspects of the event, ranging from the new design of the competition to an in-depth analysis of the results. The paper comprises also additional analyses that were conceived for measuring the progress of the state of the art, as well as for studying aspects orthogonal to solving technology, such as the effects of modeling. A detailed picture of the progress of the state of the art in ASP solving is drawn, and the ASP Competition is located in the spectrum of related events.

MSC:
68N17 Logic programming
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68-02 Research exposition (monographs, survey articles) pertaining to computer science
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alviano, M., The pyrunlim tool, (2014)
[2] Alviano, M.; Calimeri, F.; Charwat, G.; Dao-Tran, M.; Dodaro, C.; Ianni, G.; Krennwallner, T.; Kronegger, M.; Oetsch, J.; Pfandler, A.; Pührer, J.; Redl, C.; Ricca, F.; Schneider, P.; Schwengerer, M.; Spendier, L.; Wallner, J.; Xiao, G., The fourth answer set programming competition: preliminary report, (Cabalar, P.; Son, T., Proceedings of the Twelfth International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 2013, Lecture Notes in Computer Science, vol. 8148, (2013), Springer), 42-53 · Zbl 06214645
[3] Alviano, M.; Dodaro, C.; Faber, W.; Leone, N.; Ricca, F., WASP: a native ASP solver based on constraint learning, (Cabalar, P.; Son, T., Proceedings of the Twelfth International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 2013, Lecture Notes in Computer Science, vol. 8148, (2013), Springer), 54-66 · Zbl 06214646
[4] Alviano, M.; Dodaro, C.; Ricca, F., Preliminary report on WASP 2.0, (Konieczny, S.; Tompits, H., Proceedings of the Fifteenth International Workshop on Non-Monotonic Reasoning, NMR 2014, (2014), TU Vienna), 68-72
[5] Aschinger, M.; Drescher, C.; Friedrich, G.; Gottlob, G.; Jeavons, P.; Ryabokon, A.; Thorstensen, E., Optimization methods for the partner units problem, (Achterberg, T.; Beck, C., Proceedings of the Eighth International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, CPAIOR 2011, Lecture Notes in Computer Science., vol. 6697, (2011), Springer), 4-19 · Zbl 1302.90164
[6] Asparagus, Asparagus - a web-based benchmarking environment for answer set programming, (2009)
[7] (Bail, S.; Glimm, B.; Jiménez-Ruiz, E.; Matentzoglu, N.; Parsia, B.; Steigmiller, A., Proceedings of the Third International Workshop on OWL Reasoner Evaluation, ORE 2014, CEUR Workshop Proceedings, vol. 1207, (2013))
[8] Baral, C., Knowledge representation, reasoning and declarative problem solving, (2003), Cambridge University Press · Zbl 1056.68139
[9] Barrett, C.; Deters, M.; de Moura, L.; Oliveras, A.; Stump, A., 6 years of SMT-COMP, J. Autom. Reason., 50, 3, 243-277, (2013)
[10] Ben-Eliyahu, R.; Dechter, R., Propositional semantics for disjunctive logic programs, Ann. Math. Artif. Intell., 12, 1-2, 53-87, (1994) · Zbl 0858.68012
[11] Beyer, D., Status report on software verification - (competition summary SV-COMP 2014), (Ábrahám, E.; Havelund, K., Proceedings of the Twentieth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014, Lecture Notes in Computer Science, vol. 8413, (2014), Springer), 373-388
[12] Bomanson, J.; Janhunen, T., Normalizing cardinality rules using merging and sorting constructions, (Cabalar, P.; Son, T., Proceedings of the Twelfth International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 2013, Lecture Notes in Computer Science, vol. 8148, (2013), Springer), 187-199 · Zbl 1405.68044
[13] Brewka, G.; Eiter, T.; Truszczyński, M., Answer set programming at a glance, Commun. ACM, 54, 12, 92-103, (2011)
[14] Brewka, G.; Niemelä, I.; Schaub, T.; Truszczyński, M., Workshop on nonmonotonic reasoning, answer set programming and constraints, (2002)
[15] Calimeri, F.; Faber, W.; Gebser, M.; Ianni, G.; Kaminski, R.; Krennwallner, T.; Leone, N.; Ricca, F.; Schaub, T., (2013), ASP-Core-2 - input language format
[16] Calimeri, F.; Gebser, M.; Maratea, M.; Ricca, F.; Leuschel, M.; Schrijvers, T., The design of the fifth answer set programming competition, Proceedings of the Thirtieth International Conference on Logic Programming, ICLP 2014, Theory Pract. Log. Program., 14, 4-5, (2014), Online Supplement
[17] Calimeri, F.; Gebser, M.; Maratea, M.; Ricca, F., The fifth answer set programming competition (ASPCOMP 2014), (2014)
[18] Calimeri, F.; Ianni, G.; Krennwallner, T.; Ricca, F., The answer set programming competition, AI Mag., 33, 4, 114-118, (2012)
[19] Calimeri, F.; Ianni, G.; Ricca, F., The third open answer set programming competition, Theory Pract. Log. Program., 14, 1, 117-135, (2014)
[20] CASC, The seventh IJCAR ATP system competition (CASC-J7 2014), (2014)
[21] CoCo, (2014), The third confluence competition (CoCo 2014)
[22] Coles, A.; Coles, A.; García Olaya, A.; Jiménez Celorrio, S.; Linares López, C.; Sanner, S.; Yoon, S., A survey of the seventh international planning competition, AI Mag., 33, 1, 83-88, (2012)
[23] Crawford, J.; Baker, A., Experimental results on the application of satisfiability algorithms to scheduling problems, (Proceedings of the Twelfth National Conference on Artificial Intelligence, AAAI 1994, (1994), AAAI Press), 1092-1097
[24] CSC, The fourth international CSP solver competition (CSC 2009), (2009)
[25] CSSC, The configurable SAT solver challenge (CSSC 2014), (2014)
[26] Dal Palù, A.; Dovier, A.; Pontelli, E.; Rossi, G., GASP: answer set programming with lazy grounding, Fundam. Inform., 96, 3, 297-322, (2009) · Zbl 1207.68118
[27] Denecker, M.; Vennekens, J.; Bond, S.; Gebser, M.; Truszczyński, M., The second answer set programming competition, (Erdem, E.; Lin, F.; Schaub, T., Proceedings of the Tenth International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 2009, Lecture Notes in Computer Science, vol. 5753, (2009), Springer), 637-654
[28] Dovier, A.; Formisano, A.; Pontelli, E., An experimental comparison of constraint logic programming and answer set programming, (Proceedings of the Twenty-Second National Conference on Artificial Intelligence, AAAI 2007, (2007), AAAI Press), 1622-1625
[29] East, D.; Truszczyński, M., Aspps - an implementation of answer-set programming with propositional schemata, (Eiter, T.; Faber, W.; Truszczyński, M., Proceedings of the Sixth International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 2001, Lecture Notes in Computer Science, vol. 2173, (2001), Springer), 402-405 · Zbl 1007.68699
[30] Eén, N.; Sörensson, N., An extensible SAT-solver, (Giunchiglia, E.; Tacchella, A., Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing, SAT 2003, Lecture Notes in Computer Science, vol. 2919, (2003), Springer), 502-518 · Zbl 1204.68191
[31] Eiter, T.; Faber, W.; Leone, N.; Pfeifer, G., Declarative problem-solving using the DLV system, (Minker, J., Logic-Based Artificial Intelligence, International Series in Engineering and Computer Science, vol. 597, (2000), Springer), 79-103 · Zbl 0979.68091
[32] Eiter, T.; Gottlob, G., On the computational cost of disjunctive logic programming: propositional case, Ann. Math. Artif. Intell., 15, 3-4, 289-323, (1995) · Zbl 0858.68016
[33] Eiter, T.; Gottlob, G.; Mannila, H., Disjunctive Datalog, ACM Trans. Database Syst., 22, 3, 364-418, (1997)
[34] Eiter, T.; Ianni, G.; Krennwallner, T., Answer set programming: a primer, (Tessaris, S.; Franconi, E.; Eiter, T.; Gutierrez, C.; Handschuh, S.; Rousset, M.; Schmidt, R., Proceedings of the Fifth International Reasoning Web Summer School, RW 2009, Lecture Notes in Computer Science, vol. 5689, (2009), Springer), 40-110 · Zbl 1254.68248
[35] Erdem, E.; Lifschitz, V., Tight logic programs, Theory Pract. Log. Program., 3, 4-5, 499-518, (2003) · Zbl 1079.68014
[36] Faber, W.; Leone, N.; Perri, S., The intelligent grounder of DLV, (Erdem, E.; Lee, J.; Lierler, Y.; Pearce, D., Correct Reasoning: Essays on Logic-Based AI in Honour of Vladimir Lifschitz, Lecture Notes in Computer Science, vol. 7265, (2012), Springer), 247-264 · Zbl 1357.68032
[37] Faber, W.; Leone, N.; Pfeifer, G., Recursive aggregates in disjunctive logic programs: semantics and complexity, (Alferes, J.; Leite, J., Proceedings of the Ninth European Conference on Logics in Artificial Intelligence, JELIA 2004, Lecture Notes in Computer Science, vol. 3229, (2004), Springer), 200-212 · Zbl 1111.68380
[38] Faber, W.; Leone, N.; Pfeifer, G., Semantics and complexity of recursive aggregates in answer set programming, Artif. Intell., 175, 1, 278-298, (2011) · Zbl 1216.68263
[39] Faber, W.; Pfeifer, G.; Leone, N.; Dell’Armi, T.; Ielpa, G., Design and implementation of aggregate functions in the DLV system, Theory Pract. Log. Program., 8, 5-6, 545-580, (2008) · Zbl 1156.68010
[40] Fages, F., Consistency of Clark’s completion and the existence of stable models, J. Methods Logic Comput. Sci., 1, 51-60, (1994)
[41] Gebser, M.; Janhunen, T.; Rintanen, J., Answer set programming as SAT modulo acyclicity, (Schaub, T.; Friedrich, G.; O’Sullivan, B., Proceedings of the Twenty-First European Conference on Artificial Intelligence, ECAI 2014, Frontiers in Artificial Intelligence and Applications, vol. 263, (2014), IOS Press), 351-356 · Zbl 1366.68017
[42] Gebser, M.; Kaminski, R.; Kaufmann, B.; Schaub, T.; Leuschel, M.; Schrijvers, T., Clingo = ASP + control: preliminary report, Proceedings of the Thirtieth International Conference on Logic Programming, ICLP 2014, Theory Pract. Log. Program., 14, 4-5, (2014), Online Supplement
[43] Gebser, M.; Kaufmann, B.; Schaub, T., Conflict-driven answer set solving: from theory to practice, Artif. Intell., 187-188, 52-89, (2012) · Zbl 1251.68060
[44] Gebser, M.; Kaufmann, B.; Schaub, T., Multi-threaded ASP solving with clasp, Theory Pract. Log. Program., 12, 4-5, 525-545, (2012) · Zbl 1260.68061
[45] Gebser, M.; Kaufmann, B.; Schaub, T., Advanced conflict-driven disjunctive answer set solving, (Rossi, F., Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI 2013, (2013), IJCAI/AAAI Press), 912-918
[46] Gebser, M.; Liu, L.; Namasivayam, G.; Neumann, A.; Schaub, T.; Truszczyński, M., The first answer set programming system competition, (Baral, C.; Brewka, G.; Schlipf, J., Proceedings of the Ninth International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 2007, Lecture Notes in Computer Science, vol. 4483, (2007), Springer), 3-17
[47] Gelfond, M.; Leone, N., Logic programming and knowledge representation - the A-prolog perspective, Artif. Intell., 138, 1-2, 3-38, (2002) · Zbl 0995.68022
[48] Gelfond, M.; Lifschitz, V., The stable model semantics for logic programming, (Kowalski, R.; Bowen, K., Proceedings of the Fifth International Conference and Symposium of Logic Programming, ICLP 1988, (1988), MIT Press), 1070-1080
[49] Gelfond, M.; Lifschitz, V., Classical negation in logic programs and disjunctive databases, New Gener. Comput., 9, 365-385, (1991) · Zbl 0735.68012
[50] Gerevini, A.; Haslum, P.; Long, D.; Saetti, A.; Dimopoulos, Y., Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners, Artif. Intell., 173, 5-6, 619-668, (2009) · Zbl 1191.68634
[51] Ghallab, M.; Howe, A.; Knoblock, C.; McDermott, D.; Ram, A.; Veloso, M.; Weld, D.; Wilkins, D., PDDL - the planning domain definition language, (1998)
[52] Giunchiglia, E.; Lierler, Y.; Maratea, M., Answer set programming based on propositional satisfiability, J. Autom. Reason., 36, 4, 345-377, (2006) · Zbl 1107.68029
[53] Hoos, H.; Kaufmann, B.; Schaub, T.; Schneider, M., Robust benchmark set selection for Boolean constraint solvers, (Nicosia, G.; Pardalos, P., Proceedings of the Seventh International Conference on Learning and Intelligent Optimization, LION 2013, Lecture Notes in Computer Science, vol. 7997, (2013), Springer), 138-152
[54] HWMCC, The seventh hardware model checking competition (HWMCC 2014), (2014)
[55] IPC, The eighth international planning competition (IPC 2014), (2014)
[56] Janhunen, T.; Niemelä, I., Compact translations of non-disjunctive answer set programs to propositional clauses, (Balduccini, M.; Son, T., Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning: Essays Dedicated to Michael Gelfond on the Occasion of His 65th Birthday, Lecture Notes in Computer Science, vol. 6565, (2011), Springer), 111-130 · Zbl 1326.68058
[57] Janhunen, T.; Niemelä, I.; Seipel, D.; Simons, P.; You, J., Unfolding partiality and disjunctions in stable model semantics, ACM Trans. Comput. Log., 7, 1, 1-37, (2006) · Zbl 1367.68035
[58] Järvisalo, M.; Le Berre, D.; Roussel, O.; Simon, L., The international SAT solver competitions, AI Mag., 33, 1, 89-92, (2012)
[59] Krennwallner, T., Answer set solver output, (2013)
[60] Leone, N.; Pfeifer, G.; Faber, W.; Eiter, T.; Gottlob, G.; Perri, S.; Scarcello, F., The DLV system for knowledge representation and reasoning, ACM Trans. Comput. Log., 7, 3, 499-562, (2006) · Zbl 1367.68308
[61] Lifschitz, V., Answer set programming and plan generation, Artif. Intell., 138, 1-2, 39-54, (2002) · Zbl 0995.68020
[62] Lin, F.; Zhao, Y., ASSAT: computing answer sets of a logic program by SAT solvers, Artif. Intell., 157, 1-2, 115-137, (2004) · Zbl 1085.68544
[63] Liu, G.; Janhunen, T.; Niemelä, I., Answer set programming via mixed integer programming, (Brewka, G.; Eiter, T.; McIlraith, S., Proceedings of the Thirteenth International Conference on Principles of Knowledge Representation and Reasoning, KR 2012, (2012), AAAI Press), 32-42
[64] Mancini, T.; Micaletto, D.; Patrizi, F.; Cadoli, M., Evaluating ASP and commercial solvers on the csplib, Constraints, 13, 4, 407-436, (2008) · Zbl 1179.90287
[65] Marek, V.; Truszczyński, M., Stable models and an alternative logic programming paradigm, (Apt, K.; Marek, V.; Truszczyński, M.; Warren, D., The Logic Programming Paradigm: A 25-Year Perspective, (1999), Springer), 375-398 · Zbl 0979.68524
[66] Mariën, M.; Wittocx, J.; Denecker, M.; Bruynooghe, M., SAT(ID): satisfiability of propositional logic extended with inductive definitions, (Kleine Büning, H.; Zhao, X., Proceedings of the Eleventh International Conference on Theory and Applications of Satisfiability Testing, SAT 2008, Lecture Notes in Computer Science, vol. 4996, (2008), Springer), 211-224 · Zbl 1138.68547
[67] Max-SAT, The ninth MAX-SAT evaluation (MAX-SAT 2014), (2014)
[68] MiniZinc, The minizinc challenge 2014, (2014)
[69] MISC, The mancoosi international solver competition (MISC 2012), (2012)
[70] Nguyen, M.; Janhunen, T.; Niemelä, I., Translating answer-set programs into bit-vector logic, (Tompits, H.; Abreu, S.; Oetsch, J.; Pührer, J.; Seipel, D.; Umeda, M.; Wolf, A., Proceedings of the Nineteenth International Conference on Applications of Declarative Programming and Knowledge Management (INAP 2011) and the Twenty-Fifth Workshop on Logic Programming (WLP 2011), Lecture Notes in Computer Science, vol. 7773, (2011), Springer), 105-116
[71] Niemelä, I., Logic programming with stable model semantics as a constraint programming paradigm, Ann. Math. Artif. Intell., 25, 3-4, 241-273, (1999) · Zbl 0940.68018
[72] Nogueira, M.; Balduccini, M.; Gelfond, M.; Watson, R.; Barry, M., An A-prolog decision support system for the space shuttle, (Ramakrishnan, I., Proceedings of the Third International Symposium on Practical Aspects of Declarative Languages, PADL 2001, Lecture Notes in Computer Science, vol. 1990, (2001), Springer), 169-183
[73] ORE, The OWL reasoner evaluation (ORE 2014), (2014)
[74] PB, The pseudo-Boolean competition 2012 (PB 2012), (2012)
[75] QBF, The QBF gallery 2014, (2014)
[76] QBF-LIB, The quantified Boolean formulas satisfiability library, (2014)
[77] Reiter, R., The frame problem in the situation calculus: a simple solution (sometimes) and a completeness result for goal regression, (Lifschitz, V., Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, (1991), Academic Press), 359-380 · Zbl 0755.68124
[78] 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 Pract. Log. Program., 12, 3, 361-381, (2012) · Zbl 1250.90050
[79] SAT, The international SAT competitions (SAT-COMP 2014), (2014)
[80] SAT-LIB, The satisfiability library, (2014)
[81] Marques-Silva, J.; Sakallah, K., GRASP: a search algorithm for propositional satisfiability, IEEE Trans. Comput., 48, 5, 506-521, (1999) · Zbl 1392.68388
[82] Simons, P.; Niemelä, I.; Soininen, T., Extending and implementing the stable model semantics, Artif. Intell., 138, 1-2, 181-234, (2002) · Zbl 0995.68021
[83] SMT, The satisfiability modulo theories solver competition (SMT-COMP 2014), (2014)
[84] SMT-LIB, The satisfiability modulo theories library, (2014)
[85] Stuckey, P.; Feydy, T.; Schutt, A.; Tack, G.; Fischer, J., The minizinc challenge 2008-2013, AI Mag., 35, 2, 55-60, (2014)
[86] Sutcliffe, G., The CADE-24 automated theorem proving system competition - CASC-24, AI Commun., 27, 4, 405-416, (2014)
[87] SV-COMP, The third international competition on software verification (SV-COMP 2014), (2014)
[88] SyGuS-COMP, The syntax-guided synthesis competition (sygus-COMP 2014), (2014)
[89] SYNTCOMP, The synthesis competition (SYNTCOMP 2014), (2014)
[90] TermCOMP, The termination competition (termcomp 2014), (2014)
[91] Tiihonen, J.; Soininen, T.; Niemelä, I.; Sulonen, R., A practical tool for mass-customising configurable products, (Folkeson, A.; Gralen, K.; Norell, M.; Sellgren, U., Proceedings of the Fourteenth International Conference on Engineering Design, ICED 2003, (2003))
[92] Zhang, L.; Madigan, C.; Moskewicz, M.; Malik, S., Efficient conflict driven learning in a Boolean satisfiability solver, (Proceedings of the International Conference on Computer-Aided Design, ICCAD 2001, (2001), ACM Press), 279-285
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.