= Solution
An exponential increase is unavoidable for an equivalent <conjunctive normal form> over the original variables. Consider the linear-size <Boolean formula>
$$
F_n=\bigvee_{i=1}^{n}(p_i\land q_i).
$$
Distributing gives the $2^n$ <Boolean clauses>
$$
F_n\equiv\bigwedge_{(r_1,\ldots,r_n)\in\{p_1,q_1\}\times\cdots\times\{p_n,q_n\}}(r_1\lor\cdots\lor r_n).
$$
To prove that the growth is necessary, fix one choice $r_i\in\{p_i,q_i\}$. Let $\alpha_r$ make every $r_i$ false and its partner true. Each pair then contains a false variable, so $F_n$ is false. Any equivalent <conjunctive normal form> must contain a <Boolean clause> $C$ falsified by $\alpha_r$ and entailed by $F_n$.
Every individual term $p_i\land q_i$ entails $C$, because that term implies $F_n$. After tautological <Boolean clauses> are discarded, this forces $C$ to contain a positive $p_i$ or positive $q_i$ for every $i$: otherwise set both variables in that pair true and independently falsify all <Boolean literals> of $C$, contradicting the entailment. Since $C$ is false at $\alpha_r$, it must contain the false member $r_i$, never its true partner. Consequently the same $C$ cannot be false at any different $\alpha_s$. The $2^n$ different assignments therefore require at least $2^n$ different <Boolean clauses>.
Writing the answer already takes $\boxed{\Omega(2^n)\text{ time in the worst case}}$. This obstruction applies to <first-order logic> as well, since the example can be expressed using ground unary <atomic formulas>. It concerns exact equivalence without auxiliary symbols. A <Tseytin transformation> can produce a polynomial-size equisatisfiable <conjunctive normal form> with auxiliary variables, so the statement must not be extended to that different task.
Back to article page
