PS-полнота языка верных булевых формул с кванторами (TQBF)

Материал из Викиконспекты
Перейти к: навигация, поиск
Определение:
[math]TQBF[/math] расшивровывается как True Quantified Boolean Formula. Это язык верных булевых формул с кванторами. [math]TQBF=\{Q_1 x_1 Q_2 x_2 \cdots Q_n x_n \phi(x_1, x_2, \dots, x_n), Q_i \in \{\forall, \exists\}\}[/math]

Чтобы доказать, что [math]TQBF \in PSPACE-complete[/math] необходимо показать что:

Лемма (1):
[math]TQBF \in PSPACSE[/math]
Доказательство:
[math]\triangleright[/math]

Чтобы доказать это просто приведём программу, которая требует [math]O(n)[/math] дополнительной памяти и работает за конечное время.

[math]solve(Q_1 x_1 Q_2 x_2 \cdots Q_n x_n \phi(x_1, x_2, \dots, x_n))[/math]
    if [math]Q_1 == \forall[/math]
        return [math]solve(Q_2 x_2 \cdots Q_n x_n \phi(0, x_2, \dots, x_n)) \land solve(Q_2 x_2 \cdots Q_n x_n \phi(1, x_2, \dots, x_n))[/math]
    if [math]Q_1 == \exists[/math]
        return [math]solve(Q_2 x_2 \cdots Q_n x_n \phi(0, x_2, \dots, x_n)) \lor solve(Q_2 x_2 \cdots Q_n x_n \phi(1, x_2, \dots, x_n))[/math]
Эта программа требует [math]O(n)[/math] дополнительной памяти для хранения стека рекурсивных вызовов. Максимальная глубина стека — [math]n[/math]
[math]\triangleleft[/math]
Лемма (2):
[math] \forall L \in PS \Rightarrow L \leq_p TQBF[/math]
Доказательство:
[math]\triangleright[/math]
Рассмотрим какой-то язык [math]L \in PSPACE[/math]. Построим такую функцию [math]f : \forall x \in L \Leftrightarrow f(x) \in TQBF[/math]
[math]\triangleleft[/math]