Abstract Answer Set Solvers for Cautious Reasoning
Rémi Brochenin, Marco Maratea · CINECA IRIS Institutial Research Information System (University of Genoa) · 2015
Abstract solvers are a recently employed method to formally analyze algorithms that earns some advantages w.r.t. traditional ways such as pseudo-code-based description. Abstract solvers proved to be a useful tool for describing, comparing and composing solving techniques in various fields such as SAT, SMT, ASP, CASP. In ASP, abstract solvers have been so far employed for describing solvers for brave reasoning tasks. In this paper we apply, for the first time, this methodology to the analysis of ASP solvers for cautious reasoning tasks. We describe and compare the available approaches in the literature, which employ techniques for computing over- and under-approximations of the solution, the last including coherence tests for deciding the inclusion of a single atom in the solution, a technique borrowed from backbone computation of CNF formulas. Then, we show how to improve the current abstract solvers with new techniques, in order to design new solving algorithms. Abstract solvers are a relatively recently employed method to formally analyse algorithms that earns some advantages w.r.t. traditional ways such as pseudo-code-based description. In this methodology, the states of computation are represented as nodes of a graph, the solving techniques as edges between such nodes, the solving process as a path in the graph and formal properties of the algorithms are reduced to related graph properties. Abstract solvers proved to be a useful tool for describing, comparing and composing solver design techniques in various fields such as CNF satisfiability (SAT) and Satisfiability Modulo Theories (SMT) (Nieuwenhuis et al. 2006), Answer Set Programming (Lierler 2011; Lier- ler and Truszczynski 2011; Brochenin et al. 2014), and Constraint ASP (Lierler 2014). In ASP, such methodology led to the development of a new ASP solver, SUP (Lierler 2011); however,abstract solvers have been so far applied to ASP solvers for brave reasoning tasks where,givenan inputqueryanda knowledgebase expressedinASP, answersare witnessed by ASP solutions, i.e. stable models (Baral 2003; Eiter et al. 1997; Gelfond and Lifschitz