Hostname: page-component-586b7cd67f-2plfb Total loading time: 0 Render date: 2024-11-26T00:05:53.698Z Has data issue: false hasContentIssue false
  • English
  • Français

Testing and debugging techniques for answer set solver development

Published online by Cambridge University Press:  09 July 2010

ROBERT BRUMMAYER  and
MATTI JÄRVISALO
ROBERT BRUMMAYER
Affiliation:
Institute for Formal Models and Verification, Johannes Kepler University Linz, Austria
MATTI JÄRVISALO
Affiliation:
Department of Computer Science, University of Helsinki, Finland
Get access Rights & Permissions [Opens in a new window]

Abstract

This paper develops automated testing and debugging techniques for answer set solver development. We describe a flexible grammar-based black-box ASP fuzz testing tool which is able to reveal various defects such as unsound and incomplete behavior, i.e. invalid answer sets and inability to find existing solutions, in state-of-the-art answer set solver implementations. Moreover, we develop delta debugging techniques for shrinking failure-inducing inputs on which solvers exhibit defective behavior. In particular, we develop a delta debugging algorithm in the context of answer set solving, and evaluate two different elimination strategies for the algorithm.

Keywords

answer set programminganswer set solverstestingdebugging
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 10 , Special Issue 4-6: 26th International Conference on Logic Programming , July 2010 , pp. 741 - 758
Copyright
Copyright © Cambridge University Press 2010

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Anger, C., Gebser, M., Linke, T., Neumann, A. and Schaub, T. 2005. The nomore++ approach to answer set solving. In Proceedings of the 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2005), Sutcliffe, G. and Voronkov, A., Eds. Lecture Notes in Computer Science, vol. 3835. Springer, 95–109.Google Scholar
Barrett, C. and Tinelli, C. 2007. CVC3. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007), Damm, W. and Hermanns, H., Eds. Lecture Notes in Computer Science, vol. 4590. Springer, 298–302.Google Scholar
Biere, A. 2008. PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation 4, 75–97.CrossRefGoogle Scholar
Brain, B., Gebser, M., Pührer, J., Schaub, T., Tompits, H. and Woltran, S. 2007. Debugging ASP programs by means of ASP. In Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2007), Baral, C., Brewka, G., and Schlipf, J. S., Eds. Lecture Notes in Computer Science, vol. 4483. Springer, 31–43.CrossRefGoogle Scholar
Brain, M. and de Vos, M. 2005. Debugging logic programs under the answer set semantics. In Proceedings of the 3rd Workshop on Answer Set Programming: Advances in Theory and Implementation (ASP), de Vos, M. and Provetti, A., Eds. 142–152.Google Scholar
Brain, M. and De Vos, M. 2009. The significance of memory costs in answer set solver implementation. Journal of Logic and Computation 19, 4, 615–641.CrossRefGoogle Scholar
Brummayer, R. and Biere, A. 2009. Fuzzing and delta-debugging SMT solvers. In Proceedings of the 7th International Workshop on Satisfiability Modulo Theories (SMT). ACM International Conference Proceedings Series, vol. 375. ACM, 1–5.Google Scholar
Calimeri, F., Leone, N., Ricca, F. and Veltri, P. 2009. A visual tracer for DLV. In Proceedings of the 2nd International Workshop on Software Engineering for Answer Set Programming (SEA 2009), De Vos, M. and Schaub, T., Eds. 79–93.Google Scholar
Claessen, K. and Hughes, J. 2000. QuickCheck: A lightweight tool for random testing of Haskell programs. In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP 2000). SIGPLAN Notices 35(9). ACM, 268–279.Google Scholar
de Moura, L. M. and Bjørner, N. 2008. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), Ramakrishnan, C. R. and Rehof, J., Eds. Lecture Notes in Computer Science, vol. 4963. Springer, 337–340.Google Scholar
Denecker, M., Vennekens, J., Bond, S., Gebser, M., and Truszczynski, M. 2009. The second answer set programming competition. In Proceedings of the 10th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2009), Erdem, E., Lin, F., and Schaub, T., Eds. Lecture Notes in Computer Science, vol. 5753. Springer, 637–654. See also competition results at http://www.cs.kuleuven.be/~dtai/events/ASP-competition/.CrossRefGoogle Scholar
Drescher, C., Gebser, M., Grote, T., Kaufmann, B., König, A., Ostrowski, M. and Schaub, T. 2008. Conflict-driven disjunctive answer set solving. In Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR), Brewka, G. and Lang, J., Eds. AAAI Press, 422–432.Google Scholar
Dutertre, B. and de Moura, L. 2006. The Yices SMT solver. http://yices.csl.sri.com/tool-paper.pdf.Google Scholar
Eén, N. and Sörensson, N. 2004. An extensible SAT-solver. In 6th International Conference on Theory and Applications of Satisfiability Testing (SAT), Selected Revised Papers, Giunchiglia, E. and Tacchella, A., Eds. Lecture Notes in Computer Science, vol. 2919. Springer, 502–518.CrossRefGoogle Scholar
Gebser, M., Kaufmann, B., Neumann, A. and Schaub, T. 2007. Conflict-driven answer set solving. In Proceedings of the 20th International Joint Conference on Articifial Intelligence (IJCAI), Veloso, M. M., Ed. Morgan Kaufmann, 286–392.Google Scholar
Gebser, M., Liu, L., Namasivayam, G., Neumann, A., Schaub, T. and Truszczynski, M. 2007. The first answer set programming system competition. In Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), Baral, C., Brewka, G., and Schlipf, J. S., Eds. Lecture Notes in Computer Science, vol. 4483. Springer, 3–17. See also competition results at http://asparagus.cs.uni-potsdam.de/contest/.CrossRefGoogle Scholar
Gebser, M., Pührer, J., Schaub, T. and Tompits, H. 2008. A meta-programming technique for debugging answer-set programs. In Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence (AAAI), Fox, D. and Gomes, C. P., Eds. AAAI Press, 448–453.Google Scholar
Gelfond, M. and Lifschitz, V. 1988. The stable model semantics for logic programming. In Proceedings of the 5th International Conference and Symposium on Logic Programming (ICLP/SLP 1988), Kowalski, R. A. and Bowen, K. A., Eds. MIT Press, 1070–1080.Google Scholar
Giunchiglia, E., Lierler, Y. and Maratea, M. 2006. Answer set programming based on propositional satisfiability. Journal of Automated Reasoning 36, 4, 345–377.CrossRefGoogle Scholar
Janhunen, T. 2006. Some (in)translatability results for normal logic programs and propositional theories. Journal of Applied Non-Classical Logics 16, 1–2, 35–86.CrossRefGoogle Scholar
Janhunen, T. and Niemelä, I. 2004. GnT — A solver for disjunctive logic programs. In Proceedings of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2004), Lifschitz, V. and Niemelä, I., Eds. Lecture Notes in Computer Science, vol. 2923. Springer, 331–335.Google Scholar
Janhunen, T., Niemelä, I. and Sevalnev, M. 2009. Computing stable models via reductions to difference logic. In 10th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2009), Erdem, E., Lin, F., and Schaub, T., Eds. Lecture Notes in Computer Science, vol. 5753. Springer, 142–154.CrossRefGoogle Scholar
Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S. and Scarcello, F. 2006. The DLV system for knowledge representation and reasoning. ACM Transactions on Computational Logic 7, 3, 499–562.CrossRefGoogle Scholar
Lin, F. and Zhao, Y. 2004. ASSAT: Computing answer sets of a logic program by SAT solvers. Artificial Intelligence 157, 1–2, 115–137.CrossRefGoogle Scholar
Liu, L. and Truszczynski, M. 2005. Pbmodels — Software to compute stable models by pseudoboolean solvers. In Proceedings of the 8th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), Baral, C., Greco, G., Leone, N., and Terracina, G., Eds. Lecture Notes in Computer Science, vol. 3662. Springer, 410–415.CrossRefGoogle Scholar
Misherghi, G. and Su, Z. 2006. HDD: Hierarchical delta debugging. In Proceedings of the 28th International Conference on Software Engineering (ICSE), Osterweil, L. J., Rombach, H. D., and Soffa, M. L., Eds. ACM, 142–151.Google Scholar
Namasivayam, G. and Truszczyński, M. 2009. Simple random logic programs. In Proceedings of the 10th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2009), Erdem, E., Lin, F., and Schaub, T., Eds. Lecture Notes in Computer Science, vol. 5753. Springer, 223–235.CrossRefGoogle Scholar
Niemelä, I. 1999. Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence 25, 3–4, 241–273.CrossRefGoogle Scholar
Simons, P., Niemelä, I. and Soininen, T. 2002. Extending and implementing the stable model semantics. Artificial Intelligence 138, 1–2, 181–234.CrossRefGoogle Scholar
Sutton, M., Greene, A. and Amini, P. 2007. Fuzzing — Brute Force Vulnerability Discovery. Pearson Education.Google Scholar
Syrjänen, T. 2006. Debugging inconsistent answer set programs. In Proceedings of the 11th International Workshop on Nonmonotonic Reasoning (NMR), Dix, J. and Hunter, A., Eds. IfI Technical Report Series, vol. IfI-06-04. TU Clausthal, 77–83.Google Scholar
Takanen, A., Demott, J., and Miller, C. 2008. Fuzzing for Software Security Testing and Quality Assurance. Artech House.Google Scholar
Tronçon, R. and Janssens, G. 2006. A delta debugger for ILP query execution. In Proceedings of the 16th Workshop on Logic-Based Methods in Programming Environments (WLPE).Google Scholar
Tseitin, G. S. 1983. On the complexity of derivation in propositional calculus. In Automation of Reasoning 2: Classical Papers on Computational Logic 1967–1970, Siekmann, J. and Wrightson, G., Eds. Springer, 466–483.CrossRefGoogle Scholar
Ward, J. and Schlipf, J. S. 2004. Answer set programming with clause learning. In Proceedings of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), Lifschitz, V. and Niemelä, I., Eds. Lecture Notes in Computer Science, vol. 2923. Springer, 302–313.Google Scholar
Zeller, A. 2005. Why Programs Fail. A Guide to Systematic Debugging. Morgan Kaufmann.Google Scholar
Zeller, A. and Hildebrandt, R. 2002. Simplifying and isolating failure-inducing input. IEEE Transactions on Software Engineering 28, 2, 183–200.CrossRefGoogle Scholar
Zhao, Y. and Lin, F. 2003. Answer set programming phase transition: A study on randomly generated programs. In Proceedings of the 19th International Conference on Logic Programming (ICLP), Palamidessi, C., Ed. Lecture Notes in Computer Science, vol. 2916. Springer, 239–253.Google Scholar