Boolean hedonic games are a class of cooperative games involving multiple agents in which agents aim to form coalitions based on individual agents’ preferences. In this work, we provide complexity results and exact algorithms for the task of forming Nash stable coalitions under different membership rights in the dichotomous setting where agents specify preferences for which coalitions they are happy/unhappy to join. The membership rights specify veto rights for coalitions, allowing a coalition to forbid an individual agent from moving (exiting the current coalition or entering another coalition) even if the agent themself would become more happy to move. We establish that various problem variants and their refinements in this setting are often situated on the second level of the polynomial hierarchy, complete for Σp2. Building on the complexity results, we develop Boolean satisfiability (SAT) based counterexample-guided abstraction refinement algorithms for the Σp2 problem variants and empirically evaluate a first-of-kind implementation of the approaches.

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.

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.

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.

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.

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.

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.

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 algo- rithms, 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.

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.

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.

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

Decision lists are one of the most easily explainable machine learning models. Given the renewed emphasis on explainable machine learning decisions, this machine learning model is increasingly attractive, combining small size and clear explainability. In this paper, we show for the first time how to construct optimal "perfect" decision lists which are perfectly accurate on the training data, and minimal in size, making use of modern SAT solving technology. We also give a new method for determining optimal sparse decision lists, which trade off size and accuracy. We contrast the size and test accuracy of optimal decisions lists versus optimal decision sets, as well as other state-of-the-art methods for determining optimal decision lists. We also examine the size of average explanations generated by decision sets and decision lists.

Abstract 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 Σ3p. 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.

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 under-developed. We address this current shortcoming by developing algorithms for NP-hard and coNP-hard variants of acceptance problems over incomplete AFs via harnessing Boolean satisfiability (SAT) solvers. Focusing on nonempty conflict-free or admissible sets and on stable extensions, we also provide new complexity results for a refined 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 refinement 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.

Peer reviewed

Peer reviewed

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.

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.

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.

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.

We present a computational study of effectiveness of declarative approaches for three optimization problems in the realm of abstract argumentation. In the largest extension problem, the task is to compute a σ-extension of largest cardinality (rather than, e.g., a subset-maximal extension) among the σ-extensions of a given argumentation framework (AF). The two other problems considered deal with a form of dynamics in AFs: given a subset S of arguments of an AF, the task is to compute a closest σ-extension within a distance-based setting, either by repairing S into a σ-extension of the AF, or by adjusting S to be a σ-extension containing (or not containing) a given argument. For each of the problems, we consider both iterative Boolean satisfiability (SAT) based approaches as well as directly solving the problems via Boolean optimization using maximum satisfiability (MaxSAT) solvers. We present results from an extensive empirical evaluation under several AF semantics σ using the ICCMA 2017 competition instances and several state-of-the-art solvers. The results indicate that the choice of the approach can play a significant role in the ability to solve these problems, and that a specific MaxSAT approach yields quite generally good results. Furthermore, with impact on SAT-based AF reasoning systems more generally, we demonstrate that, especially on dense AFs, taking into account the local structure of AFs can have a significant positive effect on the overall solving efficiency.

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.

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.

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

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.