\documentclass[conference]{IEEEtran}
\IEEEoverridecommandlockouts
% The preceding line is only needed to identify funding in the first footnote. If that is unneeded, please comment it out.
\usepackage{cite}
\usepackage{amsmath,amssymb,amsfonts}
\usepackage{algorithmic}
\usepackage{graphicx}
\usepackage{textcomp}
\usepackage{xcolor}
\def\BibTeX{{\rm B\kern-.05em{\sc i\kern-.025em b}\kern-.08em
    T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}}
\usepackage{amssymb,amsmath}
\usepackage{amsthm}
\usepackage{xspace}
\usepackage{hyperref}
   
    
    
%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\TODO}[1]{~\newline\noindent \textcolor{magenta}{\fbox{\parbox{\columnwidth}{#1}}}}	% general todo macro
\newcommand{\AF}{\ensuremath{\mathsf{AF}}\xspace}						% Abstract argumentation framework
\newcommand{\arguments}{\ensuremath{\mathsf{A}}\xspace}				% Set of arguments
\newcommand{\attacks}{\ensuremath{\mathsf{R}}\xspace}				% Attack relation
\newcommand{\attackers}[1]{\ensuremath{#1^{-}\xspace}}				% Attacker set
\newcommand{\AFcomplete}{\ensuremath{\AF=(\arguments,\attacks)}\xspace}		% Definition of an abstract argumentation framework

\newcommand{\co}{\ensuremath{CO}}
\newcommand{\gr}{\ensuremath{GR}}
\newcommand{\st}{\ensuremath{ST}}
\newcommand{\pr}{\ensuremath{PR}}
\newcommand{\id}{\ensuremath{ID}}
\newcommand{\sst}{\ensuremath{SST}}
\newcommand{\stg}{\ensuremath{STG}}
\newtheorem{theorem}{Theorem}
\newcommand{\fudge}{\textsc{Fudge v3.3.4}}
%%%%%%%%%%%%%%%%%%%%%%%
    
\begin{document}

\title{\fudge}

\author{\IEEEauthorblockN{Matthias Thimm}
\IEEEauthorblockA{\textit{Artificial Intelligence Group} \\
\textit{University of Hagen}\\
Germany \\
matthias.thimm@fernuni-hagen.de}
\and
\IEEEauthorblockN{Federico Cerutti}
\IEEEauthorblockA{\textit{Department of Information Engineering} \\
\textit{University of Brescia}\\
Italy \\
federico.cerutti@unibs.it}
\and
\IEEEauthorblockN{Mauro Vallati}
\IEEEauthorblockA{\textit{School of Computing and Engineering} \\
\textit{University of Huddersfield}\\
United Kingdom\\
m.vallati@hud.ac.u}
}

\maketitle

\begin{abstract}
We present \fudge, an abstract argumentation solver that tightly integrates satisfiability solving technology to solve a series of abstract argumentation problems. While most of the encodings used by \fudge\ derive from standard translation approaches, \fudge\ makes use of sophisticated encodings to solve the skeptical reasoning problem wrt.\ preferred semantics and problems wrt.\ ideal semantics.
\end{abstract}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}
An \emph{abstract argumentation framework} $\AF$ is a tuple $\AF=(\arguments,\attacks)$ where \arguments is a (finite) set of arguments and \attacks is a relation $\attacks\subseteq \arguments\times\arguments$ \cite{Dung:1995}.
 For two arguments $a,b\in\arguments$ the relation $a \attacks b$ means that argument $a$ attacks argument $b$. For a set $S\subseteq \arguments$ we define
\begin{align*}
    S^+ & = \{a\in \arguments\mid \exists b\in S, b\attacks a\} \\
    S^- & = \{a\in \arguments\mid \exists b\in S, a\attacks b\}
\end{align*}
We say that a set $S\subseteq\arguments$ is \emph{conflict-free} if for all $a,b\in S$ it is not the case that $a\attacks b$.
A set $S$ \emph{defends} an argument $b\in\arguments$ if for all $a$ with $a\attacks b$ there is $c\in S$ with $c\attacks a$.
A conflict-free set $S$ is called \emph{admissible} if $S$ defends all $a\in S$. 

Different semantics \cite{Baroni:2011} can be phrased by imposing constraints on admissible sets. 
In particular, set $E$
\begin{itemize}
   	 \item is a \emph{complete} (\co) extension iff it is admissible and for all $a\in \arguments$, if $E$ defends $a$ then $a\in E$,
	\item is a \emph{grounded} (\gr) extension iff it is complete and minimal,
	\item is a \emph{stable} (\st) extension iff it is conflict-free and $E\cup E^+ =\arguments$,
	\item is a \emph{preferred} (\pr) extension iff it is admissible and maximal,
	\item is an \emph{ideal} (\id) extension iff $E\subseteq E'$ for each preferred extension $E'$, $E$ is admissible, and $E$ is maximal,
	\item is a \emph{semi-stable} (\sst) extension $E$ is admissible and $E\cup E^+$ is maximal, and
	\item is a \emph{stage} (\sst) extension $E$ is conflict-free and $E\cup E^+$ is maximal.
\end{itemize}
All statements on minimality/maximality are meant to be with respect to set inclusion.

Given an abstract argumentation framework $\AFcomplete$ and a semantics $\sigma\in\{\co,\gr,\st,\pr,\id,\sst,\stg\}$ we are interested in the following computational problems:
\begin{description}
    \item \textsf{SE-$\sigma$}: Given $\AF$, compute some $\sigma$-extension.
%    \item \textsf{CE-$\sigma$}: For a given abstract argumentation framework $\AF$, determine the number of all $\sigma$-extensions.
	\item \textsf{DC-$\sigma$}: Given $\AF$ and an argument $a$, decide whether $a$ is in at least one $\sigma$-extension of $\AF$.
	\item \textsf{DS-$\sigma$}: Given $\AF$ and an argument $a$, decide whether $a$ is in all $\sigma$-extensions of $\AF$.
\end{description}
Note that \textsf{DC-$\sigma$} and \textsf{DS-$\sigma$} are equivalent for $\sigma\in\{\gr,\id\}$ as those extensions are uniquely defined \cite{Baroni:2011}. For these, we will only consider \textsf{DS-$\sigma$}.

The \fudge\ solver supports solving the above-mentioned computational problems wrt.\  all $\sigma\in\{\co,\gr,\st,\pr,\id,\sst,\stg\}$.
In the remainder of this system description, we give a brief overview on the architecture of \fudge\ (Section~\ref{sec:architecture}), highlight the changes made since the ICCMA'23 version (Section~\ref{sec:changes}), and conclude in Section~\ref{sec:summary}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Architecture}\label{sec:architecture}
\fudge\ follows the standard reduction-based approach to solve the above-mentioned reasoning problems \cite{Besnard:2014,Cerutti:2018a} with the target formalism being the satisfiability problem \textsf{SAT} \cite{Biere:2009}. For example, given the problem \textsf{SE-ST} and an input argumentation framework $\AFcomplete$, first, for each argument $a\in \arguments$, we create propositional variables $\text{in}_{a}$ and $\text{out}_{a}$, with the meaning that $\text{in}_{a}$ (resp.\ $\text{out}_{a}$) is true in a satisfying assignment iff the argument $a$ is in (resp.\ attacked by) the stable extension to be found. Then
	\begin{align*}
		\Phi_1(\AF) = \bigwedge_{a\in\arguments}	 (\neg \text{in}_a \vee \neg \text{out}_a)
	\end{align*}
	and
	\begin{align*}
		\Phi_2(\AF) = \bigwedge_{a\in\arguments}	 (\text{out}_a \Leftrightarrow \bigvee_{(b,a)\in \attacks}\text{in}_b )
	\end{align*}
	model the basic intuition behind these variables and, in particular, ensure conflict-freeness of the modelled extension. The constraint that all arguments not included in the extension must be attacked can be modelled by
\begin{align*}
    \Phi_3(\AF) & = \bigwedge_{a\in \arguments}(\text{in}_a \vee \text{out}_a)
\end{align*}
Then the formula $\Phi_1(\AF)\wedge \Phi_2(\AF)\wedge \Phi_3(\AF)$ is satisfiable iff $\AF$ has a stable extension and a stable extension can be easily extracted from a satisfying assignment of $\Phi_1(\AF)\wedge \Phi_2(\AF)\wedge \Phi_3(\AF)$. All reasoning problems on the first level of the polynomial hierarchy \cite{Dvorak:2018} can be solved in a similar manner.% and their corresponding counting problems can be realised by iterative satisfiability tests to enumerate all extensions.

Particularly challenging problems are those wrt.\ preferred semantics as, in particular, $DS$-$PR$ is $\Pi_2^P$-complete \cite{Dvorak:2018}. To solve that problem, we use the approach of \cite{Thimm:2021}. This approach relies on the following observation\footnote{Define $S'\attacks S$ iff there is $a\in S'$ and $b\in S$ with $(a,b)\in\attacks$.}:
\begin{theorem}[\cite{Thimm:2021}]
    $a\in\arguments$ is skeptically accepted wrt.\ preferred semantics iff
    \begin{enumerate}
        \item there is an admissible set $S$ with $a\in S$ and
        \item for every admissible set $S$ with $a \in S$ and every admissible set $S'$ with $S'\attacks S$, there is an admissible set $S''$ with $S' \cup \{a\} \subseteq S''$.
    \end{enumerate}
\end{theorem}
The above theorem states that we can decide skeptical acceptance wrt.\ preferred semantics by considering only those admissible sets that attack an admissible set containing the argument in question. As an admissibility check can be solved by a satisfiability check, similarly as above, the above insight leads to an algorithm that can solve $DS$-$PR$ without actually computing preferred extensions.
%The algorithm is presented in detail in \cite{Thimm:2021} and experiments confirm a significant performance improvement compared to previous encoding approaches.

Coming to ideal semantics, it is worth recalling \cite[Theorem 3.3]{ideal}.

\begin{theorem}[{\cite[Theorem 3.3]{ideal}}]
    An admissible set of arguments $S$ is ideal iff for each argument $a$ attacking $S$ there exists no admissible set of arguments containing $a$.
\end{theorem}

The interesting aspect of \cite[Theorem 3.3]{ideal} is that ideal semantics, although defined based on skeptical acceptance wrt.\ preferred semantics, does not rely on that notion. Moreover, in \cite{Thimm:2021} we also prove that starting from the set of arguments which are not attacked by an admissible set, its largest admissible set is the ideal extension. We can therefore tweak the machinery we created for computing skeptical acceptance wrt.\ preferred semantics to compute the ideal extension too. The complete algorithm is presented in \cite{Thimm:2021}.

\fudge\ is written in C++ and uses the IPASIR\footnote{\url{https://github.com/biotomas/ipasir}} interface to connect to a satisfiability solver. It comes with CaDiCaL 2.1.0\footnote{\url{http://fmv.jku.at/cadical/}} pre-configured. \fudge\ improves over its previous version v2.4 submitted at ICCMA'21 by using a different method for calling the SAT solver, as well as streamlined encodings, and support for the semi-stable and stage semantics.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Changes to \textsc{Fudge v3.2.8} (ICCMA'23 version)}\label{sec:changes}
The most significant change is the adoption of the IPASIR interface to connect to any satisfiability solver. Further changes pertain to bug fixes and code streamlining.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Summary}\label{sec:summary}
We presented \fudge\, a reduction-based solver for various problems in abstract argumentation. \fudge\ leverages on a mix of standard and novel SAT encodings to solve reasoning problems, with the aim of avoiding the costly maximisation step that is characteristic of some of the abstract argumentation problems. 
The source code of \fudge\ is available at \url{https://github.com/aig-hagen/taas-fudge}.

\bibliographystyle{plain}
\bibliography{references.bib}

\end{document}
