Abstract
This paper introduces WASP, an ASP solver handling disjunctive logic programs under the stable model semantics. WASP implements techniques originally introduced for SAT solving that have been extended to cope with ASP programs. Among them are restarts, conflict-driven constraint learning and backjumping. Moreover, WASP combines these SAT-based techniques with optimization methods that have been specifically designed for ASP computation, such as source pointers enhancing unfounded-sets computation, forward and backward inference operators based on atom support, and techniques for stable model checking. Concerning the branching heuristics, WASP adopts the BerkMin criterion hybridized with look-ahead techniques. The paper also reports on the results of experiments, in which WASP has been run on the system track of the third ASP Competition.
This research has been partly supported by project PIA KnowRex POR FESR 2007- 2013 BURC n. 49 s.s. n. 1 16/12/2010, by MIUR project FRAME PON01_02477/4, and by the European Commission, European Social Fund and Regione Calabria.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Stable Model Semantic
- Disjunctive Logic Program
- Implication Graph
- Backtrack Search Algorithm
- Propositional Program
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Gelfond, M., Lifschitz, V.: Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing 9, 365–385 (1991)
Eiter, T., Gottlob, G., Mannila, H.: Disjunctive Datalog. ACM Transactions on Database Systems 22, 364–418 (1997)
Alviano, M., Faber, W., Leone, N., Perri, S., Pfeifer, G., Terracina, G.: The disjunctive datalog system DLV. In: de Moor, O., Gottlob, G., Furche, T., Sellers, A. (eds.) Datalog 2010. LNCS, vol. 6702, pp. 282–301. Springer, Heidelberg (2011)
Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Conflict-driven answer set solving. In: Twentieth International Joint Conference on Artificial Intelligence, IJCAI 2007, pp. 386–392. Morgan Kaufmann Publishers (2007)
Lierler, Y., Maratea, M.: Cmodels-2: SAT-based Answer Set Solver Enhanced to Non-tight Programs. In: Lifschitz, V., Niemelä, I. (eds.) LPNMR 2004. LNCS (LNAI), vol. 2923, pp. 346–350. Springer, Heidelberg (2003)
Grasso, G., Iiritano, S., Leone, N., Ricca, F.: Some DLV applications for knowledge management. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol. 5753, pp. 591–597. Springer, Heidelberg (2009)
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 12, 361–381 (2012)
Manna, M., Oro, E., Ruffolo, M., Alviano, M., Leone, N.: The HiLeX system for semantic information extraction. In: Hameurlain, A., Küng, J., Wagner, R. (eds.) TLDKS V. LNCS, vol. 7100, pp. 91–125. Springer, Heidelberg (2012)
Ricca, F., Alviano, M., Dimasi, A., Grasso, G., Ielpa, S.M., Iiritano, S., Manna, M., Leone, N.: A Logic-Based System for e-Tourism. Fundamenta Informaticae 105, 35–55 (2010)
Calimeri, F., et al.: The Third Answer Set Programming Competition: Preliminary Report of the System Competition Track. In: Delgrande, J.P., Faber, W. (eds.) LPNMR 2011. LNCS, vol. 6645, pp. 388–403. Springer, Heidelberg (2011)
Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Communications of the ACM 5, 394–397 (1962)
Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient Conflict Driven Learning in Boolean Satisfiability Solver. In: Proceedings of ICCAD 2001, pp. 279–285 (2001)
Gaschnig, J.: Performance measurement and analysis of certain search algorithms. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA (1979) TR CMU-CS-79-124
Gomes, C.P., Selman, B., Kautz, H.A.: Boosting Combinatorial Search Through Randomization. In: Proceedings of AAAI/IAAI 1998, pp. 431–437. AAAI Press (1998)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of DAC 2001, pp. 530–535. ACM (2001)
Goldberg, E., Novikov, Y.: BerkMin: A Fast and Robust Sat-Solver. In: Design, Automation and Test in Europe Conference and Exposition, DATE 2002, Paris, France, pp. 142–149. IEEE Computer Society (2002)
Faber, W., Leone, N., Pfeifer, G.: Pushing Goal Derivation in DLP Computations. In: Gelfond, M., Leone, N., Pfeifer, G. (eds.) LPNMR 1999. LNCS (LNAI), vol. 1730, pp. 177–191. Springer, Heidelberg (1999)
Simons, P., Niemelä, I., Soininen, T.: Extending and Implementing the Stable Model Semantics. Artificial Intelligence 138, 181–234 (2002)
Koch, C., Leone, N., Pfeifer, G.: Enhancing Disjunctive Logic Programming Systems by SAT Checkers. Artificial Intelligence 15, 177–212 (2003)
Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Ben-Eliyahu, R., Dechter, R.: Propositional Semantics for Disjunctive Logic Programs. Annals of Mathematics and Artificial Intelligence 12, 53–87 (1994)
Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of las vegas algorithms. Inf. Process. Lett. 47, 173–180 (1993)
Goldberg, E., Novikov, Y.: Berkmin: A fast and robust sat-solver. Discrete Appl. Math. 155, 1549–1561 (2007)
Gebser, M., Schaub, T.: Tableau calculi for answer set programming. In: Etalle, S., Truszczyński, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 11–25. Springer, Heidelberg (2006)
Ward, J., Schlipf, J.: Answer Set Programming with Clause Learning. In: Lifschitz, V., Niemelä, I. (eds.) LPNMR 2004. LNCS (LNAI), vol. 2923, pp. 302–313. Springer, Heidelberg (2003)
Ricca, F., Faber, W., Leone, N.: A Backjumping Technique for Disjunctive Logic Programming. AI Communications 19, 155–172 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alviano, M., Dodaro, C., Faber, W., Leone, N., Ricca, F. (2013). WASP: A Native ASP Solver Based on Constraint Learning. In: Cabalar, P., Son, T.C. (eds) Logic Programming and Nonmonotonic Reasoning. LPNMR 2013. Lecture Notes in Computer Science(), vol 8148. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40564-8_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-40564-8_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40563-1
Online ISBN: 978-3-642-40564-8
eBook Packages: Computer ScienceComputer Science (R0)