Изменения
Нет описания правки
<tex>S\in \mathrm{SPARSE}</tex>, следовательно <tex>\forall n \; |S \cap \Sigma^n|\leqslant p(n)</tex>, где <tex>p</tex> — некоторый полином.
Тогда <tex>|\{x\in S \mid |x| \leqslant q(|\varphi|)\}| = \displaystyle\sum\limits_{i=1}^{q(|\varphi|)}|S \cap \Sigma^i| \leqslant \displaystyle\sum\limits_{i=1}^{q(|\varphi|)} p(i) = r(|\varphi|)</tex>, где <tex>r</tex> — также полином.
Опишем алгоритм для нахождения лексикографически минимальной строки <tex>x</tex>, удовлетворяющей формуле <tex>\varphi</tex>.
Пусть <tex>n=|\varphi|, r=r(|\varphi|)</tex>. Изначально область поиска для <tex>x</tex> — все строки длины <tex>n</tex>. Опишем одну итерацию поиска.
Разобьём текущее множество строк на <tex>r+1</tex> подотрезок примерно равной длины. Обозначим концы полученных подотрезков <tex>w_0, \ldots ,w_{r+1}</tex>. И <tex>w_0 < w_1 < \ldots < w_{r+1}</tex>. Пусть теперь <tex>z_i=f(\langle\varphi,w_i\rangle)</tex>.
Из леммы (2) мы знаем, что, начиная с некоторого <tex>l</tex>, все пары <tex>\langle\varphi, w_l\rangle \in \mathrm{LSAT}</tex>. Тогда по сведению <tex>z_j \in S</tex> для всех <tex>j\geqslant l</tex>.
Рассмотрим два случая:
# <tex>\exists i \ne j : z_i=z_j</tex> для некоторого <tex> j > i </tex>. Строки <tex>z_i</tex> и <tex>z_j</tex> либо обе лежат в <tex>S</tex>, либо обе не лежат в <tex>S</tex>. Если <tex>z_i, z_j \in S</tex>, то по сведению <tex> \langle \varphi, w_i \rangle, \langle \varphi, w_j \rangle \in \mathrm{LSAT}</tex>, то есть получаем <tex> x \leqslant w_i < w_j </tex>. Тогда по вышеуказанной причине <tex>x\notin (w_i, w_j]</tex>. Значит мы можем исключить этот полуинтервал из рассматриваемого множества. Таким образом, мы удаляем не менее <tex>\dfrac 1{r+1}</tex> часть множества подстановок.
# <tex>z_i \ne z_j \, \forall i \ne j</tex>. Как было показано выше, если <tex>x \in [w_0, w_1]</tex>, то все <tex>z_i</tex>, начиная с <tex>z_1</tex>, лежат в <tex>S</tex>, но тогда <tex>S</tex> содержит <tex>r+1</tex> строку длины не более, чем <tex>q(|\varphi|)</tex>, что противоречит условию <tex>|\{x\in S \mid |x| \leqslant q(|\varphi|)\}| \leqslant r(|\varphi|)</tex>. Следовательно, <tex>x\notin[w_0,w_1]</tex>, то есть его можно убрать из рассмотрения.
