# A doubt on converting NOT gate to CNF formula

For a NOT gate if $$x_1$$ is input and $$x_2$$ is the corresponding output, I see the equivalent CNF (conjunctive normal form) is $$(x_1 \lor x_2) \land (\overline x_1 \lor \overline x_2)$$.

My expectations was that the CNF should not include $$x_2$$ as it is the output of the gate. I was rather hoping the formula to be of a form $$x_2=F(x_1, b_1, b_2, ...)$$ where $$b_1$$, $$b_2$$, .. are the boolean constants such that when $$x_1$$ is zero, the $$F(.,.,..)$$ would yield true just like the NOT gate.

Can anyone help me understand, how come this CNF including $$x_2$$ is equivalent to a NOT gate. How to draw a truth table for this CNF form as in what value to assign for $$x_2$$!

Your formula does actually look like $$x_2 = F(x_1)$$, it's just written with different symbols.

First, we can rewrite the two clauses using implication. Since $$(a \to b) \iff (\neg a \lor b)$$, we can rewrite the formula as

$$(\neg x_1 \to x_2) \land (x_2 \to\neg x_1)$$

Now, you can recognize that this is $$(a \to b) \land (b \to a)$$, which is to say $$a \iff b$$.

$$\iff$$ as a boolean operator behaves the same way as $$=$$; it evaluates to true when its left hand side and right hand side are the same. So your formula is equivalent to

$$x_2 \iff \neg x_1$$

Viewing this as a constraint (assuming $$x_1$$ can be treated as "fixed"), $$x_2$$ is fixed as $$x_2 := \neg x_1$$

• @ Curtis F - This definitely proves that the CNF formula is equivalent to NOT gate. However, my specific confusion is - supposes I've a CNF solver which upon receiving the CNF formula above confirms two sets of satisfying assignments ($x_1$=1, $x_2$=0) and ($x_1$=0, $x_2$=1). This means if I choose to use CNF SAT solver instead of solving NOT gate directly, I'll get two solutions, whereas direct solution will yield only $x_1$=0 as valid assignment. Put another way, typically in a Karp-reduction, we transform input x in a problem A to f(x) in B in polynomial time. Here what is f(x) here ? – KGhatak Aug 12 '19 at 12:45