<p>If "independent" means "not inferred by unit propagation", then the answer is "no". Eg. 
$$ 
\lnot a \lor b, x\lor \lnot b,\lnot x\lor \lnot b
$$.</p>

CC BY-SA 3.0
2011-07-03T09:15:17.510Z
I interpreted "independent" as "does not appear in", that is, no occurrence of $b$ appears in $F_{\neg a}$. But the question should indeed be modified to provide a definition.
Dave Clarke
CC BY-SA 3.0
2011-07-03T11:53:18.547Z
@Dave Right, I see what you mean. But then the question's  trivial.
Mikolas
CC BY-SA 3.0
2011-07-03T08:24:35.540Z
2011-07-03T08:24:35.540Z
Mikolas
<p>Let's denote $F$ a Boolean formula (in CNF if you wish) and $F_{a}$ the same formula where literal $a$ was assigned and propagated (using <a href="http://en.wikipedia.org/wiki/Unit_propagation" rel="nofollow">unit propagation</a>).</p>

<p>If $F_{a} \rightarrow b$ (b is propagated from a) and $F_{\neg a} \rightarrow b$ then I can imply $b$ ($\neg a \rightarrow b \land a \rightarrow b \Rightarrow b $). In other words, any satisfying assignment for $F$ must have $b$.</p>

<p>If $F_{a} \rightarrow b$ and $F_{\neg a}$ is independent of $b$, is there always a satisfying assignment for $F$ that has $b$ when $F$ can be satisfied?</p>

CC BY-SA 3.0
2011-07-02T18:19:45.403Z
There is a satisfying assignment with $b$ true. As $F$ is satisfiable, then there is an assignment $\sigma$ which includes either $a$ or $\neg a$. In the first case, $F_a\to b$, so $\sigma$ must include $b$. In the second case, as $F_{\neg a}$ is independent of $b$, both $\sigma$ and $\sigma$ with $b$ negated are satisfying assignments.
Dave Clarke
CC BY-SA 3.0
2011-07-03T09:15:58.967Z
Due to the different interpretations people have of "independent", can you please clarify your question. What do you mean by independent?
Dave Clarke
<sat>
Does assigning missing literals after unit propagation keep a Boolean formula satisfiable?
Alexandru
# Does assigning missing literals after unit propagation keep a Boolean formula satisfiable?

(Asked by: username_0 on 2011-07-02)

Let's denote $F$ a Boolean formula (in CNF if you wish) and $F\_{a}$ the same formula where literal $a$ was assigned and propagated (using [unit propagation](http://en.wikipedia.org/wiki/Unit_propagation)).

If $F\_{a} \rightarrow b$ (b is propagated from a) and $F\_{\neg a} \rightarrow b$ then I can imply $b$ ($\neg a \rightarrow b \land a \rightarrow b \Rightarrow b $). In other words, any satisfying assignment for $F$ must have $b$.

If $F\_{a} \rightarrow b$ and $F\_{\neg a}$ is independent of $b$, is there always a satisfying assignment for $F$ that has $b$ when $F$ can be satisfied?

**Tags:** sat

> **Comments:**
> **username_1**: There is a satisfying assignment with $b$ true. As $F$ is satisfiable, then there is an assignment $\sigma$ which includes either $a$ or $\neg a$. In the first case, $F_a\to b$, so $\sigma$ must include $b$. In the second case, as $F_{\neg a}$ is independent of $b$, both $\sigma$ and $\sigma$ with $b$ negated are satisfying assignments.  
> **username_1**: Due to the different interpretations people have of "independent", can you please clarify your question. What do you mean by independent?  

---

## 1 answers

### Answer by username_2 on 2011-07-03. Score: 1

If "independent" means "not inferred by unit propagation", then the answer is "no". Eg.
$$
\lnot a \lor b, x\lor \lnot b,\lnot x\lor \lnot b
$$.

> **Comments:**
> **username_1**: I interpreted "independent" as "does not appear in", that is, no occurrence of $b$ appears in $F_{\neg a}$. But the question should indeed be modified to provide a definition.  
> **username_2**: @Dave Right, I see what you mean. But then the question's  trivial.  

---

