# Lower bound on the size of Skolem functions

Consider a quantified Boolean formula $$f$$. We can convert it into Skolem Normal Form formula $$f^*$$ such that $$f$$ is satisfiable iff $$f^*$$ is satisfiable, by replacing variables that are existentially quantified with Skolem functions (that satisfy certain conditions).

It seems to me that $$|f^*|$$ can be exponentially larger than $$|f|$$, but I'm struggling to find a good reference for that.

I see that in this question: How to generate Skolem function in practice, the answer states that we don't need to compute the Skolem functions in practice, but I'm actually interested in computing them.

I don't know if my intuition is correct (about $$|f^*|$$ potentially having an exponential blow-up), but if it is, I'd be grateful if someone could point me towards such a reference.

Edit: My intuition stems from the fact that if there were a polynomial upper bound on those Skolem functions, then that would put QBF in $$\Sigma_2^p$$--- ($$\exists$$ Skolem functions)($$\forall$$ assignments)[formula is true].

• How do you measure the size of the functions? Sep 29 at 18:16
• Good question. I'm not sure. I was trying to think about this in the general case. Obviously, using truth tables won't do. Perhaps just viewing the Skolem functions as Boolean formulas? Sep 29 at 18:47
• Since the Skolem functions are computable in PSPACE, even a superpolynomial lower bound on them would imply that PSPACE is not included in nonuniform $\mathrm{NC}^1$ (in fact, this is equivalent). We do not know how to prove unconditionally such separations using the current state of art. Sep 29 at 19:18