# 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? Commented Sep 29, 2022 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? Commented Sep 29, 2022 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. Commented Sep 29, 2022 at 19:18