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].

  • $\begingroup$ How do you measure the size of the functions? $\endgroup$ Sep 29, 2022 at 18:16
  • $\begingroup$ 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? $\endgroup$ Sep 29, 2022 at 18:47
  • 4
    $\begingroup$ 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. $\endgroup$ Sep 29, 2022 at 19:18
  • $\begingroup$ Interesting! Do you have a reference that I can consult to learn more about this? $\endgroup$ Sep 29, 2022 at 19:27


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.