Testing and debugging techniques for answer set solver development

DOI10.1017/S1471068410000396zbMATH Open1206.68292arXiv1007.3223OpenAlexW2134211750MaRDI QIDQ3585183FDOQ3585183

Authors: Robert Brummayer, Matti Järvisalo 

Publication date: 19 August 2010

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1007.3223

Recommendations

• Automated testing and debugging of SAT and QBF solvers
• Debugging non-ground ASP programs: technique and graphical tools
• Debugging ASP Programs by Means of ASP
• Interactive debugging of non-ground ASP programs
• On testing answer-set programs

zbMATH Keywords

testinganswer set programmingdebugginganswer set solvers

Mathematics Subject Classification ID

Knowledge representation (68T30)

Cites Work

• ASSAT: computing answer sets of a logic program by SAT solvers
• The nomore + + Approach to Answer Set Solving
• Extending and implementing the stable model semantics
• The DLV system for knowledge representation and reasoning
• Logic programs with stable model semantics as a constraint programming paradigm
• Answer set programming based on propositional satisfiability
• Debugging ASP Programs by Means of ASP
• Some (in)translatability results for normal logic programs and propositional theories
• The Significance of Memory Costs in Answer Set Solver Implementation
• Computing Stable Models via Reductions to Difference Logic
• Simple Random Logic Programs
• Fuzzing for software security testing and quality assurance

Cited In (3)

• Debugging for Model Expansion
• Automated testing and debugging of SAT and QBF solvers
• \(\mathsf {Harvey}\): a system for random testing in ASP

Uses Software

• GNT
• MiniSat
• ASSAT
• Yices
• cvc3
• PicoSAT
• QuickCheck

This page was built for publication: Testing and debugging techniques for answer set solver development

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3585183)