<p>Consider a quantified Boolean formula <span class="math-container">$f$</span>. We can convert it into Skolem Normal Form formula <span class="math-container">$f^*$</span> such that <span class="math-container">$f$</span> is satisfiable iff <span class="math-container">$f^*$</span> is satisfiable, by replacing variables that are existentially quantified with Skolem functions (that satisfy certain conditions).</p>
<p>It seems to me that <span class="math-container">$|f^*|$</span> can be exponentially larger than <span class="math-container">$|f|$</span>, but I'm struggling to find a good reference for that.</p>
<p>I see that in this question: <a href="https://cstheory.stackexchange.com/questions/38481/how-to-generate-skolem-function-in-practice">How to generate Skolem function in practice</a>,  the answer states that we don't need to compute the Skolem functions in practice, but I'm actually interested in computing them.</p>
<p>I don't know if my intuition is correct (about <span class="math-container">$|f^*|$</span> potentially having an exponential blow-up), but if it is, I'd be grateful if someone could point me towards such a reference.</p>
<p>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 <span class="math-container">$\Sigma_2^p$</span>--- (<span class="math-container">$\exists$</span> Skolem functions)(<span class="math-container">$\forall$</span> assignments)[formula is true].</p>

CC BY-SA 4.0
2022-09-29T18:16:13.060Z
How do you measure the size of the functions?
Emil Jeřábek
CC BY-SA 4.0
2022-09-29T18:47:20.977Z
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?
veryinteresting
CC BY-SA 4.0
2022-09-29T19:18:42.567Z
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.
Emil Jeřábek
CC BY-SA 4.0
2022-09-29T19:27:01.483Z
Interesting! Do you have a reference that I can consult to learn more about this?
veryinteresting
<reference-request><lo.logic><boolean-formulas>
Lower bound on the size of Skolem functions
veryinteresting
# Lower bound on the size of Skolem functions

(Asked by: username_0 on 2022-09-29)

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](https://cstheory.stackexchange.com/questions/38481/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].

**Tags:** reference-request, lo.logic, boolean-formulas

> **Comments:**
> **username_1**: How do you measure the size of the functions?  
> **username_0**: 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?  
> **username_1**: 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.  
> **username_0**: Interesting! Do you have a reference that I can consult to learn more about this?  

---

## 0 answers

