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$ 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$ 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$ Apr 1 '11 at 22:45
  • $\begingroup$ @Radu: Thanks for the pointer to that paper. I'm reading it right now. $\endgroup$ 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.

  • $\begingroup$ I prefer the definition where all the literals are backbone for an unsatisfiable formula. $\endgroup$ 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.