3
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ That answers practical part of problem. But I'm still interested to know - is there polinomial SPACE reduction? $\endgroup$ Jul 27 at 12:46
  • $\begingroup$ @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. $\endgroup$
    – idmean
    Jul 27 at 13:24
1
$\begingroup$

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.

$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.