Let $F$ be a CNF formula. Let $l$ be one of $F$'s literals.
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'$: $l$ is then a backbone literal of $F$ if and only if $F'$ is unsatisfiable. I'm asking if there is another way.