Timeline for Compact representation for quantified boolean formula
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 30, 2021 at 15:48 | vote | accept | Alexey Kholodkov | ||
| Jul 27, 2021 at 13:24 | comment | added | idmean | @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, 2021 at 12:46 | comment | added | Alexey Kholodkov | That answers practical part of problem. But I'm still interested to know - is there polinomial SPACE reduction? | |
| Jul 27, 2021 at 6:26 | history | answered | idmean | CC BY-SA 4.0 |