Теорема Иммермана — различия между версиями
Akhi (обсуждение | вклад) |
Akhi (обсуждение | вклад) |
||
Строка 9: | Строка 9: | ||
:<tex>\text{STNONCON}=\{\langle G=\langle V,E\rangle,s,t\rangle\colon </tex> нет пути из <tex>s</tex> в <tex>t</tex> в графе <tex>G\}</tex> | :<tex>\text{STNONCON}=\{\langle G=\langle V,E\rangle,s,t\rangle\colon </tex> нет пути из <tex>s</tex> в <tex>t</tex> в графе <tex>G\}</tex> | ||
− | Чтобы показать, что '''STNONCON''' входит в '''NL''', | + | Чтобы показать, что '''STNONCON''' входит в '''NL''', придумаем недетерминированый алгоритм, использующий <tex>O(\log |G|)</tex> памяти, который |
проверяет достижима ли вершина <tex>t</tex> из <tex>s</tex>. | проверяет достижима ли вершина <tex>t</tex> из <tex>s</tex>. | ||
− | Чтобы показать правильность работы алгоритма | + | Чтобы показать правильность работы алгоритма требуется: |
*В случае недостижимости <tex>t</tex> из <tex>s</tex> недетерминированные выборы приводят алгоритм к допуску. | *В случае недостижимости <tex>t</tex> из <tex>s</tex> недетерминированные выборы приводят алгоритм к допуску. | ||
*Если <tex>t</tex> достижима из <tex>s</tex>, то вне зависимости от недетерминированных выборов, совершаемых алгоритмом, алгоритм не приходит к допуску. | *Если <tex>t</tex> достижима из <tex>s</tex>, то вне зависимости от недетерминированных выборов, совершаемых алгоритмом, алгоритм не приходит к допуску. | ||
− | Определим <tex>R_i = | + | Определим <tex>R_i</tex> = {<tex>v:</tex> существует путь из <tex>s</tex> в <tex>v</tex> длиной ≤ <tex>i</tex>}. |
− | достижимых из <tex>s</tex> не более чем за <tex>i</tex> шагов. Обозначим <tex>|R_i|</tex> за <tex>r_i</tex>. | + | Другими словами это множество всех вершин, достижимых из <tex>s</tex> не более чем за <tex>i</tex> шагов. |
− | Заметим, что если <tex>t \notin R_{n-1}</tex>, где <tex>n = |V|</tex>, то не существует путь <tex>s</tex> в <tex>t</tex> в графе <tex>G</tex>, | + | Обозначим <tex>|R_i|</tex> за <tex>r_i</tex>. |
− | то есть <tex><G, s, t></tex> ∈ '''STNONCON'''. | + | Заметим, что если <tex>t \notin R_{n-1}</tex>, где <tex>n = |V|</tex>, то не существует путь <tex>s</tex> в <tex>t</tex> в графе <tex>G</tex>, то есть <tex><G, s, t></tex> ∈ '''STNONCON'''. |
− | '''Лемма''': Можно построить недетерминированный алгоритм, который будет | + | '''Лемма''': Можно построить недетерминированный алгоритм, который будет допускать <tex>r_i</tex> и при этом будет перечислять все вершины из <tex>R_i</tex> на <tex>O(\log |G|)</tex> памяти. |
<code> | <code> | ||
Enum(s, i, r<sub>i</sub>, G) | Enum(s, i, r<sub>i</sub>, G) | ||
− | counter := 0 | + | counter := 0 //''количество уже найденных и выведенных элементов'' |
− | '''for''' v = 1..n '''do''' | + | '''for''' v = 1..n '''do''' //''перебираем все вершины графа'' |
− | '''continue''' or ''find path'' | + | '''continue''' or ''find path'' //''недетерминированно угадываем путь из s до v или переходим к следующей вершине'' |
− | counter++ | + | counter++ |
− | '''yield return''' v | + | '''yield return''' v //''выдаем вершину, до которой угадали путь'' |
− | '''if''' counter ≥ r<sub>i</sub> '''then''' //''нашли r<sub>i</sub> вершин, допускаем завершаем работу'' | + | '''if''' counter ≥ r<sub>i</sub> '''then''' //''нашли r<sub>i</sub> вершин, допускаем завершаем работу'' |
'''ACCEPT''' | '''ACCEPT''' | ||
− | '''REJECT''' //''не нашли r<sub>i</sub> вершин, не допускаем'' | + | '''REJECT''' //''не нашли r<sub>i</sub> вершин, не допускаем'' |
</code> | </code> | ||
Строка 48: | Строка 48: | ||
<code> | <code> | ||
Next(s, i, r<sub>i</sub>, G) | Next(s, i, r<sub>i</sub>, G) | ||
− | r := 1 //''r<sub>i+1</sub> хотя бы один, так как s ∈ R<sub>i+1</sub>'' | + | r := 1 //''r<sub>i+1</sub> хотя бы один, так как s ∈ R<sub>i+1</sub>'' |
− | '''for''' v = 1..n; v ≠ s '''do''' //''перебираем все вершины графа, кроме s — это кандидаты на попадание в R<sub>i+1</sub>'' | + | '''for''' v = 1..n; v ≠ s '''do''' //''перебираем все вершины графа, кроме s — это кандидаты на попадание в R<sub>i+1</sub>'' |
− | '''for''' u : (u,v) ∈ E '''do''' //''перебираем все ребра, входящие в v'' | + | '''for''' u : (u,v) ∈ E '''do''' //''перебираем все ребра, входящие в v'' |
− | + | //''перечисляем все вершины из R<sub>i</sub>'' | |
− | '''if''' u '''in''' Enum(s, i, r<sub>i</sub>, G) '''then''' //''если u одна из них, то v ∈ R<sub>i+1</sub>'' | + | '''if''' u '''in''' Enum(s, i, r<sub>i</sub>, G) '''then''' //''если u одна из них, то v ∈ R<sub>i+1</sub>'' |
− | r++ | + | r++ //''увеличиваем количество найденных вершин и переходим к рассмотрению следующего кандидата'' |
− | '''break''' | + | '''break''' |
'''return''' r | '''return''' r | ||
</code> | </code> | ||
− | Данный алгоритм изначально учитывает <tex>s</tex>, а затем перебирает всех возможных кандидатов на попадание в <tex>R_{i + 1}</tex>. | + | Данный алгоритм изначально учитывает <tex>s</tex>, а затем перебирает всех возможных кандидатов <tex>v</tex> на попадание в <tex>R_{i + 1}</tex>. |
Для каждого из них перебираются все ребра, в него входящие. | Для каждого из них перебираются все ребра, в него входящие. | ||
Затем перечисляются все вершины из <tex>R_i</tex> и, если начало нашего ребра было перечислено, то <tex>v \in R_{i + 1}</tex>. | Затем перечисляются все вершины из <tex>R_i</tex> и, если начало нашего ребра было перечислено, то <tex>v \in R_{i + 1}</tex>. | ||
Строка 69: | Строка 69: | ||
<code> | <code> | ||
NONCON(G, s, t) | NONCON(G, s, t) | ||
− | r<sub>n</sub> := 1 //''r<sub>0</sub>'' | + | r<sub>n</sub> := 1 //''r<sub>0</sub> = 1'' |
− | '''for''' i = 0..(n - 2) '''do''' //''Вычисляем r<sub>n-1</sub | + | '''for''' i = 0..(n - 2) '''do''' //''Вычисляем r<sub>n-1</sub>'' |
r<sub>n</sub> := Next(s, i, r<sub>n</sub>, G) | r<sub>n</sub> := Next(s, i, r<sub>n</sub>, G) | ||
− | + | //''Перечисляем вершины из R<sub>n-1</sub>'' | |
− | '''if''' t in Enum(s, n - 1, r<sub>n</sub>, G) '''then''' //''Если t была перечислена, то t достижима и выдаем REJECT, иначе ACCEPT'' | + | '''if''' t in Enum(s, n - 1, r<sub>n</sub>, G) '''then''' //''Если t была перечислена, то t достижима и выдаем REJECT, иначе ACCEPT'' |
'''REJECT''' | '''REJECT''' | ||
'''else''' | '''else''' | ||
Строка 79: | Строка 79: | ||
</code> | </code> | ||
− | Данный алгоритм использует <tex>O(\log |G|)</tex> памяти, так как для хранения <tex>r_n</tex> и <tex>i</tex> необходимо <tex> | + | Данный алгоритм использует <tex>O(\log |G|)</tex> памяти, так как для хранения <tex>r_n</tex> и <tex>i</tex> необходимо <tex>O(\log |G|)</tex>, |
+ | и для вызываемых <code>Next</code> и <code>Enum</code> необходимо <tex>O(\log |G|)</tex> памяти. | ||
Таким образом показано, что '''STNONCON''' ∈ '''NL'''. | Таким образом показано, что '''STNONCON''' ∈ '''NL'''. | ||
Поскольку '''STNONCON''' ∈ '''coNLC''', то получаем, что любую задачу из '''coNL''' можно свести к задаче из '''NL''', а значит '''coNL''' ⊂ '''NL'''</tex>. | Поскольку '''STNONCON''' ∈ '''coNLC''', то получаем, что любую задачу из '''coNL''' можно свести к задаче из '''NL''', а значит '''coNL''' ⊂ '''NL'''</tex>. | ||
Из соображений симметрии '''NL''' ⊂ '''coNL''', а значит '''NL''' = '''coNL'''. | Из соображений симметрии '''NL''' ⊂ '''coNL''', а значит '''NL''' = '''coNL'''. |
Версия 18:43, 15 апреля 2010
Теорема Иммермана
Утверждение теоремы
NL = coNL
Доказательство
Решим задачу STNONCON (s-t non connectivity) на логарифмической памяти и покажем, что STNONCON ∈ NL.
- нет пути из в в графе
Чтобы показать, что STNONCON входит в NL, придумаем недетерминированый алгоритм, использующий
памяти, который проверяет достижима ли вершина из .Чтобы показать правильность работы алгоритма требуется:
- В случае недостижимости из недетерминированные выборы приводят алгоритм к допуску.
- Если достижима из , то вне зависимости от недетерминированных выборов, совершаемых алгоритмом, алгоритм не приходит к допуску.
Определим
= { существует путь из в длиной ≤ }. Другими словами это множество всех вершин, достижимых из не более чем за шагов. Обозначим за . Заметим, что если , где , то не существует путь в в графе , то есть ∈ STNONCON.Лемма: Можно построить недетерминированный алгоритм, который будет допускать
и при этом будет перечислять все вершины из на памяти.
Enum(s, i, ri, G) counter := 0 //количество уже найденных и выведенных элементов for v = 1..n do //перебираем все вершины графа continue or find path //недетерминированно угадываем путь из s до v или переходим к следующей вершине counter++ yield return v //выдаем вершину, до которой угадали путь if counter ≥ ri then //нашли ri вершин, допускаем завершаем работу ACCEPT REJECT //не нашли ri вершин, не допускаем
Enum
перебирает все вершины на логарифмической памяти и пытается угадать путь до этой вершины из .
Под угадыванием пути подразумевается последовательность недетерминированных выборов следующей вершины пути из в .
Для угадывания пути необходимо памяти, так как необходимо лишь хранить текущую и следующую угадываемую вершины угадываемого пути.
Enum
является недетерминированым алгоритмом, и если существует порядок его исполнения достигающий ACCEPT
, то происходит допуск.
Теперь имея Enum
, можно индуктивно находить .
Очевидно, что , так как содержит единственную вершину — .
Пусть известно значение .
Напишем программу, которая на логарифмической памяти будет находить .
Next(s, i, ri, G) r := 1 //ri+1 хотя бы один, так как s ∈ Ri+1 for v = 1..n; v ≠ s do //перебираем все вершины графа, кроме s — это кандидаты на попадание в Ri+1 for u : (u,v) ∈ E do //перебираем все ребра, входящие в v //перечисляем все вершины из Ri if u in Enum(s, i, ri, G) then //если u одна из них, то v ∈ Ri+1 r++ //увеличиваем количество найденных вершин и переходим к рассмотрению следующего кандидата break return r
Данный алгоритм изначально учитывает Enum
.
Теперь напишем алгоритм, который будет недетерминированно решать задачу STNONCON на логарифмической памяти.
Он будет состоять из двух частей: вычисление Next
раз, при этом каждый раз в качестве подставляется новое полученное значение.
NONCON(G, s, t) rn := 1 //r0 = 1 for i = 0..(n - 2) do //Вычисляем rn-1 rn := Next(s, i, rn, G) //Перечисляем вершины из Rn-1 if t in Enum(s, n - 1, rn, G) then //Если t была перечислена, то t достижима и выдаем REJECT, иначе ACCEPT REJECT else ACCEPT
Данный алгоритм использует Next
и Enum
необходимо памяти.
Таким образом показано, что STNONCON ∈ NL. Поскольку STNONCON ∈ coNLC, то получаем, что любую задачу из coNL можно свести к задаче из NL, а значит coNL ⊂ NL</tex>. Из соображений симметрии NL ⊂ coNL, а значит NL = coNL.