3
$\begingroup$

I have a problem with the application of the Shannon expansion for to obtain the negation of a formula boolean, than will need for implement the negation operator on OBDD (Order Binary Decision Diagram) that is, show that:

$\qquad \displaystyle \neg f(x_1,\ldots,x_n) = (\neg x_1 \wedge \neg f|_{x_1=0}) \vee (x_1 \wedge \neg f|_{x_1=1})$

where $f|_{x_i=b}$ is the function boolean in which replaces $x_i$ with b, that is:

$\qquad \displaystyle f|_{x_i=b}(x_1,\ldots,x_n)=f(x_1,\ldots,x_{i-1},b,x_{i+1},\ldots,x_n)$.

The proof says:

$\qquad \displaystyle\neg f(x_1,\ldots,x_n) = \neg((\neg x_1 \wedge f|_{x_1=0}) \vee (x_1 \wedge f|_{x_1=1}))$.

Applying the negation (skip the intermediate steps), we get:

$\qquad \displaystyle (x_1 \wedge \neg x_1) \vee (\neg x_1 \wedge \neg f|_{x_1=0}) \vee (x_1 \wedge \neg f|_{x_1=1}) \vee (\neg f|_{x_1=0} \wedge \neg f|_{x_1=1}) $.

Now $(x_1 \wedge \neg x_1)= \mathrm{false}$ can be dropped, which leads to

$\qquad \displaystyle (\neg x_1 \wedge \neg f|_{x_1=0}) \vee (x_1 \wedge \neg f|_{x_1=1}) \vee (\neg f|_{x_1=0} \wedge \neg f|_{x_1=1}) $

which in turn is, finally, equal to

$\qquad \displaystyle (\neg x_1 \wedge \neg f|_{x_1=0}) \vee (x_1 \wedge \neg f|_{x_1=1})$.

Why does this hold?

$\endgroup$
4
$\begingroup$

Maybe it is better to understand if you make a truth table for both functions. You can see that if $(\neg f|_{x_1=0} \wedge \neg f|_{x_1=1})$ is true then $(\neg x_1 \wedge \neg f|_{x_1=0}) \vee (x_1 \wedge \neg f|_{x_1=1})$ is also true, because both $f$ terms are true and either $x_1$ is true or $\neg x_1$ is true. And if $(\neg f|_{x_1=0} \wedge \neg f|_{x_1=1})$ is false then you have to do a case study:

  • If both $f$ terms are false then is $(\neg x_1 \wedge \neg f|_{x_1=0}) \vee (x_1 \wedge \neg f|_{x_1=1})$ also false
  • If exactly one $f$ term (w.l.o.g. $\neg f|_{x_1=0}$) is false then it is equivalent to $(x_1 \wedge \neg f|_{x_1=1})$

Therefore, both formulas $(\neg x_1 \wedge \neg f|_{x_1=0}) \vee (x_1 \wedge \neg f|_{x_1=1}) \vee (\neg f|_{x_1=0} \wedge \neg f|_{x_1=1})$ and $(\neg x_1 \wedge \neg f|_{x_1=0}) \vee (x_1 \wedge \neg f|_{x_1=1})$ are equivalent.

$\endgroup$
  • $\begingroup$ That the formula holds is easily verifiable as you show, but this does not answer the question of how it was derived in the first place, which would explain to some extent why it holds. $\endgroup$ – Dilip Sarwate Jul 3 '12 at 18:58

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.