Many proposals for logic-based formalisations of argumentation consider an argument as a pair (Φ,α), where the support Φ is understood as a minimal consistent subset of a given knowledge base which has to entail the claim α. In case the arguments are given in the full language of classical propositional logic reasoning in such frameworks becomes a computationally costly task. For instance, the problem of deciding whether there exists a support for a given claim has been shown to be -complete. In order to better understand the sources of complexity (and to identify tractable fragments), we focus on arguments given over formulæ in which the allowed connectives are taken from certain sets of Boolean functions. We provide a complexity classification for four different decision problems (existence of a support, checking the validity of an argument, relevance and dispensability) with respect to all possible sets of Boolean functions. Moreover, we make use of a general schema to enumerate all arguments to show that certain restricted fragments permit polynomial delay. Finally, we give a classification also in terms of counting complexity.
Argumentation is nowadays a main research topic within the area of Artificial Intelligence (Bench-Capon and Dunne 2007; Besnard and Hunter 2008; Rahwan and Simari 2009) aiming to formally analyse the pros and cons of statements within a certain scenario in order to understand implicit conflicts and to support decision-making. The overall process of formal argumentation can be considered as a sequence of the following steps; see, for instance, the work by Caminada and Amgoud (2007) or Gorogiannis and Hunter (2011): Given a knowledge base Δ, in the first step arguments are formed, and then conflicts between the arguments are identified. Next, one abstracts from the concrete contents of the arguments and uses certain semantics to find acceptable subsets of arguments by analysing solely the graph obtained from the arguments and conflicts; this particular step was first proposed by Dung (1995) who invented the concept of abstract argumentation frameworks. Finally, by inspecting selected arguments certain conclusions can be made. Towards practicably efficient realisations, a good understanding of the computational complexity of all these single steps is thus of high importance.
We focus here on the first step of this process, i.e. forming valid and plausible arguments from a given set of formulæ. This step is also sometimes referred to as logic-based argumentation (Chesñevar, Maguitman, and Loui 2000; Prakken and Vreeswijk 2002; Besnard and Hunter 2008; Amgoud and Besnard 2010) in order to separate it from the abstraction as used in Dung's frameworks. One goal in logic-based argumentation is thus to find a concrete formal representation of an argument and then to define – on top of this concept – notions such as counterarguments, rebuttals or undercuts (see Besnard and Hunter 2001). Many proposals consider an argument as a pair , where the support Φ is a consistent set (or a minimal consistent set) of formulæ from a given knowledge base that entails the claim α which is a formula (Cayrol 1995; Besnard and Hunter 2001; Amgoud and Cayrol 2002; García and Simari 2004; Dung, Kowalski, and Toni 2006). Different logical formalisms provide different definitions for consistency and entailment and hence give different options for defining the notion of an argument. One natural candidate for formalising arguments is the full language of classical propositional logic. However, it is computationally challenging to generate arguments from a knowledge base Δ, using classical logic; in fact, the problem of deciding whether there exists a support for a given claim α has been shown to be -complete by Parsons, Wooldridge, and Amgoud (2003).
Computing the support for an argument underlies many reasoning problems in logic-based argumentation, for instance, the computation of argument trees as proposed by Besnard and Hunter (2001). Since the basic task of finding a support is already computationally involved, it is indispensable to understand its sources of complexity and to identify fragments for which that problem becomes tractable. In this paper, we contribute to this line of research by restricting the formulæ involved (i.e. formulæ in the knowledge base and thus in the support, as well as the formula used as the claim). In fact, we restrict formulæ to use only connectives from a given set B of Boolean functions and study the decision problems of existence, validity, relevance, and respectively, dispensability, which are defined as follows:
• Arg (Argumentation): given Δ, α, does there exist a support for α?
• Arg-Check (Argument Checking): given a pair , is it an argument?
• Arg-Rel (Argument Relevance): given Δ, α, ϕ, is there an argument such that ?
• Arg-Disp (Argument Dispensability): given Δ, α, ϕ, is there an argument such that ?
• #Arg (Argument Counting): given Δ, α, how many arguments with exist?
• Enum-Arg (Argument Enumeration): given Δ, α, output all arguments such that .
It can be seen that the minimality condition is only important for the decision problems Arg-Check and Arg-Rel (for instance, in case of Arg-Disp, there exists a support Φ without ϕ for α exactly if there exists a minimal such support; we will make this more precise in Section 2.3) as well as for #Arg and Enum-Arg. For the Enum-Arg problem, we will provide a general scheme to compute all arguments making use of decision procedures for Arg-Check, Arg-Rel and Arg-Disp. This also indicates the practical relevance of the decision problems we study, since enumerating all arguments is the central task in the overall process discussed above. However, also counting the number of arguments is of importance. Consider two different formulæ α, β, it might be of interest to know whether more arguments of form than arguments of form exist for a given knowledge base. Usually, such counting problems are considered without explicitly making use of enumeration procedures. Note that the latter might have to output an exponential number of solutions (thus requiring exponential time), although the number of solutions may be efficiently computable. In fact, counting complexity recently gained interest in AI as is witnessed by work from Hermann and Pichler (2010) or Durand and Hermann (2008). However, except recent work by Barnoi, Dunne, and Giacomin (2010), who consider counting complexity for abstract argumentation, we are not aware of such investigations in the area of argumentation.
A major tool when analysing the complexity of problems parameterised by a given set B of Boolean connectives is Post's lattice: a lattice showing the inclusion relations between all existing sets of Boolean functions that are closed under superposition (that is, roughly speaking, closed under arbitrary composition, see Section 2.2 for a formal definition). Several complexity classifications have already been obtained in this so-called Post's framework, such as the classical satisfiability problem (Lewis 1979), equivalence and implication problems (Reith 2003; Beyersdorff, Meier, Thomas, and Vollmer 2009a), satisfiability and model checking in modal and temporal logics (Bauland, Hemaspaandra, Schnoor, and Schnoor 2006; Bauland, Schneider, Schnoor, Schnoor, and Vollmer 2008), default logic (Beyersdorff, Meier, Thomas, and Vollmer 2009b), circumscription (Thomas 2009) and abduction (Creignou, Schmidt, and Thomas 2010).
The main contribution of this paper is a systematic complexity classification for the six aforementioned problems in terms of all possible sets of Boolean connectives.
• Concerning the four decision problems, we show that, depending on the chosen set of connectives, the problems range from inside P up to the second level of the polynomial hierarchy, and we identify those fragments complete for NP, coNP, and also for DP, the class of differences of problems in NP. We also show that unless the polynomial hierarchy collapses there exist particular sets of Boolean connectives such that: (i) deciding the existence of an argument is easier than verifying a given one; (ii) deciding the dispensability of a formula for some argument is easier than deciding its relevance.
• We provide a general schema for enumerating all arguments. For the fragments which have their decision problems in P, we also obtain positive results in terms of enumeration by showing that either each solution is computed with at most polynomial delay (for the fragments where the number of arguments might be exponential) or that all solutions can be computed in polynomial time (which obviously is only possible for fragments where the number of arguments is bounded polynomially in the size of the knowledge base and the claim). Finally, we complement our picture by considering the problem of counting the number of arguments in terms of all possible sets of Boolean connectives.
The paper is structured as follows. Section 2 contains the necessary background on complexity theory (Section 2.1) and on Post's lattice (Section 2.2). Moreover, we define the studied framework of argumentation and relevant problems in Section 2.3. We then turn to our main results which are given in Sections 3 and 4. More specifically, the complexity of the decision problems is classified in Sections 3.2–3.4, enumeration is studied in Section 4.1 and counting complexity is dealt with in Section 4.2. We summarise our results and discuss their relation to similar work (as e.g. in the area of abduction) in a dedicated Section 5. Finally, Section 6 concludes with a brief recapitulation of the achieved results as well as future research directions.
We assume familiarity with propositional logic. The set of all propositional formulæ is denoted by ℒ. A model for a formula ϕ is a truth assignment to the set of its variables that satisfies ϕ. Further, we denote by the formula obtained from ϕ by replacing all occurrences of α with β.
For a given formula ϕ, we denote by the set of variables occurring in ϕ. We extend this definition on sets of formulæ Γ as . We identify finite Γ with the conjunction of all the formulæ in Γ, . Naturally, then stands for . We say that two formulæ ϕ and ψ are equivalent (written ) if every assignment on the combined variable sets satisfies ϕ if and only if it satisfies ψ. For any formula , we write if Γ entails ϕ, i.e. if ϕ is satisfied in every model of Γ.
A literal l is a variable x or its negation ¬ x. A positive literal is a variable x, a negative literal is the negation of a variable ¬ x. Given a set of variables V, Lits(V) denotes the set of all literals formed upon the variables in V, i.e. . A clause is a disjunction of literals and a term is a conjunction of literals.
We require standard notions of the complexity theory. For the decision problems, the arising complexity degrees encompass the classes Logspace, P, NP, coNP, DP and . The class DP is defined as the set of languages recognisable by the difference of two languages in NP, i.e. . The class is the set of languages recognisable by non-deterministic polynomial-time Turing machines with an NP oracle. For our hardness results, we employ logspace many-one reductions, defined as follows: a language A is logspace many-one reducible to some language B (written ) if there exists a logspace-computable function f such that x∈A if and only if f(x)∈B. Thus, for 𝒞 being any of the complexity class NP, coNP, DP or , we call 𝒞-hard a problem G if any instance of a generic problem in 𝒞 can be reduced to an instance of G by means of a logspace many-one reduction. If in addition G belongs to the class 𝒞, then it is called 𝒞-complete. A complete problem for DP is Critical-Sat, the problem to decide whether a given formula in 3CNF is unsatisfiable, but removing any of its clauses makes it satisfiable (Papadimitriou and Wolfe 1988). A prototypical -complete problem is deciding the truth of an expression where β is a propositional formula over the set of variables X∪Y. This quantified formula is valid if and only if there exists a truth assignment to the variables of X such that for all truth assignments to the variables of Y the formula β is true. In this paper, we use a more restricted version, that we denote by , in which the formula β is 3-DNF, and which is still -complete.
When analysing an enumeration algorithm, polynomial time complexity is not a suitable yardstick of efficiency since the output size is usually exponential in the size of the input. We consider an enumeration algorithm to be efficient, when it runs in polynomial delay, i.e. if the delay until the first solution is output, thereafter the delay between any two consecutive solutions, and the delay between the last solution and termination is bounded by a polynomial p(n) in the input size n. This notion of efficiency for enumeration has first been introduced by Johnson, Papadimitriou, and Yannakakis (1988). We denote the corresponding complexity class by DelayP.
A counting problem is represented using a witness function w, which for every input x returns a finite set of witnesses. This witness function gives rise to the following counting problem: given an instance x, find the cardinality of the witness set w(x). The class #P; is the class of counting problems naturally associated with decision problems in NP. According to Hemaspaandra and Vollmer (1995), if 𝒞 is a complexity class of decision problems, we define to be the class of all counting problems whose witness function is such that the size of every witness y of x is polynomially bounded in the size of x, and checking whether y∈w(x) is in 𝒞. Thus, we have and . Completeness of counting problems is usually proved by means of Turing reductions. A stronger notion is the parsimonious reduction (Papadimitriou 1994), where the exact number of solutions is conserved by the reduction function. When there is a parsimonious reduction from a counting problem #A to a counting problem #B we write .
For more background information on complexity theory, the reader is referred to Papadimitriou (1994).
A Boolean function is an n-ary function . A clone is a set of Boolean functions that is closed under superposition, i.e. it contains all projections (that is, the functions for all 1≤k≤n and ) and is closed under arbitrary composition (that is, application of one function to the results of other functions). Let B be a finite set of Boolean functions. We denote by [B] the smallest clone containing B and call B a base for [B]. Post (1941) identified, the set of all clones of Boolean functions. He gave a finite base for each of the clones and showed that they form a lattice under the usual ⊆-relation, hence the name Post's lattice (Figure 1). To define the clones, we introduce the following notions, where f is an n-ary Boolean function:
• f is c-reproducing if , . The binary (∧) and the binary (∨) are 0- and 1-reproducing, the binary exclusive or (⊕) is 0-reproducing, but not 1-reproducing, whereas the unary negation (¬ ) is neither 1- nor 0-reproducing.
• f is monotonic if implies . Boolean functions built up on composition of only ∧, ∨, 0, 1 are monotonic, like for instance .
• f is c-separating of degree k if for all of size |A|=k there exists an such that implies ai=c, . The (m+1)-ary function being true if and only if ‘at least m variables are true’ is 1-separating of degree m. For instance is 1-separating of degree 2.
• f is c-separating if f is c-separating of degree | f−1(c)|. The implication is 0-separating.
• f is self-dual if , where . The function is self-dual.
• f is affine if with . The function is affine and self-dual.
• the clone of all Boolean functions
• the monotonic clones , e.g. ,
• the affine clones , e.g. ,
• the disjunctive clones , e.g. ,
• the conjunctive clones , e.g. ,
• the c-reproducing clones , 1-repr., 0-repr., 1- and 0-repr.
• the implication clone
• the negated-implication clone
• the dual clones , self-dual, ,
• the clones , and
|All Boolean functions|
|is a disjunction of variables or constants</texlscub>|
|is a conjunction of variables or constants</texlscub>|
|depends on at most one variable</texlscub>|
For an example on how these identities will be useful, see Section 3.1, in particular at the end.
A propositional formula using only functions from B as connectives is called a B-formula. The set of all B-formulæ is denoted by .
Let f be an n-ary Boolean function. A B-formula ϕ is called B-representation of f if . Such a B-representation exists for every f∈[B]. Yet, it may happen that the B-representation of some function uses some input variable more than once, see Example 2.1.
Example 2.1Exponential blow up
Let . An -representation of the binary , , is . Observe that an -representation of the n-ary , , based on the recursive application of the -representation of the binary to the formula
Throughout the paper, Δ is assumed to be a given finite set of formulæ (the knowledge base) representing a large depositary of information, from which arguments can be constructed for arbitrary claims.
Following Besnard and Hunter (2001), an argument is a pair , where Φ is a set of formulæ and α is a formula such that
(1) Φ is consistent,
(3) Φ is minimal with this last property, i.e. no proper subset of Φ entails α.
(C1) Φ is satisfiable,
(C2) is unsatisfiable (i.e. ), and
(C3) for all , is satisfiable (i.e. Φ is minimal).
Let B be a finite set of Boolean functions. Then the argument existence problem for B-formulæ is defined as
Instance: , where and .
Question: Does there exist Φ such that is an argument in Δ?
Besides the decision problem for the existence of an argument, we are interested in the decision problems for B-formulæ for validity, relevance and dispensability. They are defined as follows and deal with formulæ in only.
Instance: , where and .
Question: Is an argument?
Instance: , where and .
Question: Does there exist an argument in Δ such that ?
Instance: , where and .
Question: Does there exist an argument in Δ such that ?
Observe that the minimality of the support is only relevant to the problems Arg-Check and Arg-Rel. For Arg and Arg-Disp, the existence of a consistent subset Φ of the knowledge base Δ that entails the claim α (and does not contain some formula ϕ) implies a consistent such that and for all . To decide the existence of an argument, it therefore suffices to find any consistent subset of Δ that entails α. For Arg-Rel, on the other hand, we have to decide whether there exists an argument for α that contains the formula ϕ. The existence of some consistent set with and does not help here, because ϕ might be excluded from the minimal subset yielding an argument for α. Consequently, unlike in other non-monotonic reasoning formalisms, the complexity of deciding relevance and dispensability of a formula for some argument may differ. Indeed, we will show that there exist sets B such that Arg-Rel(B) is harder to decide than Arg-Disp(B) unless the polynomial hierarchy collapses. Similarly, for Arg-Check, we have to verify that the set Φ in the given pair is indeed minimal with respect to consistency and entailment of α. While this is supposedly easier to decide than Arg, we will see that owing to the verification of minimality there exist sets B such that Arg-Check(B) is harder to decide than Arg(B) unless the polynomial hierarchy collapses.
Other interesting tasks are to enumerate all solutions or to count them.
Instance: , where and .
Output: Generate all arguments in Δ without repetition.
Instance: , where and .
Output: Number of arguments in Δ.
Obviously, for both Enum-Arg(B) and #Arg(B), minimality of the support plays a crucial role, as well.
3.1Tools and methods
Observe that if B1 and B2 are two sets of Boolean functions such that , then every function of B1 can be expressed by a B2-formula, namely by its B2-representation. This way there is a canonical reduction between Arg and Arg if : replace all B1-connectives by their B2-representation. This reduction is not necessarily polynomial: Since the B2-representation of some function may use some input variable more than once, the formula size may grow exponentially, see Example 2.1. (The existence or not of a polynomial-size B2-representation for any B1-formula is a topic of independent interest, which has been addressed several times in the literature, see e.g. Spira 1971; Karchmer and Wigderson 1988). Nevertheless, we will use the idea of this canonical reduction very frequently, dealing only with cases where exponential blow up can be avoided by special structures of the B1-formulæ, similar to Example 2.1.
When we show hardness-results for Arg(B) for some B such that (C a clone), we generally show hardness first only for Arg(C) and show then in a second step that the proof can indeed be extended to show hardness also for Arg(B), using the above-mentioned canonical reduction.
The following lemmas show that we can often suppose that our considered B contains the constant 1. This will reduce the number of cases to study.
Let Arg- denote any of the problems Arg, Arg-Check or Arg-Rel. Let B be a finite set of Boolean functions such that i.e. . Then Arg- Arg-.
Let ℐ be the given instance. We map ℐ to the instance ℐ′ obtained by replacing each formula ψ occurring in ℐ by , where t is said to be a fresh variable. ▪
In addition on this, one can also eliminate the constant 1 for the problems Arg(B) and Arg-Rel(B) when .
Let B be a finite set of Boolean functions such that . Then Arg Arg(B) and Arg-Rel Arg-Rel(B).
Let . The function g is a base of and evaluates to true if and only if at least two of the variables are set to true. Given an instance of Arg , we define an instance of Arg(B) by and ,where t and q are fresh variables. We claim that there is an argument for α in Δ if and only if there is an argument for α′ in Δ′.
Let Φ be an argument for α in Δ. Consider . Observe that . Thus Φ′ is satisfiable and , hence , as t does not occur in α. Therefore, we obtain . Moreover, either Φ′ or is minimal with this property. Indeed, suppose that there exists a with for some ψ∈Φ such that . Then as q does not occur in Φ′, and hence , contradictory to the minimality of Φ.
Conversely, with similar arguments, it is easy to see that if Φ′ is an argument for α′ in Δ′, then is an argument for α in Δ: as q does not occur in Φ′, implies that .
This proves a correctness of the reduction from Arg to Arg(B). The analogous result for Arg-Rel follows from the same arguments as above, mapping the additional component ϕ to . ▪
Observe that this reduction does not work for Arg-Check: one would have to decide whether to map Φ to Φ′ or to to ensure minimality, which requires the ability to decide whether in Logspace. Further observe that an analogous statement of Lemma 3.1 for the constant 0 cannot be obtained in the obvious way. Replacing every formula ψ by for a fresh variable f fails since such a reduction does not preserve consistency.
Let us show in an example how one can use these lemmas. Suppose, we want to show hardness results for Arg-Rel(B) in the case where or or (see Theorem 3.9). Since in the latter two cases either or , according to Lemmas 3.1 and 3.2 we have Arg-Rel Arg-Rel(B). Therefore, it is sufficient to prove hardness for Arg-Rel . Observe that if then and if then . Since and , we have in both cases . So, finally in order to prove that Arg-Rel(B) is hard in the case where or or , it is sufficient to prove that the hardness holds for B such that .
We will henceforth give less details when applying Lemmas 3.1 and 3.2.
3.2The complexity of verification
We commence our study of the introduced argumentation problems with the argument verification problem. This problem is in DP. Indeed, it is readily observed, as there are languages A, B with A∈NP and B∈coNP such that Arg-Check = , with
The next two results will cover all cases where we have a matching lower bound, i.e. we provide those clones for which DP-hardness holds.
Let . Then Arg-Check(B) is DP-complete.
To prove DP-hardness, we establish a reduction from Critical-Sat. Let be an instance of Critical-Sat, and . Let be fresh, pairwise distinct variables. Note that if Critical-Sat then each variable of ψ appears both as positive and as negative literal. Let further for 1≤j≤m and . We map ψ to , where we define
Since x∨ y and are functions of , α and all C′j’s are -formulæ. These are by definition 1-reproducing. Therefore, Φ and α are satisfiable. For 1≤k≤m, let Φk, ψk, ψk′ denote the respective set of clauses where we deleted the kth clause. Note that always and .
Suppose now that ψ ∈ Critical-Sat, i.e. ψ is unsatisfiable and ψk is satisfiable for all . We show that Φ entails α. Since is unsatisfiable, and is monotonic, all models of Φ have to set both xi and x′i to 1 for at least one . Since , we therefore have . Obviously also , thus we have .
It remains to prove that Φ is minimal. Since for each is satisfiable, no entails . A fortiori no Φk entails α.
Conversely suppose that Arg-Check. Then, in particular, Φ entails α[u/0]. Thus, we have , which implies that ψ is unsatisfiable. By the minimality of Φ we know that no Φk entails α. Since , we conclude that , which implies that is satisfiable. As ψk′ is monotonic, we also obtain that and hence ψk itself is satisfiable.
We finally transform into a B-instance for all B such that by replacing every connective by its B-representation. This transformation works in logarithmic space for Φ since it consists in clauses of size 3. It also does for α if we first represent it as an ∨-tree of depth logarithmic in n. ▪
Let B be a finite set of Boolean functions such that . Then Arg-Check(B) is DP-complete.
We give a reduction from Critical-Sat similar to Proposition 3.3. For , we define gk as the (k+1)-ary function verifying
We map ψ to , where we define
Obviously α and the formulæ in Φ are -formulæ and thus satisfiable. Let and for 1≤k≤m, let Φk, ψk, ψk′ denote the respective set of formulæ (clauses) where we deleted the kth formula (clause).
Note that if Critical-Sat then each variable of ψ appears both as positive and as negative literal. Without loss of generality we may further assume that each literal has at least two occurrences in two different clauses. These two properties will assure that we have for all
(i) : and . Since is unsatisfiable and ψ′ is monotonic, all models of ψ′ have to set both xi and xi′ to 1 for at least one . Therefore, .
(ii) (u, v)=(0, 0): and . Obviously .
It remains to prove that Φ is minimal. Since Critical-Sat, is satisfiable and hence does not entail , i.e. .
Conversely suppose that Arg-Check. Then, in particular, Φ[u/1] entails . Thus, we have , which implies that ψ is unsatisfiable. By the minimality of Φ, we obtain that no Φk entails α. One easily verifies that in the cases Φk still entails α (use Equation (2) for (u, v)=(0, 0)). Thus, we have that , which implies that is satisfiable. As ψk′ is monotonic, we obtain that and hence ψk itself is satisfiable, too.
Finally, we transform into a B-instance for all B such that in replacing all occurrences of gk by its B-representation. This transformation works in logarithmic space, because we may assume the function gn to be a g2-tree of depth logarithmic in n. ▪
The full picture for Arg-Check(B) is given in the forthcoming theorem, where we also provide the results for the ‘easier’ clones.
Let B be a finite set of Boolean functions. Then the argument validity problem for propositional B-formulæ, Arg – Check (B), is
(1) DP-complete if or or
(2) in P if
(3) in Logspace if or or .
For DP-completeness, according to Propositions 3.3 and 3.4, it remains only to deal with the case . Since , we obtain that Arg-Check is DP-hard by Proposition 3.4. As ∧∈[B], we may apply Lemma 3.1 and obtain the DP-hardness of Arg-Check(B).
In the case , the sets Φ, , and for all can be easily transformed into systems of linear equations. Thus, checking the three conditions as mentioned in Section 2.3 comes down to solving a polynomial number of systems of linear equations. This can be done in polynomial time, using Gaussian elimination. For , for , and for this check can be done in logarithmic space, as in this case the satisfiability of sets of B-formulæ can be determined in logarithmic space (Schnoor 2005). ▪
3.3The complexity of existence and dispensability
We next consider the problems Arg(B) and Arg-Disp(B). For the membership part of the forthcoming results, we can make use of the results from the previous subsection.
Let B be a finite set of Boolean functions. Then the argument existence problem for propositional B -formulæ, Arg(B), is
(1) -complete if or
(2) coNP-complete if with and
(3) in NP if
(4) in P if and
(5) in Logspace if or or .
The general argumentation problem has been shown to be -complete by Parsons et al. (2003) via a reduction from . An instance of this problem is a quantified formula , and one may assume that the formula β is in 3DNF, i.e. with exactly three literals by term. The authors map such an instance to , where , and . We use this reduction to obtain -completeness for Arg(B) if . We insert parentheses in β and obtain a formula of logarithmic parentheses-depth only. We can now substitute all occurring connectives with their B-representations and obtain this way in logarithmic space an instance of Arg(B) which is equivalent to the original .
As and , we obtain -completeness for the case according to Lemma 3.1. For the case , we obtain -completeness by Lemma 3.2, since and .
For with and , membership in NP follows from the facts that satisfiability is in Logspace (Lewis 1979), while entailment is in coNP (Beyersdorff et al. 2009a). To prove the coNP-hardness of Arg(B), we give a reduction from the implication problem for B-formulæ, which is coNP-hard if [B] contains one of the clones , , . Let be a pair of B-formulæ. We map this instance to if ψ is satisfiable (which is easy to decide) and to a trivial positive instance otherwise.
For , membership in NP follows from the fact that in this case Arg-Check is in P. Owing to the trivial satisfiability of B-formulæ for , we can improve the upper bound for Arg(B) with to membership in P.
In all other cases, Logspace-membership follows from the fact that both problems, satisfiability and entailment, are contained in Logspace (see Beyersdorff et al. 2009a) for B-formulæ.
Finally, observe that we have Arg-Disp Arg(B). To prove that Arg Arg-Disp(B), map to . For the converse direction, map to . ▪
3.4The complexity of relevance
The remaining decision problem to analyse is Arg-Rel(B) which turns out to be the most difficult in terms of complexity.
Let B be a finite set of Boolean functions such that . Then Arg-Rel(B) is -complete.
To see that Arg-Rel(B) is contained in , observe that, given an instance , we can guess a set such that and verify conditions (C1)–(C3) in polynomial time using an NP-oracle.
To prove -hardness, we provide a reduction from the problem . An instance of this problem is a quantified formula , where with exactly three literals by term. Let and . Let u, v, be fresh variables. We transform to , where
We show that is valid if and only if Arg-Rel . If is valid, then there exists an assignment such that . Consequently, for , we obtain . As Φ is consistent, it thus remains to show that u is relevant, i.e. that . This follows from the fact that is satisfied by any assignment σ′ extending σ with and , while such a σ′ does not entail and hence .
For the converse direction, let Φ be a support for α such that u∈Φ. Since we conclude that and hence , for some . From also follows that . From the minimality of Φ, we conclude that in particular . And therefore . That is is satisfiable and since Φ is monotonic, consequently also is satisfiable. Summed up, we know that is satisfiable and . Hence, a fortiori, is satisfiable and . Define now if , otherwise. Obviously any extension of σX to Y satisfies β and therefore is valid.
It remains to transform into an Arg-Rel(B)-instance for all B such that . As both ∧ and ∨ are associative, we can insert parentheses into , such that we can represent each formula as binary -tree of logarithmic depth. Let f be a fresh variable and let h be the Boolean function in defined by . We further transform our instance into , where are obtained by replacing each occurrence of x ∧ y by h( f, x, y). One easily verifies that is in Arg-Rel if and only if Arg-Rel . We finally replace ∨ and h by their B-representation. ▪
Let B be a finite set of Boolean functions such that or or . Then Arg-Rel(B) is in Logspace.
We assume the representation of -, -, or -formulæ as respectively positive clauses, positive terms, or literals. Let us first consider Arg-Rel(B) for . It is easy to observe that a set of positive terms Δ entails a positive term α if and only if . We claim that Algorithm 1 decides Arg-Rel(B).
Algorithm 1 can be implemented using only a logarithmic amount of space if we do not construct Δx entirely, but rather check the condition in line 3 directly: holds if and only if .
To prove correctness, notice that Algorithm 1 accepts only if there exists a such that and . Thus Δx contains a support Φ such that . Conversely, let Φ be a support such that . Since and , there is at least one . For this xi, the algorithm constructs . Obviously and therefore which causes the algorithm to accept.
Next, consider Arg-Rel(B) for . Observe that a set of positive clauses C entails a positive clause α if and only if there is a clause c∈C such that . Thus if there is a support Φ with then it is the singleton . Given as an instance of Arg-Rel , it hence suffices to check whether , which can be done in Logspace.
Finally Arg-Rel(B) for is in Logspace, since each B-formula can be transformed into a single literal. ▪
We obtain the following complexity classification for Arg-Rel.
Let B be a finite set of Boolean functions. Then the argument relevance problem for propositional B -formulæ, Arg-Rel(B), is
(1) -complete if or or
(2) in NP if
(3) in Logspace if or or .
4.Enumeration and counting problems
A general procedure to enumerate all supports in Δ for a given claim α is given in Algorithm 2. The initial call has to be done by Enum . The idea is to build supports recursively, picking up at each step a formula ϕ from Δ and deciding whether ϕ will be present in the currently constructed support or not. The decision procedures for Arg-Rel and Arg-Disp are used in order to avoid backtracking.
The correctness of the procedure is based on the deduction theorem, which says that if and only if . Observe that, in general, when initially called on B-formulæ, this procedure deals in its recursive calls with some formulæ which are not B-formulæ anymore (because of the formula ). There is an exception to the sets B such that , since in this case and thus can be represented as a B-formula.
Note that the only cases in which we can hope to obtain polynomial delay enumeration algorithms are those for which the decision problem Arg(B) is tractable, i.e. the cases or or or . Indeed the presented procedure can be slightly modified in these cases, except for the case , in order to either avoid recursive calls or manage recursive calls on B-formulæ only. As a consequence and since in these cases the three decision problems Arg-Check(B), Arg-Rel(B) and Arg-Disp(B) are in P, the procedure will generate efficiently all possible arguments. This is made precise in the following proposition.
Let B be a finite set of Boolean functions. If or then Enum-Arg(B) is in FP. If then Enum-Arg(B) is in DelayP.
If or then we have seen (in the proof of Proposition 3.8) that every support for α consists of a single formula. For this reason, no recursive call in the procedure is necessary. It is enough to check whether every single formula from Δ is a support for α. Since Arg-Check(B) is in P in this case (see Theorem 3.5), we are done.
If then every B-formula is a positive term. Recall that if Φ is a set of positive terms, and ϕ is a positive term, then we have if and only if . As a consequence, in the case of positive terms if and only if where denotes the term obtained from α by removing those variables that occur in ϕ. Therefore, in the general enumeration procedure described above, we can make the recursive call on instead of . In this way, starting from B-formulæ, all recursive calls will be made on B-formulæ as well. Since Arg-Check(B), Arg-Rel(B) and Arg-Disp(B) are all in P for any B such that (see Theorems 3.9 and 3.6), it is then clear that the procedure runs with polynomial delay and uses only polynomial space. ▪
The argument counting problem #Arg(B) belongs to . This follows from the facts that checking an argument is in (see Section 3.2) and from the equality (see Hemaspaandra and Vollmer 1995).
Let B be a finite set of Boolean functions such that either or . Then #Arg(B) is -complete.
We show -hardness by giving a parsimonious reduction from the following -hard problem: Count the number of satisfying assignments of , where ϕ is a DNF-formula (Durand, Hermann, and Kolaitis 2005).
Let be fresh variables. We map ψ to which we define as follows:
Since and , we can use Lemmas 3.1 and 3.2. Observe that the reductions used in the proofs of these lemmas are parsimonious. Therefore we have #Arg #Arg(B). Thus, it is sufficient to prove that hardness holds for #Arg . Since and , it suffices finally to prove that hardness of #Arg(B) holds for any B such that . Suppose that and let Γ′ be the set of formulæ obtained from Γ by replacing by the set of clauses . Then Γ′ is a set of disjunctions of literals, whose size is polynomially bounded by |Γ|. Hence, by the associativity of ∨, Γ′ can be transformed in logarithmic space into an equivalent set of B-formulæ. This provides a parsimonious reduction from the above -complete problem to #Arg(B). ▪
Let B be a finite set of Boolean functions such that with and . Then #Arg (B) is in and #P;-hard.
Since the reductions in Lemmas 3.1 and 3.2 are parsimonious, analogously to Theorem 3.9, it suffices to show hardness for the case .
We prove #P;-hardness by giving a parsimonious reduction from the following #P;-hard problem: count the number of models of a positive 2-CNF-formula. Let with be such a formula. Let be fresh variables. We map ϕ to which we define as follows:
It remains to show that α can be transformed in polynomial time into a B-formula for all B such that . As ∧ and ∨ are monotonic, we can insert parentheses such that α is represented as a binary -tree of logarithmic depth. Let f be a fresh variable and let h be the Boolean functions in defined by . We further transform α into α′ by replacing every occurrence of x∧ y by h( f, x, y). Since f does not occur in Δ it is clear that the arguments for α in Δ are the ones for α′. Since , we finally replace ∨ and h by their B-representation, thus concluding the proof. ▪
Let B be a finite set of Boolean functions such that . Then #Arg(B) is #P;-complete.
Membership in #P; follows from the fact that Arg for every B such that .
To prove #P;-hardness, we establish a parsimonious reduction from the same #P;-hard problem as in the previous proposition. So let with be a positive 2-CNF-formula. We introduce p new variables that will represent the clauses. For every 1≤i≤n let . We map ϕ to which we define as follows:
By minimality every support for α contains for every i either xi or , but not both. One easily verifies that by , we define a bijection between the models of ϕ and the supports for α in Δ.
It remains to transform α and the formulæ in Δ into B-formulæ. We can insert parentheses in each term in order to represent it as a binary ∧-tree of logarithmic depth. Then it suffices to replace the ∧-connective by its B-representation which exists since . ▪
Let B be a finite set of Boolean functions. Then the argument counting problem for propositional B -formulæ, #Arg (B), is
(1) -complete if or
(2) in and #P;-hard if with and
(3) in #P; if
(4) #P;-complete if and
(5) in FP if or .
Items (1), (2) and (4) follow directly from the above three propositions. Item (3) follows from the fact that Arg for B such that (see Theorem 3.6). In the last case, all supports are singletons (see e.g. Theorem 3.8), thus there is at most a polynomial number of supports that can hence be parsed in polynomial time in order to determine the exact number of solutions. ▪
Let us conclude this section by pointing out that for the case where , i.e. when formulæ may depend on more than one variable and are representable as positive terms, the counting problem is intractable (#P;-hard, Proposition 4.4), whereas enumeration is tractable (, Proposition 4.1).
5.Discussion of results
Complexity classifications along the lines of Boolean clones have already been carried out for AI formalisms as circumscription (Thomas 2009) and abduction (Creignou et al. 2010). In particular, the latter work is closely related to the contents of this paper. To make this more precise, let us consider the positive abduction problem . It takes as an instance a triple , where , , H is a set of variables, and asks whether there exists an explanation E⊆ H such that is satisfiable and . Hence, the main differences to argumentation are as follows: (a) the knowledge base Γ is always entirely used (together with a selected subset of hypotheses) in the tests for consistency and entailment, while for argumentation these tests are performed on a chosen subset of the knowledge base Δ; (b) the parameterisation via B-formula affects only ‘fixed’ parts Γ and m in abduction (the hypotheses are by definition restricted); while in argumentation, the parameterisation is applied to the knowledge base Δ from which one has to select a subset. Nonetheless, the following relations between these two formalisms hold:
(1) if ∧∈[B], i.e. if , then Arg(B)
(2) if , i.e. if , then Arg
It turns out that Arg and Arg-Disp have the same complexity classification as positive abduction. This is due to the fact that minimality of the argument plays no role in Arg and Arg-Disp. However, for Arg-Rel the situation is different but we expect similarly harder complexity for the relevance problem in abduction with respect to subset-minimal explanations (see Eiter and Gottlob 1995 for the definitions) which has not been analysed by Creignou et al. (2010). In other words, the results provided in the present paper can be used to obtain novel results for certain variants of abduction, which have not been classified yet.
Table 2 gives an overview of the results for the studied argumentation problems. The small numbers on the right side in the table cells refer to the corresponding theorem/proposition/remark.
|Arg-Check||∈L, 3.5||∈L, 3.5||∈P, 3.5 ∈P, 3.5||DP-c, 3.3, 3.4||DP-c, 3.3, 3.4|
|Arg, Arg-Disp||∈L, 3.6||∈L, 3.6||∈P, 3.6||∈NP, 3.6||, 3.6||-c, 3.6|
|Arg-Rel||∈L, 3.8||∈L, 3.8||∈NP, 3.9||∈NP, 3.9||-c, 3.7||-c, 3.7|
|Enum-Arg||∈FP, 4.1||, 4.1||Unknown||Unknown||coNP-h, 3.6||-h, 3.6|
|#Arg||∈FP, 4.5||#P;-c, 4.4||∈#P;, 4.5||∈#P;, 4.5||, #P;-h, 4.3||-c, 4.2|
Note: The *-subscripts on clones denote all valid completions, L abbreviates Logspace, and ‘-c’ and ‘-h’ indicate, respectively, completeness and hardness.
Our results show, for instance, that when the knowledge base's formulæ are restricted to be represented as positive clauses or single literals (column ) then all considered decision problems as well as counting and enumeration are very easy. When allowing for positive terms (column *), the decision problems remain very easy, the enumeration problem becomes less trivial but still tractable (DelayP), whereas the counting problem becomes even intractable, namely #P;-complete.
Notably are the sets B of Boolean connectives where with and . This case typically applies to monotonic formulæ in which no negation is involved. Such sets of B give coNP-completeness for Arg(B), while Arg-Rel(B) remains complete for . It may come as a surprise that in these cases verifying an argument is potentially harder than deciding the existence of an argument (Arg-Check is DP-complete, Arg is only coNP-complete). This is due to the fact that when verifying an argument, the minimality condition of a support has to be checked, whereas this condition is of no importance to the argument existence problem.
The results obtained for the -cases are partial. This corresponds to the case where individual formulæ are linear equations over the two-element field. The fact that Arg(B) with is in P relies on Gaussian elimination, knowing that in this case we only have to check whether , that is whether the linear system is satisfiable. For the corresponding problems Arg-Rel(B), in which minimality plays a role, we only have an NP upper-bound, so far. In fact, the exact classification of the problems into tractable and intractable cases remains open for affine sets of Boolean connectives in the following cases: Arg(B) with and Arg-Rel(B) with .11
6.Conclusion and future work
To summarise, we took in this paper first steps to understanding the complexity of logic-based argumentation. We provided a classification of the complexity of four important decision tasks (Figure 1), as well as a classification of the complexity of enumeration and counting, for all possible restrictions on the set of allowed connectives.
The interpretation of our results is twofold: first, we have shown that the high complexity (i.e. ) only shows up for small parts of the lattice. In other words, only a few Boolean clones provide the inherent full complexity, while others allow for alternative, less involved, algorithms. Nonetheless, for the important problem of Arg-Rel, covers the most interesting areas of the lattice. The bad news is that all tractable fragments are of little practical relevance. Recall that these fragments were literals, positive terms, positive clauses, and with each of the latter two restrictions we cannot even construct an inconsistent Δ. This also hints that for future work, it might be important to restrict the connectives in Δ, and respectively, α independently.
The complexity of the problems studied in this paper is also a computational core for evaluating more complex argumentation problems, for instance, the warranted formula problem (WFP) on argument trees, which has recently been shown to be PSPACE-complete by Hirsch and Gorogiannis (2011). We expect that fragments studied here also lower the complexity of WFP, but leave details for future work. Another problem which is amenable to the kind of complexity analysis we did in this paper is the identification of conflicts between two arguments (different notions for conflicts between arguments based on classical logic exist, see e.g. Gorogiannis and Hunter 2011) which is an intractable problem itself; however, since most conflicts are identified via the implication problem, we expect results similar to the one derived by Beyersdorff et al. (2009a). A complexity analysis in that direction has already been undertaken by Wooldridge, Dunne, and Parsons (2006). In that paper, the authors studied problems as, for instance, equivalence of arguments. Further future work also concerns studying the complexity of all the problems investigated here in the popular Schaefer's framework in which formulas are in generalised conjunctive normal form (see Creignou and Zanuttini (2006), Nordh and Zanuttini (2008) for complexity classifications of abduction in this framework, and Creignou and Vollmer (2008) for a survey of results obtained for various non-monotonic logics).
1 We note that the complexity of the corresponding fragments remained unclassified also for circumscription and positive abduction.
Supported by ANR ENUM 07-BLAN-0327-04, WWTF grant ICT 08-028, FWF grant P20704-N18, ÖAD grant Amadée 17/2011/EGIDE PHC Amadeus project 24908NM, and DFG grant VO 630/6-2.
Amgoud, L. and Besnard, P. A Formal Analysis of Logic-based Argumentation Systems. Proceedings of the 4th International Conference on Scalable Uncertainty Management (SUM’10, Toulouse, France). Edited by: Deshpande, A. and Hunter, A. pp. 42–55. Springer Verlag. Vol. 6379 of Lecture Notes in Computer Science
Amgoud, L. and Cayrol, C. (2002) . A Reasoning Model Based on the Production of Acceptable Arguments. Annals of Mathematics and Artificial Intelligence, 34: : 197–215.
Baroni, P., Dunne, P. and Giacomin, M. On Extension Counting Problems in Argumentation Frameworks. Proceedings of the 3rd International Conference on Computational Models of Argument (COMMA 2010, Desenzano del Garda, Italy). Edited by: Baroni, P., Cerutti, F., Giacomin, M. and Simari, G. pp. 63–74. IOS Press. Vol. 216 of Frontiers in Artificial Intelligence and Applications
Bauland, M., Hemaspaandra, E., Schnoor, H. and Schnoor, I. Generalized Modal Satisfiability. Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science (STACS 2006, Marseille, France). Edited by: Durand, B. and Thomas, W. pp. 500–511. Springer Verlag. Vol. 3884 of Lecture Notes in Computer Science
Bauland, M., Schneider, T., Schnoor, H., Schnoor, I. and Vollmer, H. (2008) . The Complexity of Generalized Satisfiability for Linear Temporal Logic. Logical Methods in Computer Science, : 5
Bench-Capon, T. and Dunne, P. (2007) . Argumentation in Artificial Intelligence. Artificial Intelligence, 171: : 619–641.
Besnard, P. and Hunter, A. (2001) . A Logic-based Theory of Deductive Arguments. Artificial Intelligence, 128: : 203–235.
Besnard, P. and Hunter, A. (2008) . Elements of Argumentation, MIT Press.
Beyersdorff, O., Meier, A., Thomas, M. and Vollmer, H. (2009) a. The Complexity of Propositional Implication. Information Processing Letters, 109: : 1071–1077.
Beyersdorff, O., Meier, A., Thomas, M. and Vollmer, H. The Complexity of Reasoning for Fragments of Default Logic. Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT 2009, Swansea, UK). Edited by: Kullmann, O. pp. 51–64. Springer Verlag. Vol. 5584 of Lecture Notes in Computer Science
Caminada, M. and Amgoud, L. (2007) . On the Evaluation of Argumentation Formalisms. Artificial Intelligence, 171: : 286–310.
Cayrol, C. On the Relation between Argumentation and Non-monotonic Coherence-based Entailment. Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI 1995, Montréal, Canada). pp. 1443–1448. Morgan Kaufmann.
Chesñevar, C., Maguitman, A. and Loui, R. (2000) . Logical Models of Argument. ACM Compututing Surveys, 32: : 337–383.
Creignou, N., Schmidt, J. and Thomas, M. Complexity of Propositional Abduction for Restricted Sets of Boolean Functions. Proceedings of the 12th International Conference on Principles of Knowledge Representation and Reasoning (KR 2010, Toronto, Canada). Edited by: Lin, F., Sattler, U. and Truszczynski, M. pp. 8–16. AAAI Press. (full review to appear in Journal of Logic and Computation 2011)
Creignou, N. and Vollmer, H. Boolean Constraint Satisfaction Problems: When Does Post's Lattice Help?. Complexity of Constraints – An Overview of Current Research Themes. Edited by: Creignou, N., Kolaitis, P. G. and Vollmer, H. pp. 3–37. Springer. Vol. 5250 of Lecture Notes in Computer Science
Creignou, N. and Zanuttini, B. (2006) . A Complete Classification of the Complexity of Propositional Abduction. SIAM Journal on Computing, 36: : 207–229.
Dung, P., Kowalski, R. and Toni, F. (2006) . Dialectical Proof Procedures for Assumption-based Admissible Argumentation. Artificial Intelligence, 170: : 114–159.
Dung, P. M. (1995) . On the Acceptability of Arguments and its Fundamental Role in Nonmonotonic Reasoning, Logic Programming and n-Person Games. Artificial Intelligence, 77: : 321–358.
Durand, A., Hermann, M. and Kolaitis, P. G. (2005) . Subtractive Deductions and Complete Problems for Counting Complexity Classes. Theoretical Computer Science, 340: : 496–513.
Durand, A. and Hermann, M. (2008) . On the Counting Complexity of Propositional Circumscription. Information Processing Letters, 106: : 164–170.
Eiter, T. and Gottlob, G. (1995) . The Complexity of Logic-based Abduction. Journal of the ACM, 42: : 3–42.
García, A. and Simari, G. (2004) . Defeasible Logic Programming: An Argumentative Approach. Theory and Practice of Logic Programming, 4: : 95–138.
Gorogiannis, N. and Hunter, A. (2011) . Instantiating Abstract Argumentation with Classical Logic Arguments: Postulates and Properties. Artificial Intelligence, 175: : 1479–1497.
Hemaspaandra, L. and Vollmer, H. (1995) . The Satanic Notations: Counting Classes Beyond #P and Other Definitional Adventures. Complexity Theory Column 8, ACM-SIGACT News, 26: : 2–13.
Hermann, M. and Pichler, R. (2010) . Counting Complexity of Propositional Abduction. Journal of Computer and System Sciences, 76: : 634–649.
Hirsch, R. and Gorogiannis, N. (2010) . The Complexity of the Warranted Formula Problem in Propositional Argumentation. Journal of Logic and Computation, 20: : 481–499.
Johnson, D., Papadimitriou, C. and Yannakakis, M. (1988) . On Generating All Maximal Independent Sets. Information Processing Letters, 27: : 119–123.
Karchmer, M. and Wigderson, A. Monotone Circuits for Connectivity Require Super-logarithmic Depth. Proceedings of the 20th Annual ACM Symposium on Theory of Computing (STOC 1988, Chicago, Illinois, USA). Edited by: Simon, J. pp. 539–550. ACM.
Lewis, H. (1979) . Satisfiability Problems for Propositional Calculi. Mathematical Systems Theory, 13: : 45–53.
Nordh, G. and Zanuttini, B. (2008) . What Makes Propositional Abduction Tractable. Artificial Intelligence, 172: : 1245–1284.
Papadimitriou, C. (1994) . Computational Complexity, Addison-Wesley.
Papadimitriou, C. and Wolfe, D. (1988) . The Complexity of Facets Resolved. Journal of Computer and System Sciences, 37: : 2–13.
Parsons, S., Wooldridge, M. and Amgoud, L. (2003) . Properties and Complexity of Some Formal Inter-agent Dialogues. Journal of Logic and Computation, 13: : 347–376.
Post, E. (1941) . The Two-valued Iterative Systems of Mathematical Logic. Annals of Mathematics Studies, 5: : 1–122.
Prakken, H. and Vreeswijk, G. (2002) . “Logical Systems for Defeasible Argumentation”. In Handbook of Philosophical Logic, Edited by: Gabbay, D. Kluwer.
Rahwan, I. and Simari, G. (2009) . Argumentation in Artificial Intelligence, Edited by: Rahwan, I. and Simari, G. Springer Verlag.
Reith, S. On the Complexity of some Equivalence Problems for Propositional Calculi. Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science (MFCS 2003, Bratislava, Slovakia). Edited by: Rovan, B. and Vojtás, P. pp. 632–641. Springer Verlag. Vol. 2747 of Lecture Notes in Computer Science
Schnoor, H. (2005) . The Complexity of the Boolean Formula Value Problem, University of Hannover. Technical Report, Theoretical Computer Science
Spira, P.M. (1971), ‘On Time-hardware Complexity Tradeoffs for Boolean Functions’, Proceedings of the 4th Hawaii International Symposium on System Sciences, pp. 525–527
Thomas, M. The Complexity of Circumscriptive Inference in Post's Lattice. Proceedings of the 10th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2009, Potsdam, Germany). Edited by: Erdem, E., Lin, F. and Schaub, T. pp. 290–302. Springer Verlag. Vol. 5753 of Lecture Notes in Computer Science
Wooldridge, M., Dunne, P. and Parsons, S. On the Complexity of Linking Deductive and Abstract Argument Systems. Proceedings of the 21st National Conference on Artificial Intelligence (AAAI 2006, Boston, Massachusetts, USA). pp. 299–304. MIT Press.