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

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

NL = co-NL

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

Решим задачу 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[/math] = {[math]v:[/math] существует путь из [math]s[/math] в [math]v[/math] длиной ≤ [math]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] и при этом будет перечислять все вершины из [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
       if u in Enum(s, i, r_i, G) then   //перечисляем все вершины из R_i, если u одна из них, то v ∈ R_i+1
         r++                            //увеличиваем количество найденных вершин и переходим к рассмотрению следующего кандидата
         break 
   return r

Данный алгоритм изначально учитывает [math]s[/math], а затем перебирает всех возможных кандидатов [math]v[/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 (n - 1) раз, при этом каждый раз в качестве [math]r_i[/math] подставляется новое полученное значение.

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

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

Таким образом показано, что STNONCON ∈ NL. Поскольку STNONCON ∈ co-NLC, то получаем, что любую задачу из co-NL можно свести к задаче из NL, а значит co-NL ⊂ NL. Из соображений симметрии NL ⊂ co-NL, а значит NL = co-NL.

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