From the link Solving SAT by converting to disjunctive normal form, I learnt that the algorithm to transform any boolean formula to disjunctive form takes exponential time in worst case.
But I have a question that for unsatisfiable boolean formulas, does it also take exponential time to transform them into disjunctive form?
More specifically, for 3CNF unsatisfiable boolean formulas, does it take exponential time to transform them into disjunctive form？
For 3CNF unsatisfiable boolean formulas, does it take exponential time to transform them into disjunctive form？
For unsatisfiable formulas, the answer is trivially no -- in fact it takes constant time. Output any disjunctive unsatisfiable formula, like $(p \land \lnot p)$.
It is possible to fix your question so that it's not trivially answered, but that does require some more effort. We could ask: is there an algorithm that takes as input a 3CNF boolean formula, and outputs a disjunctive normal form, such that for unsatisfiable inputs, the algorithm takes sub-exponential time (but it is allowed to take exponential or longer time on the satisfiable inputs)? To this question, D.W.'s answer applies.
We don't know. If P=NP, then no, it doesn't take exponential time. If P$\ne$NP, then it cannot be done in polynomial time (but we don't know whether it requires exponential time). If the Exponential Time Hypothesis holds, it requires exponential time.
The procedure in your reference still holds for unsatisfiable instances; it's just that each clause produced by that procedure will have a pair of opposite literals $... \land a \land \neg a$.
The minimized disjunctive normal form of an unsatisfiable problem (the set after removing subsumptions and contradictions) is the set $\emptyset$ with no clauses. As the interpretation of DNF is that each clause be disjoined, you end up with an empty disjunction, which is vacuously false.
To be clear, it is possible to convert the formula to DNF in polynomial time an an approach akin to the Tseitin trasnformation, but the quantification of the Tseitin variables would have to be universal instead of existential, so it would no longer be a SAT problem.
