<p>The complexity is <em>co-NP</em> complete because you're converting to <b>un</b>satisfiability of $F \land \lnot l$. I have a proof of the completeness in my <a href="http://sat.inesc-id.pt/~mikolas/th.pdf" rel="nofollow">PhD thesis, Claim 2</a> (if I may blatantly advertise myself).</p>

<p>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 <em>co-NP</em>. If, however, the set of backbone literals is empty for an unsatisfiable formula, you also need <em>NP</em>.</p>

CC BY-SA 3.0
2011-04-18T13:00:20.237Z
I prefer the definition where all the literals are backbone for an unsatisfiable formula.
Giorgio Camerani
CC BY-SA 3.0
2011-04-02T16:31:00.273Z
2011-04-18T14:42:36.590Z
2011-04-18T14:42:36.590Z
Mikolas
<p>Let $F$ be a CNF formula. Let $l$ be one of $F$'s literals.</p>

<blockquote>
  <p><b>Question</b><br><br>
  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.</p>
</blockquote>

CC BY-SA 2.5
2011-04-01T17:04:12.860Z
Isn't that just SAT of $F\land\lnot l$? That is, it's NP-complete. Am I missing something?
Radu GRIGore
CC BY-SA 2.5
2011-04-01T17:10:27.013Z
@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
CC BY-SA 2.5
2011-04-01T21:09:49.797Z
*Backbone* literals look very similar to *frozen* variables. There are ways to determine/approximate them in random k-CNF literature.
Kaveh
CC BY-SA 2.5
2011-04-01T22:45:40.720Z
For practical algorithms, I believe [Marques-Silva, Janota, and Lynce](http://sat.inesc-id.pt/~mikolas/ecai10.pdf) is a good place to look.
Radu GRIGore
CC BY-SA 2.5
2011-04-02T09:11:53.223Z
@Radu: Thanks for the pointer to that paper. I'm reading it right now.
Giorgio Camerani
<cc.complexity-theory><ds.algorithms><sat>
SAT - Hardness of determining backbone literals
Giorgio Camerani
# SAT - Hardness of determining backbone literals

(Asked by: username_0 on 2011-04-01)

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.

**Tags:** cc.complexity-theory, ds.algorithms, sat

> **Comments:**
> **username_1**: Isn't that just SAT of $F\land\lnot l$? That is, it's NP-complete. Am I missing something?  
> **username_0**: @username_1: 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.  
> **username_2**: *Backbone* literals look very similar to *frozen* variables. There are ways to determine/approximate them in random k-CNF literature.  
> **username_1**: For practical algorithms, I believe [Marques-Silva, Janota, and Lynce](http://sat.inesc-id.pt/~mikolas/ecai10.pdf) is a good place to look.  
> **username_0**: @Radu: Thanks for the pointer to that paper. I'm reading it right now.  

---

## 1 answers

### Answer by username_3 on 2011-04-02. Score: 7 | Accepted answer

The complexity is *co-NP* complete because you're converting to **un**satisfiability of $F \land \lnot l$. I have a proof of the completeness in my [PhD thesis, Claim 2](http://sat.inesc-id.pt/~mikolas/th.pdf) (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*.

> **Comments:**
> **username_0**: I prefer the definition where all the literals are backbone for an unsatisfiable formula.  

---

