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

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

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

NL = coNL

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

Решим задачу STNONCON на логарифмической памяти.

[math]\text{STNONCON}=\{\langle G=\langle V,E\rangle,s,t\rangle\colon [/math] нет пути из [math]s[/math] в [math]t[/math] в графе [math]G\}.[/math]

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

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

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

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

Лемма: Можно построить алгоритм, который по данному r_i будет перечислять все вершины из R_i и удачно завершаться на логарифмической памяти. Если r_i больше истинного размера R_i, то алгоритм завершится неудачно; однако если r_i меньше истинного размера R_i, то алгоритм завершится удачно, но перечислит лишь некое подмножество R_i.

Enum(s, i, r_i, G)

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

Enum перебирает все вершины на логарифмической памяти и пытается угадать путь до этой вершины из s.