Machine learning is increasingly used in the real world, including in sensitive contexts. This, combined with their innate non-transparency, gives rise to the need for explaining the decisions of machine learning models. We focus on optimal counterfactual explanations for random forests, a well-performing and popular classifier, intuitively answering the question “What is the cheapest way to change a given classification?” We propose an algorithm based on state-of-the-art maximum satisfiability (MaxSAT) solving and a compact and faithful formal model of the classifier. An optimal counterfactual is guaranteed to be found for any sample, and further plausibility constraints (e.g. immutability of some features) as well as custom cost function can be seamlessly incorporated. We conduct an empirical evaluation showing promising run time performance for our approach compared to existing optimal algorithms for computing counterfactuals for random forests, outperforming previous approaches on many datasets.

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.

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.

Reasoning under incomplete information is an important research direction in the study of computational argumentation. Most advances in this direction so far have focused on abstract argumentation frameworks. In particular, development of computational approaches to reasoning under incomplete information in structured formalisms remains to a large extent a challenge. We address this challenge by studying the problems of determining stability and relevance—with the aim of analyzing aspects of resilience of acceptance statuses in light of new information—in the central structured formalism of ASPIC+ . The specific ASPIC+ instantiation and grounded argumentation semantics we focus on are motivated by current applications in criminal investigation at the Netherlands Police. Our contributions consist of a theoretical analysis of the complexity of deciding stability and relevance as well as first exact algorithms for reasoning about stability and relevance in incomplete ASPIC+ theories. In terms of complexity results, we show that deciding stability is coNP-complete for incomplete ASPIC+ when assuming a preference ordering on defeasible rules via the last-link ordering, while deciding relevance is significantly more complex, namely NP^NP-complete. Complementing the complexity results, we develop practical algorithms for deciding stability and relevance based on the declarative paradigm of answer set programming (ASP). Furthermore, we provide an open-source implementation of the algorithms, and show empirically that the implementation exhibits promising scalability on both real-world and synthetic data. Our exact approach to stability is competitive with a previously proposed inexact approach, and the run times of our algorithms for both stability and relevance are sufficiently low on real-world data to be used in online settings.

Most existing computational tools for assumption-based argumentation (ABA) focus on so-called flat frameworks, disregarding the more general case. Here, we study an instantiation-based approach for reasoning in possibly non-flat ABA. For complete-based semantics, an approach of this kind was recently introduced, based on a semantics-preserving translation between ABA and bipolar argumentation frameworks (BAFs). Admissible semantics, however, require us to consider an extension of BAFs which also makes use of premises of arguments (pBAFs). We explore basic properties of pBAFs which we require as a theoretical underpinning for our proposed instantiation-based solver for non-flat ABA under admissible semantics. As our empirical evaluation shows, depending on the ABA instances, the instantiation-based solver is competitive against an ASP-based approach implemented in the style of state-of-the-art solvers for hard argumentation problems.

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.

We provide complexity results and algorithms for reasoning in the central structured argumentation formalism of ASPIC+. Considering ASPIC+ accommodated with preferences under the last-link principle, the results are made possible by rephrasing several argumentation semantics---admissible, complete, stable, preferred and grounded---in terms of defeasible elements of an ASPIC+ theory for both democratic and elitist last-link lifting. Via the rephrasing, we establish that acceptance is polynomial-time computable under grounded semantics, and complete for either NP, coNP, or Pi_P^2, depending on the reasoning mode and semantics. We also detail answer set programming encodings for deciding acceptance for the NP/coNP-complete reasoning tasks, and empirically show that it scales significantly better than first translating ASPIC+ reasoning tasks to abstract argumentation. Finally, we show that, in contrast to the last-link principle, it is NP-hard to compute the grounded extension under the weakest-link principle.

A key ingredient of computational argumentation in AI is the generation of arguments in favor of or against claims under scrutiny. In this paper we look at the complexity of argument construction and reasoning in the prominent structured formalism of assumption-based argumentation (ABA). We point out that reasoning in ABA by means of constructing an abstract argumentation framework (AF) gives rise to two main sources of complexity: (i) constructing the AF and (ii) reasoning within the constructed graph. Since both steps are intractable in general, it is no surprise that the best performing state-of-the-art ABA reasoners skip the instantiation procedure entirely and perform tasks directly on the input knowledge base. Driven by this observation, we identify and study atomic and symmetric ABA, two ABA fragments that preserve the expressive power of general ABA, and that can be utilized to have milder complexity in the first or second step. We show that using atomic ABA allows for an instantiation procedure for general ABA leading to polynomially-bounded AFs and that symmetric ABA can be used to create AFs that have mild complexity to reason on. By an experimental evaluation, we show that using the former approach with modern AF solvers can be competitive with state-of-the-art ABA solvers, improving on previous AF instantiation approaches that are hindered by intractable argument construction.

Reasoning under incomplete information is an important research direction in AI argumentation. Most computational advances in this direction have so-far focused on abstract argumentation frameworks. Development of computational approaches to reasoning under incomplete information in structured formalisms remains to-date to a large extent a challenge. We address this challenge by studying the so-called stability and relevance problems---with the aim of analyzing aspects of resilience of acceptance statuses in light of new information---in the central structured formalism of ASPIC+. Focusing on the case of the grounded semantics and an ASPIC+ fragment motivated through application scenarios, we develop exact ASP-based algorithms for stability and relevance in incomplete ASPIC+ theories, and pinpoint the complexity of reasoning about stability (coNP-complete) and relevance (Sigma_2^P-complete), further justifying our ASP-based approaches. Empirically, the algorithms exhibit promising scalability, outperforming even a recent inexact approach to stability, with our ASP-based iterative approach being the first algorithm proposed for reasoning about relevance in ASPIC+.

Assumption-based argumentation (ABA) is one of the most-studied formalisms for structured argumentation. While ABA is a general formalism that can be instantiated with various different logics, most attention from the computational perspective has been focused on the logic programming (LP) instantiation of ABA. Going beyond the LP-instantiation, we develop an algorithmic approach to reasoning in the propositional default logic (DL) instantiation of ABA. Our approach is based on iterative applications of Boolean satisfiability (SAT) solvers as a natural choice for implementing derivations as entailment checks in DL. We instantiate the approach for deciding acceptance and for assumption-set enumeration in the DL-instantiation of ABA under several central argumentation semantics, and empirically evaluate an implementation of the approach.

The study of computational models for argumentation is a vibrant area of artificial intelligence and, in particular, knowledge representation and reasoning research. Arguments most often have an intrinsic structure made explicit through derivations from more basic structures. Computational models for structured argumentation enable making the internal structure of arguments explicit. Assumption-based argumentation (ABA) is a central structured formalism for argumentation in AI. In this article, we make both algorithmic and complexity-theoretic advances in the study of ABA. In terms of algorithms, we propose a new approach to reasoning in a commonly studied fragment of ABA (namely the logic programming fragment) with and without preferences. While previous approaches to reasoning over ABA frameworks apply either specialized algorithms or translate ABA reasoning to reasoning over abstract argumentation frameworks, we develop a direct declarative approach to ABA reasoning by encoding ABA reasoning tasks in answer set programming. We show via an extensive empirical evaluation that our approach significantly improves on the empirical performance of current ABA reasoning systems. In terms of computational complexity, while the complexity of reasoning over ABA frameworks is well-understood, the complexity of reasoning in the ABA+ formalism integrating preferences into ABA is currently not fully established. Towards bridging this gap, our results suggest that the integration of preferential information into ABA via so-called reverse attacks results in increased problem complexity for several central argumentation semantics.

Abstract Assumption-based argumentation (ABA) is a central structured argumentation formalism. As shown recently, answer set programming (ASP) enables efficiently solving NP-hard reasoning tasks of ABA in practice, in particular in the commonly studied logic programming fragment of ABA. In this work, we harness recent advances in incremental ASP solving for developing effective algorithms for reasoning tasks in the logic programming fragment of ABA that are presumably hard for the second level of the polynomial hierarchy, including skeptical reasoning under preferred semantics as well as preferential reasoning. In particular, we develop non-trivial counterexample-guided abstraction refinement procedures based on incremental ASP solving for these tasks. We also show empirically that the procedures are significantly more effective than previously proposed algorithms for the tasks.

A major research direction in AI argumentation is the study and development of practical computational techniques for reasoning in different argumentation formalisms. Compared to abstract argumentation, developing algorithmic techniques for different structured argumentation formalisms, such as assumption-based argumentation and the general ASPIC+ framework, is more challenging. At present, there is a lack of efficient approaches to reasoning in ASPIC+. We develop a direct declarative approach based on answer set programming (ASP) to reasoning in an instantiation of the ASPIC+ framework. We establish formal foundations for direct declarative encodings for reasoning in ASPIC+ without preferences for several central argumentation semantics, and detail ASP encodings of semantics for which reasoning about acceptance is NP-hard in ASPIC+. Empirically, the ASP approach scales up to frameworks of significant size, thereby answering the current lack of practical computational approaches to reasoning in ASPIC+ and providing a promising base for capturing further generalizations within ASPIC+.

Focusing on assumption-based argumentation (ABA) as a central structured formalism to AI argumentation, we propose a new approach to reasoning in ABA with and without preferences. While previous approaches apply either specialized algorithms or translate ABA reasoning to reasoning over abstract argumentation frameworks, we develop a direct approach by encoding ABA reasoning tasks in answer set programming. This significantly improves on the empirical performance of current ABA reasoning systems. We also give new complexity results for reasoning in ABA+, suggesting that the integration of preferential information into ABA results in increased problem complexity for several central argumentation semantics.

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.