# 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'$: $l$ is then a backbone literal of $F$ if and only if $F'$ is unsatisfiable. I'm asking if there is another way.

• Isn't that just SAT of $F\land\lnot l$? That is, it's NP-complete. Am I missing something? – Radu GRIGore Apr 1 '11 at 17:04
• @Radu GRIGore: What you say is of course right, it is the obvious and natural way to do that: just reduce the question to SAT (note this doesn't mean the question is NP-complete too). I wonder if there is another way. – Giorgio Camerani Apr 1 '11 at 17:10
• Backbone literals look very similar to frozen variables. There are ways to determine/approximate them in random k-CNF literature. – Kaveh Apr 1 '11 at 21:09
• For practical algorithms, I believe Marques-Silva, Janota, and Lynce is a good place to look. – Radu GRIGore Apr 1 '11 at 22:45
• @Radu: Thanks for the pointer to that paper. I'm reading it right now. – Giorgio Camerani Apr 2 '11 at 9:11

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).