NAVAS Workshop 2022 in Vienna

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

The NAVAS workshop on Navigation Approaches for Answer Sets is jointly organized by research groups at TU Wien and TU Dresden will take place in Vienna, Austria, May 23-24, 2022.

Vienna Skyline

Due to the continuous development in recent years, a large number of demanding combinatorial search problems of enormous practical relevance can now be efficiently solved by Answer Set Programming (ASP). Depending on the scope of the problem to be solved, a "combinatorial explosion" of the number of solutions can occur very quickly. While modern ASP solvers can easily calculate several million solutions in a short time, this poses a new problem for the user: How should the enormous solution space be handled and made accessible? Typically, the Answer Sets are output in any order. However, many of these solutions are very similar. In practice, however, often only solutions are of interest that are sufficiently different from each other, that have special properties, or that are similar to a given set of solutions. In this workshop we present recent developments on answer set navigation and related work in formal argumentation.

This workshop is supported by:

Bundesministerium für Bildung und Forschung (BMBF), Grant 01IS20056 NAVAS

DFG through the Collaborative Research Center, Grant TRR 248 (see [1] project ID 389792660)

The NaVAS workshop will take place from Monday, May 23th until Wednesday May 25th of 2022.

Monday, May 23th:

  • 09:15 - 09:20 Welcome
  • 09:20 - 09:45 Talk: The NAVAS Project and NEXAS - A Visual Tool for Navigating and Exploring Argumentation Solution Spaces - Sarah Alice Gaggl
  • 09:45 - 10:15 Talk: Tunas - Fishing for Diverse Answer Sets: A Multi-Shot Trade up Strategy - Elisa Böhl
  • 10:15 - 10:45 Talk: Flexible Dispute Derivations with Forward and Backward Arguments for Assumption-Based Argumentation - Martin Diller
  • 10:45 - 11:00 Coffee break
  • 11:00 - 11:30 Talk (tent.): Abstraction for non-ground answer set programs - Zeynep G. Saribatur
  • 11:30 - 12:00 Talk: Rushing and Strolling among Answer Sets - Navigation Made Easy - Dominik Rusovac
  • 12:00 - 12:30 Talk: Existential Abstraction on Argumentation Frameworks via Clustering - Johannes Wallner
  • 12:30 - 12:45 Talk: Utilizing Treewidth for Quantitative Reasoning on Epistemic Logic Programs - Viktor Besin
  • 12:45 - 13:00 Talk: Approximate Answer Set Counting - Johannes Fichte
  • 13:00 - 14:00 Lunch Break
  • 14:00 - 18:00 Internal Meetings
  • 19:00 - 21:00 Dinner

Tuesday, May 24th:

For the schedule on on Monday, May 23th the following talks are presented.

NEXAS - A Visual Tool for Navigating and Exploring Argumentation Solution Spaces

Sarah Gaggl

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.

Fishing for Diverse Answer Sets: A Multi-Shot Trade up Strategy

Elisa Böhl

Answer set programming (ASP) solvers have advanced in the recent years, with a variety of different specialisation and overall development. Thus, even more complex and detailed programs can be solved. A side effect of this development are growing solution spaces and the problem of how to find those answer sets one is interested in. One general approach is to give an overview in form of a small number of highly diverse answer sets. By choosing a favourite and repeating the process the user is able to leap through the solution space. But finding highly diverse answer sets is computationally expensive. In this paper we introduce a new approach called Tunas for Trade Up Navigation for Answer Sets to find diverse answer sets by reworking existing solution collections. The core idea is to collect diverse answer sets. Once no more answer sets can be added to the collection, the program is allowed to trade answer sets from the collection for different answer sets, as long as the collection grows and stays diverse. Elaboration of the approach is possible in three variations, which we implemented and compared to established methods in an empirical evaluation. The evaluation shows that the Tunas approach is competitive with existing methods, and that efficiency of the approach is highly connected to the underlying logic program.

Flexible Dispute Derivations with Forward and Backward Arguments for Assumption-Based Argumentation

Martin Diller

Assumption-based argumentation (ABA) is one of the main general frameworks for structured argumentation. Dispute derivations for ABA allow for evaluating claims in a dialectical manner: i.e. on the basis of an exchange of arguments and counter-arguments for a claim between a proponent and an opponent of the claim. Current versions of dispute derivations are geared towards determining (credulous) acceptance of claims w.r.t. the admissibility-based semantics that ABA inherits from abstract argumentation. Relatedly, they make use of backwards or top down reasoning for constructing arguments. In this work we define flexible dispute derivations with forward as well as backward reasoning allowing us, in particular, to also have dispute derivations for finding admissible, complete, and stable assumption sets rather than only determine acceptability of claims. We give an argumentation-based definition of such dispute derivations and a more implementation friendly alternative representation in which disputes involve exchange of claims and rules rather than arguments. These can be seen as elaborations on, in particular, existing graph-based dispute derivations on two fronts: first, in also allowing for forward reasoning; second, in that all arguments put forward in the dispute are represented by a graph and not only the proponents.

Rushing and Strolling among Answer Sets - Navigation Made Easy

Dominik Rusovac

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. 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.

Abstraction for non-ground answer set programs

Zeynep G. Saribatur

Abstraction is an important technique utilized by humans in model building and problem solving, in order to figure out key elements and relevant details of a world of interest. This naturally has led to investigations of using abstraction in AI and Computer Science to simplify problems, especially in the design of intelligent agents and automated problem solving. By omitting details, scenarios are reduced to ones that are easier to deal with and to understand, where further details are added back only when they matter. Despite the fact that abstraction is a powerful technique, it has not been considered much in the context of nonmonotonic knowledge representation and reasoning, and specifically not in Answer Set Programming (ASP), apart from some related simplification methods. In this work, we introduce a notion for abstracting from the domain of an ASP program such that the domain size shrinks while the set of answer sets (i.e., models) of the program is over-approximated. To achieve the latter, the program is transformed into an abstract program over the abstract domain while preserving the structure of the rules. We show in elaboration how this can be also achieved for single or multiple sub-domains (sorts) of a domain, and in case of structured domains like grid environments in which structure should be preserved. Furthermore, we introduce an abstraction-&-refinement methodology that makes it possible to start with an initial abstraction and to automatically achieve an abstraction with an associated abstract answer set that matches an answer set of the original program, provided that the program is satisfiable. Experiments based on prototypical implementations reveal the potential of the approach for problem analysis, by its ability to focus on the parts of the program that cause unsatisfiability and by achieving concrete abstract answer sets that merely reflect relevant details. This makes domain abstraction an interesting topic of research whose further use in important areas like Explainable AI remains to be explored.

Existential Abstraction on Argumentation Frameworks via Clustering

Johannes Wallner

Argumentation in Artificial Intelligence (AI) builds on formal approaches to reasoning argumentatively. Common to many such approaches is to use argumentation frameworks (AFs) as reasoning engines, with AFs being composed of arguments and attacks between arguments, which are instantiated from knowledge bases in a principle-based manner. While representing what can be argued for in an AF provides a conceptually clean way, this process can face challenges arising from generating a large number of arguments, which can act as a barrier to explainability. Inspired by successful approaches to model checking where the state explosion is mitigated by applying existential abstraction, we study an adaption of existential abstraction in form of clustering arguments in an AF to address an associated "argument explosion". In the paper on which this talk is based on, we provide a foundational investigation of this form of existential abstraction by defining semantics of the resulting clustered AFs, which balance two inherent aspects of existential abstractions: abstracting from concrete AFs and not permitting too much spuriousness (i.e., conclusions that hold on the abstraction but not on the original AF). Moreover, we show properties of clustered AFs, including complexity results, discuss use of clusterings for explaining results of reasoning tasks, and employ the recently introduced methodology of abstraction in answer set programming (ASP) for obtaining and reasoning over clustered AFs.

Utilizing Treewidth for Quantitative Reasoning on Epistemic Logic Programs

Viktor Besin

Extending the popular answer set programming paradigm by introspective reasoning capacities has received increasing interest within the last years. Particular attention is given to the formalism of epistemic logic programs (ELPs) where standard rules are equipped with modal operators which allow to express conditions on literals for being known or possible, that is, contained in all or some answer sets, respectively. ELPs thus deliver multiple collections of answer sets, known as world views. Employing ELPs for reasoning problems so far has mainly been restricted to standard decision problems (complexity analysis) and enumeration (development of systems) of world views. In this paper, we take a next step and contribute to epistemic logic programming in two ways: First, we establish quantitative reasoning for ELPs, where the acceptance of a certain set of literals depends on the number (proportion) of world views that are compatible with the set. Second, we present a novel system that is capable of efficiently solving the underlying counting problems required to answer such quantitative reasoning problems. Our system exploits the graph-based measure treewidth and works by iteratively finding and refining (graph) abstractions of an ELP program. On top of these abstractions, we apply dynamic programming that is combined with utilizing existing search-based solvers like (e)clingo for hard combinatorial subproblems that appear during solving. It turns out that our approach is competitive with existing systems that were introduced recently.

Approximate Answer Set Counting

Johannes Fichte

Answer Set Programming (ASP) is a framework in artificial intelligence and knowledge representation for declarative modeling and problem solving. Modern ASP solvers focus on the computation or enumeration of answer sets. However, a variety of probabilistic applications in reasoning or logic programming require counting answer sets. While counting can be done by enumeration, simple enumeration becomes immediately infeasible if the number of solutions is high. On the other hand, approaches to exact counting are of high worst-case complexity. In fact, in propositional model counting, exact counting becomes impractical. In this work, we present a scalable approach to approximate counting for ASP. Our approach is based on systematically adding parity (XOR) constraints to ASP programs, which divide the search space. We prove that adding random XOR constraints partitions the answer sets of an ASP program. In practice, we use a Gaussian elimination based approach by lifting ideas from SAT to ASP and integrate it into a state of the art ASP solver.

Finally, our experimental evaluation shows the scalability of our approach over existing ASP systems.