Теорема Иммермана

Утверждение теоремы

NL = coNL

Доказательство

Решим задачу STNONCON (s-t non connectivity) на логарифмической памяти и покажем, что STNONCON ∈ NL.

нет пути из в в графе

Чтобы показать, что STNONCON входит в NL, можно придумать недетерминированый алгоритм, использующий [math]O(\log |G|)[/math] памяти, который проверяет достижима ли вершина [math]t[/math] из [math]s[/math].

Чтобы показать правильность работы алгоритма необходимо показать:

В случае недостижимости [math]t[/math] из [math]s[/math] недетерминированные выборы приводят алгоритм к допуску.
Если [math]t[/math] достижима из [math]s[/math], то вне зависимости от недетерминированных выборов, совершаемых алгоритмом, алгоритм не приходит к допуску.

Определим [math]R_i = \{v:[/math] существует путь из [math]s[/math] в [math]v[/math] длиной [math]\le i\}[/math]. Другими словами это множество всех вершин, достижимых из [math]s[/math] не более чем за [math]i[/math] шагов. Обозначим [math]|R_i|[/math] за [math]r_i[/math]. Заметим, что если [math]t \notin R_{n-1}[/math], где [math]n = |V|[/math], то не существует путь [math]s[/math] в [math]t[/math] в графе [math]G[/math], то есть [math]\lt G, s, t\gt [/math] ∈ STNONCON.

Лемма: Можно построить недетерминированный алгоритм, который будет принимать верно заданное [math]r_i[/math] (AAAA) и при этом будет перечислять все вершины из [math]R_i[/math] на [math]O(\log |G|)[/math] памяти.


 Enum(s, i, r_i, G)
   counter := 0                        //количество уже найденных и выведенных элементов
   for v = 1..n do         //перебираем все вершины графа
     continue or find path   //недетерминированно угадываем путь из s до v или переходим к следующей вершине
     counter++ 
     yield return v              //выдаем вершину, до которой угадали путь
     if counter ≥ r_i then //нашли r_i вершин, допускаем завершаем работу
       ACCEPT
   REJECT //не нашли r_i вершин, не допускаем

Enum перебирает все вершины на логарифмической памяти и пытается угадать путь до этой вершины из [math]s[/math]. Под угадыванием пути подразумевается последовательность недетерминированных выборов следующей вершины пути из [math]s[/math] в [math]v[/math]. Для угадывания пути необходимо [math]O(\log |G|)[/math] памяти, так как необходимо лишь хранить текущую и следующую угадываемую вершины угадываемого пути. Enum является недетерминированым алгоритмом, и если существует порядок его исполнения достигающий ACCEPT, то происходит допуск.

Теперь имея Enum, можно индуктивно находить [math]r_i[/math]. Очевидно, что [math]r_0 = 1[/math], так как [math]R_0[/math] содержит единственную вершину — [math]s[/math]. Пусть известно значение [math]r_i[/math]. Напишем программу, которая на логарифмической памяти будет находить [math]r_{i + 1}[/math].


 Next(s, i, r_i, G)
   r := 1 //r_i+1 хотя бы один, так как s ∈ R_i+1
   for v = 1..n; v ≠ s do //перебираем все вершины графа, кроме s — это кандидаты на попадание в R_i+1
     for u : (u,v) ∈ E do //перебираем все ребра, входящие в v
        //перечисляем все вершины из R_i
       if u in Enum(s, i, r_i, G) then //если u одна из них, то v ∈ R_i+1
         r++   //увеличиваем количество найденных вершин и переходим к рассмотрению следующего кандидата
         break
   return r

Данный алгоритм изначально учитывает [math]s[/math], а затем перебирает всех возможных кандидатов на попадание в [math]R_{i + 1}[/math]. Для каждого из них перебираются все ребра, в него входящие. Затем перечисляются все вершины из [math]R_i[/math] и, если начало нашего ребра было перечислено, то [math]v \in R_{i + 1}[/math]. Алгоритм использует [math]O(\log |G|)[/math] памяти, так необходимо хранить лишь [math]v[/math], [math]u[/math], [math]r[/math] и еще поочередно значения полученные в результате вызова Enum.

Теперь напишем алгоритм, который будет недетерминированно решать задачу STNONCON на логарифмической памяти. Он будет состоять из двух частей: вычисление [math]r_{n-1}[/math] и перечисление всех вершин из [math]R_{n - 1}[/math]. Вычисление [math]r_{n-1}[/math] происходит путем вызова Next [math]n - 1[/math] раз, при этом каждый раз в качестве [math]r_i[/math] подставляется новое полученное значение.


 NONCON(G, s, t)
   r_n := 1 //r₀
   for i = 0..(n - 2) do //Вычисляем r_n-1</tex>
     r_n := Next(s, i, r_n, G)
   //Перечисляем вершины из R_n-1
   if t in Enum(s, n - 1, r_n, G) then //Если t была перечислена, то t достижима и выдаем REJECT, иначе ACCEPT
     REJECT
   else
     ACCEPT

Данный алгоритм использует [math]O(\log |G|)[/math] памяти, так как для хранения [math]r_n[/math] и [math]i[/math] необходимо [math]2\log |G|[/math], а для вызываемых [math]\text{Next}[/math] и [math]\text{Enum}[/math] необходимо [math]O(\log |G|)[/math] памяти.

Таким образом показано, что STNONCON ∈ NL. Поскольку STNONCON ∈ coNLC, то получаем, что любую задачу из coNL можно свести к задаче из NL, а значит coNL ⊂ NL</tex>. Из соображений симметрии NL ⊂ coNL, а значит NL = coNL.

Теорема Иммермана