[Solved]: Formulas for which any equivalent CNF formula has exponential length

Problem Detail: 

I read a claim that

there are formulas for which any equivalent CNF has exponential length.

Can you show me an example for such a boolean formula? I have been trying to build it myself and failed.

Asked By : Ilya_Gazman

Answered By : Realz Slaw

There might be a difference between equivalence and equisatisfiability that you are getting caught up on.

If you want an example where an equivalent conversion into CNF has an exponential growth, see wikipedia on Conjunctive normal form: Conversion into CNF:

$$(X_1 \wedge Y_1) \vee (X_2 \wedge Y_2) \vee \dots \vee (X_n \wedge Y_n).$$

This formula leads to exponential length CNF formulas, if the conversion must be equivalent.

The article continues on about how by introducing new variables, one can obtain an equisatisfiable formula that grows only linearly. These types of conversions usually create new models that contain the old model, so while the new formula is not equivalent, a satisfying assignment to the new formula will directly give a satisfying assignment to the old formula.

Though, there might be conversions that do not contain the old model, I've not seen one. As a side-note, Boolean satisfiabilty is self-reducible, which means that an algorithm that solves the decision problem, can be used to solve the optimization problem, via forcing one variable, and repeated calls to the solver. This means that even if you have a conversion that generates another, equisatisfiable formula, but for which the models are very different, you can find the satisfying assignment of the original formula (in time bounded by a polynomial of the runtime of the solver).

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/18409