3
$\begingroup$

Maybe this is not enough research level, but I've been scratching my head on it for a while...

I'm interested in the Shannon expansion of an existentially quantified Boolean formula of the form:

$$ \exists \bar x\, \phi(\bar x,\bar y) $$

where $\phi(\bar x)$ is quantifier-free and $\bar x$ is a vector of potentially many variables. I need an equivalent quantifier-free formula over $\bar y$, so I apply Shannon expansion. For example, for a single $x$:

$$ \exists x \phi(x, \bar y) \equiv \phi(\top, \bar y) \lor \phi(\bot, \bar y) $$

But, if the number of quantified variables is large, this is exponential of course in the worst case.

Now, in practical uses, one can hope that the disjuncts can be simplified enough at each step so that the result is not too big. But still, doing it is quite a lot of work, computationally.

So, the meta-question is:

  • is there a more clever way than just doing Shannon expansion by hand and simplifying the formula consequently?

For example, I thought about using QBF solvers.

When given a QBF formula of the form:

$$ \forall \bar y \, \exists \bar x \, \phi(\bar x, \bar y) $$

if the formula is true, a certifying QBF solver can produce the corresponding Skolem functions for the variables in $\bar x$. This is not what I need though, because I cannot assume the formula to be true.

What I'd need, instead, is to somehow give the formula $\exists \bar x\,\phi(\bar x, \bar y)$ to the QBF solver, and ask it to search for a formula equivalent to its Shannon expansion.

The only thing I can come up with is the following:

$$ \forall \bar y\,\exists r\bigl( r \leftrightarrow \exists \bar x \,\phi(\bar x, \bar y)\bigr) $$

with this, the Skolem function for $r$ should give me exactly the Boolean formula equivalent to $\exists\bar x\, \phi(\bar x, \bar y)$.

But, this formula is $\Pi^P_2$, and it sounds too expensive to me. I would expect something so "simple", conceptually, to be doable with less alternation.

So the question is twofold:

  • Is the above approach correct, and is there a faster way?
  • Also, is this worth it at all, or will I always get the same performance (in terms of time, or in terms of size of the result) that I could obtain by manually computing the Shannon expansion?

P.S.: I noticed there is no qbf tag, so I'm tagging this as sat.

$\endgroup$

0

Your Answer

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

Browse other questions tagged or ask your own question.