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$ Commented 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$ Commented 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$ Commented Apr 9, 2022 at 10:58

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.