SAT - Hardness of determining backbone literals Let $F$ be a CNF formula. Let $l$ be one of $F$'s literals.


  Question
  Which is the complexity of determining whether $l$ is a backbone literal or not? The obvious way to do that is to propagate $\lnot l$ on $F$, obtaining $F&#39;$: $l$ is then a backbone literal of $F$ if and only if $F&#39;$ is unsatisfiable. I'm asking if there is another way.
The complexity is co-NP complete because you're converting to unsatisfiability of $F \land \lnot l$. I have a proof of the completeness in my PhD thesis, Claim 2 (if I may blatantly advertise myself).

There's a small problem for unsatisfiable formulas, if your definition of a backbone means that all the literals are backbone for an unsatisfiable formula, then the problem stays in co-NP. If, however, the set of backbone literals is empty for an unsatisfiable formula, you also need NP.