# Does assigning missing literals after unit propagation keep a Boolean formula satisfiable?

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

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?

• 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 Jul 2 '11 at 18:19
• Due to the different interpretations people have of "independent", can you please clarify your question. What do you mean by independent? – Dave Clarke Jul 3 '11 at 9:15

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$$.
• 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 Jul 3 '11 at 9:15