By Carmine Dodaro,
Università della Calabria
January 2015
Abstract
Answer Set Programming (ASP) is a declarative programming paradigm based on the stable model semantics. The idea of ASP is to encode a computational problem into a logic problem, whose stable models correspond to the solution of the original problem. The high expressivity of ASP, combined with the growing number of applications, made the implementation of new ASP solvers a challenging and crucial research topic.
The implementation of an ASP solver requires to provide solutions for several computational tasks. This thesis focuses on the ones related to reasoning with propositional ASP programs, such as model generation, answer set checking, optimum answer set search, and cautious reasoning. The combination of the first two tasks is basically the computation of answer sets. Indeed, model generation amounts to generating models of the input program, whose stability is subsequently verified by calling an answer set checker. Model generation is similar to SAT solving, and it is usually addressed by employing a CDCL-like backtracking algorithm. Answer set checking is a co-NP complete task in general, and is usually reduced to checking the unsatisfiability of a SAT formula. In presence of optimization constructs the goal of an ASP solver becomes optimum answer set search, and requires to find an answer set that minimizes the violations of the so-called weak constraints. In data- oriented applications of ASP cautious reasoning is often the main task, and amounts to the computation of (a subset of) the certain answers, i.e., those that belong to all answer sets of a program.
These tasks are computationally very hard in general, and this thesis provides algorithms and solutions to solve them efficiently. In particular the contributions of this thesis can be summarized as follows:
- The task of generating model candidates has been studied, and a combination of techniques, which were originally introduced for SAT solving has been implemented in a new ASP solver.
- A new algorithm for answer set checking has been proposed that minimizes the overhead of executing multiple calls to a co-NP oracle by resorting to an incremental evaluation strategy and specific heuristics.
- A family of algorithms for computing optimum answer sets of programs with weak constraints has been implemented by porting to the ASP setting several algorithms introduced for MaxSAT solving.
- A new framework of anytime algorithms for computing the cautious consequences of an ASP knowledge base has been introduced, that extends existing proposals and includes a new algorithm inspired by techniques for the computation of backbones of propositional theories.
These techniques have been implemented in wasp 2, a new solver for propositional ASP programs. The effectiveness of the proposed techniques and the performance of the new system have been validated empirically on publicly-available benchmarks taken from ASP competitions and other repositories of ASP applications.