Abstract Solving a decision theory problem usually involves finding the actions, among a set of possible ones, which optimize the expected reward, while possibly accounting for the uncertainty of the environment. In this paper, we introduce the possibility to encode decision theory problems with Probabilistic Answer Set Programming under the credal semantics via decision atoms and utility attributes. To solve the task, we propose an algorithm based on three layers of Algebraic Model Counting, that we test on several synthetic datasets against an algorithm that adopts answer set enumeration. Empirical results show that our algorithm can manage non-trivial instances of programs in a reasonable amount of time.

Answer Set Programming (ASP) is a generic problem modeling and solving framework with a strong focus on knowledge representation and a rapid growth of industrial applications. So far, the study of complexity resulted in characterizing hardness and determining their sources, fine-grained insights in the form of dichotomy-style results, as well as detailed parameterized complexity landscapes. Unfortunately, for the well-known parameter treewidth disjunctive programs require double-exponential runtime under reasonable complexity assumptions. This quickly becomes out of reach. We deal with the classification of structural parameters for disjunctive ASP on the program's rule structure (incidence graph). First, we provide a polynomial kernel to obtain single-exponential runtime in terms of vertex cover size, despite subset-minimization being not represented in the program’s structure. Then we turn our attention to strictly better structural parameters between vertex cover size and treewidth. Here, we provide double-exponential lower bounds for the most prominent parameters in that range: treedepth, feedback vertex size, and cliquewidth. Based on this, we argue that unfortunately our options beyond vertex cover size are limited. Our results provide an in-depth hardness study, relying on a novel reduction from normal to disjunctive programs, trading the increase of complexity for an exponential parameter compression.

In the last decade, there has been increasing interest in extensions of answer set programming (ASP) that cater for quantitative information such as weights or probabilities. A wide range of quantitative reasoning tasks for ASP and logic programming, among them probabilistic inference and parameter learning in the neuro-symbolic setting, can be expressed as algebraic answer set counting (AASC) tasks, i.e., weighted model counting for ASP with weights calculated over some semiring, which makes makes efficient solvers for AASC desirable. In this article, we present , a new solver for AASC that pushes the limits of efficient solvability. Notably, provides improved performance compared to the state of the art in probabilistic inference by exploiting three insights gained from thorough theoretical investigations in our work. Namely, we consider the knowledge compilation step in the AASC pipeline, where the underlying logical theory specified by the answer set program is converted into a tractable circuit representation, on which AASC is feasible in polynomial time. First, we provide a detailed comparison of different approaches to knowledge compilation for programs, revealing that translation to propositional formulas followed by compilation to sd-DNNF seems favorable. Second, we study how the translation to propositional formulas should proceed to result in efficient compilation. This leads to the second and third insight, namely a novel way of breaking the positive cyclic dependencies in a program, called TP-Unfolding, and an improvement to the Clark Completion, the procedure used to transform programs without positive cyclic dependencies into propositional formulas. Both improvements are tailored towards efficient knowledge compilation. Our empirical evaluation reveals that while all three advancements contribute to the success of , TP-Unfolding improves performance significantly by allowing us to handle cyclic instances better.

We propose a new approach to the Directed Feedback Vertex Set Problem (DFVSP), where the input is a directed graph and the solution is a minimum set of vertices whose removal makes the graph acyclic.

Answer Set Programming is a widely used paradigm in knowledge representation and reasoning, which strongly relates to the satisfiability (SAT) of propositional formulas. While in the area of SAT the last couple of years brought significant advances and different techniques for solving hard counting-based problems (e.g., #SAT, weighted counting, projected counting) that require more effort than deciding satisfiability, ASP still falls short. Intuitively, one explanation for this lies in the structure of a program, that – compared to SAT – was shown to yield strong evidence for being slightly less useful during solving. Indeed, for the well-known structural measure treewidth that plays an important role in counting-based variants of SAT, ASP is expected to be at least slightly harder than SAT. The underlying source of this hardness increase lies in cyclic dependencies in the positive dependency graph. In this work, we consider which strategies are appropriate to tackle counting-based problems for ASP depending on cycle lengths. To this end, we present different encodings to counting-based variants of SAT that thereby directly utilize recent advances. For small cycle lengths, we demonstrate a novel strategy based on feedback vertex sets. While medium cycle lengths still leave room for future improvements, surprisingly, in case of cycles that are significantly larger than the structural dependencies (treewidth), we can even obtain a polynomial algorithm.

SharpSAT-TD is a recently published exact model counter that performed exceptionally well in the recent editions of the Model Counting Competition (https://mccompetition.org/). Notably, it additionally features *weighted* model counting capabilities over any semiring. In this work, we show how to exploit this fact to use SharpSAT-TD as a knowledge compiler to the class of sd-DNNF circuits. Our experimental evaluation shows that the efficiency of SharpSAT-TD for (weighted) model counting transfers to knowledge compilation, since it outperforms other state of the art knowledge compilers on standard benchmark sets. Additionally, we generalized SharpSAT-TD's preprocessing to support arbitrary semirings and consider the utility of auxiliary variables in this setting.

Many important problems in AI, among them #SAT, parameter learning and probabilistic inference go beyond the classical satisfiability problem. Here, instead of finding a solution we are interested in a quantity associated with the set of solutions, such as the number of solutions, the optimal solution or the probability that a query holds in a solution. To model such quantitative problems in a uniform manner, a number of frameworks, e.g. Algebraic Model Counting and Semiring-based Constraint Satisfaction Problems, employ what we call the semiring paradigm. In the latter the abstract algebraic structure of the semiring serves as a means of parameterizing the problem definition, thus allowing for different modes of quantitative computations by choosing different semirings. While efficiently solvable cases have been widely studied, a systematic study of the computational complexity of such problems depending on the semiring parameter is missing. In this work, we characterize the latter by NP(R), a novel generalization of NP over semiring R, and obtain NP(R)-completeness results for a selection of semiring frameworks. To obtain more tangible insights into the hardness of NP(R), we link it to well-known complexity classes from the literature. Interestingly, we manage to connect the computational hardness to properties of the semiring. Using this insight, we see that, on the one hand, NP(R) is always at least as hard as NP or ModpP depending on the semiring R and in general unlikely to be in FPSPACEpoly. On the other hand, for broad subclasses of semirings relevant in practice we can employ reductions to NP, ModpP and #P. These results show that in many cases solutions are only mildly harder to compute than functions in NP, ModpP and #P, give us new insights into how problems that involve counting on semirings can be approached, and provide a means of assessing whether an algorithm is appropriate for a given class of problems.

Abstract A ProbLog program is a logic program with facts that only hold with a specified probability. In this contribution, we extend this ProbLog language by the ability to answer “What if” queries. Intuitively, a ProbLog program defines a distribution by solving a system of equations in terms of mutually independent predefined Boolean random variables. In the theory of causality, Judea Pearl proposes a counterfactual reasoning for such systems of equations. Based on Pearl’s calculus, we provide a procedure for processing these counterfactual queries on ProbLog programs, together with a proof of correctness and a full implementation. Using the latter, we provide insights into the influence of different parameters on the scalability of inference. Finally, we also show that our approach is consistent with CP-logic, that is with the causal semantics for logic programs with annotated with disjunctions.

We propose a new approach to the Directed Feedback Vertex Set Problem (DFVSP), where the input is a directed graph and the solution is a minimum set of vertices whose removal makes the graph acyclic. Our approach, implemented in the solver DAGer, is based on two novel contributions: Firstly, we add a wide range of data reductions that are partially inspired by reductions for the similar vertex cover problem. For this, we give a theoretical basis for lifting reductions from vertex cover to DFVSP but also incorporate novel ideas into strictly more general and new DFVSP reductions. Secondly, we propose dynamically encoding DFVSP in propositional logic using cycle propagation for improved performance. Cycle propagation builds on the idea that already a limited number of the constraints in a propositional encoding is usually sufficient for finding an optimal solution. Our algorithm, therefore, starts with a small number of constraints and cycle propagation adds additional constraints when necessary. We propose an efficient integration of cycle propagation into the workflow of MaxSAT solvers, further improving the performance of our algorithm. Our extensive experimental evaluation shows that DAGer significantly outperforms the state-of-the-art solvers and that our data reductions alone directly solve many of the instances.

Abstract Quantitative extensions of logic programming often require the solution of so called second level inference tasks, that is, problems that involve a third operation, such as maximization or normalization, on top of addition and multiplication, and thus go beyond the well-known weighted or algebraic model counting setting of probabilistic logic programming under the distribution semantics. We introduce Second Level Algebraic Model Counting (2AMC) as a generic framework for these kinds of problems. As 2AMC is to (algebraic) model counting what forall-exists-SAT is to propositional satisfiability, it is notoriously hard to solve. First level techniques based on Knowledge Compilation (KC) have been adapted for specific 2AMC instances by imposing variable order constraints on the resulting circuit. However, those constraints can severely increase the circuit size and thus decrease the efficiency of such approaches. We show that we can exploit the logical structure of a 2AMC problem to omit parts of these constraints, thus limiting the negative effect. Furthermore, we introduce and implement a strategy to generate a sufficient set of constraints statically, with a priori guarantees for the performance of KC. Our empirical evaluation on several benchmarks and tasks confirms that our theoretical results can translate into more efficient solving in practice.

Many important problems in AI, among them SAT, #SAT, and probabilistic inference, amount to Sum-of-Products Problems, i.e. evaluating a sum of products of values from some semiring R. While efficiently solvable cases are known, a systematic study of the complexity of this problem is missing. We characterize the latter by NP(R), a novel generalization of NP over semiring R, and link it to well-known complexity classes. While NP(R) is unlikely to be contained in FPSPACE(poly) in general, for a wide range of commutative (resp. in addition idempotent) semirings, there are reductions to #P (resp. NP) and solutions are thus only mildly harder to compute. We finally discuss NP(R)-complete reasoning problems in well-known semiring formalisms, among them Semiring-based Constraint Satisfaction Problems, obtaining new insights into their computational properties.

Probabilistic reasoning, parameter learning, and most probable explanation inference for answer set programming have recently received growing attention. They are only some of the problems that can be formulated as Algebraic Answer Set Counting (AASC) problems. The latter are however hard to solve, and efficient evaluation techniques are needed. Inspired by Vlasser et al.'s Tp-compilation (JAR, 2016), we introduce Tp-unfolding, which employs forward reasoning to break the cycles in the positive dependency graph of a program by unfolding them. Tp-unfolding is defined for any normal answer set program and unfolds programs with respect to unfolding sequences, which are akin to elimination orders in SAT-solving. Using "good" unfolding sequences, we can ensure that the increase of the treewidth of the unfolded program is small. Treewidth is a measure adhering to a program's tree-likeness, which gives performance guarantees for AASC. We give sufficient conditions for the existence of good unfolding sequences based on the novel notion of component-boosted backdoor size, which measures the cyclicity of the positive dependencies in a program. The experimental evaluation of a prototype implementation, the AASC solver aspmc, shows promising results.

Abstract Dealing with context-dependent knowledge has led to different formalizations of the notion of context. Among them is the Contextualized Knowledge Repository (CKR) framework, which is rooted in description logics but links on the reasoning side strongly to logic programs and Answer Set Programming (ASP) in particular. The CKR framework caters for reasoning with defeasible axioms and exceptions in contexts, which was extended to knowledge inheritance across contexts in a coverage (specificity) hierarchy. However, the approach supports only this single type of contextual relation and the reasoning procedures work only for restricted hierarchies, due to nontrivial issues with model preference under exceptions. In this paper, we overcome these limitations and present a generalization of CKR hierarchies to multiple contextual relations, along with their interpretation of defeasible axioms and preference. To support reasoning, we use ASP with algebraic measures, which is a recent extension of ASP with weighted formulas over semirings that allows one to associate quantities with interpretations depending on the truth values of propositional atoms. Notably, we show that for a relevant fragment of CKR hierarchies with multiple contextual relations, query answering can be realized with the popular asprin framework. The algebraic measures approach is more powerful and enables, for example, reasoning with epistemic queries over CKRs, which opens interesting perspectives for the use of quantitative ASP extensions in other applications.

Abstract Weighted Logic is a powerful tool for the specification of calculations over semirings that depend on qualitative information. Using a novel combination of Weighted Logic and Here-and-There (HT) Logic, in which this dependence is based on intuitionistic grounds, we introduce Answer Set Programming with Algebraic Constraints (ASP( $\mathcal A \mathcal C$ )), where rules may contain constraints that compare semiring values to weighted formula evaluations. Such constraints provide streamlined access to a manifold of constructs available in ASP, like aggregates, choice constraints, and arithmetic operators. They extend some of them and provide a generic framework for defining programs with algebraic computation, which can be fruitfully used e.g. for provenance semantics of datalog programs. While undecidable in general, expressive fragments of ASP( $\mathcal A \mathcal C$ ) can be exploited for effective problem solving in a rich framework.