Abductive reasoning is a popular non-monotonic paradigm that aims to explain observedsymptoms and manifestations. It has many applications, such as diagnosis and planning in artificial intelligence and database updates. In propositional abduction, we focus on specifying knowledge by a propositional formula. The computational complexity of tasks in propositional abduction has been systematically characterized – even with detailed classifications for Boolean fragments. Unsurprisingly, the most insightful reasoning problems (counting and enumeration) are computationally highly challenging. Therefore, we consider reasoning between decisions and counting, allowing us to understand explanations better while maintaining favorable complexity.We introduce facets to propositional abductions, which are literals that occur in some explanation (relevant) but not all explanations (dispensable). Reasoning with facets provides a more fine-grained understanding of variability in explanations (heterogeneous). In addition, we consider the distance between two explanations, enabling a better understanding of heterogeneity/homogeneity. We comprehensively analyze facets of propositional abduction in various settings, including analmost complete characterization in Post’s framework.

Classical planning asks for a sequence of operators reach-ing a given goal. While the most common case is to compute a plan, many scenarios require more than that. However, quantitative reasoning on the plan space remains mostly unexplored. A fundamental problem is to count plans, which relates to the conditional probability on the plan space. Indeed, qualitative and quantitative approaches are well-established in various other areas of automated reasoning.

We present the first study to quantitative and qualitative reasoning on the plan space. In particular, we focus on polynomially bounded plans. On the theoretical side, we study its complexity, which gives rise to rich reasoning modes. Sincecounting is hard in general, we introduce the easier notion of facets, which enables understanding the significance of operators. On the practical side, we implement quantitative reasoning for planning. Thereby, we transform a planning task into a propositional formula and use knowledge compilationto count different plans. This framework scales well to largeplan spaces, while enabling rich reasoning capabilities suchas learning pruning functions and explainable planning.

Argumentation is a central subarea of Artificial Intelligence (AI) for modeling and reasoning about arguments. The semantics of abstract argumentation frameworks (AFs) is given by sets of arguments (extensions) and conditions on the relationship between them, such as stable or admissible. Today's solvers implement tasks such as finding extensions, deciding credulous or skeptical acceptance, counting, or enumerating extensions. While these tasks are well charted, the area between decision, counting/enumeration and fine-grained reasoning requires expensive reasoning so far. We introduce a novel concept (facets) for reasoning between decision and enumeration. Facets are arguments that belong to some extensions (credulous) but not to all extensions (skeptical). They are most natural when a user aims to navigate, filter, or comprehend the significance of specific arguments, according to their needs. We study the complexity and show that tasks involving facets are much easier than counting extensions. Finally, we provide an implementation, and conduct experiments to demonstrate feasibility.

Many planning applications require not only a single solution but benefit substantially from having a set of possible plans from which users can select according to preferences. Surprisingly, planning research has primarily focused on quickly finding single plans for decades. Only recently have researchers started to investigate plan enumeration by top-k planning, offering more flexibility to the user. But simply enumerating the k best plans is far from targeted due to the time-consuming nature of enumeration, likely feeding many similar plans to the user, and forcing the user to define filters beforehand. In fact, in extensive search spaces, enumeration is hardly practical. We present an approach and a tool called PlanPilot to navigate solution spaces of planning tasks iteratively and interactively. We build on answer-set programming (ASP) to restrict the plan space. To that end, we employ facets, which are meaningful actions that appear in some, but not all plans. Enforcing or forbidding such facets allows for navigating even large plan spaces while ensuring desired properties quickly and step by step. 

Many planning applications require not only a single solution but benefit substantially from having a set of possible plans from which users can select, for example, when explaining plans. For decades, research in classical AI planning has primarily focused on quickly finding single plans. Only recently have researchers started to investigate preferences, enumerate plans by top-k planning, or count plans to reason about the plan space. Unfortunately, reasoning about the plan space is computationally extremely hard and feeding many similar plans to the user is hardly practical. To circumvent computational shortcomings while still being able to reason about variability in plans, faceted actions have been introduced very recently. These are meaningful actions that can be used by some plan but are not required by all plans. Enforcing or forbidding such facets allows for navigating even large plan spaces while ensuring desired properties quickly and step by step. In this paper, we illustrate an industrial challenge where reasoning with facets enables targeted plan space navigation. We present an approach to handle large plan spaces iteratively and interactively and present a tool that we call PlanPilot. 

Boolean satisfiability (SAT) asks to decide whether a formula can be evaluated to true. In certified SAT solving, one additionally asks to provide a certificate or verifiable proof to ensure correctness of the solver’s output. A crucial component in this process are fast verified, proof checkers. However, constructing efficient, formally verified checkers remains challenging. 

In this paper, we study whether the Ada/SPARK programming language can enable reliable, efficient, verifiable proof checkers. SPARK 2014, with its design-by-contract capabilities, allows to express core concepts of propositional logic and modern redundancy criteria with functional correctness. We introduce a methodology for implementing SAT specifications in SPARK, accompanied by formal proofs with a focus on Resolution Asymmetric Tautologies (RAT). While a complete verified proof checker is not yet realized, our work establishes the foundational framework necessary for its future development, and demonstrates that strong correctness guarantees can be realiized in SPARK.

In this paper, we consider counting and projected model counting of extensions in abstract argumentation for various semantics, including credulous reasoning. When asking for projected counts, we are interested in counting the number of extensions of a given argumentation framework, while multiple extensions that are identical when restricted to the projected arguments count as only one projected extension. We establish classical complexity results and parameterized complexity results when the problems are parameterized by the treewidth of the undirected argumentation graph. To obtain upper bounds for counting projected extensions, we introduce novel algorithms that exploit small treewidth of the undirected argumentation graph of the input instance by dynamic programming. Our algorithms run in double or triple exponential time in the treewidth, depending on the semantics under consideration. Finally, we establish lower bounds of bounded treewidth algorithms for counting extensions and projected extension under the exponential time hypothesis (ETH).

This paper establishes the computational complexity of non-ground ELPs. We provide a comprehensive picture for well-known program fragments, which turns out to be complete for the class NEXPTIME with access to oracles up to SigmaP2. In the quantitative setting, which enables more fine-grained reasoning, we establish complexity results for counting complexity beyond #EXP. To mitigate the high complexity, we establish encouraging results in case of bounded predicate arity, reaching up to the fourth level of the polynomial hierarchy. Finally, we provide ETH-tight runtime results for the structural parameter treewidth, which has applications in quantitative reasoning modes, where we reason on (marginal) probabilities of epistemic literals.

Answer set programming (ASP) is a popular declarative programming paradigm with various applications. Programs can easily have many answer sets that cannot be enumerated in practice, but counting still allows quantifying solution spaces. If one counts under assumptions on literals, one obtains a tool to comprehend parts of the solution space, so-called answer set navigation. However, navigating through parts of the solution space requires counting many times, which is expensive in theory. Knowledge compilation compiles instances into representations on which counting works in polynomial time. However, these techniques exist only for conjunctive normal form (CNF) formulas, and compiling ASP programs into CNF formulas can introduce an exponential overhead. This paper introduces a technique to iteratively count answer sets under assumptions on knowledge compilations of CNFs that encode supported models. Our anytime technique uses the inclusion-exclusion principle to improve bounds by over- and undercounting systematically. In a preliminary empirical analysis, we demonstrate promising results. After compiling the input (offline phase), our approach quickly (re)counts.

Answer set programming is a popular declarative paradigm with countless applications for modeling and solving combinatorial problems. We can view a program as a knowledge database compactly representing conditions for solutions. Often we are interested in reasoning about solutions of filtering answer sets. At the heart of these questions is brave and cautious reasoning. For browsing answer sets, we combine both as restricting atoms of answer sets is only meaningful for atoms called facets that belong to some (brave) but not to all answer sets (cautious). Surprisingly, the precise computational complexity of facet problems remained widely open so far. In this paper, we study the complexity of answer set facets. We establish tight results for reasoning with facets, deciding upper and lower bounds as well as the exact number of facets, and comparing facets. Facet reasoning seems to be a natural problem formalism, residing in complexity families ΣP , ΠP , DP , and ΘP, up to the third level. Moreover, our study considers quantitative importance questions on facets and generalizing from facets to conjunctions, disjunctions, and arbitrary queries. We complete our results by an experimental evaluation.