
## Proof :

- Determining whether DepLit(E) = L is BH2-complete.

- Membership.

DepLit(Σ) = L if and only if (i) l ↦ Σ holds for every l ∈ L and (ii) l ̸ A Σ
holds for every l E Lit(E) \ L; the set of instances (E, L) such that (i) holds is the union of a linear number of problems in NP, thus it is in NP; similarly, the set of instances ( Σ, L ) such that (ii) holds is a problem in coNP. This proves the membership to BH 2 of the problem of determining whether DepLit(Σ) = L .

- Hardness.

Let (Φ, Γ) be a pair of propositional formulas. Without loss of generality, we assume that Φ and Γ do not share any variable and that X = V ar(Φ) = { x 1 , ..., x n };
Var(Γ) = { z 1 , ..., z p } . Furthermore we assume that X ̸= ∅ (if it were not the case it would then be sufficient then to replace Φ by Φ Λ (t V ¬t) before performing the reduction). We prove that (Φ,Γ) is a positive instance of SAT-UNSAT, i.e., Φ
is satisfiable and Γ is unsatisfiable, if and only if DepLit ( Φ ∧ ¬Γ) = Lit ( Σ( Φ))
where Σ(Φ) = (ΦVΦ[X/¬X]) ^ Λ x ; ε χ x ¡ ⇔ y i as in a previous proof (note that L(Q) and F do not share any variables).

(i) if Φ is satisfiable and Γ is unsatisfiable, then Σ(Φ) is Lit-simplified according to the previous proof and thus DepLit(E(O)) = Lit(E(O)) whereas DepLit(¬Γ) = 0, which together entail that DepLit(Σ(Φ) ∧¬Γ) = Lit(Σ(Φ)).

(ii) Assume that Φ is unsatisfiable and DepLit(Σ(Φ) ∧ ¬Γ) = Lit(Σ(Φ)). Then
‡(Ø) is not simplified (recall that Var(Ø) is not empty and hence so is Lit(Ë(Ø)), thus DepLit(E(O)) C Lit(E(O)). Now, DepLit(E(O)A¬F) = Lit(E(O)) implies DepLit(E(Q) A -F) N Lit(F) = Q, which is possible only if F is a tautology (because E(Φ) and Γ do not share any variables); but in this case, Σ(Φ) Λ ¬Γ is inconsistent and thus DepLit(E(@) A ¬ Γ) = 0, hence, Lit(Σ(@)) = 0, which is contradictory.

(iii) Assume that Γ is satisfiable and DepLit(Σ(Φ) ∧¬Γ) = Lit(Σ(Φ)).

The second condition can hold only if )() is unsatisfiable, hence not Litsimplified (since Lit(E(~)) ~ ~), so ~ is unsatisfiable as well; this takes us back to the case (ii), which leads us to the same contradiction again.

- Computing DepLit(Σ) is in FΔ 2 since FL DEPENDENCE is in NP and DepLit(Σ) ⊆
Lit(E) (hence, it is sufficient to test for every l E Lit(E) whether or not E is Litindependent from it). It is also both NP-hard and coNP-hard. NP-hardness is showed by the following polynomial reduction from SAT: A CNF formula F is satisfiable if and only if F is valid or DepLit(F) ̸= 0; clearly enough, valid CNF formulas can be recognized in polynomial time. Thus, SAT can be solved if we know how to compute DepLit ( Σ ) for any Σ , which shows that computing DepLit ( Σ ) is NP-hard. The proof of coNP-hardness is similar ( F is unsatisfiable if and only if F is not valid and DepLit(F) = 0).