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.

  • $\begingroup$ Isn't that just SAT of $F\land\lnot l$? That is, it's NP-complete. Am I missing something? $\endgroup$ – Radu GRIGore Apr 1 '11 at 17:04
  • $\begingroup$ @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. $\endgroup$ – Giorgio Camerani Apr 1 '11 at 17:10
  • 1
    $\begingroup$ Backbone literals look very similar to frozen variables. There are ways to determine/approximate them in random k-CNF literature. $\endgroup$ – Kaveh Apr 1 '11 at 21:09
  • 2
    $\begingroup$ For practical algorithms, I believe Marques-Silva, Janota, and Lynce is a good place to look. $\endgroup$ – Radu GRIGore Apr 1 '11 at 22:45
  • $\begingroup$ @Radu: Thanks for the pointer to that paper. I'm reading it right now. $\endgroup$ – 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).

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.

| cite | improve this answer | |
  • $\begingroup$ I prefer the definition where all the literals are backbone for an unsatisfiable formula. $\endgroup$ – Giorgio Camerani Apr 18 '11 at 13:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.