Reasoning in abstract dialectical frameworks using quantified Boolean formulas

1.Introduction

Since its invention by Dung (1995), abstract argumentation constitutes one of the main research branches for computational models of argument. Hereby, the conflict resolution between arguments is done by abstracting away from the arguments' contents, yielding a simple yet powerful framework for reasoning used as a core model in many argumentation tasks and applications. Although very general, Dung's argumentation frameworks (AFs) do not directly support modelling more complex interactions between arguments. For this and similar issues, several extensions of AFs have been proposed to date (e.g. those presented by Baroni, Cerutti, Giacomin, Guida, 2011; Bench-Capon, 2003; Cayrol & Lagasquie-Schiex, 2005; Brewka, Polberg, & Woltran, 2014 provide a survey of this line of research), one of the most general being that of abstract dialectical frameworks (ADFs) by Brewka and Woltran (2010). In this last framework, acceptance conditions in the form of arbitrary Boolean formulas are associated to every argument. Proper generalisations of Dung's semantics have been given by Brewka, Ellmauthaler, Strass, Wallner, and Woltran (2013).

Various reasoning tasks can be defined on abstract argumentation frameworks, some of the central ones being those that evaluate the ‘acceptability’ of an argument with respect to a given framework and semantics. Already for AFs, most of the reasoning tasks have been shown to suffer from high computational complexity (see e.g. the work by Dunne & Bench-Capon, 2002). For ADFs, the complexity of many of the main reasoning tasks with respect to the generalised semantics jump up one level of the polynomial hierarchy (as has been shown by Strass & Wallner, 2014; Wallner, 2014), resulting in some of the reasoning tasks even being on the third level of the polynomial hierarchy.

One successful approach for implementing problems of high computational complexity is to employ a so-called reduction approach (Charwat, Dvořák, Gaggl, Wallner, & Woltran, 2015). Hereby the underlying idea is to exploit existing efficient software which has originally been developed for other purposes. To this end, one has to formalise the reasoning problems within other formalisms like, for instance, propositional logic, thus directly benefiting from the high level of sophistication today's systems for SAT (satisfiability in propositional logic) have reached (Franco & Martin, 2009).

In this work we follow this idea and present translations of the main reasoning tasks defined for ADFs into the satisfiability problem of quantified Boolean formulas (QBFs). QBFs are an extension of propositional logic, allowing for quantification over propositional atoms (Büning Bubeck, 2009). Its associated satisfiability problem (QSAT) is complete for PSPACE while types of QBFs classified according to the structure of quantification provide us with complete problems for each level of the polynomial hierarchy. These results indicate that reasoning problems for ADFs can be efficiently transformed into QSAT problems with a certain quantifier structure. Employing the framework of QBFs thus allows for

Providing reductions to QSAT is increasingly seen as a promising approach to tackle computational problems in the polynomial hierarchy. Planning (see the work by Ferraris & Giunchiglia, 2000; Rintanen, 1999) and formal methods for determining correctness of software systems (as shown by Benedetti & Mangassarian, 2008; Bryant, Lahiri, & Seshia, 2003; Giunchiglia, Narizzano, & Tacchella, 2007; Ling, Singh, & Brown, 2005; Mneimneh & Sakallah, 2003) are notable examples of areas where QSAT solvers have found their way into practice. Moreover, reductions of many reasoning problems in different areas including knowledge representation and reasoning (reductions of autoepistemic, default logic, disjunctive logic programming, and circumscription problems into QSAT are given by Egly, Eiter, Tompits, & Woltran, 2000 for example) into QSAT have also been proposed in the literature. Giunchiglia, Marin, and Narizzano (2009) list several more examples of reductions of computational problems to QSAT.

Our work specifically continues the line of of study that has been initiated for Dung style AFs by Egly and Woltran (2006) and Arieli and Caminada (2013). In both of these works, reductions of the problems of evaluating Dung style AFs into the setting of quantified Boolean logic are given. The more recent work by Arieli and Caminada in particular, which is based on a so called ‘labelling approach’ (Caminada & Gabbay, 2009) to defining the semantics of AFs presents some parallels with the approach followed by Brewka et al. (2013) and Strass (2013), respectively, to define the semantics for ADFs. Thus this work has been particularly influential for the approach we follow to give encodings for the reasoning problems defined for ADFs.

Summarising, in this article we provide complexity sensitive encodings of all the main reasoning problems defined for ADFs (evaluation, credulous acceptance, skeptical acceptance and verification) with respect to the most prominent semantics (two valued models, admissible, complete, preferred, grounded and stable) in the context of QBFs. Further, we present the formal framework required to prove that our encodings are correct as well as detailed proofs. This article extends the work of Diller, Wallner, and Woltran (2014) and Diller (2014) by three novel contributions: (1) we additionally consider the reasoning task of verifying a given candidate solution, (2) we expanded all proofs, and (3) we present here complexity sensitive encodings also for the grounded and stable semantics.

2.Background

2.2.Abstract dialectical frameworks

An abstract dialectical framework (ADF) is a directed graph whose vertices represent statements which can be accepted or not. The links represent dependencies: the status of a node s only depends on the status of its parents (denoted parents(s)), that is, the nodes with a direct link to s. In addition, each node s has an associated acceptance condition Cs specifying the conditions under which s can be accepted. Cs is a function assigning to each subset of parents(s) one of the truth values t, f.

Definition 2.4.

An ADF is a tuple D=(S,L,C) where

• S is a set of statements (positions, nodes),

• L⊆S×S is a set of links,

• C={Cs}s∈S is a set of total functions Cs:2parents(s)→{t,f}, one for each statement s. Cs is called acceptance condition of s.

We represent the acceptance conditions C as a collection {φs}s∈S of propositional formulas, which provide a compact way to specify Boolean functions. This leads to the logical representation of ADFs we use in this paper where an ADF D is a pair (S,C) with the set of links L implicitly given as (a,b)∈L iff a appears in φb.

We consider ADF semantics as defined by Brewka et al. (2013). A semantics σ assigns to an ADF D a collection of two or three valued interpretations, denoted by σ(D). To distinguish between interpretations of ADFs and QBFs we use vˆ,wˆ for QBF interpretations and v,w for interpretations of ADFs. For σ we consider in this paper admissible, complete, grounded, preferred, model and stable semantics of ADFs. We denote the semantics by adm,com, grd, prf, mod and stb.

The interpretations map statements to truth values. We use {t,f,u} as truth values, denoting true, false and undecided, respectively. The three truth values are partially ordered by ⩽i according to their information content: we have u<it and u<if and no other pair in <i. The information ordering ⩽i extends in a straightforward way to interpretations v1,v2 over S in thatv1⩽iv2 iff v1(s)⩽iv2(s) for all s∈S.

A three valued interpretation v is two valued if all statements are mapped to either true or false. For a three valued interpretation v, we say that a two valued interpretation w extends v iff v⩽iw. This means that all statements mapped to u by v are mapped to t orf by w. We denote by [v]2 the set of all two valued interpretations that extend v.

For an ADF D=(S,C), s∈S and a three valued interpretation v, the characteristic function ΓD(v)=v′ is given by

v′(s)=t if w(φs)=t for all w∈[v]2,f if w(φs)=f for all w∈[v]2,u otherwise.

That is, the operator returns a three valued interpretation, mapping a statement s to t, or, respectively f, if all two-valued interpretations extending v evaluate φs to true, respectively false. If there are w1,w2∈[v]2, s.t. w1(φs)=t and w2(φs)=f, then the result is u. Note that the characteristic function is defined on three-valued interpretations, while we evaluate acceptance conditions under two-valued interpretations (two-valued extensions of three-valued interpretations).

Definition 2.5.

Let D=(S,L,C) be an ADF. A three valued interpretation v is

• in adm(D) if v⩽iΓD(v);

• in com(D) if v=ΓD(v);

• in grd(D) if v∈com(D) and there is no w∈com(D) with w<iv;

• in prf(D) if v∈adm(D) and there is no w∈adm(D) with v<iw.

No other elements except those stipulated by the items above are in adm(D), com(D), grd(D) and prf(D), respectively.

For any ADF one has that all preferred interpretations are complete and all complete interpretations are admissible. Brewka et al. (2013) have also shown that the operator ΓD is monotonic for any ADF D, hence an interpretation v is the grounded interpretation of an ADF D if and only if it is equal to the ⩽i least fixpoint (l.f.p.) of ΓD. The l.f.p. can be calculated by iteratively applying ΓD starting with the interpretation US mapping all statements s∈S of D to u. Then ΓD0:=US and ΓDi+1:=ΓD(ΓDi) fori⩾0.

The mod and stb semantics rely on two valued interpretations. A two valued interpretation v is a model of an ADF D=(S,C={φs}s∈S) if v(s)=v(φs) for all s∈S. Stable models are defined via a reduct.

Definition 2.6.

Let D=(S,L,C) be an ADF with C={φs}s∈S. A two-valued model v of D is a stable model of D iff Ev={s∈S∣v(s)=t} equals the statements set to true in the grounded interpretation of the reduced ADF Dv=(Ev,Lv,Cv), whereLv=L∩(Ev×Ev) and for s∈Ev we set φsv=φs[b/⊥:v(b)=f].

Example 2.7.

In Figure 1 we see an example ADF D=({a,b,c},C) with φa=b∨¬b≡⊤, φb=b and φc=c→b. The acceptance conditions are also shown below the statements.

Figure 1.

ADF example.

The admissible interpretations of D are shown in Table 1. Furthermore the right-most column shows further semantics the interpretations belong to. For instance the interpretation v8 mapping each statement to true is admissible, complete and preferred in D and a model of D. This ADF has no stable model. The only model of D is v8, with the reduct of this model being Dv8=D. The grounded interpretation of D is v6, which is different than v8. Therefore v8 is not a stable model.

We recall three important reasoning tasks on ADFs for a semantics σ. A statement s is credulously accepted in an ADF D for σ if s is true in at least one v∈σ(D). The corresponding decision problem is denoted by Credσ. If s is true in all v∈σ(D), then it is skeptically accepted in D w.r.t. σ, the decision problem denoted by Skeptσ. Lastly, the verification problem, Verσ, decides whether a given three (two) valued interpretation v is a σ interpretation for a given ADF D, that is, whether it holds that v∈σ(D). The computational complexity of reasoning in ADFs is summarised in Table 2. The results were shown by Brewka et al. (2013), Strass and Wallner (2014) and Wallner (2014).

Table 1.

All admissible interpretations of the ADF from Figure 1.

	a	b	c
v1	u	u	u	adm
v2	u	f	u	adm
v3	u	t	u	adm
v4	t	t	u	adm
v5	u	t	t	adm
v6	t	u	u	adm, com, grd
v7	t	f	u	adm, com, prf
v8	t	t	t	adm, com, prf, mod

Note: Right-most column shows further semantics the interpretations belong to.

Table 2.

Complexity results for semantics of ADFs.

σ	adm	com	prf	grd	mod	stb
Credσ	Σ2P-c	Σ2P-c	Σ2P-c	coNP-c	NP-c	Σ2P-c
Skeptσ	trivial	coNP-c	Π3P-c	coNP-c	coNP-c	Π2P-c
Verσ	coNP-c	DP-c	Π2P-c	DP-c	in P	coNP-c

Example 2.8.

Continuing Example 2.7 we can see that a is skeptically accepted w.r.t. preferred semantics in the ADF D. (i.e. Skeptprf(a,D) is true). The statement b is not skeptically accepted for preferred semantics, however it is credulously accepted under this semantics. In fact here all statements are credulously accepted under admissible, complete, preferred and model semantics. As on all ADFs, credulous and skeptical acceptance coincide for grounded semantics and in this example only a is accepted w.r.t. the grounded semantics.

3.Encodings

In this section we present the encodings of reasoning tasks for ADFs into QBFs. After dealing with some preliminaries for our encodings, we develop for each semantics σ∈{adm,com,grd,prf,mod,stb} a defining encoding function, denoted by Eσ. Given an ADF D=(S,C), Eσ returns a QBF whose models correspond to the σ interpretations of D. Such defining encoding functions return the encoding of the enumeration problem for the different semantics and can be used in a generic fashion to provide encodings for the reasoning tasks we consider in this work. We describe how to do so at the end of Section 3.2.

This method for providing encodings has the advantage of being general in the sense that the encodings of the reasoning tasks we provide at the end of Section 3.2 for some semantics σ remain correct if the defining encoding function Eσ is redefined. On the other hand, whether or not the encodings for the reasoning tasks are mapped to a fragment of QSAT that matches the complexity of the tasks depends on the definition of the encoding function. For a few of the reasoning tasks we consider in this work, the defining encoding functions we provide result in encodings that are not sensitive to the complexity of the tasks. These cases either are equivalent to some other reasoning task for which we provide encodings that are adequate with respect to the complexity, or otherwise we provide alternative complexity sensitive encodings in Section 3.3.

As indicated above, we begin with some preliminaries. To express constraints on the values to which an interpretation on ADFs can map statements, in our encodings we make use of variables that stand for the statements of an ADF. Since the definitions of semantics of ADFs often refer to several interpretations (e.g. the extensions of a given interpretation) to express such definitions in the language of quantified Boolean logic we in fact need to use several disjoint sets of propositional variables standing for statements to implicitly refer to these different interpretations in our encodings. We generate such sets by using priming (with p′ denoting the primed version of a propositional variable p) on a base set of variables representing the statements of a given ADF. We call variables which stand for statements of ADFs variable set copies of the set of statements.

The purpose of introducing the notation S¯ and S¯¯ in Definition 3.1 is that this enables stating the content of the propositions in this section in a manner that covers any possible variable set copy that can be used when instantiating the encodings the propositions refer to. This makes it possible to simplify proofs about properties of encodings which are constructed in a modular fashion.

To encode expressions about two valued interpretations on a set of statements S as QBFs we use a variable set copy of S. To refer to three valued interpretations inside QBFs on the other hand we follow the procedure that has already been used by Arieli and Caminada (2013) to encode expressions about (three valued) labellings for AFs. Specifically, we assume that for every set S¯ of propositional variables representing statements of some ADF the alphabet of QBFs also contains the set of signed variables corresponding to S¯.

The intended meaning of s¯⊕ is that s is accepted and s¯⊖ that s is rejected under some interpretation. Intuitively, a statement is undecided if both s¯⊕ and s¯⊖ are false in a model.

ADF semantics are based on three or two truth values. Since there are four possible truth value assignments for a statement s via s¯⊕,s¯⊖∈S¯3, we need to restrict attention to coherent interpretations for QBFs, which exclude the possibility for a model to satisfy both s¯⊕ ands¯⊖.

We now formally define the correspondence we require of the models of the QBFs returned by a defining encoding Eσ for a semantics σ and the σ interpretations of the ADFs.

The following lemma is a straightforward consequence of Definition 3.4 we make often use of in the proofs of correctness of the encodings we provide in this work.

We are finally in a position to provide the formal definition of a defining encoding function Eσ for a given semantics σ for ADFs. Given an ADF D=(S,C), Eσ returns a QBF whose every model corresponds (in the sense of Definition 3.4) to one of the σ interpretations of D (‘soundness’). In turn, every σ interpretation corresponds to a model of ϕ (‘completeness’). Given a variable set copy S¯ of S and depending on whether σ returns two valued or three valued interpretations, Eσ returns a QBF with free variables in a set of signed (S¯3) or unsigned (S¯) variables standing for the statements of the ADFs, respectively. We thus write Eσ[(S¯,C¯)] for the application of the defining encoding function Eσ to the ADF D=(S,C). In addition to soundness and completeness, when σ returns three valued interpretations (σ∈{adm,com,prf,grd,mod,stb}), Eσ[(S¯,C¯)] must also be a QBF whose models are coherent on S¯3 in the sense of Definition 3.3.