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?

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

  • $\begingroup$ 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. $\endgroup$ Jul 3 '11 at 9:15
  • $\begingroup$ @Dave Right, I see what you mean. But then the question's trivial. $\endgroup$
    – Mikolas
    Jul 3 '11 at 11:53

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.