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 researchers have 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, the Beluga logistics problem of Airbus, 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.

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 Σᴾ, Πᴾ, Dᴾ, and Θᴾ, 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.

Abstract 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 (ASP) is a popular problem solving paradigm with applications in planning and configuration. In practice, the number of answer sets can be overwhelmingly high, which naturally causes interest in a concise characterisation of the solution space in terms of representative answer sets. We establish a notion of representativeness that refers to the entropy of specified target atoms within a collection of answer sets. Accordingly, we propose different approaches for collecting such representative answer sets, based on answer set navigation. Finally, we conduct experiments using our prototypical implementation, which reveals promising results.

Answer set programming (ASP) is a popular declarative programming paradigm with a wide range of applications in artificial intelligence. Oftentimes, when modeling an AI problem with ASP, and in particular when we are interested beyond simple search for optimal solutions, an actual solution, differences between solutions, or number of solutions of the ASP program matter. For example, when a user aims to identify a specific answer set according to her needs, or requires the total number of diverging solutions to comprehend probabilistic applications such as reasoning in medical domains. Then, there are only certain problem specific and handcrafted encoding techniques available to navigate the solution space of ASP programs, which is oftentimes not enough. In this paper, we propose a formal and general framework for interactive navigation toward desired subsets of answer sets analogous to faceted browsing. Our approach enables the user to explore the solution space by consciously zooming in or out of sub-spaces of solutions at a certain configurable pace. We illustrate that weighted faceted navigation is computationally hard. Finally, we provide an implementation of our approach that demonstrates the feasibility of our framework for incomprehensible solution spaces.

Dialectical Frameworks [1] (ADF) are a generalisation of Dung's Argumentation frameworks [2].Multiple approaches for reasoning under various semantics have been proposed over the last decade [3,4,5,6].We present "Abstract Dialectical Frameworks solved by Binary Decision Diagrams, developed in Dresden" (ADF-BDD) 2 , a novel approach that relies on the translation of the acceptance conditions of a given ADF into reduced ordered binary decision diagrams (roBDD) [7].Our system is based on the consideration that many otherwise hard to decide problems in ADF semantics (e. g., answering SAT-questions) can be solved in polynomial time on roBDDs (see [8] for an in-depth analysis).Our novel approach differs to the currently used systems, like the SAT-based approach K++ADF [5] or the wide spectrum of answer set programming (ASP) focused approaches like the DIAMOND family (e.g., DIAMOND [3] or GODIA-MOND [4]) and YADF [6].ADF-BDD is written in RUST [9] to provide good performance while enforcing a high amount of memory-and type-safety.In addition the rust-compiler produces highly optimised machine code, while keeping the whole tech stack simple.ADF-BDD accepts the established input format, introduced first in [10].There statements are unary predicates s, defining the labels and the acceptance conditions are binary predicates ac, relating the label to a formula.It allows to enumerate the grounded and complete interpretations, and stable models of the given input instance.The set of statements is the shared signature of all acceptance conditions, hence our implementation uses a single structure to store the nodes of all the roBDDs, which represent each acceptance condition.This allows for efficient caching of nodes and to eliminate duplicate node candidates.Another side-effect is that shared sub-BDDs are computed only once.ADF-BDD provides the explained implementation of roBDDs as the representation of the acceptance conditions.As the instantiation of roBDDs is a computational hard task, it is possible to utilise another state-of-the art competitive library called Biodivine/LibBDD 3 .It is part of the Biodivine software in the AEON project [11].While LibBDD is faster in 1 This work is partly supported by the BMBF, Grant 01IS20056 NAVAS, by the Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI), and by the DFG through the Collaborative Research Center, Grant TRR 248 project ID 389792660.2

Recent developments on solvers for abstract argumentation frameworks (AFs) made them capable to compute extensions for many semantics efficiently. However, for many input instances these solution spaces can become very large and incomprehensible. So far, for the further exploration and investigation of the AF solution space the user needs to use post-processing methods or handcrafted tools. To compare and explore the solution spaces of two selected semantics, we propose an approach that visually supports the user, via a combination of dimensionality reduction of argumentation extensions and a projection of extensions to sets of accepted or rejected arguments. We introduce the novel web-based visualization tool NEXAS that allows for an interactive exploration of the solution space together with a statistical analysis of the acceptance of individual arguments for the selected semantics, as well as provides an interactive correlation matrix for the acceptance of arguments. We validate the tool with a walk-through along three use cases.