QuantASP - Quantitative Reasoning and Counting for ASP

Solving computationally hard problems is a key challenge in computer science. In the last decades, the focus of these problems increasingly contained counting problems and quantitative questions. Such counting problems do not only consider the existence of just a single solution, but concern the computation of the total number of solutions, which actually yields a plethora of applications in computational biology, artificial intelligence, and quantitative reasoning. Observe that counting for example allows us to reason about the role, importance, and consequences of certain solution parts, depending on whether these parts appear in some or many solutions, or even in the vast majority of solutions. One concrete approach towards solving hard problems relies on decomposing an instance into smaller parts, thereby solving the problem step-by-step via a dedicated algorithm that suitably combines solutions of the single parts into a solution of the whole instance. This method is known as dynamic programming and has been applied many times and on several problems. However, for counting problems there are still exciting questions that remained unsolved and have been left open. Some of these open questions originate when counting solutions of logic programs, whose solutions are stable (minimal) answers, formally described by means of rule-like constraints that have to be fulfilled. Our working hypothesis is that the stability criteria of these answers is the inherent reason why counting answers by means of dynamic programming indeed requires excessively more solving effort than deciding or obtaining just one answer. We expect to formally show that counting problems on key fragments of logic programs are indeed harder than corresponding decision problems, even in the case of structurally simple instances, whose program structure is close to tree-like structures (bounded treewidth). This then yields precise runtime lower bounds (hardness results), which we will generalize in order to provide a methodology for simply showing lower bounds for a list of further counting problems. Despite these expected lower bounds, we will research on efficient approaches for counting answers in practice, where we focus on the following two principles: (1) Abstractions, which aim for simplifications and solving the problem incrementally; (2) Systematic over- and undercounting, where the goal is to constantly improve already obtained upper and lower bounds in order to approach the total number of solutions. We are convinced that a combination of these principles will yield techniques that pave the way towards establishing and solving new applications in the area of computational biology.