Skip to main content
SpringerLink
Log in

WASP: A Native ASP Solver Based on Constraint Learning

  • Conference paper
Logic Programming and Nonmonotonic Reasoning (LPNMR 2013)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 8148))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Gelfond, M., Lifschitz, V.: Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing 9, 365–385 (1991)

    Article  Google Scholar 

  2. Eiter, T., Gottlob, G., Mannila, H.: Disjunctive Datalog. ACM Transactions on Database Systems 22, 364–418 (1997)

    Article  Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. 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)

    Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. 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)

    Chapter  Google Scholar 

  7. 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)

    Article  MathSciNet  MATH  Google Scholar 

  8. 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)

    Chapter  Google Scholar 

  9. 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)

    MathSciNet  Google Scholar 

  10. 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)

    Chapter  Google Scholar 

  11. Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Communications of the ACM 5, 394–397 (1962)

    Article  MathSciNet  MATH  Google Scholar 

  12. 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)

    Google Scholar 

  13. Gaschnig, J.: Performance measurement and analysis of certain search algorithms. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA (1979) TR CMU-CS-79-124

    Google Scholar 

  14. 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)

    Google Scholar 

  15. 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)

    Google Scholar 

  16. 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)

    Google Scholar 

  17. 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)

    Chapter  Google Scholar 

  18. Simons, P., Niemelä, I., Soininen, T.: Extending and Implementing the Stable Model Semantics. Artificial Intelligence 138, 181–234 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  19. Koch, C., Leone, N., Pfeifer, G.: Enhancing Disjunctive Logic Programming Systems by SAT Checkers. Artificial Intelligence 15, 177–212 (2003)

    Article  MathSciNet  Google Scholar 

  20. 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)

    Chapter  Google Scholar 

  21. Ben-Eliyahu, R., Dechter, R.: Propositional Semantics for Disjunctive Logic Programs. Annals of Mathematics and Artificial Intelligence 12, 53–87 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  22. Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of las vegas algorithms. Inf. Process. Lett. 47, 173–180 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  23. Goldberg, E., Novikov, Y.: Berkmin: A fast and robust sat-solver. Discrete Appl. Math. 155, 1549–1561 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  24. 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)

    Chapter  Google Scholar 

  25. 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)

    Chapter  Google Scholar 

  26. Ricca, F., Faber, W., Leone, N.: A Backjumping Technique for Disjunctive Logic Programming. AI Communications 19, 155–172 (2006)

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics and Computer Science, University of Calabria, 87036, Rende, Italy

    Mario Alviano, Carmine Dodaro, Wolfgang Faber, Nicola Leone & Francesco Ricca

Authors
  1. Mario Alviano
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Carmine Dodaro
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Wolfgang Faber
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Nicola Leone
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Francesco Ricca
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Corunna, Campus de Elviña s/n, 15071, Corunna, Spain

    Pedro Cabalar

  2. Department of Computer Science, New Mexico State University, 1290 Frenger Mall, SH 123, MSC CS, P.O. Box 30001, 88003, Las Cruces, NM, USA

    Tran Cao Son

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation