I'm wondering if there are any references on "reverse skolemization", that is, converting a formula with functions into one purely consisting of quantifiers by eliminating function applications.

I'm working in a boolean domain, and my end goal is to make something that can be solved by a QSAT solver.

For example, if I have a formula $\phi$ like this:

$\exists f : \mathbb{B}^n \to \mathbb{B}^n \ldotp \exists g : \mathbb{B}^n \to \mathbb{B} \ldotp \forall x : \mathbb{B}^n \ldotp g(x) \implies g(f(x)) $

I want to be able to convert it into an equi-satisfiable formula that quantifies over booleans, not functions, i.e. a formula whose skolemization is $\phi$.

Is this possible, and if so, are there any references for how to do this algorithmically in the general case?

  • 3
    $\begingroup$ You can obviously replace a quantifier over $f\colon\{0,1\}^n\to\{0,1\}^m$ by $m2^n$ Boolean quantifiers specifying the truth-table of $f$. This will give an exponentially larger formula. I’m pretty sure this is best possible in general, as the problem should be complete for alternating exponential time with polynomially many alternations, or something like that. $\endgroup$ – Emil Jeřábek Jul 8 '19 at 6:13
  • 3
    $\begingroup$ In fact, already the special case of sentences of the form $\exists f\colon\mathbb B^n\to\mathbb B\,\forall x_1,\dots,x_m\in\mathbb B\,\phi(f,\vec x)$ with $\phi$ quantifier-free, is NEXP-complete to evaluate, hence it should not have any subexponential reduction to a PSPACE-complete problem like QSAT. $\endgroup$ – Emil Jeřábek Jul 8 '19 at 7:17
  • 2
    $\begingroup$ I guess there are various variants of such results appearing in the literature. The specific result abount NEXP-completeness of sentences of the form $\exists f\colon\mathbb B^n\to\mathbb B\,\forall x_1,\dots,x_m\in\mathbb B\,\phi(f,\vec x)$ with quantifier-free $\phi$ is a restatement of Lemma 3.1 in my paper “Complexity of admissible rules” (note that quantification over $X\in\mathcal{P(P(}[n]))$ is the same as quantification over $\mathbb B^n\to\mathbb B$, and likewise, quantification over $a\in\mathcal P([n])$ is equivalent to quantification over $\mathbb B^n$). More generally, ... $\endgroup$ – Emil Jeřábek Jul 9 '19 at 13:49
  • 1
    $\begingroup$ Just a note: the reverse of skolemization is trivially possible if each function symbol is used only once, in which case you can replace the application of the function with a quantifier. $\endgroup$ – gigabytes Jul 10 '19 at 6:13
  • 1
    $\begingroup$ When Skolemizing we never get "nested" Skolem functions - so your example can't occur because of the "$g(f(-))$" bit. Indeed, plenty of sentences of this form aren't equivalent to first-order sentences at all - see e.g. this old MSE question. $\endgroup$ – Noah Schweber Jul 12 '19 at 22:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.