Arrow Research search

Author name cluster

Markus Hecher

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

46 papers
2 author rows

Possible papers

46

AAAI Conference 2026 Conference Paper

Structure-Aware Encodings of Argumentation Properties for Clique-width

  • Yasir Mahmood
  • Markus Hecher
  • Johanna Groven
  • Johannes K. Fichte

Structural measures of graphs, such as treewidth, are central tools in computational complexity resulting in efficient algorithms when exploiting the parameter. It is even known that modern SAT solvers work efficiently on instances of small treewidth. Since these solvers are widely applied, research interests in compact encodings into (Q)SAT for solving and to understand encoding limitations. Even more general is the graph parameter clique-width, which unlike treewidth can be small for dense graphs. Although algorithms are available for clique-width, little is known about encodings. We initiate the quest to understand encoding capabilities with clique-width by considering abstract argumentation, which is a robust framework for reasoning with conflicting arguments. It is based on directed graphs and asks for computationally challenging properties, making it a natural candidate to study computational properties. We design novel reductions from argumentation problems to (Q)SAT. Our reductions linearly preserve the clique-width, resulting in directed decomposition-guided (DDG) reductions. We establish novel results for all argumentation semantics, including counting. Notably, the overhead caused by our DDG reductions cannot be significantly improved under reasonable assumptions.

PDF Details DOI

AAAI Conference 2025 Conference Paper

Counting and Reasoning with Plans

  • David Speck
  • Markus Hecher
  • Daniel Gnad
  • Johannes K. Fichte
  • Augusto B. Corrêa

Classical planning asks for a sequence of operators reaching 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. Since counting 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 compilation to count different plans. This framework scales well to large plan spaces, while enabling rich reasoning capabilities such as learning pruning functions and explainable planning.

PDF Details DOI

KR Conference 2025 Conference Paper

Counting Solutions Under Cardinality Constraints: Structure Counts in Counting

  • Max Bannach
  • Markus Hecher

Model counting is a powerful extension of constraint reasoning that, instead of finding a solution to a constraint system, allows to identify the number of such solutions. Cardinality constraints are used to filter solutions of a certain quality by restricting the number of elements that can be added to the solution. Naturally, one would like to combine both in order to count the number of solutions of good quality. Unfortunately, the two concepts do not get along so well as (1) cardinality constraints may not be parsimonious (due to auxiliary variables, the system’s number of solutions may change in an uncontrolled way) and (2) such constraints may destroy structural properties, which are crucial for the performance of modern solvers. This article provides a systematic study of existing cardinality constraints in the light of model counting, observing that none of them are both, parsimonious and treewidth-preserving. We present structure-aware cardinality constraints that are parsimonious and guaranteed to increase the input’s treewidth only in a controlled way. Detailed experiments reveal that our encodings outperform existing ones.

PDF Details DOI

AAAI Conference 2025 Conference Paper

Dung’s Argumentation Framework: Unveiling the Expressive Power with Inconsistent Databases

  • Yasir Mahmood
  • Markus Hecher
  • Axel-Cyrille Ngonga Ngomo

The connection between inconsistent databases and Dung’s abstract argumentation framework has recently drawn growing interest. Specifically, an inconsistent database, involving certain types of integrity constraints such as functional and inclusion dependencies, can be viewed as an argumentation framework in Dung’s setting. Nevertheless, no prior work has explored the exact expressive power of Dung’s theory of argumentation when compared to inconsistent databases and integrity constraints. In this paper, we close this gap by arguing that an argumentation framework can also be viewed as an inconsistent database. We first establish a connection between subset-repairs for databases and extensions for AFs considering conflict-free, naive, admissible, and preferred semantics. Further, we define a new family of attribute-based repairs based on the principle of maximal content preservation. The effectiveness of these repairs is then highlighted by connecting them to stable, semi-stable, and stage semantics. Our main contributions include translating an argumentation framework into a database together with integrity constraints. Moreover, this translation can be achieved in polynomial time, which is essential in transferring complexity results between the two formalisms.

PDF Details DOI

IJCAI Conference 2025 Conference Paper

Facets in Argumentation: A Formal Approach to Argument Significance

  • Johannes K. Fichte
  • Nicolas Fröhlich
  • Markus Hecher
  • Victor Lagerkvist
  • Yasir Mahmood
  • Arne Meier
  • Jonathan Persson

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 arguments, such as stable or admissible. Today's solvers implement tasks such as finding extensions, deciding credulously or skeptically acceptance, counting, or enumerating extensions. While these tasks are well charted, the area between decision and 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 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.

PDF Details DOI

KR Conference 2025 Conference Paper

FastFound: Easing the ASP Bottleneck via Predicate-Decoupled Grounding

  • Alexander Beiser
  • Martin Gebser
  • Markus Hecher
  • Stefan Woltran

The grounding bottleneck in Answer Set Programming prohibits large instances from being solved. This is caused by a combinatorial explosion in the grounding phase of standard ground&solve systems. A promising alternative is Body-Decoupled Grounding (BDG), which grounds each body predicate on its own. However, BDG faces challenges in terms of worst-case grounding size and limited interoperability with other systems. This paper addresses shortcomings of BDG by introducing FastFound: an alternative foundedness check that significantly reduces grounding sizes, by grounding each predicate on its own. FastFound’s foundedness check is done implicitly, which leads to a quadratic reduction in grounding size. We start by introducing FastFound for tight normal rules, where we observe that this cannot be substantially improved. Then we extend FastFound to head-cycle-free programs and give novel interoperability results for full disjunctive programs. An experimental evaluation on our prototype shows promising results, as we solve more grounding-heavy tasks than both standard ground&solve systems and BDG.

PDF Details DOI

KR Conference 2025 System Paper

Interactive Exploration of Plan Spaces

  • Daniel Gnad
  • Markus Hecher
  • Sarah Alice Gaggl
  • Dominik Rusovac
  • David Speck
  • Johannes K. Fichte

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.

PDF Details DOI

KR Conference 2025 Conference Paper

Reasoning with Restricted Statistical Statements in Probabilistic Answer Set Programming: Complexity and Algorithms

  • Damiano Azzolini
  • Markus Hecher

Statistical statements are an expressive tool for representing statistical information of a domain of interest. Recently, these statements were given a meaning in the context of Probabilistic Answer Set Programming (PASP), allowing one to encode properties like "x% of elements of a domain have the feature y". Although the computational complexity of different tasks in PASP is well known, the complexity of restricted programs composed only of statistical statements and probabilistic facts has not been studied. As a first contribution, we address this problem, confirming that even in seemingly restricted cases the complexity is high. Indeed, even with this restriction we do not lose expressiveness, reaching higher levels of the polynomial hierarchy. To mitigate these high complexities, we focus on the structure of the programs. Thereby, we design novel structure-guided reductions, demonstrating how one can efficiently answer queries along treewidth decompositions. We obtain precise upper bounds and we show that under reasonable assumptions in complexity theory we cannot significantly improve, as we give matching lower bounds.

PDF Details DOI

AIJ Journal 2024 Journal Article

aspmc: New frontiers of algebraic answer set counting

  • Thomas Eiter
  • Markus Hecher
  • Rafael Kiesel

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 efficient solvers for AASC desirable. In this article, we present Image 1, a new solver for AASC that pushes the limits of efficient solvability. Notably, Image 1 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 T P -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 Image 1, T P -Unfolding improves performance significantly by allowing us to handle cyclic instances better.

Details DOI

IJCAI Conference 2024 Conference Paper

Bypassing the ASP Bottleneck: Hybrid Grounding by Splitting and Rewriting

  • Alexander Beiser
  • Markus Hecher
  • Kaan Unalan
  • Stefan Woltran

Answer Set Programming (ASP) is a key paradigm for problems in artificial intelligence and industrial contexts. In ASP, problems are modeled via a set of rules. Over the time this paradigm grew into a rich language, enabling complex rule types like aggregate expressions. Most practical ASP systems follow a ground-and-solve pattern, where rule schemes are grounded and resulting rules are solved. There, the so-called grounding bottleneck may prevent from solving, due to sheer grounding sizes. Recently body-decoupled grounding (BDG) demonstrated how to reduce grounding sizes by delegating effort to solving. However, BDG provides limited interoperability with traditional grounders and only covers simple rule types. In this work, we establish hybrid grounding — based on a novel splitting theorem that allows us to freely combine BDG with traditional grounders. To mitigate huge groundings in practice, we define rewriting procedures for efficiently deferring grounding effort of aggregates to solving. Our experimental results indicate that this approach is competitive, especially for instances, where traditional grounding fails.

PDF Details DOI

JAIR Journal 2024 Journal Article

Counting Complexity for Reasoning in Abstract Argumentation

  • Johannes K. Fichte
  • Markus Hecher
  • Arne Meier

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

PDF Details DOI

IJCAI Conference 2024 Conference Paper

Epistemic Logic Programs: Non-Ground and Counting Complexity

  • Thomas Eiter
  • Johannes K. Fichte
  • Markus Hecher
  • Stefan Woltran

Answer Set Programming (ASP) is a prominent problem-modeling and solving framework, whose solutions are called answer sets. Epistemic logic programs (ELP) extend ASP to reason about all or some answer sets. Solutions to an ELP can be seen as consequences over multiple collections of answer sets, known as world views. While the complexity of propositional programs is well studied, the non-ground case remains open. This paper establishes the 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, we establish complexity results for counting complexity beyond #EXP. To mitigate high complexity, we establish 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 parameter treewidth, which has applications in quantitative reasoning, where we reason on (marginal) probabilities of epistemic literals.

PDF Details DOI

IJCAI Conference 2024 Conference Paper

Finite Groundings for ASP with Functions: A Journey through Consistency

  • Lukas Gerlach
  • David Carral
  • Markus Hecher

Answer set programming (ASP) is a logic programming formalism used in various areas of artificial intelligence like combinatorial problem solving and knowledge representation and reasoning. It is known that enhancing ASP with function symbols makes basic reasoning problems highly undecidable. However, even in simple cases, state of the art reasoners, specifically those relying on a ground-and-solve approach, fail to produce a result. Therefore, we reconsider consistency as a basic reasoning problem for ASP. We show reductions that give an intuition for the high level of undecidability. These insights allow for a more fine-grained analysis where we characterize ASP programs as "frugal" and "non-proliferous". For such programs, we are not only able to semi-decide consistency but we also propose a grounding procedure that yields finite groundings on more ASP programs with the concept of "forbidden" facts.

PDF Details DOI

NMR Workshop 2024 Conference Paper

Finite Groundings for ASP with Functions: A Journey through Consistency (Extended Abstract)

  • Lukas Gerlach 0002
  • David Carral
  • Markus Hecher

Answer set programming (ASP) is a logic programming formalism used in various areas of artificial intelligence like combinatorial problem solving and knowledge representation and reasoning. It is known that enhancing ASP with function symbols makes basic reasoning problems highly undecidable. However, even in simple cases, state of the art reasoners, specifically those relying on a ground-and-solve approach, fail to produce a result. Therefore, we reconsider consistency as a basic reasoning problem for ASP. We show reductions that give an intuition for the high level of undecidability. These insights allow for a more fine-grained analysis where we characterize ASP programs as “frugal” and “non-proliferous”. For such programs, we are not only able to semi-decide consistency but we also propose a grounding procedure that yields finite groundings on more ASP programs with the concept of “forbidden” facts.

Details

KR Conference 2024 Conference Paper

Navigating and Querying Answer Sets: How Hard Is It Really and Why?

  • Dominik Rusovac
  • Markus Hecher
  • Martin Gebser
  • Sarah Alice Gaggl
  • Johannes K. Fichte

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.

PDF Details DOI

AAAI Conference 2024 Conference Paper

On the Structural Hardness of Answer Set Programming: Can Structure Efficiently Confine the Power of Disjunctions?

  • Markus Hecher
  • Rafael Kiesel

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.

PDF Details DOI

AAAI Conference 2024 Conference Paper

Parallel Empirical Evaluations: Resilience despite Concurrency

  • Johannes K. Fichte
  • Tobias Geibinger
  • Markus Hecher
  • Matthias Schlögel

Computational evaluations are crucial in modern problem-solving when we surpass theoretical algorithms or bounds. These experiments frequently take much work, and the sheer amount of needed resources makes it impossible to execute them on a single personal computer or laptop. Cluster schedulers allow for automatizing these tasks and scale to many computers. But, when we evaluate implementations of combinatorial algorithms, we depend on stable runtime results. Common approaches either limit parallelism or suffer from unstable runtime measurements due to interference among jobs on modern hardware. The former is inefficient and not sustainable. The latter results in unreplicable experiments. In this work, we address this issue and offer an acceptable balance between efficiency, software, hardware complexity, reliability, and replicability. We investigate effects towards replicability stability and illustrate how to efficiently use widely employed cluster resources for parallel evaluations. Furthermore, we present solutions which mitigate issues that emerge from the concurrent execution of benchmark jobs. Our experimental evaluation shows that – despite parallel execution – our approach reduces the runtime instability on the majority of instances to one second.

PDF Details DOI

IJCAI Conference 2024 Conference Paper

Quantitative Claim-Centric Reasoning in Logic-Based Argumentation

  • Markus Hecher
  • Yasir Mahmood
  • Arne Meier
  • Johannes Schmidt

Argumentation is a well-established formalism for nonmonotonic reasoning, with popular frameworks being Dung’s abstract argumentation (AFs) or logic-based argumentation (Besnard-Hunter’s framework). Structurally, a set of formulas forms support for a claim if it is consistent, subset-minimal, and implies the claim. Then, an argument comprises support and a claim. We observe that the computational task (ARG) of asking for support of a claim in a knowledge base is “brave”, since many claims with a single support are accepted. As a result, ARG falls short when it comes to the question of confidence in a claim, or claim strength. In this paper, we propose a concept for measuring the (acceptance) strength of claims, based on counting supports for a claim. Further, we settle classical and structural complexity of counting arguments favoring a given claim in propositional knowledge bases (KBs). We introduce quantitative reasoning to measure the strength of claims in a KB and to determine the relevance strength of a formula for a claim.

PDF Details DOI

ECAI Conference 2024 Conference Paper

Rejection in Abstract Argumentation: Harder Than Acceptance?

  • Johannes Klaus Fichte
  • Markus Hecher
  • Yasir Mahmood 0002
  • Arne Meier

Abstract argumentation is a popular toolkit for modeling, evaluating, and comparing arguments. Relationships between arguments are specified in argumentation frameworks (AFs), and conditions are placed on sets (extensions) of arguments that allow AFs to be evaluated. For more expressiveness, AFs are augmented with acceptance conditions on directly interacting arguments or a constraint on the admissible sets of arguments, resulting in dialectic frameworks or constrained argumentation frameworks. In this paper, we consider flexible conditions for rejecting an argument from an extension, which we call rejection conditions (RCs). On the technical level, we associate each argument with a specific logic program. We analyze the resulting complexity, including the structural parameter treewidth. Rejection AFs are highly expressive, giving rise to natural problems on higher levels of the polynomial hierarchy.

Details

SAT Conference 2024 Conference Paper

The Relative Strength of #SAT Proof Systems

  • Olaf Beyersdorff
  • Johannes Klaus Fichte
  • Markus Hecher
  • Tim Hoffmann
  • Kaspar Kasche

The propositional model counting problem #SAT asks to compute the number of satisfying assignments for a given propositional formula. Recently, three #SAT proof systems kcps (knowledge compilation proof system), MICE (model counting induction by claim extension), and CPOG (certified partitioned-operation graphs) have been introduced with the aim to model #SAT solving and enable proof logging for solvers. Prior to this paper, the relations between these proof systems have been unclear and very few proof complexity results are known. We completely determine the simulation order of the three systems, establishing that CPOG simulates both MICE and kcps, while MICE and kcps are exponentially incomparable. This implies that CPOG is strictly stronger than the other two systems.

Details

AAAI Conference 2023 Conference Paper

Characterizing Structural Hardness of Logic Programs: What Makes Cycles and Reachability Hard for Treewidth?

  • Markus Hecher

Answer Set Programming (ASP) is a problem modeling and solving framework for several problems in KR with growing industrial applications. Also for studies of computational complexity and deeper insights into the hardness and its sources, ASP has been attracting researchers for many years. These studies resulted in fruitful characterizations in terms of complexity classes, fine-grained insights in form of dichotomy-style results, as well as detailed parameterized complexity landscapes. Recently, this lead to a novel result establishing that for the measure treewidth, which captures structural density of a program, the evaluation of the well-known class of normal programs is expected to be slightly harder than deciding satisfiability (SAT). However, it is unclear how to utilize this structural power of ASP. This paper deals with a novel reduction from SAT to normal ASP that goes beyond well-known encodings: We explicitly utilize the structural power of ASP, whereby we sublinearly decrease the treewidth, which probably cannot be significantly improved. Then, compared to existing results, this characterizes hardness in a fine-grained way by establishing the required functional dependency of the dependency graph’s cycle length (SCC size) on the treewidth.

PDF Details DOI

ICAPS Conference 2023 Conference Paper

Grounding Planning Tasks Using Tree Decompositions and Iterated Solving

  • Augusto B. Corrêa
  • Markus Hecher
  • Malte Helmert
  • Davide Mario Longo
  • Florian Pommerening
  • Stefan Woltran

Classical planning tasks are commonly described in a first-order language. However, most classical planners translate tasks by grounding them and then rewriting them into a propositional language. In recent years, the grounding step has become a larger bottleneck. In this work, we study how to improve it. We build on top of the most common grounder for planning tasks which uses Datalog to find all reachable atoms and actions. Inspired by recent progress in lifted planning, database theory, and algorithmics, we develop a new method to ground these Datalog programs. Our algorithm can ground more instances than the baseline, and most tasks it cannot ground are out of reach from any ground planner.

Details

AAAI Conference 2023 Conference Paper

Inconsistent Cores for ASP: The Perks and Perils of Non-monotonicity

  • Johannes K. Fichte
  • Markus Hecher
  • Stefan Szeider

Answer Set Programming (ASP) is a prominent modeling and solving framework. An inconsistent core (IC) of an ASP program is an inconsistent subset of rules. In the case of inconsistent programs, a smallest or subset-minimal IC contains crucial rules for the inconsistency. In this work, we study fnding minimal ICs of ASP programs and key fragments from a complexity-theoretic perspective. Interestingly, due to ASP’s non-monotonic behavior, also consistent programs admit ICs. It turns out that there is an entire landscape of problems involving ICs with a diverse range of complexities up to the fourth level of the Polynomial Hierarchy. Deciding the existence of an IC is, already for tight programs, on the second level of the Polynomial Hierarchy. Furthermore, we give encodings for IC-related problems on the fragment of tight programs and illustrate feasibility on small instance sets.

PDF Details DOI

ECAI Conference 2023 Conference Paper

On the Structural Complexity of Grounding - Tackling the ASP Grounding Bottleneck via Epistemic Programs and Treewidth

  • Viktor Besin
  • Markus Hecher
  • Stefan Woltran

Answer Set Programming is widely applied research area for knowledge representation and for solving industrial domains. One of the challenges of this formalism focuses on the so-called grounding bottleneck, which addresses the efficient replacement of first-order variables by means of domain values. Recently, there have been several works in this direction, ranging from lazy grounding, hybrid solving, over translational approaches. Inspired by a translation from non-ground normal programs to ground disjunctive programs, we attack the grounding bottleneck from a more general angle. We provide a polynomial reduction for grounding disjunctive programs of bounded domain size by reducing to propositional epistemic logic programs (ELPs). By slightly adapting our reduction, we show new complexity results for non-ground programs that adhere to the measure treewidth. We complement these results by matching lower bounds under the exponential time hypothesis, ruling out significantly better algorithms.

Details

IJCAI Conference 2023 Conference Paper

Quantitative Reasoning and Structural Complexity for Claim-Centric Argumentation

  • Johannes K. Fichte
  • Markus Hecher
  • Yasir Mahmood
  • Arne Meier

Argumentation is a well-established formalism for nonmonotonic reasoning and a vibrant area of research in AI. Claim-augmented argumentation frameworks (CAFs) have been introduced to deploy a conclusion-oriented perspective. CAFs expand argumentation frameworks by an additional step which involves retaining claims for an accepted set of arguments. We introduce a novel concept of a justification status for claims, a quantitative measure of extensions supporting a particular claim. The well-studied problems of credulous and skeptical reasoning can then be seen as simply the two endpoints of the spectrum when considered as a justification level of a claim. Furthermore, we explore the parameterized complexity of various reasoning problems for CAFs, including the quantitative reasoning for claim assertions. We begin by presenting a suitable graph representation that includes arguments and their associated claims. Our analysis includes the parameter treewidth, and we present decomposition-guided reductions between reasoning problems in CAF and the validity problem for QBF.

PDF Details DOI

AIJ Journal 2023 Journal Article

Solving Projected Model Counting by Utilizing Treewidth and its Limits

  • Johannes K. Fichte
  • Markus Hecher
  • Michael Morak
  • Patrick Thier
  • Stefan Woltran

In this paper, we introduce a novel algorithm to solve projected model counting (PMC). PMC asks to count solutions of a Boolean formula with respect to a given set of projection variables, where multiple solutions that are identical when restricted to the projection variables count as only one solution. Inspired by the observation that the so-called “treewidth” is one of the most prominent structural parameters, our algorithm utilizes small treewidth of the primal graph of the input instance. More precisely, it runs in time O ( 2 2 k + 4 n 2 ) where k is the treewidth and n is the input size of the instance. In other words, we obtain that the problem PMC is fixed-parameter tractable when parameterized by treewidth. Further, we take the exponential time hypothesis (ETH) into consideration and establish lower bounds of bounded treewidth algorithms for PMC, yielding asymptotically tight runtime bounds of our algorithm. While the algorithm above serves as a first theoretical upper bound and although it might be quite appealing for small values of k, unsurprisingly a naive implementation adhering to this runtime bound suffers already from instances of relatively small width. Therefore, we turn our attention to several measures in order to resolve this issue towards exploiting treewidth in practice: We present a technique called nested dynamic programming, where different levels of abstractions of the primal graph are used to (recursively) compute and refine tree decompositions of a given instance. Further, we integrate the concept of hybrid solving, where subproblems hidden by the abstraction are solved by classical search-based solvers, which leads to an interleaving of parameterized and classical solving. Finally, we provide a nested dynamic programming algorithm and an implementation that relies on database technology for PMC and a prominent special case of PMC, namely model counting (#Sat). Experiments indicate that the advancements are promising, allowing us to solve instances of treewidth upper bounds beyond 200.

Details DOI

KR Conference 2023 Conference Paper

The Impact of Structure in Answer Set Counting: Fighting Cycles and its Limits

  • Markus Hecher
  • Rafael Kiesel

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.

PDF Details DOI

IJCAI Conference 2023 Conference Paper

Treewidth-Aware Complexity for Evaluating Epistemic Logic Programs

  • Jorge Fandinno
  • Markus Hecher

Logic programs are a popular formalism for encoding many problems relevant to knowledge representation and reasoning as well as artificial intelligence. However, for modeling rational behavior it is oftentimes required to represent the concepts of knowledge and possibility. Epistemic logic programs (ELPs) is such an extension that enables both concepts, which correspond to being true in all or some possible worlds or stable models. For these programs, the parameter treewidth has recently regained popularity. We present complexity results for the evaluation of key ELP fragments for treewidth, which are exponentially better than known results for full ELPs. Unfortunately, we prove that obtained runtimes can not be significantly improved, assuming the exponential time hypothesis. Our approach defines treewidth-aware reductions between quantified Boolean formulas and ELPs. We also establish that the completion of a program, as used in modern solvers, can be turned treewidth-aware, thereby linearly preserving treewidth.

PDF Details DOI

AAAI Conference 2022 Conference Paper

ApproxASP – a Scalable Approximate Answer Set Counter

  • Mohimenul Kabir
  • Flavio O Everardo
  • Ankit K Shukla
  • Markus Hecher
  • Johannes Klaus Fichte
  • Kuldeep S Meel

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 eliminationbased approach by lifting ideas from SAT to ASP and integrate it into a state of the art ASP solver, which we call ApproxASP. Finally, our experimental evaluation shows the scalability of our approach over existing ASP systems.

PDF Details

IJCAI Conference 2022 Conference Paper

Body-Decoupled Grounding via Solving: A Novel Approach on the ASP Bottleneck

  • Viktor Besin
  • Markus Hecher
  • Stefan Woltran

Answer-Set Programming (ASP) has seen tremendous progress over the last two decades and is nowadays successfully applied in many real-world domains. However, for certain types of problems, the well-known ASP grounding bottleneck still causes severe problems. This becomes virulent when grounding of rules, where the variables have to be replaced by constants, leads to a ground pro- gram that is too huge to be processed by the ASP solver. In this work, we tackle this problem by a novel method that decouples non-ground atoms in rules in order to delegate the evaluation of rule bodies to the solving process. Our procedure translates a non-ground normal program into a ground disjunctive program that is exponential only in the maximum predicate arity, and thus polynomial if this arity is assumed to be bounded by a constant. We demonstrate the feasibility of this new method experimentally by comparing it to standard ASP technology in terms of grounding size, grounding time and total runtime.

PDF Details DOI

IJCAI Conference 2022 Conference Paper

Plausibility Reasoning via Projected Answer Set Counting - A Hybrid Approach

  • Johannes K. Fichte
  • Markus Hecher
  • Mohamed A. Nadeem

Answer set programming is a form of declarative programming widely used to solve difficult search problems. Probabilistic applications however require to go beyond simple search for one solution and need counting. One such application is plausibility reasoning, which provides more fine-grained reasoning mode between simple brave and cautious reasoning. When modeling with ASP, we oftentimes introduce auxiliary atoms in the program. If these atoms are functionally independent of the atoms of interest, we need to hide the auxiliary atoms and project the count to the atoms of interest resulting in the problem projected answer set counting. In practice, counting becomes quickly infeasible with standard systems such as clasp. In this paper, we present a novel hybrid approach for plausibility reasoning under projections, thereby relying on projected answer set counting as basis. Our approach combines existing systems with fast dynamic programming, which in our experiments shows advantages over existing ASP systems.

PDF Details DOI

SAT Conference 2022 Conference Paper

Proofs for Propositional Model Counting

  • Johannes Klaus Fichte
  • Markus Hecher
  • Valentin Roland

Although propositional model counting (#SAT) was long considered too hard to be practical, today’s highly efficient solvers facilitate applications in probabilistic reasoning, reliability estimation, quantitative design space exploration, and more. The current trend of solvers growing more capable every year is likely to continue as a diverse range of algorithms are explored in the field. However, to establish model counters as reliable tools like SAT-solvers, correctness is as critical as speed. As in the nature of complex systems, bugs emerge as soon as the tools are widely used. To identify and avoid bugs, explain decisions, and provide trustworthy results, we need verifiable results. We propose a novel system for certifying model counts. We show how proof traces can be generated for exact model counters based on dynamic programming, counting CDCL with component caching, and knowledge compilation to Decision-DNNF, which are the predominant techniques in today’s exact implementations. We provide proof-of-concepts for emitting proofs and a parallel trace checker. Based on this, we show the feasibility of using certified model counting in an empirical experiment.

Details

AAAI Conference 2022 Conference Paper

Tractable Abstract Argumentation via Backdoor-Treewidth

  • Wolfgang Dvořák
  • Markus Hecher
  • Matthias König
  • André Schidler
  • Stefan Szeider
  • Stefan Woltran

Argumentation frameworks (AFs) are a core formalism in the field of formal argumentation. As most standard computational tasks regarding AFs are hard for the first or second level of the Polynomial Hierarchy, a variety of algorithmic approaches to achieve manageable runtimes have been considered in the past. Among them, the backdoor-approach and the treewidth-approach turned out to yield fixed-parameter tractable fragments. However, many applications yield high parameter values for these methods, often rendering them infeasible in practice. We introduce the backdoor-treewidth approach for abstract argumentation, combining the best of both worlds with a guaranteed parameter value that does not exceed the minimum of the backdoor- and treewidth-parameter. In particular, we formally define backdoor-treewidth and establish fixed-parameter tractability for standard reasoning tasks of abstract argumentation. Moreover, we provide systems to find and exploit backdoors of small width, and conduct systematic experiments evaluating the new parameter.

PDF Details

AIJ Journal 2022 Journal Article

Treewidth-aware reductions of normal ASP to SAT – Is normal ASP harder than SAT after all?

  • Markus Hecher

Answer Set Programming (ASP) is a paradigm for modeling and solving problems for knowledge representation and reasoning. There are plenty of results dedicated to studying the hardness of (fragments of) ASP. So far, these studies resulted in characterizations in terms of computational complexity as well as in fine-grained insights presented in form of dichotomy-style results, lower bounds when translating to other formalisms like propositional satisfiability (SAT), and even detailed parameterized complexity landscapes. A generic parameter in parameterized complexity originating from graph theory is the so-called treewidth, which in a sense captures structural density of a program. Recently, there was an increase in the number of treewidth-based solvers related to SAT. While there are translations from (normal) ASP to SAT, no reduction that preserves treewidth or at least keeps track of the treewidth increase is known. In this paper we propose a novel reduction from normal ASP to SAT that is aware of the treewidth, and guarantees that a slight increase of treewidth is indeed sufficient. Further, we show a new result establishing that, when considering treewidth, already the fragment of normal ASP is slightly harder than SAT (under reasonable assumptions in computational complexity). This also confirms that our reduction probably cannot be significantly improved and that the slight increase of treewidth is unavoidable. Finally, we present an empirical study of our novel reduction from normal ASP to SAT, where we compare treewidth upper bounds that are obtained via known decomposition heuristics. Overall, our reduction works better with these heuristics than existing translations.

Details DOI

IJCAI Conference 2022 Conference Paper

Utilizing Treewidth for Quantitative Reasoning on Epistemic Logic Programs (Extended Abstract)

  • Viktor Besin
  • Markus Hecher
  • Stefan Woltran

Extending the popular Answer Set Programming (ASP) 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, i. e. , 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 deci- sion problems (complexity analysis) and enumeration (development of systems) of world views. In this paper, we first 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 capable of efficiently solving the underlying counting problems required for quantitative reasoning. Our system exploits the graph-based measure treewidth by iteratively finding (graph) abstractions of ELPs.

PDF Details DOI

IJCAI Conference 2021 Conference Paper

Decomposition-Guided Reductions for Argumentation and Treewidth

  • Johannes Fichte
  • Markus Hecher
  • Yasir Mahmood
  • Arne Meier

Argumentation is a widely applied framework for modeling and evaluating arguments and its reasoning with various applications. Popular frameworks are abstract argumentation (Dung’s framework) or logic-based argumentation (Besnard-Hunter’s framework). Their computational complexity has been studied quite in-depth. Incorporating treewidth into the complexity analysis is particularly interesting, as solvers oftentimes employ SAT-based solvers, which can solve instances of low treewidth fast. In this paper, we address whether one can design reductions from argumentation problems to SAT-problems while linearly preserving the treewidth, which results in decomposition-guided (DG) reductions. It turns out that the linear treewidth overhead caused by our DG reductions, cannot be significantly improved under reasonable assumptions. Finally, we consider logic-based argumentation and establish new upper bounds using DG reductions and lower bounds.

PDF Details DOI

AAAI Conference 2021 Conference Paper

Knowledge-Base Degrees of Inconsistency: Complexity and Counting

  • Johannes K. Fichte
  • Markus Hecher
  • Arne Meier

Description logics (DLs) are knowledge representation languages that are used in the field of artificial intelligence (AI). A common technique is to query DL knowledge-bases, e. g. , by Boolean Datalog queries, and ask for entailment. But real world knowledge-bases often have a certain inconsistency (with respect to a given query) or we are required to estimate a degree of inconsistency when using a knowledge-base. In this paper, we provide a complexity analysis of fixed-domain nonentailment (NE) on Datalog programs for well-established families of knowledge-bases (KBs). We exhibit a detailed complexity map for the decision cases, counting and projected counting, which may serve as a quantitative measure for inconsistency of a KB with respect to a query. Our results show that NE is natural for the second, third, and fourth level of the polynomial (counting) hierarchy depending on the type of the studied query (stratified, tight, normal, disjunctive) and one level higher for the projected versions. Further, we show fixed-parameter tractability by bounding the treewidth, provide a constructive algorithm, and show its theoretical limitation in terms of conditional lower bounds.

PDF Details

AAAI Conference 2021 Conference Paper

Treewidth-Aware Complexity in ASP: Not all Positive Cycles are Equally Hard

  • Jorge Fandinno
  • Markus Hecher

It is well-known that deciding consistency for normal answer set programs (ASP) is NP-complete, thus, as hard as the satisfaction problem for propositional logic (SAT). The exponential time hypothesis (ETH) implies that the best algorithms to solve these problems take exponential time in the worst case. However, accounting for the treewidth, the consistency problem for ASP is slightly harder than SAT: while SAT can be solved by an algorithm that runs in exponential time in the treewidth k, normal ASP requires exponential time in k ·log(k). This extra cost is due to checking that there are no self-supported true atoms because of positive cycles in the program. In this paper, we refine this recent result and show that consistency for ASP can be decided in exponential time in k · log(ι) where ι is a novel measure, bounded by both treewidth k and the size ` of the largest strongly-connected component of the positive dependency graph of the program. We provide a treewidth-aware reduction from ASP to SAT that adheres to the above limit.

PDF Details

KR Conference 2021 Conference Paper

Treewidth-Aware Cycle Breaking for Algebraic Answer Set Counting

  • Thomas Eiter
  • Markus Hecher
  • Rafael Kiesel

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.

PDF Details DOI

AAAI Conference 2020 Conference Paper

Structural Decompositions of Epistemic Logic Programs

  • Markus Hecher
  • Michael Morak
  • Stefan Woltran

Epistemic logic programs (ELPs) are a popular generalization of standard Answer Set Programming (ASP) providing means for reasoning over answer sets within the language. This richer formalism comes at the price of higher computational complexity reaching up to the fourth level of the polynomial hierarchy. However, in contrast to standard ASP, dedicated investigations towards tractability have not been undertaken yet. In this paper, we give first results in this direction and show that central ELP problems can be solved in linear time for ELPs exhibiting structural properties in terms of bounded treewidth. We also provide a full dynamic programming algorithm that adheres to these bounds. Finally, we show that applying treewidth to a novel dependency structure—given in terms of epistemic literals—allows to bound the number of ASP solver calls in typical ELP solving procedures.

PDF Details

SAT Conference 2020 Conference Paper

Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology

  • Markus Hecher
  • Patrick Thier
  • Stefan Woltran

Abstract Treewidth is one of the most prominent structural parameters. While numerous theoretical results establish tractability under the assumption of fixed treewidth, the practical success of exploiting this parameter is far behind what theoretical runtime bounds have promised. In particular, a naive application of dynamic programming (DP) on tree decompositions (TDs) suffers already from instances of medium width. In this paper, we present several measures to advance this paradigm towards general applicability in practice: We present nested DP, where different levels of abstractions are used to (recursively) compute TDs of a given instance. Further, we integrate the concept of hybrid solving, where subproblems hidden by the abstraction are solved by classical search-based solvers, which leads to an interleaving of parameterized and classical solving. Finally, we provide nested DP algorithms and implementations relying on database technology for variants and extensions of Boolean satisfiability. Experiments indicate that the advancements are promising.

Details

KR Conference 2020 Conference Paper

Treewidth-aware Reductions of Normal ASP to SAT - Is Normal ASP Harder than SAT after All?

  • Markus Hecher

Answer Set Programming (ASP) is a paradigm and problem modeling/solving toolkit for KR that is often invoked. There are plenty of results dedicated to studying the hardness of (fragments of) ASP. So far, these studies resulted in characterizations in terms of computational complexity as well as in fine-grained insights presented in form of dichotomy-style results, lower bounds when translating to other formalisms like propositional satisfiability (SAT), and even detailed parameterized complexity landscapes. A quite generic and prominent parameter in parameterized complexity originating from graph theory is the so-called treewidth, which in a sense captures structural density of a program. Recently, there was an increase in the number of treewidth-based solvers related to SAT. While there exist several translations from (normal) ASP to SAT, yet there is no reduction preserving treewidth or at least being aware of the treewidth increase. This paper deals with a novel reduction from normal ASP to SAT that is aware of the treewidth, and guarantees that a slight increase of treewidth is indeed sufficient. Then, we also present a new result establishing that when considering treewidth, already the fragment of normal ASP is slightly harder than SAT (under reasonable assumptions in computational complexity). This also confirms that our reduction probably cannot be significantly improved and that the slight increase of treewidth is unavoidable.

PDF Details DOI

AAAI Conference 2019 Conference Paper

Counting Complexity for Reasoning in Abstract Argumentation

  • Johannes K. Fichte
  • Markus Hecher
  • Arne Meier

In this paper, we consider counting and projected model counting of extensions in abstract argumentation for various semantics. 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 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 (DP). Our algorithms run in time double or triple exponential in the treewidth depending on the considered semantics. Finally, we take the exponential time hypothesis (ETH) into account and establish lower bounds of bounded treewidth algorithms for counting extensions and projected extension.

PDF Details

KR Conference 2018 Short Paper

Exploiting Treewidth for Counting Projected Answer Sets

  • Johannes K. Fichte
  • Markus Hecher

Answer Set Programming (ASP) is an active research area of artificial intelligence. We consider the problem projected answer set counting (#PDA) for disjunctive propositional ASP. #PDA asks to count the number of answer sets with respect to a given set of projected atoms, where multiple answer sets that are identical when restricted to the projected atoms count as only one projected answer set. Our approach exploits small treewidth of the primal graph of the input instance. Finally, we state a hypothesis (3ETH) that one cannot solve 3-QBF in polynomial time in the instance size while being significantly better than triple exponential in the treewidth. Taking 3ETH into account, we show that one can not expect to solve #PDA significantly better than triple exponential in the treewidth.

SAT Conference 2018 Conference Paper

Exploiting Treewidth for Projected Model Counting and Its Limits

  • Johannes Klaus Fichte
  • Markus Hecher
  • Michael Morak
  • Stefan Woltran

Abstract In this paper, we introduce a novel algorithm to solve projected model counting ( PMC ). PMC asks to count solutions of a Boolean formula with respect to a given set of projected variables, where multiple solutions that are identical when restricted to the projected variables count as only one solution. Our algorithm exploits small treewidth of the primal graph of the input instance. It runs in time \({\mathcal O}(2^{2^{k+4}} n^2)\) where k is the treewidth and n is the input size of the instance. In other words, we obtain that the problem PMC is fixed-parameter tractable when parameterized by treewidth. Further, we take the exponential time hypothesis (ETH) into consideration and establish lower bounds of bounded treewidth algorithms for PMC, yielding asymptotically tight runtime bounds of our algorithm.

Details

JELIA Conference 2014 Conference Paper

The D-FLAT System for Dynamic Programming on Tree Decompositions

  • Michael Abseher
  • Bernhard Bliem
  • Günther Charwat
  • Frederico Dusberger
  • Markus Hecher
  • Stefan Woltran

Abstract Complex reasoning problems over large amounts of data pose a great challenge for computer science. To overcome the obstacle of high computational complexity, exploiting structure by means of tree decompositions has proved to be effective in many cases. However, the implementation of suitable efficient algorithms is often tedious. D-FLAT is a software system that combines the logic programming language Answer Set Programming with problem solving on tree decompositions and can serve as a rapid prototyping tool for such algorithms. Since we initially proposed D-FLAT, we have made major changes to the system, improving its range of applicability and its usability. In this paper, we present the system resulting from these efforts.

Details