- Membership. In order to show that E is Var-dependent on V, it is sufficient to guess a variable x from V and a (Var(E) \ {x})-world ω that is not a model of the formula ∑ x ←o ↔ ∑ x →1. This test can be achieved in time polynomial in | ∑ |.

- Hardness.

Similar to the hardness proof of FL-dependence, replacing "Litdependent" by "Var-dependent".

## - Full Fl Dependence

- Membership. Σ is fully Lit-dependent on L = { l 1 , ..., l n } if and only if Σ l , ← l ̸ =
‡ i ← 0 and … and Σ i ∞ ← 1 ̸ = Σ i ∞ ← 0 holds. Equivalently, Σ is fully Lit-dependent on L = { l 1 , ..., l n } if and only if the formula rename 1 ( Σ l , ← 1 ∧ ¬Σ l , ← 0 ) ∧ ... ∧ renamen (Σ tn ← 1 ∧¬Σ tn ← 0 ) is satisfiable, where each rename is a renaming that maps variables to new symbols (in a uniform way). Since this formula can be computed in time polynomial in [Σ ] + [ V ], the membership of FULL FL DEPEN-
DENCE to NP follows.

 Hardness. Full FL-dependence and FL-dependence coincide in the case in which L is composed of a single literal. Since the NP-hardness of FL-dependence has been proved using a set L composed of a single literal, the NP-hardness of full FL dependence follows.

## - Full Fv Dependence

- Membership. Σ is fully Var-dependent on V = { x 1 , ..., x n } if and only if Σ ̸ =
Σ x t ← 0 and … and Σ ̸ = Σ x t ← 0 holds. Equivalently, Σ is fully Var-dependent on V = { x 1 , …, x n } if and only if the formula r enam e 1 ( Σ⊕Σ x 1 ← 0 ) ∧… ∧ r enam e n ( Σ⊕ Exx ←0 ) is satisfiable, where each rename is a renaming that maps variables to new symbols (in a uniform way). Since this formula can be computed in time polynomial in [Σ ] + | V ], the membership of FULL FV DEPENDENCE to NP follows.

Hardness. Full FV-dependence and FV-dependence coincide if L is composed of a single literal.  Since the NP-hardness of FV-dependence has been proved using a set L composed of a single literal, the NP-hardness of full FV-dependence follows.
Proposition 11   Whenever Σ belongs to a class C of CNF formulas that is tractable for clausal query answering (i.e., there exists a polytime algorithm to determine whether Σ |= γ for any CNF formula γ) and stable for variable instantiation (i.e., replacing in Σ ∈ C any variable by true or by false gives a formula that still belongs to C) then FL DEPENDENCE,
FV DEPENDENCE, FULL FL DEPENDENCE and FULL FV DEPENDENCE are in P.

Proof: This is a straightforward consequence of Propositions 6 and 7. When Σ belongs to a class C of formulas that is tractable for clausal query answering and stable for variable instantiation, we can easily check whether Σ |= Σ x ← 0 and Σ x ← 0 |= Σ holds.