4
$\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?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ That answers practical part of problem. But I'm still interested to know - is there polinomial SPACE reduction? $\endgroup$
    – Alexey Kholodkov
    Jul 27, 2021 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, 2021 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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ This should be a comment, not an answer. Please see the rules for more info $\endgroup$
    – user137116
    Apr 9, 2022 at 10:58

Your Answer

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

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