211
правок
Изменения
м
Нет описания правки
Так как функция <tex>f</tex> работает полиномиальное время, и <tex>|\phi|=|y|</tex>, то <tex>f(\langle\phi,y\rangle) \le q(|\phi|)</tex>, где <tex>q</tex> — полином.
<tex>S\in SPARSE</tex>. Следовательно <tex>\forall n |S \cap \Sigma^n|\le p(n)</tex>, где <tex>p</tex> — некоторый полином. Тогда <tex>|\{x\in S\, |\, |x| \le q(|\phi|)\}| \le \sum\limits_{i=1}^{q(|\phi|)} p(i) = r(|\phi|)</tex>, где <tex>r</tex> — также полином.
Опишем алгоритм для нахождения лексиграфически минимальной строки <tex>x</tex>, удовлетворяющей формулу <tex>\phi</tex>.
# <tex>z_i \ne z_j \, \forall i \ne j</tex>. Как было показано выше, если <tex>w_0</tex> или <tex>w_1</tex> лежат в <tex>S</tex>, то все последующие <tex>w_i</tex> тоже лежат в <tex>S</tex>, но тогда <tex>S</tex> содержит не менее <tex>r+1</tex> строку длины не более, чем <tex>q(|\phi|)</tex>, что противоречит условию <tex>|\{x\in S\, |\, |x| \le q(|\phi|)\}| \le r(|\phi|)</tex>. Следовательно <tex>x\notin[w_0,w_1]</tex>, то есть его можно убрать из рассмотрения.
В обоих случаях мы сузили область поиска как минимум на <tex>\frac 1{r+1}</tex> её размера. Будем повторять эту процедуру до тех пор, пока не останется не более <tex>r+1</tex> строкстроки, которые мы можем проверить за полиномиальное время. Если какая-то из них удовлетворила формулу <tex>\phi</tex>, то <tex>x=min(w_i), w_i</tex> удовлетворяет <tex>\phi</tex>. Иначе, <tex>x</tex> не существует.
Оценим время работы нашего алгоритма. После <tex>k</tex> итераций у нас останется не более <tex>2^n(1-\frac1{r+1})^k</tex> строк. Оценим <tex>k</tex>.
