
## Appendix A: Proofs

Proposition 1 A formula Σ is Lit-independent from I if and only if, for any interpretation ω E Ωρς, if ω |= Σ then Force(ω, ¬l) |= Σ.

Proof: Assume that Σ is Lit-independent from l . Then, there exists a formula Φ in NNF
that is equivalent to Σ , and does not contain l . Then, for any ω ∈ Ω P S such that ω ├ Φ
we have Force(w, ¬ l ) = Φ. Since Φ is equivalent to Σ, we conclude that the same property holds for Σ.

Assume that, for any interpretation ω ∈ Ω P S, ω ├ Σ implies Force (ω, ¬) ├ Σ. We prove that Σ is Lit-independent from l . Indeed, let γω be the term whose only model is ω The following equivalence holds:

$$\Sigma\;\;\equiv\;\;\bigvee\{\gamma_{\omega}\;|\;\omega\models\Sigma\}$$

$\forall\ \{\gamma_{\omega}\ |\ \omega\models\Sigma\ \text{and}\ \omega\not\models l\}\cup\{\gamma_{\omega}\ |\ \omega\models\Sigma\ \text{and}\ \omega\models l\}$  $\forall\ \{\gamma_{\omega}\ |\ \omega\models\Sigma\ \text{and}\ \omega\not\models l\}\cup\{\gamma_{\omega}\ \forall\ \gamma_{Force\,(\omega,\neg l)}\ |\ \omega\models\Sigma\ \text{and}\ \omega\not\models l\}$.  
The latter step can be done because ω = Σ implies that Force ( ω, ¬ l ) is also a model of Σ . Now, if ω | ≥ l then γω does not contain l . On the other hand, if ω |= l, then Yw V YForce(w,-t) can be rewritten as a conjunction of literals not containing neither l nor its negation. As a result, the above formula (which is in NNF) does not contain l , which means that Σ is Lit-independent from l .

## Proposition 2

(1) DepLit(Σ) ⊆ Lit(Σ);
(2) If Σ ≡ Φ, then DepLit(Σ) = DepLit(Φ); (3a) DepLit(Σ ∧ Φ) ⊆ DepLit(Σ) ∪ DepLit(Φ); (3b) DepLit(Σ V Φ) ⊆ DepLit(Σ) ∪ DepLit(Φ); (4) l E DepLit(E) if and only if ¬l E DepLit(¬L).

## Proof:

1. Trivial.

2. L ¨ E if and only if there exists a formula ¨ E that is equivalent to Σ , and such that
¥ is syntactically Lit-independent from L . Since Σ = Φ , it follows that Φ = Ψ .

3. Let Ï (resp. II) be a NNF formula equivalent to E (resp. Ï) s.t. no literal of L occurs in it. Then Ψ ∧Π (resp. Ψ ∨Π) is a formula equivalent to Σ ∧Φ (resp. Σ ∨Φ), which is in NNF, and no literal of L occurs in it.

4. Straightforward from the fact that l appears in a NNF formula Σ if and only if - l appears in the NNF form of ¬Σ.