Problem Detail: 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 displaystyleneg 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?
Asked By : kafka
Answered By : Marc Bury
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.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/2595 Ask a Question Download Related Notes/Documents
