Author name cluster

Andreas Niskanen

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.

32 papers

2 author rows

AAMAS Conference 2025 Conference Paper

Computing Efficient and Envy-Free Allocations under Dichotomous Preferences using SAT

Ari Conati
Andreas Niskanen
Ronald de Haan
Matti Järvisalo

We study the problems of computing envy-free Pareto-efficient allocations in the context of fair allocation and hedonic games under dichotomous preferences. We establish Σ p 2-completeness of deciding the existence of envy-free Pareto-efficient allocations, refining earlier related results. We also develop iterative SAT-based exact algorithms for computing envy-free Pareto-efficient allocations, and extend the approach to computing minimum-envy Pareto-efficient allocations under different combinations of aggregation functions. We provide open-source implementations of the algorithms and show empirically that the approach scales to computing envy-free Pareto-efficient allocations up to hundreds of agents.

PDF

KR Conference 2025 Conference Paper

Cost-Optimal Delete-Free Classical Planning via Maximum Satisfiability

Masood Feyzbakhsh Rankooh
Andreas Niskanen
Matti Järvisalo

We propose a maximum satisfiability (MaxSAT) based approach to cost-optimal delete-free planning, also known as optimal relaxed planning. Relaxed planning is a central subclass of classical planning, consisting of computing the h+ heuristic for classical planning. As an alternative to the existing approaches to exactly computing h+, we propose a maximum satisfiability (MaxSAT) based approach, motivated by the success of SAT-based planners and significant recent advances in MaxSAT solvers. Concretely, we both adapt a recent answer set optimization approach to computing h+ for MaxSAT, propose further MaxSAT encoding variants for both representing cost-optimal plans and plan acyclicity, and combine them for further runtime improvements. Overall, our MaxSAT approach compares favourably to the current state-of-the-art answer set optimization approach.

PDF Details DOI

AIJ Journal 2025 Journal Article

ICCMA 2023: 5th International Competition on Computational Models of Argumentation

Matti Järvisalo
Tuomo Lehtonen
Andreas Niskanen

The study of computational models of argumentation and the development of practical automated approaches to reasoning over the models has developed into a vibrant area of artificial intelligence research in recent years. The series of International Competitions on Computational Models of Argumentation (ICCMA) aims at nurturing research and development of practical reasoning algorithms for models of argumentation. Organized biennially, the ICCMA competitions provide a snapshot of the current state of the art in algorithm implementations for central fundamental reasoning tasks over models of argumentation. The year 2023 marked the 5th instantiation of International Competitions on Computational Models of Argumentation, ICCMA 2023. We provide a comprehensive overview of ICCMA 2023, including details on the various new developments introduced in 2023, overview of the participating solvers, extensive details on the competition benchmarks and results, as well as lessons learned.

Details DOI

KR Conference 2025 Conference Paper

Reasoning in Assumption-Based Argumentation via SAT

Andreas Niskanen
Masood Feyzbakhsh Rankooh
Tuomo Lehtonen
Matti Järvisalo

The dominant approaches for solving NP-hard reasoning problems in computational argumentation are declarative—namely, Boolean satisfiability (SAT) in the case of abstract argumentation and answer set programming (ASP) in the case of structured formalisms such as assumption-based argumentation (ABA). ASP is particularly suited for the commonly-studied logic programming variant of ABA as acyclic derivations in ABA can be naturally modelled in ASP. In this work, we develop and evaluate various alternative approaches to realizing SAT-based reasoning for ABA, motivated by the success of SAT solvers in the realm of abstract argumentation. In contrast to ASP, non-trivial encodings or extensions to SAT solvers are needed to efficiently handle the acyclicity constraint underlying ABA reasoning. We develop and evaluate both advanced encodings and user-defined propagation mechanisms for realizing efficient SAT-based reasoning in ABA. As a result, we provide a first SAT-based ABA reasoner that can outperform the current state-of-the-art ASP approach to ABA.

PDF Details DOI

ECAI Conference 2024 Conference Paper

Complexity Results and Algorithms for Manipulation and Bribery in Judgment Aggregation

Ari Conati
Andreas Niskanen
Ronald de Haan
Matti Järvisalo

The study of limits of strategic behavior in collective decision making is a central topic in computational social choice. Focusing on judgment aggregation, we provide complexity results and algorithms for manipulation and bribery under various aggregation rules. Specifically, we show that manipulation and bribery are complete for the second level of the Polynomial Hierarchy and detail aggregation-rule-specific strong refinements for effective counterexample-guided abstraction refinement algorithms based on iterative calls to a maximum satisfiability solver for both manipulation and bribery. We provide an open-source implementation of the approach and empirically evaluate its performance on standard PrefLib datasets, showing that the strong refinement strategies developed in this work enable scaling up to solving more instances.

Details

JAIR Journal 2024 Journal Article

Declarative Approaches to Outcome Determination in Judgment Aggregation

Ari Conati
Andreas Niskanen
Matti Järvisalo

Judgment aggregation (JA) offers a generic formal framework for modeling various settings involving information aggregation by social choice mechanisms. For many judgment aggregation rules, computing collective judgments is computationally notoriously hard. The central outcome determination problem, in particular, is often complete for higher levels of the polynomial hierarchy. This complexity barrier makes it challenging to develop practical exact algorithms to outcome determination. Taking on this challenge, in this work we develop practical exact algorithms for outcome determination under a range of the most central JA rules—namely Kemeny, Slater, MaxHamming, Young, Dodgson, Reversal scoring, Condorcet, Ranked agenda, and LexiMax—by harnessing the declarative approach, in particular, Boolean satisfiability (SAT) and integer programming techniques. For the Kemeny, Slater, MaxHamming, Young, and Dodgson rules, we detail direct approaches based on maximum satisfiability (MaxSAT) and integer programming. For the Reversal scoring, Condorcet, Ranked agenda, and LexiMax rules, we develop iterative algorithms, including algorithms based on the counterexample-guided abstraction refinement (CEGAR) paradigm, making use of recent advances in incremental MaxSAT solving and preferential SAT-based reasoning. We provide an open-source implementation of the algorithms, and empirically evaluate them using real-world preference data. We compare the performance of our implementation to a recent approach which makes use of declarative solver technology for answer set programming (ASP). The results demonstrate that our approaches scale significantly beyond the reach of the ASP-based algorithms for all of the judgment aggregation rules considered.

PDF Details DOI

JAIR Journal 2024 Journal Article

From Single-Objective to Bi-Objective Maximum Satisfiability Solving

Christoph Jabs
Jeremias Berg
Andreas Niskanen
Matti Järvisalo

The declarative approach is key to efficiently finding optimal solutions to various types of NP-hard real-world combinatorial optimization problems. Most work on practical declarative solvers—ranging from classical integer programming to finite-domain constraint optimization and maximum satisfiability (MaxSAT)—has focused on optimization under a single objective; fewer advances have been made towards efficient declarative techniques for multi-objective optimization problems. Motivated by significant recent advances in practical solvers for MaxSAT, in this work we develop BiOptSat, an exact declarative approach for finding Pareto-optimal solutions to bi-objective optimization problems, with propositional logic as the underlying constraint language. BiOptSat can be viewed as an instantiation of the lexicographic method. The approach makes use of a single Boolean satisfiability solver that is incrementally employed throughout the entire search procedure, allowing for finding a single Pareto-optimal solution, finding one representative solution for each non-dominated point, and enumerating all Pareto-optimal solutions. We detail several algorithmic instantiations of BiOptSat, each building on recent algorithms proposed for single-objective MaxSAT. We empirically evaluate the instantiations compared to recently-proposed alternative approaches to multi-objective MaxSAT solving on several real-world domains from the literature, showing the practical benefits of our approach.

PDF Details DOI

IJCAI Conference 2024 Conference Paper

Learning Big Logical Rules by Joining Small Rules

Céline Hocquette
Andreas Niskanen
Rolf Morel
Matti Järvisalo
Andrew Cropper

A major challenge in inductive logic programming is learning big rules. To address this challenge, we introduce an approach where we join small rules to learn big rules. We implement our approach in a constraint-driven system and use constraint solvers to efficiently join rules. Our experiments on many domains, including game playing and drug design, show that our approach can (i) learn rules with more than 100 literals, and (ii) drastically outperform existing approaches in terms of predictive accuracies.

PDF Details DOI

AAAI Conference 2024 Conference Paper

Learning MDL Logic Programs from Noisy Data

Céline Hocquette
Andreas Niskanen
Matti Järvisalo
Andrew Cropper

Many inductive logic programming approaches struggle to learn programs from noisy data. To overcome this limitation, we introduce an approach that learns minimal description length programs from noisy data, including recursive programs. Our experiments on several domains, including drug design, game playing, and program synthesis, show that our approach can outperform existing approaches in terms of predictive accuracies and scale to moderate amounts of noise.

PDF Details DOI

ECAI Conference 2024 Conference Paper

SAT-Based Approaches to Reasoning in Choice Logics

Tuomo Lehtonen
Andreas Niskanen
Matti Järvisalo

Representing and reasoning about preferences is a fundamental task in artificial intelligence. Various logic-based languages for representing preferences have been proposed. However, developing practical algorithms for reasoning in such logic-based languages remains a challenge due to high computational complexity. In this work, we develop practical algorithms based on Boolean satisfiability (SAT) for computing preferred models and for deciding preferred model entailment in qualitative and conjunctive choice logics QCL and CCL under the so-called minmax, lexicographic, and inclusion-based preference semantics. For each of the problem variants, we detail an algorithm which adheres to the computational complexity of the reasoning task, based on either maximum satisfiability (MaxSAT) or SAT with preferences (PrefSAT) solvers. We empirically evaluate our implementation of the algorithms, and show that our approach scales significantly better than a recently proposed answer set programming approach to computing preferred models.

Details

JELIA Conference 2023 Conference Paper

Computing MUS-Based Inconsistency Measures

Isabelle Kuhlmann
Andreas Niskanen
Matti Järvisalo

Abstract We detail two instantiations of a generic algorithm for the problematic and MUS-variable-based inconsistency measures, based on answer set programming and Boolean satisfiability (SAT). Empirically, the SAT-based approach allows for more efficiently computing the measures when compared to enumerating all minimal correction subsets of a knowledge base.

Details

ECAI Conference 2023 Conference Paper

MaxSAT-Based Inconsistency Measurement

Andreas Niskanen
Isabelle Kuhlmann
Matthias Thimm
Matti Järvisalo

Inconsistency measurement aims at obtaining a quantitative assessment of the level of inconsistency in knowledge bases. While having such a quantitative assessment is beneficial in various settings, inconsistency measurement of propositional knowledge bases is under most existing measures a significantly challenging computational task. In this work, we harness Boolean satisfiability (SAT) based solving techniques for developing practical inconsistency measurement algorithms. Our algorithms—some of which constitute, to the best of our knowledge, the first practical approaches for specific inconsistency measures—are based on using natural choices of SAT-based techniques for the individual inconsistency measures, ranging from direct maximum satisfiability (MaxSAT) encodings to MaxSAT-based column generation techniques making use of incremental computations. We show through an extensive empirical evaluation that our approaches scale well in practice and significantly outperform recently-proposed answer set programming approaches to inconsistency measurement.

Details

AAMAS Conference 2023 Conference Paper

SAT-based Judgment Aggregation

Ari Conati
Andreas Niskanen
Matti Järvisalo

Judgment aggregation (JA) offers a generic formal logical framework for modeling various settings where agents must reach joint agreements through aggregating the preferences, judgments, or beliefs of individual agents by social choice mechanisms. In this work, we develop practical JA algorithms for outcome determination by harnessing Boolean satisfiability (SAT) based solvers as the underlying reasoning engines, leveraging on their ability to efficiently reason over logical representations incrementally. Concretely, we provide algorithms for outcome determination under a range of aggregation rules, using natural choices of SAT-based techniques adhering to the computational complexity of the problem for the individual rules. We also implement and empirically evaluate the approach using both synthetic and PrefLib data, showing that the approach can scale significantly beyond recently proposed alternative algorithms for JA.

PDF

AIJ Journal 2022 Journal Article

Advanced algorithms for abstract dialectical frameworks based on complexity analysis of subclasses and SAT solving

Thomas Linsbichler
Marco Maratea
Andreas Niskanen
Johannes P. Wallner
Stefan Woltran

dialectical frameworks (ADFs) constitute one of the most powerful formalisms in abstract argumentation. Their high computational complexity poses, however, certain challenges when designing efficient systems. In this paper, we tackle this issue by (i) analyzing the complexity of ADFs under structural restrictions, (ii) presenting novel algorithms which make use of these insights, and (iii) implementing these algorithms via (multiple) calls to SAT solvers. An empirical evaluation of the resulting implementation on ADF benchmarks generated from ICCMA competitions shows that our solver is able to outperform state-of-the-art ADF systems.

Details DOI

SAT Conference 2022 Conference Paper

Incremental Maximum Satisfiability

Andreas Niskanen
Jeremias Berg
Matti Järvisalo

Boolean satisfiability (SAT) solvers allow for incremental computations, which is key to efficient employment of SAT solvers iteratively for developing complex decision and optimization procedures, including maximum satisfiability (MaxSAT) solvers. However, enabling incremental computations on the level of constraint optimization remains a noticeable challenge. While incremental computations have been identified to have great potential in speeding up MaxSAT-based approaches for solving various real-world optimization problems, enabling incremental computations in MaxSAT remains to most extent unexplored. In this work, we contribute towards making incremental MaxSAT solving a reality. Firstly, building on the IPASIR interface for incremental SAT solving, we propose the IPAMIR interface for implementing incremental MaxSAT solvers and for developing applications making use of incremental MaxSAT. Secondly, we expand our recent adaptation of the implicit hitting set based MaxHS MaxSAT solver to a fully-fledged incremental MaxSAT solver in terms of implementing the IPAMIR specification in full, and detail in particular how, in addition to weight changes, assumptions are enabled without losing incrementality. Thirdly, we provide further empirical evidence on the benefits of incremental MaxSAT solving under assumptions.

Details

SAT Conference 2022 Conference Paper

MaxSAT-Based Bi-Objective Boolean Optimization

Christoph Jabs
Jeremias Berg
Andreas Niskanen
Matti Järvisalo

We explore a maximum satisfiability (MaxSAT) based approach to bi-objective optimization. Bi-objective optimization refers to the task of finding so-called Pareto-optimal solutions in terms of two objective functions. Bi-objective optimization problems naturally arise in various real-world settings. For example, in the context of learning interpretable representations, such as decision rules, from data, one wishes to balance between two objectives, the classification error and the size of the representation. Our approach is generally applicable to bi-objective optimizations which allow for propositional encodings. The approach makes heavy use of incremental Boolean satisfiability (SAT) solving and draws inspiration from modern MaxSAT solving approaches. In particular, we describe several variants of the approach which arise from different approaches to MaxSAT solving. In addition to computing a single representative solution per each point of the Pareto front, the approach allows for enumerating all Pareto-optimal solutions. We empirically compare the efficiency of the approach to recent competing approaches, showing practical benefits of our approach in the contexts of learning interpretable classification rules and bi-objective set covering.

Details

AIJ Journal 2021 Journal Article

Acceptance in incomplete argumentation frameworks

Dorothea Baumeister
Matti Järvisalo
Daniel Neugebauer
Andreas Niskanen
Jörg Rothe

argumentation frameworks (AFs), originally proposed by Dung, constitute a central formal model for the study of computational aspects of argumentation in AI. Credulous and skeptical acceptance of arguments in a given AF are well-studied problems both in terms of theoretical analysis—especially computational complexity—and the development of practical decision procedures for the problems. However, AFs make the assumption that all attacks between arguments are certain (i. e. , present attacks are known to exist, and missing attacks are known to not exist), which can in various settings be a restrictive assumption. A generalization of AFs to incomplete AFs was recently proposed as a formalism that allows the representation of both uncertain attacks and uncertain arguments in AFs. In this article, we explore the impact of allowing for modeling such uncertainties in AFs on the computational complexity of natural generalizations of acceptance problems to incomplete AFs under various central AF semantics. Complementing the complexity-theoretic analysis, we also develop the first practical decision procedures for all of the NP-hard variants of acceptance in incomplete AFs. In terms of complexity analysis, we establish a full complexity landscape, showing that depending on the variant of acceptance and property/semantics, the complexity of acceptance in incomplete AFs ranges from polynomial-time decidable to completeness for Σ 3 p. In terms of algorithms, we show through an extensive empirical evaluation that an implementation of the proposed decision procedures, based on boolean satisfiability (SAT) solving, is effective in deciding variants of acceptance under uncertainties. We also establish conditions for what type of atomic changes are guaranteed to be redundant from the perspective of preserving extensions of completions of incomplete AFs, and show that the results allow for considerably improving the empirical efficiency of the proposed SAT-based counterexample-guided abstraction refinement algorithms for acceptance in incomplete AFs for problem variants with complexity beyond NP.

Details DOI

ECAI Conference 2020 Conference Paper

Algorithms for Dynamic Argumentation Frameworks: An Incremental SAT-Based Approach

Andreas Niskanen
Matti Järvisalo

Motivated by the fact that argumentation is intrinsically a dynamic process, the study of representational and computational aspects of dynamics in argumentation is starting to gain more traction. This is also witnessed by the most recent 2019 edition of the International Competition on Computational Models of Argumentation (ICCMA 2019), which introduced a new track focusing on dynamic argumentation frameworks. In this paper, we present an efficient Boolean satisfiability (SAT) based approach to reasoning over dynamic argumentation frameworks. In particular, based on employing incremental SAT solving, we detail algorithms covering all of the reasoning tasks—credulous and skeptical acceptance, as well as the computation of a single and all extensions—and semantics—complete, preferred, stable, and grounded—constituting the ICCMA 2019 dynamic track. Furthermore, we demonstrate empirically that an implementation of the approach is highly competitive.

Details

IJCAI Conference 2020 Conference Paper

Controllability of Control Argumentation Frameworks

Andreas Niskanen
Daniel Neugebauer
Matti Järvisalo

Control argumentation frameworks (CAFs) allow for modeling uncertainties inherent in various argumentative settings. We establish a complete computational complexity map of the central computational problem of controllability in CAFs for five key semantics. We also develop Boolean satisfiability based counterexample-guided abstraction refinement algorithms and direct encodings of controllability as quantified Boolean formulas, and empirically evaluate their scalability on a range of NP-hard variants of controllability.

PDF Details DOI

AAAI Conference 2020 Conference Paper

Deciding Acceptance in Incomplete Argumentation Frameworks

Andreas Niskanen
Daniel Neugebauer
Matti Järvisalo
Jörg Rothe

Expressing incomplete knowledge in abstract argumentation frameworks (AFs) through incomplete AFs has recently received noticeable attention. However, algorithmic aspects of deciding acceptance in incomplete AFs are still underdeveloped. We address this current shortcoming by developing algorithms for NP-hard and coNP-hard variants of acceptance problems over incomplete AFs via harnessing Boolean satisﬁability (SAT) solvers. Focusing on nonempty conﬂict-free or admissible sets and on stable extensions, we also provide new complexity results for a reﬁned variant of skeptical acceptance in incomplete AFs, ranging from polynomial-time computability to hardness for the second level of the polynomial hierarchy. Furthermore, central to the proposed SAT-based counterexample-guided abstraction re- ﬁnement approach for the second-level problem variants, we establish conditions for redundant atomic changes to incomplete AFs from the perspective of preserving extensions. We show empirically that the resulting SAT-based approach for incomplete AFs scales at least as well as existing SAT-based approaches to deciding acceptance in AFs.

PDF Details

KR Conference 2020 Conference Paper

Smallest Explanations and Diagnoses of Rejection in Abstract Argumentation

Andreas Niskanen
Matti Järvisalo

Deciding acceptance of arguments is a central problem in the realm of abstract argumentation. Beyond mere acceptance status, when an argument is rejected it would be informative to analyze reasons for the rejection. Recently, two complementary notions---explanations and diagnoses---were proposed for capturing underlying reasons for rejection in terms of (small) subsets of arguments or attacks. We provide tight complexity results for deciding and computing argument-based explanations and diagnoses. Computationally, we identify that smallest explanations and diagnoses for argumentation frameworks can be computed as so-called smallest unsatisfiable subsets (SMUSes) and smallest correction sets of propositional formulas. Empirically, we show that SMUS extractors and maximum satisfiability solvers (computing smallest correction sets) offer effective ways of computing smallest explanations and diagnoses.

PDF Details DOI

ECAI Conference 2020 Conference Paper

Strong Refinements for Hard Problems in Argumentation Dynamics

Andreas Niskanen
Matti Järvisalo

Going beyond the more classically studied reasoning problems over argumentation frameworks (AFs), the study of dynamics in argumentation gives rise to new types of computational challenges. This work studies ways of extending the scalability of computational approaches to reasoning about dynamics of abstract argumentation frameworks. In particular, we focus on three recently proposed optimization problems underlying AF dynamics—two variants of enforcement in abstract argumentation and the synthesis of argumentation frameworks from examples—for semantics under which the problems are (presumably) complete for the second level of the polynomial hierarchy. As the main contributions, we show that by bridging recent theoretical results on the persistence of extensions under changes to the structure of AFs with Boolean satisfiability (SAT) counterexample-guided abstraction refinement algorithms for the considered problems, the scalability of state-of-the-art practical algorithms for each of the three problems can be significantly improved.

Details

KR Conference 2020 System Paper

µ-toksia: An Efficient Abstract Argumentation Reasoner

Andreas Niskanen
Matti Järvisalo

We describe the µ-toksia argumentation reasoning system. The system supports a range of different reasoning tasks over both standard and dynamic abstract argumentation frameworks under essentially all central argumentation semantics, covering all tracks and reasoning tasks considered in the most recent International Competition on Computational Models of Argumentation (ICCMA 2019). µ-toksia ranked first in all reasoning tasks in the main track of ICCMA 2019, and has been shown to scale noticeably better on the dynamic track tasks than its current competitors. In this paper, we provide an overview of µ-toksia and its algorithmic and implementation-level details, and provide further empirical evidence beyond ICCMA 2019 on the efficiency of µ-toksia compared to related systems.

PDF Details DOI

JELIA Conference 2019 Conference Paper

Preprocessing Argumentation Frameworks via Replacement Patterns

Wolfgang Dvorák
Matti Järvisalo
Thomas Linsbichler
Andreas Niskanen
Stefan Woltran

Abstract A fast-growing research direction in the study of formal argumentation is the development of practical systems for central reasoning problems underlying argumentation. In particular, numerous systems for abstract argumentation frameworks (AF solvers) are available today, covering several argumentation semantics and reasoning tasks. Instead of proposing another algorithmic approach for AF solving, we introduce in this paper distinct AF preprocessing techniques as a solver-independent approach to obtaining performance improvements of AF solvers. We establish a formal framework of replacement patterns to perform local simplifications that are faithful with respect to standard semantics for AFs. Moreover, we provide a collection of concrete replacement patterns. Towards potential applicability, we employ the patterns in a preliminary empirical evaluation of their influence on AF solver performance.

Details

JAIR Journal 2019 Journal Article

Synthesizing Argumentation Frameworks from Examples

Andreas Niskanen
Johannes P. Wallner
Matti Järvisalo

Argumentation is today a topical area of artificial intelligence (AI) research. Abstract argumentation, with argumentation frameworks (AFs) as the underlying knowledge representation formalism, is a central viewpoint to argumentation in AI. Indeed, from the perspective of AI and computer science, understanding computational and representational aspects of AFs is key in the study of argumentation. Realizability of AFs has been recently proposed as a central notion for analyzing the expressive power of AFs under different semantics. In this work, we propose and study the AF synthesis problem as a natural extension of realizability, addressing some of the shortcomings arising from the relatively stringent definition of realizability. In particular, realizability gives means of establishing exact conditions on when a given collection of subsets of arguments has an AF with exactly the given collection as its set of extensions under a specific argumentation semantics. However, in various settings within the study of dynamics of argumentation---including revision and aggregation of AFs---non-realizability can naturally occur. To accommodate such settings, our notion of AF synthesis seeks to construct, or synthesize, AFs that are semantically closest to the knowledge at hand even when no AFs exactly representing the knowledge exist. Going beyond defining the AF synthesis problem, we study both theoretical and practical aspects of the problem. In particular, we (i) prove NP-completeness of AF synthesis under several semantics, (ii) study basic properties of the problem in relation to realizability, (iii) develop algorithmic solutions to NP-hard AF synthesis using the constraint optimization paradigms of maximum satisfiability and answer set programming, (iv) empirically evaluate our algorithms on different forms of AF synthesis instances, as well as (v) discuss variants and generalizations of AF synthesis.

PDF Details DOI

KR Conference 2018 Conference Paper

Extension Enforcement under Grounded Semantics in Abstract Argumentation

Andreas Niskanen
Johannes P. Wallner
Matti Järvisalo

The study of dynamics in abstract argumentation gives rise to optimization problems that are NP-hard also under the grounded semantics, in contrast to argument acceptance problems over argumentation frameworks (AF). Developing efficient systems for AF reasoning under grounded semantics has received less attention compared to other central AF semantics under which acceptance is NP-hard. In particular, grounded semantics is not currently supported by recent systems for extension enforcement, despite (or due to) its nontriviality. In this work, we propose and empirically evaluate three first approaches to enforcement under grounded semantics. While each of the approaches is based on employing constraint optimization solvers, we show empirically that there are significant differences in the scalability of the approaches.

IJCAI Conference 2018 Conference Paper

Novel Algorithms for Abstract Dialectical Frameworks based on Complexity Analysis of Subclasses and SAT Solving

Thomas Linsbichler
Marco Maratea
Andreas Niskanen
Johannes P. Wallner
Stefan Woltran

Abstract dialectical frameworks (ADFs) constitute one of the most powerful formalisms in abstract argumentation. Their high computational complexity poses, however, certain challenges when designing efficient systems. In this paper, we tackle this issue by (i) analyzing the complexity of ADFs under structural restrictions, (ii) presenting novel algorithms which make use of these insights, and (iii) empirically evaluating a resulting implementation which relies on calls to SAT solvers.

PDF Details

JAIR Journal 2017 Journal Article

Complexity Results and Algorithms for Extension Enforcement in Abstract Argumentation

Johannes P. Wallner
Andreas Niskanen
Matti Järvisalo

Argumentation is an active area of modern artificial intelligence (AI) research, with connections to a range of fields, from computational complexity theory and knowledge representation and reasoning to philosophy and social sciences, as well as application-oriented work in domains such as legal reasoning, multi-agent systems, and decision support. Argumentation frameworks (AFs) of abstract argumentation have become the graph-based formal model of choice for many approaches to argumentation in AI, with semantics defining sets of jointly acceptable arguments, i.e., extensions. Understanding the dynamics of AFs has been recently recognized as an important topic in the study of argumentation in AI. In this work, we focus on the so-called extension enforcement problem in abstract argumentation as a recently proposed form of argumentation dynamics. We provide a nearly complete computational complexity map of argument-fixed extension enforcement under various major AF semantics, with results ranging from polynomial-time algorithms to completeness for the second level of the polynomial hierarchy. Complementing the complexity results, we propose algorithms for NP-hard extension enforcement based on constraint optimization under the maximum satisfiability (MaxSAT) paradigm. Going beyond NP, we propose novel MaxSAT-based counterexample-guided abstraction refinement procedures for the second-level complete problems and present empirical results on a prototype system constituting the first approach to extension enforcement in its generality.

PDF Details DOI

AAAI Conference 2016 Conference Paper

Complexity Results and Algorithms for Extension Enforcement in Abstract Argumentation

Johannes Wallner
Andreas Niskanen
Matti Järvisalo

Understanding the dynamics of argumentation frameworks (AFs) is important in the study of argumentation in AI. In this work, we focus on the so-called extension enforcement problem in abstract argumentation. We provide a nearly complete computational complexity map of ﬁxed-argument extension enforcement under various major AF semantics, with results ranging from polynomial-time algorithms to completeness for the second-level of the polynomial hierarchy. Complementing the complexity results, we propose algorithms for NP-hard extension enforcement based on constrained optimization. Going beyond NP, we propose novel counterexample-guided abstraction reﬁnement procedures for the second-level complete problems and present empirical results on a prototype system constituting the ﬁrst approach to extension enforcement in its generality.

PDF Details

IJCAI Conference 2016 Conference Paper

Optimal Status Enforcement in Abstract Argumentation

Andreas Niskanen
Johannes P. Wallner
Matti J
auml; rvisalo

We present complexity results and algorithms for optimal status enforcement in abstract argumentation. Status enforcement is the task of adjusting a given argumentation framework (AF) to support given positive and negative argument statuses, i. e. , to accept and reject specific arguments. We study optimal status enforcement as the problem of finding a structurally closest AF supporting given argument statuses. We establish complexity results for optimal status enforcement under several central AF semantics, develop constraint-based algorithms for NP and second-level complete variants of the problem, and empirically evaluate the procedures.

PDF Details

JELIA Conference 2016 Conference Paper

Pakota: A System for Enforcement in Abstract Argumentation

Andreas Niskanen
Johannes P. Wallner
Matti Järvisalo

Abstract In this paper we describe Pakota, a system implementation that allows for solving enforcement problems over argumentation frameworks. Via harnessing Boolean satisfiability (SAT) and maximum satisfiability (MaxSAT) solvers, Pakota implements algorithms for extension and status enforcement under various central AF semantics, covering a range of NP-complete—via direct MaxSAT encodings—and \(\mathrm{\Sigma }_{2}^{P}\) -complete—via MaxSAT-based counterexample-guided abstraction refinement—enforcement problems. We overview the algorithmic approaches implemented in Pakota, and describe in detail the system architecture, features, interfaces, and usage of the system. Furthermore, we present an empirical evaluation on the impact of the choice of MaxSAT solvers on the scalability of the system, and also provide benchmark generators for extension and status enforcement.

Details

ECAI Conference 2016 Conference Paper

Synthesizing Argumentation Frameworks from Examples

Andreas Niskanen
Johannes P. Wallner
Matti Järvisalo

Argumentation is nowadays a core topic in AI research. Understanding computational and representational aspects of abstract argumentation frameworks (AFs) is a central topic in the study of argumentation. The study of realizability of AFs aims at understanding the expressive power of AFs under different semantics. We propose and study the AF synthesis problem as a natural extension of realizability, addressing some of the shortcomings arising from the relatively stringent definition of realizability. Specifically, AF synthesis seeks to construct, or synthesize, AFs that are semantically closest to the knowledge at hand even when no AFs exactly representing the knowledge exist. Going beyond defining the AF synthesis problem, we (i) prove NP-completeness of AF synthesis under several semantics, (ii) study basic properties of the problem in relation to realizability, (iii) develop algorithmic solutions to AF synthesis using constrained optimization, (iv) empirically evaluate our algorithms on different forms of AF synthesis instances, as well as (v) discuss variants and generalization of AF synthesis.

Details