# Compact representation for quantified boolean formula

I got black-box (too big to analyze) boolean formula f(...) with 3 sets of input arguments: $$x_1... x_i, y_1... y_j, z_1... z_k$$. And I want to find such values for x-arguments that for every y-arguments exist z-arguments witch satisfy formula: $$(x_1...x_i): \forall (y_1...y_j) \exists (z_1...z_k) f(x_1...x_i, y_1...y_j, z_1...z_k)$$

I want encode this quantified boolean formula to DIMACS cnf format and use SAT-solver to find such $$x_1...x_i$$ values.

I think its possible by iterating over all $$2^j$$ $$(y_1...y_j)$$ value substitutions (substitute true or false for every $$y$$), adding new set of z-arguments for each of them, substitute them to f(...) and joining them with conjunction: $$f(x_1...x_i, false...false, (z_1)_1...(z_1)_k) \land f(x_1...x_i, false...true, (z_2)_1...(z_2)_k) \land ... \land f(x_1...x_i, true...true, (z_{2^j})_1...(z_{2^j})_k)$$

Problem of that solution that it will generate exponential (dependent on count of y-arguments) large boolean formula with $$2^j$$ conjunctions and then require exponential time from size of this formula to solve SAT.

Is there a more compact way to reduce this formula to formula without quantifications? Or any other way with less complexity?

When substituted for $$(x_1, ..., x_i)$$ you have a formula in monadic predicate logic.

The monadic class is the class of first-order formulas without function symbols, with unary (monadic) predicates only, but with arbitrary quantification.

SAT for monadic predicate logic is NEXPTIME-complete in general

Altogether this means in particular that Monadic-Sat is complete for NEXPTIME.

with a lower bound

$$NTIME(c^{n/\log n})$$, for some (other) c > 0, is at the same time a lower bound for this problem

You'll therefore not be able to find a polynomial time reduction to SAT unless the time complexity hierarchy collapses.

Quotes from L. Bachmair, H. Ganzinger and U. Waldmann, "Set constraints are the monadic class," [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, 1993, pp. 75-83, doi: 10.1109/LICS.1993.287598.

• That answers practical part of problem. But I'm still interested to know - is there polinomial SPACE reduction? Jul 27 at 12:46
• @AlexeyKholodkov Yes, I think so, but it's not really interesting without time bounds. A NTM $M$ can compute the answer during the reduction and output a tautology if $\forall (y_1...y_j) \exists (z_1...z_k) f(x_1...x_i, y_1...y_j, z_1...z_k)$ and a falsum otherwise. All possible assignments for $y_1 ... y_j$ are countable. There are $2^j$ such assignments, which means we need $O(j)$ bits to store our 'iteration pointer'. For each assignment the NTM $M$ simulates another NTM deciding SAT that runs in polynomial space (which exists because $SAT \in NP \subseteq PSPACE$) on the formula. Jul 27 at 13:24

You can't. You have a QBF-SAT instance. That can't be efficiently resolved/reduced to SAT (given current conjectures in complexity theory). Instead, use a QBF-SAT solver on your formula.