Testing and debugging techniques for answer set solver development

DOI10.1017/S1471068410000396MaRDI QIDQ3585183zbMATH OpenOpenAlexFDO

Authors Robert Brummayer, Matti Järvisalo

Publication date 19 August 2010

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

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

zbMATH Keywords

testinganswer set programmingdebugginganswer set solvers

Mathematics Subject Classification ID

Knowledge representation (68T30)

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.

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

Cites work

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

Cited in

(3)

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

Describes a project that uses

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)