Complexity of logic-based argumentation in Post's framework †

Abstract

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 ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ -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.

1. Introduction

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 $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ , 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 $\mathrm{\Phi }\subseteq \mathrm{\Delta }$ for a given claim α has been shown to be ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ -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 $\mathrm{\Phi }\subseteq \mathrm{\Delta }$ for α?

Arg-Check (Argument Checking): given a pair $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ , is it an argument?

Arg-Rel (Argument Relevance): given Δ, α, ϕ, is there an argument $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ such that $\mathit{\phi }\in \mathrm{\Phi }\subseteq \mathrm{\Delta }$ ?

Arg-Disp (Argument Dispensability): given Δ, α, ϕ, is there an argument $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ such that $\mathit{\phi }\notin \mathrm{\Phi }\subseteq \mathrm{\Delta }$ ?

We understand here as arguments pairs $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ with minimal support, i.e. $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ is an argument if Φ is consistent, entails α, and no ${\mathrm{\Phi }}^{\prime }⊊\mathrm{\Phi }$ entails α. Moreover, we consider the problems of enumerating and counting arguments:

• #Arg (Argument Counting): given Δ, α, how many arguments $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ with $\mathrm{\Phi }\subseteq \mathrm{\Delta }$ exist?

• Enum-Arg (Argument Enumeration): given Δ, α, output all arguments $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ such that $\mathrm{\Phi }\subseteq \mathrm{\Delta }$ .

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 $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ than arguments of form $\mathrm{(}\mathrm{\Psi }\mathrm{,}\mathit{\beta }\mathrm{)}$ 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.

2. Background

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 $\mathit{\phi }[\mathit{\alpha }\mathrm{/}\mathit{\beta }]$ the formula obtained from ϕ by replacing all occurrences of α with β.

For a given formula ϕ, we denote by $\mathrm{Vars}\mathrm{(}\mathit{\phi }\mathrm{)}$ the set of variables occurring in ϕ. We extend this definition on sets of formulæ Γ as $\mathrm{Vars}\mathrm{(}\mathrm{\Gamma }\mathrm{)}={\bigcup }_{\mathit{\phi }\in \mathrm{\Gamma }}\mathrm{Vars}\mathrm{(}\mathit{\phi }\mathrm{)}$ . We identify finite Γ with the conjunction of all the formulæ in Γ, ${\bigwedge }_{\mathit{\phi }\in \mathrm{\Gamma }}\mathit{\phi }$ . Naturally, $\mathrm{\Gamma }[\mathit{\alpha }\mathrm{/}\mathit{\beta }]$ then stands for ${\bigwedge }_{\mathit{\phi }\in \mathrm{\Gamma }}\mathit{\phi }[\mathit{\alpha }\mathrm{/}\mathit{\beta }]$ . We say that two formulæ ϕ and ψ are equivalent (written $\mathit{\phi }\equiv \mathit{\psi }$ ) if every assignment $\mathit{\sigma }:\mathrm{Vars}\mathrm{(}\mathit{\phi }\mathrm{)}\cup \mathrm{Vars}\mathrm{(}\mathit{\psi }\mathrm{)}\to \{0\mathrm{,}1\}$ on the combined variable sets satisfies ϕ if and only if it satisfies ψ. For any formula $\mathit{\phi }\in \mathcal{L}$ , we write $\mathrm{\Gamma }\vDash \mathit{\phi }$ 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. $\mathrm{Lits}\mathrm{(}\mathit{V}\mathrm{)}:=\mathit{V}\cup \{\neg \mathit{x}\mid \mathit{x}\in \mathit{V}\}$ . A clause is a disjunction of literals and a term is a conjunction of literals.

2.1 Complexity theory

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 ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ . The class DP is defined as the set of languages recognisable by the difference of two languages in NP, i.e. $\mathrm{DP}:=\{{\mathit{L}}_1\setminus {\mathit{L}}_2\mid {\mathit{L}}_1\mathrm{,}{\mathit{L}}_2\in \mathrm{NP}\}=\{{\mathit{L}}_1\cap {\mathit{L}}_2\mid {\mathit{L}}_1\in \mathrm{NP}\mathrm{,}{\mathit{L}}_2\in \mathrm{NP}\}$ . The class ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ 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 $\mathit{A}{⩽}_{\mathrm{m}}^{\log }\mathit{B}$ ) 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 ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ , 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 ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ -complete problem is deciding the truth of an expression $\exists \mathit{X}\forall \mathit{Y}\mathit{\beta }$ 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 ${\mathrm{Qsat}}_{2\mathrm{,}\exists }$ , in which the formula β is 3-DNF, and which is still ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ -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 $|\mathit{w}\mathrm{(}\mathit{x}\mathrm{)}|$ 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 $\mathrm{\#}·\mathcal{C}$ 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 $\mathrm{\#}\mathrm{P}=\mathrm{\#}·\mathrm{P}$ and $\mathrm{\#}\mathrm{P}\subseteq \mathrm{\#}·\mathrm{NP}$ . 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 $\mathrm{\#}\mathit{A}{⩽}_{!}\mathrm{\#}\mathit{B}$ .

For more background information on complexity theory, the reader is referred to Papadimitriou (1994).

2.2 Post's lattice

A Boolean function is an n-ary function $\mathit{f}:{\{0\mathrm{,}1\}}^{\mathit{n}}\to \{0\mathrm{,}1\}$ . A clone is a set of Boolean functions that is closed under superposition, i.e. it contains all projections (that is, the functions $\mathit{f}\mathrm{(}{\mathit{a}}_1\mathrm{,}\dots \mathrm{,}{\mathit{a}}_{\mathit{n}}\mathrm{)}={\mathit{a}}_{\mathit{k}}$ for all 1≤k≤n and $\mathit{n}\in \mathbb{N}$ ) 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 $\mathit{f}\mathrm{(}\mathit{c}\mathrm{,}\dots \mathrm{,}\mathit{c}\mathrm{)}=\mathit{c}$ , $\mathit{c}\in \{0\mathrm{,}1\}$ . The binary $\mathit{and}$ (∧) and the binary $\mathit{or}$ (∨) 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 ${\mathit{a}}_1⩽{\mathit{b}}_1\mathrm{,}\dots \mathrm{,}{\mathit{a}}_{\mathit{n}}⩽{\mathit{b}}_{\mathit{n}}$ implies $\mathit{f}\mathrm{(}{\mathit{a}}_1\mathrm{,}\dots \mathrm{,}{\mathit{a}}_{\mathit{n}}\mathrm{)}⩽\mathit{f}\mathrm{(}{\mathit{b}}_1\mathrm{,}\dots \mathrm{,}{\mathit{b}}_{\mathit{n}}\mathrm{)}$ . Boolean functions built up on composition of only ∧, ∨, 0, 1 are monotonic, like for instance $\mathit{g}\mathrm{(}\mathit{x}\mathrm{,}\mathit{y}\mathrm{,}\mathit{z}\mathrm{)}\equiv \mathit{x}\wedge \mathrm{(}1\wedge \mathrm{(}\mathit{y}\vee \mathit{z}\mathrm{)}\mathrm{)}$ .

f is c-separating of degree k if for all $\mathit{A}\subseteq {\mathit{f}}^{-1}\mathrm{(}\mathit{c}\mathrm{)}$ of size |A|=k there exists an $\mathit{i}\in \{1\mathrm{,}\dots \mathrm{,}\mathit{n}\}$ such that $\mathrm{(}{\mathit{a}}_1\mathrm{,}\dots \mathrm{,}{\mathit{a}}_{\mathit{n}}\mathrm{)}\in \mathit{A}$ implies a _i =c, $\mathit{c}\in \{0\mathrm{,}1\}$ . The (m+1)-ary function ${\mathit{h}}_{\mathit{m}}\mathrm{(}{\mathit{x}}_1\mathrm{,}\dots \mathrm{,}{\mathit{x}}_{\mathit{m}+1}\mathrm{)}\equiv {\bigvee }_{\mathit{i}=1}^{\mathit{m}+1}{\bigwedge }_{\mathit{j}=1\mathrm{,}\mathit{j}\ne \mathit{i}}^{\mathit{m}+1}{\mathit{x}}_{\mathit{j}}$ being true if and only if ‘at least m variables are true’ is 1-separating of degree m. For instance ${\mathit{h}}_2\mathrm{(}\mathit{x}\mathrm{,}\mathit{y}\mathrm{,}\mathit{z}\mathrm{)}\equiv \mathrm{(}\mathit{x}\wedge \mathit{y}\mathrm{)}\vee \mathrm{(}\mathit{x}\wedge \mathit{z}\mathrm{)}\vee \mathrm{(}\mathit{y}\wedge \mathit{z}\mathrm{)}$ is 1-separating of degree 2.

f is c-separating if f is c-separating of degree | f⁻¹(c)|. The implication $\mathit{g}\mathrm{(}\mathit{x}\mathrm{,}\mathit{y}\mathrm{)}\equiv \neg \mathit{x}\vee \mathit{y}$ is 0-separating.

f is self-dual if $\mathit{f}\equiv \mathrm{dual}\mathrm{(}\mathit{f}\mathrm{)}$ , where $\mathrm{dual}\mathrm{(}\mathit{f}\mathrm{)}\mathrm{(}{\mathit{x}}_1\mathrm{,}\dots \mathrm{,}{\mathit{x}}_{\mathit{n}}\mathrm{)}:=\neg \mathit{f}\mathrm{(}\neg {\mathit{x}}_1\mathrm{,}\dots \mathrm{,}\neg {\mathit{x}}_{\mathit{n}}\mathrm{)}$ . The function $\mathit{g}\mathrm{(}\mathit{x}\mathrm{,}\mathit{y}\mathrm{,}\mathit{z}\mathrm{)}\equiv \mathrm{(}\mathit{x}\wedge \neg \mathit{y}\mathrm{)}\vee \mathrm{(}\mathit{x}\wedge \neg \mathit{z}\mathrm{)}\vee \mathrm{(}\neg \mathit{y}\wedge \neg \mathit{z}\mathrm{)}$ is self-dual.

f is affine if $\mathit{f}\equiv {\mathit{x}}_1\oplus \cdots \oplus {\mathit{x}}_{\mathit{n}}\oplus \mathit{c}$ with $\mathit{c}\in \{0\mathrm{,}1\}$ . The function $\mathit{g}\mathrm{(}\mathit{x}\mathrm{,}\mathit{y}\mathrm{,}\mathit{z}\mathrm{)}\equiv \mathit{x}\oplus \mathit{y}\oplus \mathit{z}\oplus 1$ is affine and self-dual.

A list of all clones with definitions and finite bases is given in Table 1. In the naming of the clones, the semantic of single indexes is as follows. Index 2 indicates that the clone contains no constants at all. Index 0 (resp. 1) indicates that the clone contains only the constant 0 (resp. 1), but not 1 (resp. 0). Clones with no index contain both constants 0 and 1. The only exceptions to this convention are the clones $\mathsf{D}$ and ${\mathsf{D}}_1$ which do not contain any constants at all. The index * stands for all valid indexes. Clones of particular importance in this paper, since among other things they mark points in Post's lattice where the complexity of argumentation changes, are:

• the clone of all Boolean functions $\mathsf{BF}=[\wedge \mathrm{,}\neg ]=[\wedge \mathrm{,}\vee \mathrm{,}\neg \mathrm{,}0\mathrm{,}1]$

• the monotonic clones ${\mathsf{M}}_{\ast }$ , e.g. ${\mathsf{M}}_2=[\wedge \mathrm{,}\vee ]$ , $\mathsf{M}=[\wedge \mathrm{,}\vee \mathrm{,}0\mathrm{,}1]$

• the affine clones ${\mathsf{L}}_{\ast }$ , e.g. ${\mathsf{L}}_2=[\mathit{x}\oplus \mathit{y}\oplus \mathit{z}]$ , $\mathsf{L}=[\mathit{x}\oplus \mathit{y}\mathrm{,}0\mathrm{,}1]$

• the disjunctive clones ${\mathsf{V}}_{\ast }$ , e.g. ${\mathsf{V}}_2=[\vee ]$ , $\mathsf{V}=[\vee \mathrm{,}0\mathrm{,}1]$

• the conjunctive clones ${\mathsf{E}}_{\ast }$ , e.g. ${\mathsf{E}}_2=[\wedge ]$ , $\mathsf{E}=[\wedge \mathrm{,}0\mathrm{,}1]$

• the c-reproducing clones ${\mathsf{R}}_{\ast }$ , ${\mathsf{R}}_1$ 1-repr., ${\mathsf{R}}_0$ 0-repr., ${\mathsf{R}}_2$ 1- and 0-repr.

• the implication clone ${\mathsf{S}}_0=[\to ]$

• the negated-implication clone ${\mathsf{S}}_1=[\mathit{x}\wedge \neg \mathit{y}]$

• the dual clones ${\mathsf{D}}_{\ast }$ , $\mathsf{D}$ self-dual, ${\mathsf{D}}_1=\mathsf{D}\cap {\mathsf{R}}_2$ , ${\mathsf{D}}_2=\mathsf{D}\cap \mathsf{M}$

• the clones ${\mathsf{S}}_{00}={\mathsf{S}}_0\cap {\mathsf{R}}_2\cap \mathsf{M}=[\mathit{x}\vee \mathrm{(}\mathit{y}\wedge \mathit{z}\mathrm{)}]$ , ${\mathsf{S}}_{10}={\mathsf{S}}_1\cap {\mathsf{R}}_2\cap \mathsf{M}=[\mathit{x}\wedge \mathrm{(}\mathit{y}\vee \mathit{z}\mathrm{)}]$ and ${\mathsf{S}}_{12}={\mathsf{S}}_1\cap {\mathsf{R}}_2=[\mathit{x}\wedge \mathrm{(}\mathit{y}\vee \neg \mathit{z}\mathrm{)}]$

We will often add some function f∉C to a clone C and consider the clone ${\mathit{C}}^{\prime }=[\mathit{C}\cup \{\mathit{f}\}]$ generated out of C and f. With Post's lattice, one can quite easily determine this C′: it is the lowest clone above C that contains f. The following identities will be frequently used.

• $[{\mathsf{S}}_{10}\cup \{1\}]={\mathsf{M}}_1$

• $[{\mathsf{D}}_2\cup \{1\}]={\mathsf{S}}_{01}^2$

• $[{\mathsf{S}}_1\cup \{1\}]=[\mathsf{D}\cup \{1\}]=\mathsf{BF}$

Figure 1.

Post's lattice showing the complexity of the decision problems studied herein.

Table 1.

The list of all Boolean clones with definitions and bases, where ${\mathit{h}}_{\mathit{n}}:={\bigvee }_{\mathit{i}=1}^{\mathit{n}+1}{\bigwedge }_{\mathit{j}=1\mathrm{,}\mathit{j}\ne \mathit{i}}^{\mathit{n}+1}{\mathit{x}}_{\mathit{j}}$ and dual(f)(a₁, …, a _n )=¬ f(¬ a₁ …, ¬ a _n ).

Name	Definition	Base
$\mathsf{BF}$	All Boolean functions	$\{\mathit{x}\wedge \mathit{y}\mathrm{,}\neg \mathit{x}\}$
${\mathsf{R}}_0$	$\{\mathit{f}\mid \mathit{f}\text{is}$ 0 $\text{-}\mathit{reproducing}\}$	$\{\mathit{x}\wedge \mathit{y}\mathrm{,}\mathit{x}\oplus \mathit{y}\}$
${\mathsf{R}}_1$	$\{\mathit{f}\mid \mathit{f}\text{is}$ 1 $\text{-}\mathit{reproducing}\}$	$\{\mathit{x}\vee \mathit{y}\mathrm{,}\mathit{x}\oplus \mathit{y}\oplus 1\}$
${\mathsf{R}}_2$	${\mathsf{R}}_0\cap {\mathsf{R}}_1$	$\{\vee \mathrm{,}\mathit{x}\wedge \mathrm{(}\mathit{y}\oplus \mathit{z}\oplus 1\mathrm{)}\}$
$\mathsf{M}$	$\{\mathit{f}\mid \mathit{f}\text{is monotonic}\}$	$\{\mathit{x}\vee \mathit{y}\mathrm{,}\mathit{x}\wedge \mathit{y}\mathrm{,}0\mathrm{,}1\}$
${\mathsf{M}}_1$	$\mathsf{M}\cap {\mathsf{R}}_1$	$\{\mathit{x}\vee \mathit{y}\mathrm{,}\mathit{x}\wedge \mathit{y}\mathrm{,}1\}$
${\mathsf{M}}_0$	$\mathsf{M}\cap {\mathsf{R}}_0$	$\{\mathit{x}\vee \mathit{y}\mathrm{,}\mathit{x}\wedge \mathit{y}\mathrm{,}0\}$
${\mathsf{M}}_2$	$\mathsf{M}\cap {\mathsf{R}}_2$	$\{\mathit{x}\vee \mathit{y}\mathrm{,}\mathit{x}\wedge \mathit{y}\}$
${\mathsf{S}}_0^{\mathit{n}}$	$\{\mathit{f}\mid \mathit{f}\text{is}$ 0 $\text{-}\mathit{separating}\mathit{of}\mathit{degree}\mathit{n}\}$	$\{\mathit{x}\to \mathit{y}\mathrm{,}\mathrm{dual}\mathrm{(}{\mathit{h}}_{\mathit{n}}\mathrm{)}\}$
${\mathsf{S}}_0$	$\{\mathit{f}\mid \mathit{f}\mathrm{is}$ 0 $\text{-}\mathit{separating}\}$	$\{\mathit{x}\to \mathit{y}\}$
${\mathsf{S}}_1^{\mathit{n}}$	$\{\mathit{f}\mid \mathit{f}\mathrm{is}$ 1 $\text{-}\mathit{separating}\mathit{of}\mathit{degree}\mathit{n}\}$	$\{\mathit{x}\wedge \neg \mathit{y}\mathrm{,}{\mathit{h}}_{\mathit{n}}\}$
${\mathsf{S}}_1$	$\{\mathit{f}\mid \mathit{f}\mathrm{is}$ 1 $\text{-}\mathit{separating}\}$	$\{\mathit{x}\wedge \neg \mathit{y}\}$
${\mathsf{S}}_{02}^{\mathit{n}}$	${\mathsf{S}}_0^{\mathit{n}}\cap {\mathsf{R}}_2$	$\{\mathit{x}\vee \mathrm{(}\mathit{y}\wedge \neg \mathit{z}\mathrm{)}\mathrm{,}\mathrm{dual}\mathrm{(}{\mathit{h}}_{\mathit{n}}\mathrm{)}\}$
${\mathsf{S}}_{02}$	${\mathsf{S}}_0\cap {\mathsf{R}}_2$	$\{\mathit{x}\vee \mathrm{(}\mathit{y}\wedge \neg \mathit{z}\mathrm{)}\}$
${\mathsf{S}}_{01}^{\mathit{n}}$	${\mathsf{S}}_0^{\mathit{n}}\cap \mathsf{M}$	$\{\mathrm{dual}\mathrm{(}{\mathit{h}}_{\mathit{n}}\mathrm{)}\mathrm{,}1\}$
${\mathsf{S}}_{01}$	${\mathsf{S}}_0\cap \mathsf{M}$	$\{\mathit{x}\vee \mathrm{(}\mathit{y}\wedge \mathit{z}\mathrm{)}\mathrm{,}1\}$
${\mathsf{S}}_{00}^{\mathit{n}}$	${\mathsf{S}}_0^{\mathit{n}}\cap {\mathsf{R}}_2\cap \mathsf{M}$	$\{\mathit{x}\vee \mathrm{(}\mathit{y}\wedge \mathit{z}\mathrm{)}\mathrm{,}\mathrm{dual}\mathrm{(}{\mathit{h}}_{\mathit{n}}\mathrm{)}\}$
${\mathsf{S}}_{00}$	${\mathsf{S}}_0\cap {\mathsf{R}}_2\cap \mathsf{M}$	$\{\mathit{x}\vee \mathrm{(}\mathit{y}\wedge \mathit{z}\mathrm{)}\}$
${\mathsf{S}}_{12}^{\mathit{n}}$	${\mathsf{S}}_1^{\mathit{n}}\cap {\mathsf{R}}_2$	$\{\mathit{x}\wedge \mathrm{(}\mathit{y}\vee \neg \mathit{z}\mathrm{)}\mathrm{,}{\mathit{h}}_{\mathit{n}}\}$
${\mathsf{S}}_{12}$	${\mathsf{S}}_1\cap {\mathsf{R}}_2$	$\{\mathit{x}\wedge \mathrm{(}\mathit{y}\vee \neg \mathit{z}\mathrm{)}\}$
${\mathsf{S}}_{11}^{\mathit{n}}$	${\mathsf{S}}_1^{\mathit{n}}\cap \mathsf{M}$	$\{{\mathit{h}}_{\mathit{n}}\mathrm{,}0\}$
${\mathsf{S}}_{11}$	${\mathsf{S}}_1\cap \mathsf{M}$	$\{\mathit{x}\wedge \mathrm{(}\mathit{y}\vee \mathit{z}\mathrm{)}\mathrm{,}0\}$
${\mathsf{S}}_{10}^{\mathit{n}}$	${\mathsf{S}}_1^{\mathit{n}}\cap {\mathsf{R}}_2\cap \mathsf{M}$	$\{\mathit{x}\wedge \mathrm{(}\mathit{y}\vee \mathit{z}\mathrm{)}\mathrm{,}{\mathit{h}}_{\mathit{n}}\}$
${\mathsf{S}}_{10}$	${\mathsf{S}}_1\cap {\mathsf{R}}_2\cap \mathsf{M}$	$\{\mathit{x}\wedge \mathrm{(}\mathit{y}\vee \mathit{z}\mathrm{)}\}$
$\mathsf{D}$	$\{\mathit{f}\mid \mathit{f}\text{is self-dual}\}$	$\{\mathrm{(}\mathit{x}\wedge \neg \mathit{y}\mathrm{)}\vee \mathrm{(}\mathit{x}\wedge \neg \mathit{z}\mathrm{)}\vee \mathrm{(}\neg \mathit{y}\wedge \neg \mathit{z}\mathrm{)}\}$
${\mathsf{D}}_1$	$\mathsf{D}\cap {\mathsf{R}}_2$	$\{\mathrm{(}\mathit{x}\wedge \mathit{y}\mathrm{)}\vee \mathrm{(}\mathit{x}\wedge \neg \mathit{z}\mathrm{)}\vee \mathrm{(}\mathit{y}\wedge \neg \mathit{z}\mathrm{)}\}$
${\mathsf{D}}_2$	$\mathsf{D}\cap \mathsf{M}$	$\{\mathrm{(}\mathit{x}\wedge \mathit{y}\mathrm{)}\vee \mathrm{(}\mathit{x}\wedge \mathit{z}\mathrm{)}\vee \mathrm{(}\mathit{y}\wedge \mathit{z}\mathrm{)}\}$
$\mathsf{L}$	$\{\mathit{f}\mid \mathit{f}\text{is affine}\}$	$\{\mathit{x}\oplus \mathit{y}\mathrm{,}1\}$
${\mathsf{L}}_0$	$\mathsf{L}\cap {\mathsf{R}}_0$	$\{\mathit{x}\oplus \mathit{y}\}$
${\mathsf{L}}_1$	$\mathsf{L}\cap {\mathsf{R}}_1$	$\{\mathit{x}\oplus \mathit{y}\oplus 1\}$
${\mathsf{L}}_2$	$\mathsf{L}\cap {\mathsf{R}}_2$	$\{\mathit{x}\oplus \mathit{y}\oplus \mathit{z}\}$
${\mathsf{L}}_3$	$\mathsf{L}\cap \mathsf{D}$	$\{\mathit{x}\oplus \mathit{y}\oplus \mathit{z}\oplus 1\}$
$\mathsf{V}$	$\{\mathit{f}\mid \mathit{f}$ is a disjunction of variables or constants</texlscub>	$\{\mathit{x}\vee \mathit{y}\mathrm{,}0\mathrm{,}1\}$
${\mathsf{V}}_0$	$\mathsf{V}\cap {\mathsf{R}}_0$	$\{\mathit{x}\vee \mathit{y}\mathrm{,}0\}$
${\mathsf{V}}_1$	$\mathsf{V}\cap {\mathsf{R}}_1$	$\{\mathit{x}\vee \mathit{y}\mathrm{,}1\}$
${\mathsf{V}}_2$	$\mathsf{V}\cap {\mathsf{R}}_2$	$\{\mathit{x}\vee \mathit{y}\}$
$\mathsf{E}$	$\{\mathit{f}\mid \mathit{f}$ is a conjunction of variables or constants</texlscub>	$\{\mathit{x}\wedge \mathit{y}\mathrm{,}0\mathrm{,}1\}$
${\mathsf{E}}_0$	$\mathsf{E}\cap {\mathsf{R}}_0$	$\{\mathit{x}\wedge \mathit{y}\mathrm{,}0\}$
${\mathsf{E}}_1$	$\mathsf{E}\cap {\mathsf{R}}_1$	$\{\mathit{x}\wedge \mathit{y}\mathrm{,}1\}$
${\mathsf{E}}_2$	$\mathsf{E}\cap {\mathsf{R}}_2$	$\{\mathit{x}\wedge \mathit{y}\}$
$\mathsf{N}$	$\{\mathit{f}\mid \mathit{f}$ depends on at most one variable</texlscub>	$\{\neg \mathit{x}\mathrm{,}0\mathrm{,}1\}$
${\mathsf{N}}_2$	$\mathsf{N}\cap {\mathsf{R}}_2$	$\{\neg \mathit{x}\}$
$\mathsf{I}$	$\{\mathit{f}\mid \mathit{f}\text{is a projection or a constant}\}$	$\{\mathrm{id}\mathrm{,}0\mathrm{,}1\}$
${\mathsf{I}}_0$	$\mathsf{I}\cap {\mathsf{R}}_0$	$\{\mathrm{id}\mathrm{,}0\}$
${\mathsf{I}}_1$	$\mathsf{I}\cap {\mathsf{R}}_1$	$\{\mathrm{id}\mathrm{,}1\}$
${\mathsf{I}}_2$	$\mathsf{I}\cap {\mathsf{R}}_2$	$\{\mathrm{id}\}$

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 $\mathcal{L}\mathrm{(}\mathit{B}\mathrm{)}$ .

Let f be an n-ary Boolean function. A B-formula ϕ is called B-representation of f if $\mathit{f}\equiv \mathit{\phi }$ . 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.1 Exponential blow up

Let $\mathit{h}\mathrm{(}\mathit{x}\mathrm{,}\mathit{y}\mathrm{)}\equiv \neg \mathrm{(}\mathit{x}\wedge \mathit{y}\mathrm{)}$ . An $\{\mathit{h}\}$ -representation of the binary $\mathit{and}$ , $\mathit{and}\mathrm{(}\mathit{x}\mathrm{,}\mathit{y}\mathrm{)}\equiv \mathit{x}\wedge \mathit{y}$ , is $\mathit{h}\mathrm{(}\mathit{h}\mathrm{(}\mathit{x}\mathrm{,}\mathit{y}\mathrm{)}\mathrm{,}\mathit{h}\mathrm{(}\mathit{x}\mathrm{,}\mathit{y}\mathrm{)}\mathrm{)}$ . Observe that an $\{\mathit{h}\}$ -representation of the n-ary $\mathit{and}$ , ${\mathit{and}}_{\mathit{n}}\mathrm{(}{\mathit{x}}_1\mathrm{,}\dots \mathrm{,}{\mathit{x}}_{\mathit{n}}\mathrm{)}\equiv {\mathit{x}}_1\wedge \cdots \wedge {\mathit{x}}_{\mathit{n}}$ , based on the recursive application of the $\{\mathit{h}\}$ -representation $\mathit{h}\mathrm{(}\mathit{h}\mathrm{(}\mathit{x}\mathrm{,}\mathit{y}\mathrm{)}\mathrm{,}\mathit{h}\mathrm{(}\mathit{x}\mathrm{,}\mathit{y}\mathrm{)}\mathrm{)}$ of the binary $\mathit{and}$ to the formula $$\mathrm{(}\cdots \mathrm{(}\mathrm{(}\mathrm{(}{\mathit{x}}_1\wedge {\mathit{x}}_2\mathrm{)}\wedge {\mathit{x}}_3\mathrm{)}\wedge {\mathit{x}}_4\mathrm{)}\wedge \cdots \mathrm{)}\wedge {\mathit{x}}_{\mathit{n}}$$ leads to an explosion of the formula size. This is because the parentheses-depth is linear and the variables x, y appear twice in the $\{\mathit{h}\}$ -representation $\mathit{h}\mathrm{(}\mathit{h}\mathrm{(}\mathit{x}\mathrm{,}\mathit{y}\mathrm{)}\mathrm{,}\mathit{h}\mathrm{(}\mathit{x}\mathrm{,}\mathit{y}\mathrm{)}\mathrm{)}$ of the binary $\mathit{and}$ . We can avoid this exponential blow up by placing the parentheses in a way such that we get a formula of logarithmic parentheses-depth, i.e. $$\mathrm{(}\cdots \mathrm{(}\mathrm{(}{\mathit{x}}_1\wedge {\mathit{x}}_2\mathrm{)}\wedge \mathrm{(}{\mathit{x}}_3\wedge {\mathit{x}}_4\mathrm{)}\mathrm{)}\wedge \cdots \mathrm{)}\wedge \mathrm{(}\cdots \wedge \mathrm{(}\mathrm{(}{\mathit{x}}_{\mathit{n}-3}\wedge {\mathit{x}}_{\mathit{n}-2}\mathrm{)}\wedge \mathrm{(}{\mathit{x}}_{\mathit{n}-1}\wedge {\mathit{x}}_{\mathit{n}}\mathrm{)}\mathrm{)}\cdots \mathrm{)}\mathrm{,}$$

2.3 Logic-based argumentation

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 $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ , where Φ is a set of formulæ and α is a formula such that

Φ is consistent,

$\mathrm{\Phi }\vDash \mathit{\alpha }$ ,

Φ is minimal with this last property, i.e. no proper subset of Φ entails α.

We say that $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ is an argument for α. If $\mathrm{\Phi }\subseteq \mathrm{\Delta }$ , then it is said to be an argument in Δ. We call α the consequent and Φ the support of the argument. Note that these three conditions are equivalent to the following:

1. Φ is satisfiable,

2. $\mathrm{\Phi }\wedge \neg \mathit{\alpha }$ is unsatisfiable (i.e. $\mathrm{\Phi }\vDash \mathit{\alpha }$ ), and

3. for all $\mathit{\phi }\in \mathrm{\Phi }$ , $\mathrm{(}\mathrm{\Phi }\setminus \{\mathit{\phi }\}\mathrm{)}\cup \{\neg \mathit{\alpha }\}$ 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

Problem: Arg(B).

Instance: $\mathcal{A}=\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{)}$ , where $\mathrm{\Delta }\subseteq \mathcal{L}\mathrm{(}\mathit{B}\mathrm{)}$ and $\mathit{\alpha }\in \mathcal{L}\mathrm{(}\mathit{B}\mathrm{)}$ .

Question: Does there exist Φ such that $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ 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 $\mathcal{L}\mathrm{(}\mathit{B}\mathrm{)}$ only.

Problem: Arg-Check(B).

Instance: $\mathcal{A}=\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ , where $\mathrm{\Phi }\subseteq \mathcal{L}\mathrm{(}\mathit{B}\mathrm{)}$ and $\mathit{\alpha }\in \mathcal{L}\mathrm{(}\mathit{B}\mathrm{)}$ .

Question: Is $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ an argument?

• Problem: Arg-Rel(B).

• Instance: $\mathcal{A}=\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{,}\mathit{\phi }\mathrm{)}$ , where $\mathrm{\Delta }\subseteq \mathcal{L}\mathrm{(}\mathit{B}\mathrm{)}$ and $\mathit{\alpha }\mathrm{,}\mathit{\phi }\in \mathcal{L}\mathrm{(}\mathit{B}\mathrm{)}$ .

• Question: Does there exist an argument $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ in Δ such that $\mathit{\phi }\in \mathrm{\Phi }$ ?

• Problem: Arg-Disp(B).

• Instance: $\mathcal{A}=\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{,}\mathit{\phi }\mathrm{)}$ , where $\mathrm{\Delta }\subseteq \mathcal{L}\mathrm{(}\mathit{B}\mathrm{)}$ and $\mathit{\alpha }\mathrm{,}\mathit{\phi }\in \mathcal{L}\mathrm{(}\mathit{B}\mathrm{)}$ .

• Question: Does there exist an argument $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ in Δ such that $\mathit{\phi }\notin \mathrm{\Phi }$ ?

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 ${\mathrm{\Phi }}^{\prime }\subseteq \mathrm{\Phi }$ such that ${\mathrm{\Phi }}^{\prime }\vDash \mathit{\alpha }$ and ${\mathrm{\Phi }}^{\prime }\setminus \{\mathit{\psi }\}⊭\mathit{\alpha }$ for all $\mathit{\psi }\in {\mathrm{\Phi }}^{\prime }$ . 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 $\mathrm{\Phi }\subseteq \mathrm{\Delta }$ with $\mathit{\phi }\in \mathrm{\Phi }$ and $\mathrm{\Phi }\vDash \mathit{\alpha }$ does not help here, because ϕ might be excluded from the minimal subset ${\mathrm{\Phi }}^{\prime }\subseteq \mathrm{\Phi }$ 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 $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ 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.

Problem: Enum-Arg(B).

Instance: $\mathcal{A}=\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{)}$ , where $\mathrm{\Delta }\subseteq \mathcal{L}\mathrm{(}\mathit{B}\mathrm{)}$ and $\mathit{\alpha }\in \mathcal{L}\mathrm{(}\mathit{B}\mathrm{)}$ .

Output: Generate all arguments $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ in Δ without repetition.

• Problem: #Arg(B).

• Instance: $\mathcal{A}=\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{)}$ , where $\mathrm{\Delta }\subseteq \mathcal{L}\mathrm{(}\mathit{B}\mathrm{)}$ and $\mathit{\alpha }\in \mathcal{L}\mathrm{(}\mathit{B}\mathrm{)}$ .

• Output: Number of arguments $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ in Δ.

Obviously, for both Enum-Arg(B) and #Arg(B), minimality of the support plays a crucial role, as well.

3. Decision problems

3.1 Tools and methods

Observe that if B₁ and B₂ are two sets of Boolean functions such that ${\mathit{B}}_1\subseteq [{\mathit{B}}_2]$ , then every function of B₁ can be expressed by a B₂-formula, namely by its B₂-representation. This way there is a canonical reduction between Arg $\mathrm{(}{\mathit{B}}_1\mathrm{,}\mathcal{M}\mathrm{)}$ and Arg $\mathrm{(}{\mathit{B}}_2\mathrm{,}\mathcal{M}\mathrm{)}$ if ${\mathit{B}}_1\subseteq [{\mathit{B}}_2]$ : replace all B₁-connectives by their B₂-representation. This reduction is not necessarily polynomial: Since the B₂-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 B₂-representation for any B₁-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 B₁-formulæ, similar to Example 2.1.

When we show hardness-results for Arg(B) for some B such that $\mathit{C}\subseteq [\mathit{B}]$ (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.

Lemma 3.1

Let Arg- $\mathfrak{P}$ denote any of the problems Arg, Arg-Check or Arg-Rel. Let B be a finite set of Boolean functions such that $\wedge \in [\mathit{B}]\mathrm{,}$ i.e. ${\mathsf{E}}_2\subseteq [\mathit{B}]$ . Then Arg- $\mathfrak{P}\mathrm{(}\mathit{B}\cup \{1\}\mathrm{)}{⩽}_{\mathrm{m}}^{\log }$ Arg- $\mathfrak{P}\mathrm{(}\mathit{B}\mathrm{)}$ .

Proof

Let ℐ be the given instance. We map ℐ to the instance ℐ′ obtained by replacing each formula ψ occurring in ℐ by $\mathit{\psi }[1\mathrm{/}\mathit{t}]\wedge \mathit{t}$ , 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 ${\mathsf{D}}_2\subseteq [\mathit{B}]$ .

Lemma 3.2

Let B be a finite set of Boolean functions such that ${\mathsf{D}}_2\subseteq [\mathit{B}]$ . Then Arg $\mathrm{(}\mathit{B}\cup \{1\}\mathrm{)}{⩽}_{\mathrm{m}}^{\log }$ Arg(B) and Arg-Rel $\mathrm{(}\mathit{B}\cup \{1\}\mathrm{)}{⩽}_{\mathrm{m}}^{\log }$ Arg-Rel(B).

Proof

Let $\mathit{g}\mathrm{(}\mathit{x}\mathrm{,}\mathit{y}\mathrm{,}\mathit{z}\mathrm{)}:=\mathrm{(}\mathit{x}\wedge \mathit{y}\mathrm{)}\vee \mathrm{(}\mathit{x}\wedge \mathit{z}\mathrm{)}\vee \mathrm{(}\mathit{y}\wedge \mathit{z}\mathrm{)}$ . The function g is a base of ${\mathsf{D}}_2$ and evaluates to true if and only if at least two of the variables are set to true. Given an instance $\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{)}$ of Arg $\mathrm{(}\mathit{B}\cup \{1\}\mathrm{)}$ , we define an instance $\mathrm{(}{\mathrm{\Delta }}^{\prime }\mathrm{,}{\mathit{\alpha }}^{\prime }\mathrm{)}$ of Arg(B) by ${\mathrm{\Delta }}^{\prime }:=\{\mathit{\psi }[1\mathrm{/}\mathit{t}]\mid \mathit{\psi }\in \mathrm{\Delta }\}\cup \{\mathit{t}\}$ and ${\mathit{\alpha }}^{\prime }=\mathit{g}\mathrm{(}\mathit{\alpha }[1\mathrm{/}\mathit{t}]\mathrm{,}\mathit{t}\mathrm{,}\mathit{q}\mathrm{)}$ ,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 ${\mathrm{\Phi }}^{\prime }:=\{\mathit{\psi }[1\mathrm{/}\mathit{t}]\mid \mathit{\psi }\in \mathrm{\Phi }\}\cup \{\mathit{t}\}$ . Observe that ${\mathrm{\Phi }}^{\prime }\equiv \mathrm{\Phi }$ . Thus Φ′ is satisfiable and ${\mathrm{\Phi }}^{\prime }\vDash \mathit{\alpha }$ , hence ${\mathrm{\Phi }}^{\prime }\vDash \mathit{\alpha }[1\mathrm{/}\mathit{t}]\wedge \mathit{t}$ , as t does not occur in α. Therefore, we obtain ${\mathrm{\Phi }}^{\prime }\vDash \mathit{g}\mathrm{(}\mathit{\alpha }[1\mathrm{/}\mathit{t}]\mathrm{,}\mathit{t}\mathrm{,}\mathit{q}\mathrm{)}$ . Moreover, either Φ′ or ${\mathrm{\Phi }}^{\prime }\setminus \{\mathit{t}\}$ is minimal with this property. Indeed, suppose that there exists a ${\mathit{\psi }}^{\prime }\in {\mathrm{\Phi }}^{\prime }$ with ${\mathit{\psi }}^{\prime }=\mathit{\psi }[1\mathrm{/}\mathit{t}]$ for some ψ∈Φ such that ${\mathrm{\Phi }}^{\prime }\setminus \{{\mathit{\psi }}^{\prime }\}\vDash \mathit{g}\mathrm{(}\mathit{\alpha }[1\mathrm{/}\mathit{t}]\mathrm{,}\mathit{t}\mathrm{,}\mathit{q}\mathrm{)}$ . Then ${\mathrm{\Phi }}^{\prime }\setminus \{{\mathit{\psi }}^{\prime }\}\vDash \mathit{\alpha }[1\mathrm{/}\mathit{t}]\wedge \mathit{t}$ as q does not occur in Φ′, and hence $\mathrm{\Phi }\setminus \{\mathit{\psi }\}\vDash \mathit{\alpha }$ , contradictory to the minimality of Φ.

Conversely, with similar arguments, it is easy to see that if Φ′ is an argument for α′ in Δ′, then $\mathrm{\Phi }:=\{\mathit{\psi }[\mathit{t}\mathrm{/}1]\mid \mathit{\psi }\in {\mathrm{\Phi }}^{\prime }\mathrm{,}\mathit{\psi }\ne \mathit{t}\}$ is an argument for α in Δ: as q does not occur in Φ′, ${\mathrm{\Phi }}^{\prime }\vDash {\mathit{\alpha }}^{\prime }$ implies that ${\mathrm{\Phi }}^{\prime }\vDash \mathit{\alpha }[1\mathrm{/}\mathit{t}]\wedge \mathit{t}$ .

This proves a correctness of the reduction from Arg $\mathrm{(}\mathit{B}\cup \{1\}\mathrm{)}$ to Arg(B). The analogous result for Arg-Rel follows from the same arguments as above, mapping the additional component ϕ to ${\mathit{\phi }}^{\prime }:=\mathit{\phi }[1\mathrm{/}\mathit{t}]$ .  ▪

Remark 1

Observe that this reduction does not work for Arg-Check: one would have to decide whether to map Φ to Φ′ or to ${\mathrm{\Phi }}^{\prime }\setminus \{\mathit{t}\}$ to ensure minimality, which requires the ability to decide whether ${\mathrm{\Phi }}^{\prime }\setminus \{\mathit{t}\}\vDash \mathit{t}$ 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 $\mathit{\psi }[0\mathrm{/}\mathit{f}]\vee \mathit{f}$ 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 ${\mathsf{S}}_{00}\subseteq [\mathit{B}]$ or ${\mathsf{D}}_2\subseteq [\mathit{B}]$ or ${\mathsf{S}}_{10}\subseteq [\mathit{B}]$ (see Theorem 3.9). Since in the latter two cases either ${\mathsf{D}}_2\subseteq [\mathit{B}]$ or ${\mathsf{E}}_2\subseteq [\mathit{B}]$ , according to Lemmas 3.1 and 3.2 we have Arg-Rel $\mathrm{(}\mathit{B}\cup \{1\}\mathrm{)}{⩽}_{\mathrm{m}}^{\log }$ Arg-Rel(B). Therefore, it is sufficient to prove hardness for Arg-Rel $\mathrm{(}\mathit{B}\cup \{1\}\mathrm{)}$ . Observe that if ${\mathsf{D}}_2\subseteq [\mathit{B}]$ then ${\mathsf{S}}_{01}^2=[{\mathsf{D}}_2\cup \{1\}]\subseteq [[\mathit{B}]\cup \{1\}]=[\mathit{B}\cup \{1\}]$ and if ${\mathsf{S}}_{10}\subseteq [\mathit{B}]$ then ${\mathsf{M}}_1=[{\mathsf{S}}_{10}\cup \{1\}]\subseteq [\mathit{B}\cup \{1\}]$ . Since ${\mathsf{S}}_{00}\subseteq {\mathsf{S}}_{01}^2$ and ${\mathsf{S}}_{00}\subseteq {\mathsf{M}}_1$ , we have in both cases ${\mathsf{S}}_{00}\subseteq [\mathit{B}\cup \{1\}]$ . So, finally in order to prove that Arg-Rel(B) is hard in the case where ${\mathsf{S}}_{00}\subseteq [\mathit{B}]$ or ${\mathsf{D}}_2\subseteq [\mathit{B}]$ or ${\mathsf{S}}_{10}\subseteq [\mathit{B}]$ , it is sufficient to prove that the hardness holds for B such that ${\mathsf{S}}_{00}\subseteq [\mathit{B}]$ .

We will henceforth give less details when applying Lemmas 3.1 and 3.2.

3.2 The 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 = $\mathit{A}\cap \mathit{B}$ , with $$\begin{array}{c}\mathit{A}=\{\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}\mid \mathrm{\Phi }\text{is satisfiable}\mathrm{,}\forall \mathit{\phi }\in \mathrm{\Phi }:\mathrm{\Phi }\setminus \{\mathit{\phi }\}⊭\mathit{\alpha }\};\hfill \\ \mathit{B}=\{\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}\mid \mathrm{\Phi }\vDash \mathit{\alpha }\}.\hfill \end{array}$$

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.

Proposition 3.3

Let ${\mathsf{S}}_{00}\subseteq [\mathit{B}]$ . Then Arg-Check(B) is DP-complete.

Proof

To prove DP-hardness, we establish a reduction from Critical-Sat. Let $\mathit{\psi }={\bigwedge }_{\mathit{j}=1}^{\mathit{m}}{\mathit{C}}_{\mathit{j}}$ be an instance of Critical-Sat, and $\mathrm{Vars}\mathrm{(}\mathit{\psi }\mathrm{)}=\{{\mathit{x}}_1\mathrm{,}\dots \mathrm{,}{\mathit{x}}_{\mathit{n}}\}$ . Let $\mathit{u}\mathrm{,}{\mathit{x}}_1^{\prime }\mathrm{,}\dots \mathrm{,}{\mathit{x}}_{\mathit{n}}^{\prime }$ be fresh, pairwise distinct variables. Note that if $\mathit{\psi }\in$ Critical-Sat then each variable of ψ appears both as positive and as negative literal. Let further ${\mathit{C}}_{\mathit{j}}^{\prime }:={\mathit{C}}_{\mathit{j}}[\neg {\mathit{x}}_{\mathit{i}}\mathrm{/}{\mathit{x}}_{\mathit{i}}^{\prime }\mid 1⩽\mathit{i}⩽\mathit{n}]$ for 1≤j≤m and ${\mathit{\psi }}^{\prime }={\bigwedge }_{\mathit{j}=1}^{\mathit{m}}{\mathit{C}}_{\mathit{j}}^{\prime }$ . We map ψ to $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ , where we define $$\begin{array}{ccc}\hfill \mathrm{\Phi }& \hfill =\hfill & \{{\mathit{C}}_{\mathit{j}}^{\prime }|1⩽\mathit{j}⩽\mathit{m}\}\text{and}\hfill \\ \hfill \mathit{\alpha }& \hfill =\hfill & \underset{\mathit{i}=1}{\overset{\mathit{n}}{{\displaystyle \bigvee }}}\mathit{u}\vee \mathrm{(}{\mathit{x}}_{\mathit{i}}\wedge {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}.\hfill \end{array}$$

Since x∨ y and $\mathit{x}\vee \mathrm{(}\mathit{y}\wedge \mathit{z}\mathrm{)}$ are functions of ${\mathsf{S}}_{00}$ , α and all C′ _j ’s are ${\mathsf{S}}_{00}$ -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 $\mathrm{\Phi }\equiv {\mathit{\psi }}^{\prime }$ and ${\mathrm{\Phi }}_{\mathit{k}}\equiv {\mathit{\psi }}_{\mathit{k}}^{\prime }$ .

Suppose now that ψ ∈ Critical-Sat, i.e. ψ is unsatisfiable and ψ _k is satisfiable for all $\mathit{k}\in \{1\mathrm{,}\dots \mathrm{,}\mathit{m}\}$ . We show that Φ entails α. Since $\mathit{\psi }\equiv {\mathit{\psi }}^{\prime }\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\oplus {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ is unsatisfiable, and ${\mathit{\psi }}^{\prime }\equiv \mathrm{\Phi }$ is monotonic, all models of Φ have to set both x _i and x′ _i to 1 for at least one $\mathit{i}\in \{1\mathrm{,}\dots \mathrm{,}\mathit{n}\}$ . Since $\mathit{\alpha }[\mathit{u}\mathrm{/}0]\equiv {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\wedge {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ , we therefore have $\mathrm{\Phi }\vDash \mathit{\alpha }[\mathit{u}\mathrm{/}0]$ . Obviously also $\mathrm{\Phi }\vDash \mathit{\alpha }[\mathit{u}\mathrm{/}1]$ , thus we have $\mathrm{\Phi }\vDash \mathit{\alpha }$ .

It remains to prove that Φ is minimal. Since for each $\mathit{k}\in \{1\mathrm{,}\dots \mathrm{,}\mathit{m}\}$ ${\mathit{\psi }}_{\mathit{k}}\equiv {\mathit{\psi }}_{\mathit{k}}^{\prime }\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\oplus {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ is satisfiable, no ${\mathit{\psi }}_{\mathit{k}}^{\prime }\equiv {\mathrm{\Phi }}_{\mathit{k}}$ entails $\mathit{\alpha }[\mathit{u}\mathrm{/}0]\equiv {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\wedge {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ . A fortiori no Φ _k entails α.

Conversely suppose that $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}\in$ Arg-Check. Then, in particular, Φ entails α[u/0]. Thus, we have ${\mathit{\psi }}^{\prime }\vDash {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\wedge {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ , which implies that ψ is unsatisfiable. By the minimality of Φ we know that no Φ _k entails α. Since ${\mathrm{\Phi }}_{\mathit{k}}\vDash \mathit{\alpha }[\mathit{u}\mathrm{/}1]$ , we conclude that ${\mathrm{\Phi }}_{\mathit{k}}⊭\mathit{\alpha }[\mathit{u}\mathrm{/}0]$ , which implies that ${\mathit{\psi }}_{\mathit{k}}^{\prime }\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}\neg {\mathit{x}}_{\mathit{i}}\vee \neg {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ is satisfiable. As ψ _k ′ is monotonic, we also obtain that ${\mathit{\psi }}_{\mathit{k}}^{\prime }\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\oplus {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ and hence ψ _k itself is satisfiable.

We finally transform $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ into a B-instance for all B such that ${\mathsf{S}}_{00}\subseteq [\mathit{B}]$ 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.  ▪

Proposition 3.4

Let B be a finite set of Boolean functions such that ${\mathsf{D}}_2\subseteq [\mathit{B}]$ . Then Arg-Check(B) is DP-complete.

Proof

We give a reduction from Critical-Sat similar to Proposition 3.3. For $\mathit{k}\in \mathbb{N}$ , we define g _k as the (k+1)-ary function verifying

${\mathit{g}}_{\mathit{k}}\mathrm{(}{\mathit{z}}_1\mathrm{,}\dots \mathrm{,}{\mathit{z}}_{\mathit{k}}\mathrm{,}0\mathrm{)}\equiv {\bigwedge }_{\mathit{i}=1}^{\mathit{k}}{\mathit{z}}_{\mathit{i}}$ and

${\mathit{g}}_{\mathit{k}}\mathrm{(}{\mathit{z}}_1\mathrm{,}\dots \mathrm{,}{\mathit{z}}_{\mathit{k}}\mathrm{,}1\mathrm{)}\equiv {\bigwedge }_{\mathit{i}=1}^{\mathit{k}}{\mathit{z}}_{\mathit{i}}$ .

Note that for every $\mathit{k}\in \mathbb{N}$ , g _k is monotonic and self-dual, and thus contained in ${\mathsf{D}}_2$ . By abuse of notation, given a clause $\mathit{C}=\mathrm{(}{\mathit{l}}^1\vee {\mathit{l}}^2\vee {\mathit{l}}^3\mathrm{)}$ and a variable x, g₃(C, x) stands for ${\mathit{g}}_3\mathrm{(}{\mathit{l}}^1\mathrm{,}{\mathit{l}}^2\mathrm{,}{\mathit{l}}^3\mathrm{,}\mathit{x}\mathrm{)}$ . Let $\mathit{\psi }={\bigwedge }_{\mathit{j}=1}^{\mathit{m}}{\mathit{C}}_{\mathit{j}}$ be an instance of Critical-Sat with ${\mathit{C}}_{\mathit{j}}=\mathrm{(}{\mathit{l}}_{\mathit{j}}^1\vee {\mathit{l}}_{\mathit{j}}^2\vee {\mathit{l}}_{\mathit{j}}^3\mathrm{)}$ and $\mathrm{Vars}\mathrm{(}\mathit{\psi }\mathrm{)}=\{{\mathit{x}}_1\mathrm{,}\dots \mathrm{,}{\mathit{x}}_{\mathit{n}}\}$ . Let further $\mathit{u}\mathrm{,}\mathit{v}\mathrm{,}{\mathit{x}}_1^{\prime }\mathrm{,}\dots \mathrm{,}{\mathit{x}}_{\mathit{n}}^{\prime }$ be fresh, pairwise distinct variables and ${\mathit{C}}_{\mathit{j}}^{\prime }:={\mathit{C}}_{\mathit{j}}[\neg {\mathit{x}}_{\mathit{i}}\mathrm{/}{\mathit{x}}_{\mathit{i}}^{\prime }\mid 1⩽\mathit{i}⩽\mathit{n}]$ for 1≤j≤m.

We map ψ to $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ , where we define $$\begin{array}{ccc}\hfill \mathrm{\Phi }& \hfill =\hfill & \{{\mathit{g}}_3\mathrm{(}{\mathit{C}}_{\mathit{j}}^{\prime }\mathrm{,}\mathit{u}\mathrm{)}\mid 1⩽\mathit{j}⩽\mathit{m}\}\mathrm{,}\text{and}\hfill \\ \hfill \mathit{\alpha }& \hfill =\hfill & {\mathit{g}}_{\mathit{n}}\mathrm{(}{\mathrm{(}{\mathit{g}}_2\mathrm{(}{\mathit{x}}_{\mathit{i}}\mathrm{,}{\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{,}\mathit{v}\mathrm{)}\mathrm{)}}_{1⩽\mathit{i}⩽\mathit{n}}\mathrm{,}\mathit{u}\mathrm{)}.\hfill \end{array}$$

Obviously α and the formulæ in Φ are ${\mathsf{D}}_2$ -formulæ and thus satisfiable. Let ${\mathit{\psi }}^{\prime }:={\bigwedge }_{\mathit{j}=1}^{\mathit{m}}{\mathit{C}}_{\mathit{j}}^{\prime }$ 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 $\mathit{\psi }\in$ 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 $\mathit{k}\in \{1\mathrm{,}\dots \mathrm{,}\mathit{m}\}$ $$\begin{array}{cccc}\hfill \mathrm{Vars}\mathrm{(}{\mathit{\psi }}^{\prime }\mathrm{)}& \hfill =\hfill & \mathrm{Vars}\mathrm{(}{\mathit{\psi }}_{\mathit{k}}\mathrm{)}=\{{\mathit{x}}_{\mathit{i}}\mathrm{,}{\mathit{x}}_{\mathit{i}}^{\prime }|1⩽\mathit{i}⩽\mathit{n}\}.\hfill & \mathrm{(}1\mathrm{)}\hfill \\ \hfill \mathrm{Vars}\mathrm{(}\mathrm{\Phi }\mathrm{)}& \hfill =\hfill & \mathrm{Vars}\mathrm{(}{\mathrm{\Phi }}_{\mathit{k}}\mathrm{)}=\{{\mathit{x}}_{\mathit{i}}\mathrm{,}{\mathit{x}}_{\mathit{i}}^{\prime }|1⩽\mathit{i}⩽\mathit{n}\}\cup \{\mathit{u}\}.\hfill & \mathrm{(}2\mathrm{)}\hfill \end{array}$$ Suppose now that $\mathit{\psi }\in$ Critical-Sat, i.e. ψ is unsatisfiable and ψ _k is satisfiable for all $\mathit{k}\in \{1\mathrm{,}\dots \mathrm{,}\mathit{m}\}$ . We show that Φ entails α for all possible values of u, v, where we consider in detail only the case where v=0. The case v=1 is analogous.

$\mathrm{(}\mathit{u}\mathrm{,}\mathit{v}\mathrm{)}=\mathrm{(}1\mathrm{,}0\mathrm{)}$ : $\mathrm{\Phi }[\mathit{u}\mathrm{/}1]\equiv {\mathit{\psi }}^{\prime }$ and $\mathit{\alpha }[\mathit{u}\mathrm{/}1\mathrm{,}\mathit{v}\mathrm{/}0]\equiv {\bigvee }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\wedge {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ . Since $\mathit{\psi }\equiv {\mathit{\psi }}^{\prime }\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\oplus {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ is unsatisfiable and ψ′ is monotonic, all models of ψ′ have to set both x _i and x _i ′ to 1 for at least one $\mathit{i}\in \{1\mathrm{,}\dots \mathrm{,}\mathit{n}\}$ . Therefore, $\mathrm{\Phi }[\mathit{u}\mathrm{/}1]\vDash \mathit{\alpha }[\mathit{u}\mathrm{/}1\mathrm{,}\mathit{v}\mathrm{/}0]$ .

(u, v)=(0, 0): $\mathrm{\Phi }[\mathit{u}\mathrm{/}0]\equiv {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\wedge {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ and $\mathit{\alpha }[\mathit{u}\mathrm{/}0\mathrm{,}\mathit{v}\mathrm{/}0]\equiv {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\wedge {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ . Obviously $\mathrm{\Phi }[\mathit{u}\mathrm{/}0]\vDash \mathit{\alpha }[\mathit{u}\mathrm{/}0\mathrm{,}\mathit{v}\mathrm{/}0]$ .

It remains to prove that Φ is minimal. Since $\mathit{\psi }\in$ Critical-Sat, ${\mathit{\psi }}_{\mathit{k}}\equiv {\mathit{\psi }}_{\mathit{k}}^{\prime }\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\oplus {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ is satisfiable and hence ${\mathrm{\Phi }}_{\mathit{k}}[\mathit{u}\mathrm{/}1]\equiv {\mathit{\psi }}_{\mathit{k}}^{\prime }$ does not entail $\mathit{\alpha }[\mathit{u}\mathrm{/}1\mathrm{,}\mathit{v}\mathrm{/}0]\equiv {\bigvee }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\wedge {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ , i.e. ${\mathrm{\Phi }}_{\mathit{k}}⊭\mathit{\alpha }$ .

Conversely suppose that $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}\in$ Arg-Check. Then, in particular, Φ[u/1] entails $\mathit{\alpha }[\mathit{u}\mathrm{/}1\mathrm{,}\mathit{v}\mathrm{/}0]$ . Thus, we have ${\mathit{\psi }}^{\prime }\vDash {\bigvee }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\wedge {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ , which implies that ψ is unsatisfiable. By the minimality of Φ, we obtain that no Φ _k entails α. One easily verifies that in the cases $\mathrm{(}\mathit{u}\mathrm{,}\mathit{v}\mathrm{)}\in \{\mathrm{(}0\mathrm{,}0\mathrm{)}\mathrm{,}\mathrm{(}0\mathrm{,}1\mathrm{)}\mathrm{,}\mathrm{(}1\mathrm{,}1\mathrm{)}\}$ Φ _k still entails α (use Equation (2) for (u, v)=(0, 0)). Thus, we have that ${\mathrm{\Phi }}_{\mathit{k}}[\mathit{u}\mathrm{/}1]⊭\mathit{\alpha }[\mathit{u}\mathrm{/}1\mathrm{,}\mathit{v}\mathrm{/}0]$ , which implies that ${\mathit{\psi }}_{\mathit{k}}^{\prime }\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}\neg {\mathit{x}}_{\mathit{i}}\vee \neg {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ is satisfiable. As ψ _k ′ is monotonic, we obtain that ${\mathit{\psi }}_{\mathit{k}}^{\prime }\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\oplus {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ and hence ψ _k itself is satisfiable, too.

Finally, we transform $\mathrm{(}\mathrm{\Phi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ into a B-instance for all B such that ${\mathsf{D}}_2\subseteq [\mathit{B}]$ in replacing all occurrences of g _k by its B-representation. This transformation works in logarithmic space, because we may assume the function g _n to be a g₂-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.

Theorem 3.5

Let B be a finite set of Boolean functions. Then the argument validity problem for propositional B-formulæ, Arg – Check (B), is

DP-complete if ${\mathsf{S}}_{00}\subseteq [\mathit{B}]$ or ${\mathsf{S}}_{10}\subseteq [\mathit{B}]$ or ${\mathsf{D}}_2\subseteq [\mathit{B}]\mathrm{,}$

in P if ${\mathsf{L}}_2\subseteq [\mathit{B}]\subseteq \mathsf{L}\mathrm{,}$

in Logspace if $[\mathit{B}]\subseteq \mathsf{V}$ or $[\mathit{B}]\subseteq \mathsf{E}$ or $[\mathit{B}]\subseteq \mathsf{N}$ .

Proof

For DP-completeness, according to Propositions 3.3 and 3.4, it remains only to deal with the case ${\mathsf{S}}_{10}\subseteq [\mathit{B}]$ . Since ${\mathsf{D}}_2\subseteq {\mathsf{M}}_1=[{\mathsf{S}}_{10}\cup \{1\}]\subseteq [\mathit{B}\cup \{1\}]$ , we obtain that Arg-Check $\mathrm{(}\mathit{B}\cup \{1\}\mathrm{)}$ 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 ${\mathsf{L}}_2\subseteq [\mathit{B}]\subseteq \mathsf{L}$ , the sets Φ, $\mathrm{\Phi }\cup \{\neg \mathit{\alpha }\}$ , and $\mathrm{(}\mathrm{\Phi }\setminus \{\mathit{\phi }\}\mathrm{)}\cup \{\neg \mathit{\alpha }\}$ for all $\mathit{\phi }\in \mathrm{\Phi }$ 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 $[\mathit{B}]\subseteq \mathsf{V}$ , for $[\mathit{B}]\subseteq \mathsf{E}$ , and for $[\mathit{B}]\subseteq \mathsf{N}$ 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.3 The 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.

Theorem 3.6

Let B be a finite set of Boolean functions. Then the argument existence problem for propositional B -formulæ, Arg(B), is

${\mathrm{\Sigma }}_2^{\mathrm{p}}$ -complete if $\mathsf{D}\subseteq [\mathit{B}]$ or ${\mathsf{S}}_1\subseteq [\mathit{B}]\mathrm{,}$

coNP-complete if $\mathcal{X}\subseteq [\mathit{B}]\subseteq \mathcal{Y}$ with $\mathcal{X}\in \{{\mathsf{S}}_{00}\mathrm{,}{\mathsf{S}}_{10}\mathrm{,}{\mathsf{D}}_2\}$ and $\mathcal{Y}\in \{\mathsf{M}\mathrm{,}{\mathsf{R}}_1\}\mathrm{,}$

in NP if $[\mathit{B}]\in \{\mathsf{L}\mathrm{,}{\mathsf{L}}_0\mathrm{,}{\mathsf{L}}_3\}\mathrm{,}$

in P if $[\mathit{B}]\in \{{\mathsf{L}}_1\mathrm{,}{\mathsf{L}}_2\}\mathrm{,}$ and

in Logspace if $[\mathit{B}]\subseteq \mathsf{V}$ or $[\mathit{B}]\subseteq \mathsf{E}$ or $[\mathit{B}]\subseteq \mathsf{N}$ .

The same classification holds for Arg-Disp(B).

Proof

The general argumentation problem has been shown to be ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ -complete by Parsons et al. (2003) via a reduction from ${\mathrm{Qsat}}_{2\mathrm{,}\exists }$ . An instance of this problem is a quantified formula $\exists \mathit{X}\forall \mathit{Y}\mathit{\beta }$ , and one may assume that the formula β is in 3DNF, i.e. $\mathit{\beta }={\bigvee }_{\mathit{j}=1}^{\mathit{p}}{\mathit{t}}_{\mathit{j}}$ with exactly three literals by term. The authors map such an instance $\exists \mathit{X}\forall \mathit{Y}\mathit{\beta }$ to $\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{)}$ , where $\mathrm{\Delta }:=\{\mathit{x}\leftrightarrow 0\mathrm{,}\mathit{x}\leftrightarrow 1|\mathit{x}\in \mathit{X}\}$ , and $\mathit{\alpha }:=\mathit{\beta }$ . We use this reduction to obtain ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ -completeness for Arg(B) if $[\mathit{B}]=\mathsf{BF}$ . 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 $\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{)}$ .

As $\wedge \in {\mathsf{S}}_1$ and $[{\mathsf{S}}_1\cup \{1\}]=\mathsf{BF}$ , we obtain ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ -completeness for the case ${\mathsf{S}}_1\subseteq [\mathit{B}]$ according to Lemma 3.1. For the case $\mathsf{D}\subseteq [\mathit{B}]$ , we obtain ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ -completeness by Lemma 3.2, since ${\mathsf{D}}_2\subseteq \mathsf{D}$ and $[\mathsf{D}\cup \{1\}]=\mathsf{BF}$ .

For $\mathcal{X}\subseteq [\mathit{B}]\subseteq \mathcal{Y}$ with $\mathcal{X}\in \{{\mathsf{S}}_{00}\mathrm{,}{\mathsf{S}}_{10}\mathrm{,}{\mathsf{D}}_2\}$ and $\mathcal{Y}\in \{\mathsf{M}\mathrm{,}{\mathsf{R}}_1\}$ , 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 ${\mathsf{S}}_{00}$ , ${\mathsf{S}}_{10}$ , ${\mathsf{D}}_2$ . Let $\mathrm{(}\mathit{\psi }\mathrm{,}\mathit{\alpha }\mathrm{)}$ be a pair of B-formulæ. We map this instance to $\mathrm{(}\{\mathit{\psi }\}\mathrm{,}\mathit{\alpha }\mathrm{)}$ if ψ is satisfiable (which is easy to decide) and to a trivial positive instance otherwise.

For $[\mathit{B}]\in \{\mathsf{L}\mathrm{,}{\mathsf{L}}_0\mathrm{,}{\mathsf{L}}_3\}$ , 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 $[\mathit{B}]\in \{{\mathsf{L}}_1\mathrm{,}{\mathsf{L}}_2\}$ , we can improve the upper bound for Arg(B) with $[\mathit{B}]\in \{{\mathsf{L}}_1\mathrm{,}{\mathsf{L}}_2\}$ 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 $\mathrm{(}\mathit{B}\mathrm{)}{\equiv }_{\mathrm{m}}^{\log }$ Arg(B). To prove that Arg $\mathrm{(}\mathit{B}\mathrm{)}{⩽}_{\mathrm{m}}^{\log }$ Arg-Disp(B), map $\mathcal{A}=\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{)}$ to $\mathcal{D}:=\mathrm{(}\mathrm{\Delta }\cup \{\mathit{t}\}\mathrm{,}\mathit{\alpha }\mathrm{,}\mathit{t}\mathrm{)}$ . For the converse direction, map $\mathcal{D}=\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{,}\mathit{\phi }\mathrm{)}$ to $\mathcal{A}:=\mathrm{(}\mathrm{\Delta }\setminus \{\mathit{\phi }\}\mathrm{,}\mathit{\alpha }\mathrm{)}$ .  ▪

3.4 The 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.

Proposition 3.7

Let B be a finite set of Boolean functions such that ${\mathsf{S}}_{00}\subseteq [\mathit{B}]$ . Then Arg-Rel(B) is ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ -complete.

Proof

To see that Arg-Rel(B) is contained in ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ , observe that, given an instance $\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{,}\mathit{\phi }\mathrm{)}$ , we can guess a set $\mathrm{\Phi }\subseteq \mathrm{\Delta }$ such that $\mathit{\phi }\in \mathrm{\Phi }$ and verify conditions (C1)–(C3) in polynomial time using an NP-oracle.

To prove ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ -hardness, we provide a reduction from the problem ${\mathrm{Qsat}}_{2\mathrm{,}\exists }$ . An instance of this problem is a quantified formula $\exists \mathit{X}\forall \mathit{Y}\mathit{\beta }$ , where $\mathit{\beta }={\bigvee }_{\mathit{j}=1}^{\mathit{p}}{\mathit{t}}_{\mathit{j}}$ with exactly three literals by term. Let $\mathit{X}=\{{\mathit{x}}_1\mathrm{,}\dots \mathrm{,}{\mathit{x}}_{\mathit{n}}\}$ and $\mathit{Y}=\{{\mathit{y}}_1\mathrm{,}\dots \mathrm{,}{\mathit{y}}_{\mathit{m}}\}$ . Let u, v, ${\mathit{x}}_1^{\prime }\mathrm{,}\dots \mathrm{,}{\mathit{x}}_{\mathit{n}}^{\prime }\mathrm{,}{\mathit{y}}_1^{\prime }\mathrm{,}\dots \mathrm{,}{\mathit{y}}_{\mathit{m}}^{\prime }$ be fresh variables. We transform $\exists \mathit{X}\forall \mathit{Y}\mathit{\beta }$ to $\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{,}\mathit{\phi }\mathrm{)}$ , where $$\begin{array}{ccc}\hfill \mathrm{\Delta }& \hfill :=\hfill & \{{\mathit{x}}_{\mathit{i}}\mathrm{,}{\mathit{x}}_{\mathit{i}}^{\prime }\mid 1⩽\mathit{i}⩽\mathit{n}\}\cup \left\{\mathit{v}\wedge \underset{\mathit{i}=1}{\overset{\mathit{m}}{{\displaystyle \bigwedge }}}\mathrm{(}{\mathit{y}}_{\mathit{i}}\vee {\mathit{y}}_{\mathit{i}}^{\prime }\mathrm{)}\right\}\cup \{\mathit{u}\}\mathrm{,}\hfill \\ \hfill \mathit{\alpha }& \hfill :=\hfill & {\mathit{\beta }}^{\prime }\wedge \mathit{v}\wedge \left(\underset{\mathit{i}=1}{\overset{\mathit{n}}{{\displaystyle \bigvee }}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\wedge {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}\vee \mathit{u}\right)\mathrm{,}\hfill \\ \hfill \mathit{\phi }& \hfill :=\hfill & \mathit{u}\mathrm{,}\hfill \end{array}$$ and where ${\mathit{\beta }}^{\prime }={\bigvee }_{\mathit{j}=1}^{\mathit{p}}{\mathit{t}}_{\mathit{j}}^{\prime }$ and ${\mathit{t}}_{\mathit{j}}^{\prime }:={\mathit{t}}_{\mathit{j}}[\neg {\mathit{x}}_1\mathrm{/}{\mathit{x}}_1^{\prime }\mathrm{,}\dots \mathrm{,}\neg {\mathit{x}}_{\mathit{n}}\mathrm{/}{\mathit{x}}_{\mathit{n}}^{\prime }\mathrm{,}\neg {\mathit{y}}_1\mathrm{/}{\mathit{y}}_1^{\prime }\mathrm{,}\dots \mathrm{,}\neg {\mathit{y}}_{\mathit{m}}\mathrm{/}{\mathit{y}}_{\mathit{m}}^{\prime }]$ for all 1≤j≤p.

We show that $\exists \mathit{X}\forall \mathit{Y}\mathit{\beta }$ is valid if and only if $\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{,}\mathit{\phi }\mathrm{)}\in$ Arg-Rel $\mathrm{(}\{\wedge \mathrm{,}\vee \}\mathrm{)}$ . If $\exists \mathit{X}\forall \mathit{Y}\mathit{\beta }$ is valid, then there exists an assignment $\mathit{\sigma }:\mathit{X}\to \{0\mathrm{,}1\}$ such that $\mathit{\sigma }\vDash \mathit{\beta }$ . Consequently, for $\mathrm{\Phi }:=\{{\mathit{x}}_{\mathit{i}}\mid \mathit{\sigma }\mathrm{(}{\mathit{x}}_{\mathit{i}}\mathrm{)}=1\}\cup \{{\mathit{x}}_{\mathit{i}}^{\prime }\mid \mathit{\sigma }\mathrm{(}{\mathit{x}}_{\mathit{i}}\mathrm{)}=0\}\cup \{\mathit{u}\mathrm{,}\mathit{v}\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{m}}\mathrm{(}{\mathit{y}}_{\mathit{i}}\vee {\mathit{y}}_{\mathit{i}}^{\prime }\mathrm{)}\}$ , we obtain $\mathrm{\Phi }\vDash \mathit{\alpha }$ . As Φ is consistent, it thus remains to show that u is relevant, i.e. that $\mathrm{\Phi }\setminus \{\mathit{u}\}⊭\mathit{\alpha }$ . This follows from the fact that $\mathrm{\Phi }\setminus \{\mathit{u}\}$ is satisfied by any assignment σ′ extending σ with ${\mathit{\sigma }}^{\prime }\mathrm{(}\mathit{u}\mathrm{)}:=0$ and ${\mathit{\sigma }}^{\prime }\mathrm{(}{\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}:=1-\mathit{\sigma }\mathrm{(}{\mathit{x}}_{\mathit{i}}\mathrm{)}$ , while such a σ′ does not entail ${\bigvee }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\wedge {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}\vee \mathit{u}$ and hence ${\mathit{\sigma }}^{\prime }⊭\mathit{\alpha }$ .

For the converse direction, let Φ be a support for α such that u∈Φ. Since $\mathrm{\Phi }\vDash \mathit{\alpha }$ we conclude that $\mathit{v}\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{m}}\mathrm{(}{\mathit{y}}_{\mathit{i}}\vee {\mathit{y}}_{\mathit{i}}^{\prime }\mathrm{)}\in \mathrm{\Phi }$ and hence $\mathrm{\Phi }=\mathcal{X}\cup \{\mathit{v}\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{m}}\mathrm{(}{\mathit{y}}_{\mathit{i}}\vee {\mathit{y}}_{\mathit{i}}^{\prime }\mathrm{)}\}\cup \{\mathit{u}\}$ , for some $\mathcal{X}\subseteq \{{\mathit{x}}_{\mathit{i}}\mathrm{,}{\mathit{x}}_{\mathit{i}}^{\prime }\mid 1⩽\mathit{i}⩽\mathit{n}\}$ . From $\mathrm{\Phi }\vDash \mathit{\alpha }$ also follows that $\mathrm{\Phi }\vDash {\mathit{\beta }}^{\prime }$ . From the minimality of Φ, we conclude that in particular $\mathrm{\Phi }\setminus \{\mathit{u}\}⊭\mathit{\alpha }$ . And therefore $\mathrm{\Phi }⊭{\bigvee }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\wedge {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ . That is $\mathrm{\Phi }\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}\neg {\mathit{x}}_{\mathit{i}}\vee \neg {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ is satisfiable and since Φ is monotonic, consequently also $\mathrm{\Phi }\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\oplus {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}$ is satisfiable. Summed up, we know that $\mathit{\gamma }:=\mathcal{X}\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\oplus {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{m}}\mathrm{(}{\mathit{y}}_{\mathit{i}}\vee {\mathit{y}}_{\mathit{i}}^{\prime }\mathrm{)}$ is satisfiable and $\mathit{\gamma }\vDash {\mathit{\beta }}^{\prime }$ . Hence, a fortiori, ${\mathit{\gamma }}^{\prime }:=\mathcal{X}\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{n}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\oplus {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}\wedge {\bigwedge }_{\mathit{i}=1}^{\mathit{m}}\mathrm{(}{\mathit{y}}_{\mathit{i}}\oplus {\mathit{y}}_{\mathit{i}}^{\prime }\mathrm{)}$ is satisfiable and ${\mathit{\gamma }}^{\prime }\vDash {\mathit{\beta }}^{\prime }$ . Define now ${\mathit{\sigma }}_{\mathit{X}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\mathrm{)}=1$ if ${\mathit{x}}_{\mathit{i}}\in \mathcal{X}$ , ${\mathit{\sigma }}_{\mathit{X}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\mathrm{)}=0$ otherwise. Obviously any extension of σ _X to Y satisfies β and therefore $\exists \mathit{X}\forall \mathit{Y}\mathit{\beta }$ is valid.

It remains to transform $\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{,}\mathit{\phi }\mathrm{)}$ into an Arg-Rel(B)-instance for all B such that ${\mathsf{S}}_{00}\subseteq [\mathit{B}]$ . As both ∧ and ∨ are associative, we can insert parentheses into $\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{,}\mathit{\phi }\mathrm{)}$ , such that we can represent each formula as binary $\{\wedge \mathrm{,}\vee \}$ -tree of logarithmic depth. Let f be a fresh variable and let h be the Boolean function in ${\mathsf{S}}_{00}$ defined by $\mathit{h}\mathrm{(}\mathit{f}\mathrm{,}\mathit{x}\mathrm{,}\mathit{y}\mathrm{)}\equiv \mathit{f}\vee \mathrm{(}\mathit{x}\wedge \mathit{y}\mathrm{)}$ . We further transform our instance into $\mathrm{(}{\mathrm{\Delta }}^{\prime }\mathrm{,}{\mathit{\alpha }}^{\prime }\vee \mathit{f}\mathrm{,}{\mathit{\phi }}^{\prime }\mathrm{)}$ , where ${\mathrm{\Delta }}^{\prime }\mathrm{,}{\mathit{\alpha }}^{\prime }\mathrm{,}{\mathit{\phi }}^{\prime }$ are obtained by replacing each occurrence of x ∧ y by h( f, x, y). One easily verifies that $\mathrm{(}{\mathrm{\Delta }}^{\prime }\mathrm{,}{\mathit{\alpha }}^{\prime }\vee \mathit{f}\mathrm{,}{\mathit{\phi }}^{\prime }\mathrm{)}$ is in Arg-Rel $\mathrm{(}\{\vee \mathrm{,}\mathit{h}\}\mathrm{)}$ if and only if $\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{,}\mathit{\phi }\mathrm{)}\in$ Arg-Rel $\mathrm{(}\{\wedge \mathrm{,}\vee \}\mathrm{)}$ . We finally replace ∨ and h by their B-representation.  ▪

Proposition 3.8

Let B be a finite set of Boolean functions such that $[\mathit{B}]\subseteq \mathsf{V}$ or $[\mathit{B}]\subseteq \mathsf{E}$ or $[\mathit{B}]\subseteq \mathsf{N}$ . Then Arg-Rel(B) is in Logspace.

Proof

We assume the representation of $\mathsf{V}$ -, $\mathsf{E}$ -, or $\mathsf{N}$ -formulæ as respectively positive clauses, positive terms, or literals. Let us first consider Arg-Rel(B) for $[\mathit{B}]\subseteq \mathsf{E}$ . It is easy to observe that a set of positive terms Δ entails a positive term α if and only if $\mathrm{Vars}\mathrm{(}\mathit{\alpha }\mathrm{)}\subseteq \mathrm{Vars}\mathrm{(}\mathrm{\Delta }\mathrm{)}$ . 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: ${\mathrm{\Delta }}_{\mathit{x}}\vDash \mathit{\alpha }$ holds if and only if $\mathrm{Vars}\mathrm{(}\mathit{\alpha }\mathrm{)}\subseteq \mathrm{Vars}\mathrm{(}\mathit{\phi }\mathrm{)}\cup \mathrm{Vars}\mathrm{(}\{\mathit{\tau }\in \mathrm{\Delta }|\mathit{x}\notin \mathrm{Vars}\mathrm{(}\mathit{\tau }\mathrm{)}\}\mathrm{)}$ .

To prove correctness, notice that Algorithm 1 accepts only if there exists a ${\mathrm{\Delta }}_{\mathit{x}}\subseteq \mathrm{\Delta }$ such that ${\mathrm{\Delta }}_{\mathit{x}}\vDash \mathit{\alpha }$ and ${\mathrm{\Delta }}_{\mathit{x}}\setminus \{\mathit{\phi }\}⊭\mathit{\alpha }$ . Thus Δ _x contains a support Φ such that $\mathit{\phi }\in \mathrm{\Phi }$ . Conversely, let Φ be a support such that $\mathit{\phi }\in \mathrm{\Phi }$ . Since $\mathrm{\Phi }\vDash \mathit{\alpha }$ and $\mathrm{\Phi }\setminus \{\mathit{\phi }\}⊭\mathit{\alpha }$ , there is at least one ${\mathit{x}}_{\mathit{i}}\in \mathrm{(}\mathrm{Vars}\mathrm{(}\mathit{\phi }\mathrm{)}\cap \mathrm{Vars}\mathrm{(}\mathit{\alpha }\mathrm{)}\mathrm{)}\setminus \mathrm{Vars}\mathrm{(}\mathrm{\Phi }\mathrm{)}$ . For this x _i , the algorithm constructs ${\mathrm{\Delta }}_{{\mathit{x}}_{\mathit{i}}}:=\{\mathit{\phi }\}\cup \{\mathit{\tau }\in \mathrm{\Delta }\mid {\mathit{x}}_{\mathit{i}}\notin \mathrm{Vars}\mathrm{(}\mathit{\tau }\mathrm{)}\}$ . Obviously $\mathrm{\Phi }\subseteq {\mathrm{\Delta }}_{{\mathit{x}}_{\mathit{i}}}$ and therefore ${\mathrm{\Delta }}_{{\mathit{x}}_{\mathit{i}}}\vDash \mathit{\alpha }$ which causes the algorithm to accept.

Next, consider Arg-Rel(B) for $[\mathit{B}]\subseteq \mathsf{V}$ . Observe that a set of positive clauses C entails a positive clause α if and only if there is a clause c∈C such that $\mathrm{Vars}\mathrm{(}\mathit{c}\mathrm{)}\subseteq \mathrm{Vars}\mathrm{(}\mathit{\alpha }\mathrm{)}$ . Thus if there is a support Φ with $\mathit{\phi }\in \mathrm{\Phi }$ then it is the singleton $\{\mathit{\phi }\}$ . Given $\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{,}\mathit{\phi }\mathrm{)}$ as an instance of Arg-Rel $\mathrm{(}\mathsf{V}\mathrm{)}$ , it hence suffices to check whether $\mathrm{Vars}\mathrm{(}\mathit{\phi }\mathrm{)}\subseteq \mathrm{Vars}\mathrm{(}\mathit{\alpha }\mathrm{)}$ , which can be done in Logspace.

Finally Arg-Rel(B) for $[\mathit{B}]\subseteq \mathsf{N}$ is in Logspace, since each B-formula can be transformed into a single literal.  ▪

We obtain the following complexity classification for Arg-Rel.

Theorem 3.9

Let B be a finite set of Boolean functions. Then the argument relevance problem for propositional B -formulæ, Arg-Rel(B), is

${\mathrm{\Sigma }}_2^{\mathrm{p}}$ -complete if ${\mathsf{S}}_{00}\subseteq [\mathit{B}]$ or ${\mathsf{D}}_2\subseteq [\mathit{B}]$ or ${\mathsf{S}}_{10}\subseteq [\mathit{B}]\mathrm{,}$

in NP if ${\mathsf{L}}_2\subseteq [\mathit{B}]\subseteq \mathsf{L}\mathrm{,}$

in Logspace if $[\mathit{B}]\subseteq \mathsf{V}$ or $[\mathit{B}]\subseteq \mathsf{E}$ or $[\mathit{B}]\subseteq \mathsf{N}$ .

Proof

Applying Lemma 3.1 and Lemma 3.2 as shown in Section 3.1, for (1) it suffices to show hardness for B such that ${\mathsf{S}}_{00}\subseteq [\mathit{B}]$ . This has been done in Proposition 3.7. Item (2) follows from the fact that for $[\mathit{B}]\subseteq \mathsf{L}$ , Arg-Check(B) is in P (Proposition 3.5) and (3) has been shown in Proposition 3.8.  ▪

4. Enumeration and counting problems

4.1 Enumeration

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 $\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{,}\varnothing \mathrm{)}$ . 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 $\{\mathit{\phi }\}\cup \mathrm{\Phi }\vDash \mathit{\alpha }$ if and only if $\mathrm{\Phi }\vDash \mathrm{(}\mathit{\phi }\to \mathit{\alpha }\mathrm{)}$ . 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 $\mathit{\phi }\to \mathit{\alpha }$ ). There is an exception to the sets B such that ${\mathsf{S}}_0\subseteq [\mathit{B}]$ , since in this case $\to \in [\mathit{B}]$ and thus $\mathit{\phi }\to \mathit{\alpha }$ 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 $[\mathit{B}]\subseteq \mathsf{V}$ or $[\mathit{B}]\subseteq \mathsf{N}$ or $[\mathit{B}]\subseteq \mathsf{E}$ or $[\mathit{B}]\subseteq {\mathsf{L}}_1$ . Indeed the presented procedure can be slightly modified in these cases, except for the case $[\mathit{B}]\subseteq {\mathsf{L}}_1$ , 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.

Proposition 4.1

Let B be a finite set of Boolean functions. If $[\mathit{B}]\subseteq \mathsf{V}$ or $[\mathit{B}]\subseteq \mathsf{N}$ then Enum-Arg(B) is in FP. If $[\mathit{B}]\subseteq \mathsf{E}$ then Enum-Arg(B) is in DelayP.

Proof

If $[\mathit{B}]\subseteq \mathsf{V}$ or $[\mathit{B}]\subseteq \mathsf{N}$ 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 $[\mathit{B}]\subseteq \mathsf{E}$ 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 $\mathrm{\Phi }\vDash \mathit{\alpha }$ if and only if $\mathrm{Vars}\mathrm{(}\mathit{\alpha }\mathrm{)}\subseteq \mathrm{Vars}\mathrm{(}\mathrm{\Phi }\mathrm{)}$ . As a consequence, in the case of positive terms $\{\mathit{\phi }\}\cup \mathrm{\Phi }\vDash \mathit{\alpha }$ if and only if $\mathrm{\Phi }\vDash \mathit{\alpha }\setminus \mathit{\phi }\mathrm{,}$ where $\mathit{\alpha }\setminus \mathit{\phi }$ 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 $\mathit{\alpha }\setminus \mathit{\phi }$ instead of $\mathit{\alpha }\to \mathit{\phi }$ . 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 $[\mathit{B}]\subseteq \mathsf{E}$ (see Theorems 3.9 and 3.6), it is then clear that the procedure runs with polynomial delay and uses only polynomial space.  ▪

4.2 Counting

The argument counting problem #Arg(B) belongs to $\mathrm{\#}·\mathrm{NP}$ . This follows from the facts that checking an argument is in $\mathrm{DP}\subseteq {\mathrm{P}}^{\mathrm{NP}}={\mathrm{\Delta }}_2^{\mathrm{p}}$ (see Section 3.2) and from the equality $\mathrm{\#}·{\mathrm{\Delta }}_2^{\mathrm{p}}=\mathrm{\#}·\mathrm{NP}$ (see Hemaspaandra and Vollmer 1995).

Proposition 4.2

Let B be a finite set of Boolean functions such that either $\mathsf{D}\subseteq [\mathit{B}]$ or ${\mathsf{S}}_1\subseteq [\mathit{B}]$ . Then #Arg(B) is $\mathrm{\#}·\mathrm{NP}$ -complete.

Proof

We show $\mathrm{\#}·\mathrm{NP}$ -hardness by giving a parsimonious reduction from the following $\mathrm{\#}·\mathrm{NP}$ -hard problem: Count the number of satisfying assignments of $\mathit{\psi }\mathrm{(}{\mathit{x}}_1\mathrm{,}\dots \mathrm{,}{\mathit{x}}_{\mathit{n}}\mathrm{)}=\forall {\mathit{y}}_1\cdots \forall {\mathit{y}}_{\mathit{m}}\mathit{\phi }\mathrm{(}{\mathit{x}}_1\mathrm{,}\dots \mathrm{,}{\mathit{x}}_{\mathit{n}}\mathrm{,}{\mathit{y}}_1\mathrm{,}\dots \mathrm{,}{\mathit{y}}_{\mathit{m}}\mathrm{)}$ , where ϕ is a DNF-formula (Durand, Hermann, and Kolaitis 2005).

Let $\mathit{t}\mathrm{,}{\mathit{r}}_1\mathrm{,}\dots {\mathit{r}}_{\mathit{n}}$ be fresh variables. We map ψ to $\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{)}$ which we define as follows: $$\begin{array}{ccc}\hfill \mathrm{\Delta }& \hfill =\hfill & \{{\mathit{x}}_{\mathit{i}}\mathrm{,}\neg {\mathit{x}}_{\mathit{i}}\mathrm{,}{\mathit{x}}_{\mathit{i}}⟶{\mathit{r}}_{\mathit{i}}\mathrm{,}\neg {\mathit{x}}_{\mathit{i}}⟶{\mathit{r}}_{\mathit{i}}|1⩽\mathit{i}⩽\mathit{n}\}\cup \{\mathit{\phi }⟶\mathit{t}\}\hfill \\ \hfill \mathit{\alpha }& \hfill =\hfill & \mathit{t}\wedge \underset{\mathit{i}=1}{\overset{\mathit{n}}{{\displaystyle \bigwedge }}}{\mathit{r}}_{\mathit{i}}.\hfill \end{array}$$ By minimality, every support $\mathrm{\Phi }\subseteq \mathrm{\Delta }$ for α contains for every i either x _i or ¬ x _i , but not both. One easily verifies that by $\mathit{m}\mapsto \{{\mathit{x}}_{\mathit{i}}|\mathit{m}\mathrm{(}{\mathit{x}}_{\mathit{i}}\mathrm{)}=1\}\cup \{\neg {\mathit{x}}_{\mathit{i}}|\mathit{m}\mathrm{(}{\mathit{x}}_{\mathit{i}}\mathrm{)}=0\}$ we define a bijection between the models of ψ and the supports for α in Δ.

Since ${\mathsf{D}}_2\subseteq \mathsf{D}$ and ${\mathsf{E}}_2\subseteq {\mathsf{S}}_1$ , 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 $\mathrm{(}\mathit{B}\cup \{1\}\mathrm{)}{⩽}_{!}$ #Arg(B). Thus, it is sufficient to prove that hardness holds for #Arg $\mathrm{(}\mathit{B}\cup \{1\}\mathrm{)}$ . Since $\mathsf{BF}=[\mathsf{D}\cup \{1\}]\subseteq [\mathit{B}\cup \{1\}]$ and $\mathsf{BF}=[{\mathsf{S}}_1\cup \{1\}]\subseteq [\mathit{B}\cup \{1\}]$ , it suffices finally to prove that hardness of #Arg(B) holds for any B such that $\mathsf{BF}=[\mathit{B}]$ . Suppose that $\mathit{\phi }={\bigvee }_{\mathit{i}\in \mathit{I}}{\mathit{t}}_{\mathit{i}}$ and let Γ′ be the set of formulæ obtained from Γ by replacing $\mathit{\phi }\to \mathit{t}\equiv \neg \mathrm{(}{\bigvee }_{\mathit{i}\in \mathit{I}}{\mathit{t}}_{\mathit{i}}\mathrm{)}\vee \mathit{t}\equiv \mathrm{(}{\bigwedge }_{\mathit{i}\in \mathit{I}}\neg {\mathit{t}}_{\mathit{i}}\mathrm{)}\vee \mathit{t}$ by the set of clauses $\{\neg {\mathit{t}}_{\mathit{i}}\vee \mathit{t}|\mathit{i}\in \mathit{I}\}$ . 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 $\mathrm{\#}·\mathrm{NP}$ -complete problem to #Arg(B).  ▪

Proposition 4.3

Let B be a finite set of Boolean functions such that $\mathcal{X}\subseteq [\mathit{B}]\subseteq \mathcal{Y}$ with $\mathcal{X}\in \{{\mathsf{S}}_{00}\mathrm{,}{\mathsf{S}}_{10}\mathrm{,}{\mathsf{D}}_2\}$ and $\mathcal{Y}\in \{\mathsf{M}\mathrm{,}{\mathsf{R}}_1\}$ . Then #Arg (B) is in $\mathrm{\#}·\mathrm{NP}$ and #P;-hard.

Proof

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 ${\mathsf{S}}_{00}\subseteq [\mathit{B}]$ .

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 $\mathit{\phi }={\bigwedge }_{\mathit{j}=1}^{\mathit{p}}{\mathit{C}}_{\mathit{j}}$ with $\mathrm{Vars}\mathrm{(}\mathit{\phi }\mathrm{)}=\{{\mathit{x}}_1\mathrm{,}\dots \mathrm{,}{\mathit{x}}_{\mathit{n}}\}$ be such a formula. Let ${\mathit{x}}_1^{\prime }\mathrm{,}\dots \mathrm{,}{\mathit{x}}_{\mathit{n}}^{\prime }$ be fresh variables. We map ϕ to $\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{)}$ which we define as follows: $$\begin{array}{ccc}\hfill \mathrm{\Delta }& \hfill =\hfill & \{{\mathit{x}}_{\mathit{i}}\mathrm{,}{\mathit{x}}_{\mathit{i}}^{\prime }|1⩽\mathit{i}⩽\mathit{n}\}\hfill \\ \hfill \mathit{\alpha }& \hfill =\hfill & \mathit{\phi }\wedge \underset{\mathit{i}=1}{\overset{\mathit{n}}{{\displaystyle \bigwedge }}}\mathrm{(}{\mathit{x}}_{\mathit{i}}\vee {\mathit{x}}_{\mathit{i}}^{\prime }\mathrm{)}\hfill \end{array}$$ By minimality every support $\mathrm{\Phi }\subseteq \mathrm{\Delta }$ for α contains for every i either x _i or x _i ′, but not both. One easily verifies that by $\mathit{m}\mapsto \{{\mathit{x}}_{\mathit{i}}|\mathit{m}\mathrm{(}{\mathit{x}}_{\mathit{i}}\mathrm{)}=1\}\cup \{{\mathit{x}}_{\mathit{i}}^{\prime }|\mathit{m}\mathrm{(}{\mathit{x}}_{\mathit{i}}\mathrm{)}=0\}$ , we define a bijection between the models of ϕ and the supports for α in Δ.

It remains to show that α can be transformed in polynomial time into a B-formula for all B such that ${\mathsf{S}}_{00}\subseteq [\mathit{B}]$ . As ∧ and ∨ are monotonic, we can insert parentheses such that α is represented as a binary $\mathrm{(}\wedge \mathrm{,}\vee \mathrm{)}$ -tree of logarithmic depth. Let f be a fresh variable and let h be the Boolean functions in ${\mathsf{S}}_{00}$ defined by $\mathit{h}\mathrm{(}\mathit{f}\mathrm{,}\mathit{x}\mathrm{,}\mathit{y}\mathrm{)}\equiv \mathit{f}\vee \mathrm{(}\mathit{x}\wedge \mathit{y}\mathrm{)}$ . 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 $\vee \mathrm{,}\mathit{h}\in {\mathsf{S}}_{00}\subseteq [\mathit{B}]$ , we finally replace ∨ and h by their B-representation, thus concluding the proof.  ▪

Proposition 4.4

Let B be a finite set of Boolean functions such that ${\mathsf{E}}_2\subseteq [\mathit{B}]\subseteq \mathsf{E}$ . Then #Arg(B) is #P;-complete.

Proof

Membership in #P; follows from the fact that Arg $\mathrm{(}\mathit{B}\mathrm{)}\in \mathrm{P}$ for every B such that $[\mathit{B}]\subseteq \mathsf{E}$ .

To prove #P;-hardness, we establish a parsimonious reduction from the same #P;-hard problem as in the previous proposition. So let $\mathit{\phi }={\bigwedge }_{\mathit{j}=1}^{\mathit{p}}{\mathit{C}}_{\mathit{j}}$ with $\mathrm{Vars}\mathrm{(}\mathit{\phi }\mathrm{)}=\{{\mathit{x}}_1\mathrm{,}\dots \mathrm{,}{\mathit{x}}_{\mathit{n}}\}$ be a positive 2-CNF-formula. We introduce p new variables $\{{\mathit{c}}_1\mathrm{,}\dots \mathrm{,}{\mathit{c}}_{\mathit{p}}\}$ that will represent the clauses. For every 1≤i≤n let $\mathrm{occ}\mathrm{(}{\mathit{x}}_{\mathit{i}}\mathrm{)}=\{\mathit{j}|1⩽\mathit{j}⩽\mathit{p}\mathrm{,}{\mathit{x}}_{\mathit{i}}\text{occurs}{\mathit{C}}_{\mathit{j}}\}$ . We map ϕ to $\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{)}$ which we define as follows: $$\begin{array}{ccc}\hfill \mathrm{\Delta }& \hfill =\hfill & \left\{{\mathit{x}}_{\mathit{i}}\mathrm{,}{\mathit{x}}_{\mathit{i}}\wedge \underset{\mathit{j}\in \mathrm{occ}\mathrm{(}{\mathit{x}}_{\mathit{i}}\mathrm{)}}{{\displaystyle \bigwedge }}{\mathit{c}}_{\mathit{j}}|1⩽\mathit{i}⩽\mathit{n}\right\}\hfill \\ \hfill \mathit{\alpha }& \hfill =\hfill & \underset{\mathit{j}=1}{\overset{\mathit{p}}{{\displaystyle \bigwedge }}}{\mathit{c}}_{\mathit{j}}\wedge \underset{\mathit{i}=1}{\overset{\mathit{n}}{{\displaystyle \bigwedge }}}{\mathit{x}}_{\mathit{i}}\hfill \end{array}$$

By minimality every support $\mathrm{\Phi }\subseteq \mathrm{\Delta }$ for α contains for every i either x _i or ${\mathit{x}}_{\mathit{i}}\wedge {\bigwedge }_{\mathit{j}\in \mathrm{occ}\mathrm{(}{\mathit{x}}_{\mathit{i}}\mathrm{)}}{\mathit{c}}_{\mathit{j}}$ , but not both. One easily verifies that by $\mathit{m}\mapsto \{{\mathit{x}}_{\mathit{i}}\wedge {\bigwedge }_{\mathit{j}\in \mathrm{occ}\mathrm{(}{\mathit{x}}_{\mathit{i}}\mathrm{)}}{\mathit{c}}_{\mathit{j}}|\mathit{m}\mathrm{(}{\mathit{x}}_{\mathit{i}}\mathrm{)}=1\}\cup \{{\mathit{x}}_{\mathit{i}}|\mathit{m}\mathrm{(}{\mathit{x}}_{\mathit{i}}\mathrm{)}=0\}$ , 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 $\wedge \in {\mathsf{E}}_2\subseteq [\mathit{B}]$ .  ▪

Theorem 4.5

Let B be a finite set of Boolean functions. Then the argument counting problem for propositional B -formulæ, #Arg (B), is

$\mathrm{\#}·\mathrm{NP}$ -complete if $\mathsf{D}\subseteq [\mathit{B}]$ or ${\mathsf{S}}_1\subseteq [\mathit{B}]\mathrm{,}$

in $\mathrm{\#}·\mathrm{NP}$ and #P;-hard if $\mathcal{X}\subseteq [\mathit{B}]\subseteq \mathcal{Y}$ with $\mathcal{X}\in \{{\mathsf{S}}_{00}\mathrm{,}{\mathsf{S}}_{10}\mathrm{,}{\mathsf{D}}_2\}$ and $\mathcal{Y}\in \{\mathsf{M}\mathrm{,}{\mathsf{R}}_1\}\mathrm{,}$

in #P; if ${\mathsf{L}}_2\subseteq [\mathit{B}]\subseteq \mathsf{L}\mathrm{,}$

#P;-complete if ${\mathsf{E}}_2\subseteq [\mathit{B}]\subseteq \mathsf{E}\mathrm{,}$ and

in FP if $[\mathit{B}]\subseteq \mathsf{V}$ or $[\mathit{B}]\subseteq \mathsf{N}$ .

Proof

Items (1), (2) and (4) follow directly from the above three propositions. Item (3) follows from the fact that Arg $\mathrm{(}\mathit{B}\mathrm{)}\in \mathrm{NP}$ for B such that $[\mathit{B}]\subseteq \mathsf{L}$ (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 ${\mathsf{E}}_2\subseteq [\mathit{B}]\subseteq \mathsf{E}$ , 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 ( $\in \mathrm{DelayP}$ , 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 $\mathrm{P}\text{-}\mathrm{Abd}\mathrm{(}\mathit{B}\mathrm{)}$ . It takes as an instance a triple $\mathrm{(}\mathrm{\Gamma }\mathrm{,}\mathit{H}\mathrm{,}\mathit{m}\mathrm{)}$ , where $\mathrm{\Gamma }\subseteq \mathcal{L}\mathrm{(}\mathit{B}\mathrm{)}$ , $\mathit{m}\in \mathcal{L}\mathrm{(}\mathit{B}\mathrm{)}$ , H is a set of variables, and asks whether there exists an explanation E⊆ H such that $\mathrm{\Gamma }\wedge \mathit{E}$ is satisfiable and $\mathrm{\Gamma }\wedge \mathit{E}\vDash \mathit{m}$ . 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:

if ∧∈[B], i.e. if ${\mathsf{E}}_2\subseteq [\mathit{B}]$ , then $\mathrm{P}\text{-}\mathrm{Abd}\mathrm{(}\mathit{B}\mathrm{)}{⩽}_{\mathrm{m}}^{\log }$ Arg(B)

if $\to \in [\mathit{B}]$ , i.e. if ${\mathsf{S}}_0\subseteq [\mathit{B}]$ , then Arg $\mathrm{(}\mathit{B}\mathrm{)}{⩽}_{\mathrm{m}}^{\log }\mathrm{P}\text{-}\mathrm{Abd}\mathrm{(}\mathit{B}\mathrm{)}$

For (1), one can give the reduction $\mathrm{(}\mathrm{\Gamma }\mathrm{,}\mathit{A}\mathrm{,}\mathit{\psi }\mathrm{)}\mapsto \mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{)}$ , where $\mathrm{\Delta }:=\{{\bigwedge }_{\mathit{\phi }\in \mathrm{\Gamma }}\mathit{\phi }\}\cup \mathit{A}$ and $\mathit{\alpha }:=\mathit{\psi }\wedge {\bigwedge }_{\mathit{\phi }\in \mathrm{\Gamma }}\mathit{\phi }$ ; likewise the mapping $\mathrm{(}\mathrm{\Delta }\mathrm{,}\mathit{\alpha }\mathrm{)}\mapsto \mathrm{(}\mathrm{\Gamma }\mathrm{,}\mathit{A}\mathrm{,}\mathit{\alpha }\mathrm{)}$ , where $\mathit{A}:=\{{\mathit{x}}_{\mathit{\phi }}\mid \mathit{\phi }\in \mathrm{\Delta }\}$ and $\mathrm{\Gamma }:=\{{\mathit{x}}_{\mathit{\phi }}\leftrightarrow \mathit{\phi };|\mathit{\phi }\in \mathrm{\Delta }\}$ underlies (2).

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.

Table 2.

The complexity of the argumentation problems.

	${\mathsf{N}}_{\ast }\mathrm{,}{\mathsf{V}}_{\ast }$	$\mathsf{E}$ *	${\mathsf{L}}_1\mathrm{,}{\mathsf{L}}_2$	$\mathsf{L}\mathrm{,}{\mathsf{L}}_0\mathrm{,}{\mathsf{L}}_3$	${\mathsf{D}}_2\mathrm{,}{\mathsf{S}}_{\ast 0}\subseteq$ $[\mathit{B}]\subseteq \mathsf{M}\mathrm{,}{\mathsf{R}}_1$	$\mathsf{D}\mathrm{,}{\mathsf{S}}_1\subseteq$ $[\mathit{B}]\subseteq \mathsf{BF}$
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	$\mathrm{coNP}\text{-}\mathrm{c}$ , 3.6	${\mathrm{\Sigma }}_2^{\mathrm{p}}$ -c, 3.6
Arg-Rel	∈L, 3.8	∈L, 3.8	∈NP, 3.9	∈NP, 3.9	${\mathrm{\Sigma }}_2^{\mathrm{p}}$ -c, 3.7	${\mathrm{\Sigma }}_2^{\mathrm{p}}$ -c, 3.7
Enum-Arg	∈FP, 4.1	$\in \mathrm{DelayP}$ , 4.1	Unknown	Unknown	coNP-h, 3.6	${\mathrm{\Sigma }}_2^{\mathrm{p}}$ -h, 3.6
#Arg	∈FP, 4.5	#P;-c, 4.4	∈#P;, 4.5	∈#P;, 4.5	$\in \mathrm{\#}·\mathrm{NP}$ , #P;-h, 4.3	$\mathrm{\#}·\mathrm{NP}$ -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 ${\mathsf{V}}_{\ast }\mathrm{,}{\mathsf{N}}_{\ast }$ ) then all considered decision problems as well as counting and enumeration are very easy. When allowing for positive terms (column $\mathsf{E}$ _*), 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 $\mathcal{X}\subseteq [\mathit{B}]\subseteq \mathcal{Y}$ with $\mathcal{X}\in \{{\mathsf{S}}_{00}\mathrm{,}{\mathsf{S}}_{10}\mathrm{,}{\mathsf{D}}_2\}$ and $\mathcal{Y}\in \{\mathsf{M}\mathrm{,}{\mathsf{R}}_1\}$ . 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 ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ . 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 $\mathsf{L}$ -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 ${\mathsf{L}}_2\subseteq [\mathit{B}]\subseteq {\mathsf{L}}_1$ is in P relies on Gaussian elimination, knowing that in this case we only have to check whether $\mathrm{\Phi }\vDash \mathit{\alpha }$ , that is whether the linear system $\mathrm{\Phi }\wedge \neg \mathit{\alpha }$ 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 $[\mathit{B}]\in \{\mathsf{L}\mathrm{,}{\mathsf{L}}_0\mathrm{,}{\mathsf{L}}_3\}$ and Arg-Rel(B) with ${\mathsf{L}}_2\subseteq [\mathit{B}]\subseteq \mathsf{L}$ .1 1

We note that the complexity of the corresponding fragments remained unclassified also for circumscription and positive abduction.

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. ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ ) 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, ${\mathrm{\Sigma }}_2^{\mathrm{p}}$ 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).