Теорема Иммермана — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 5: Строка 5:
  
 
=== Доказательство ===
 
=== Доказательство ===
Решим задачу STNONCON на логарифмической памяти.
+
Решим задачу STNONCON на логарифмической памяти и покажем, что STNONCON ∈ NL.
  
 
:<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>
Строка 36: Строка 36:
 
</code>
 
</code>
  
Enum перебирает все вершины на логарифмической памяти и пытается угадать путь до этой вершины из ''s''. Для угадывания пути достаточно логарифмической памяти, так как необходимо помнить лишь текущую вершину пути и пытаться угадывать следующую. Enum является недетерминированой программой и если существует порядок исполнения, чтобы достичь ACCEPT, то он достигается.
+
Enum перебирает все вершины на логарифмической памяти и пытается угадать путь до этой вершины из ''s''. Для угадывания пути достаточно <tex>O(\log |G|)</tex> памяти, так как необходимо помнить лишь текущую вершину пути и пытаться угадывать следующую. Enum является недетерминированой программой и если существует порядок исполнения, чтобы достичь ACCEPT, то он достигается.
  
 
Теперь имея Enum, можно индуктивно находить ''r<sub>i</sub>''. Очевидно, что <tex>r_0 = 1</tex>, так как <tex>R_0</tex> содержит единственную вершину ''s''. Пусть известно значение ''r<sub>i</sub>''. Напишем программу, которая на логарифмической памяти будет находить ''r<sub>i + 1</sub>''.
 
Теперь имея Enum, можно индуктивно находить ''r<sub>i</sub>''. Очевидно, что <tex>r_0 = 1</tex>, так как <tex>R_0</tex> содержит единственную вершину ''s''. Пусть известно значение ''r<sub>i</sub>''. Напишем программу, которая на логарифмической памяти будет находить ''r<sub>i + 1</sub>''.
Строка 52: Строка 52:
 
</code>
 
</code>
  
Данный алгоритм изначально учитывает ''s'', а затем перебирает всех возможных кандидатов на попадание в <tex>R_{i + 1}</tex>. Для каждого из них перебираются все ребра, в него входящие. Затем перечисляются все вершины из <tex>R_i</tex> и, если начало нашего ребра было перечислено, то <tex>v \in R_{i + 1}</tex>. Алгоритм использует логарифмическую память, так необходимо хранить лишь ''v'', ''u'', ''r'' и еще поочередно значения полученные в результате вызова Enum.
+
Данный алгоритм изначально учитывает ''s'', а затем перебирает всех возможных кандидатов на попадание в <tex>R_{i + 1}</tex>. Для каждого из них перебираются все ребра, в него входящие. Затем перечисляются все вершины из <tex>R_i</tex> и, если начало нашего ребра было перечислено, то <tex>v \in R_{i + 1}</tex>. Алгоритм использует <tex>O(\log |G|)</tex> памяти, так необходимо хранить лишь ''v'', ''u'', ''r'' и еще поочередно значения полученные в результате вызова Enum.
  
Теперь можно написать алгоритм, который будет недетерминировано решать задачу ''STNONCON'' на логарифмической памяти. Он будет состоять из двух частей: вычисление <tex>r_{n-1}</tex> и перечисление всех вершин
+
Теперь можно написать алгоритм, который будет недетерминировано решать задачу ''STNONCON'' на логарифмической памяти. Он будет состоять из двух частей: вычисление <tex>r_{n-1}</tex> и перечисление всех вершин из <tex>R_{n - 1}</tex>. Вычисление <tex>r_{n-1}</tex> происходит путем вызова Next <tex>n - 1</tex>, при этом каждый раз в качестве <tex>r_i</tex> подставляется новое полученное значение.
 +
 
 +
<code>
 +
NONCON(G, s, t)
 +
  r_n := 1 //''<tex>r_0</tex>''
 +
  '''for''' i = 0..n-2 '''do''' //''Вычисляем <tex>r_{n - 1}</tex>''
 +
    r_n := Next(s, i, r_n, G)
 +
  Enum(s, n - 1, r_n, G) //''Перечисляем вершины из <tex>R_{n - 1}</tex>''
 +
  '''if''' t in output '''then''' //''Если t была перечислена то t достижима и выдаем REJECT, иначе ACCEPT''
 +
    REJECT
 +
  '''else'''
 +
    ACCEPT
 +
</code>
 +
 
 +
Данный алгоритм использует <tex>O(\log |G|)</tex> памяти, так как для хранения ''r_n'' и ''i'' необходимо <tex>2\log |G|</tex>, а для вызываемых Next и Enum необходимо <tex>O(\log |G|)</tex> памяти.
 +
 
 +
Таким образом показано, что STNONCON ∈ NL.

Версия 18:06, 6 апреля 2010

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

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

NL = coNL

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

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

[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, то вне зависимости от недетерминированых выбором, совершаемых алгоритмом, результат ноль.

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

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

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. Для угадывания пути достаточно [math]O(\log |G|)[/math] памяти, так как необходимо помнить лишь текущую вершину пути и пытаться угадывать следующую. Enum является недетерминированой программой и если существует порядок исполнения, чтобы достичь ACCEPT, то он достигается.

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

Next(s, i, r_i, G)

 r := 1 //[math]r_{i+1}[/math] хотя бы один, так как [math]s \in R_{i + 1}[/math]
 for v = 1 .. n; [math]v \neq s[/math] do //перебираем все вершины графа, кроме s -- это кандидаты на попадание в [math]R_{i + 1}[/math]
   for u : (u,v)∈E do //перебираем все ребра, входящие в v
     Enum(s, i, r_i, G) //перечисляем все вершины из [math]R_i[/math]
     if u in output then //если u одна из них, то [math]v \in R_{i + 1}[/math]
       r++   //увеличиваем количество найденных вершин и переходим к рассмотрению следующего кандидата
       break
 write r

Данный алгоритм изначально учитывает s, а затем перебирает всех возможных кандидатов на попадание в [math]R_{i + 1}[/math]. Для каждого из них перебираются все ребра, в него входящие. Затем перечисляются все вершины из [math]R_i[/math] и, если начало нашего ребра было перечислено, то [math]v \in R_{i + 1}[/math]. Алгоритм использует [math]O(\log |G|)[/math] памяти, так необходимо хранить лишь v, u, r и еще поочередно значения полученные в результате вызова 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 //[math]r_0[/math]
 for i = 0..n-2 do //Вычисляем [math]r_{n - 1}[/math]
   r_n := Next(s, i, r_n, G)
 Enum(s, n - 1, r_n, G) //Перечисляем вершины из [math]R_{n - 1}[/math]
 if t in output then //Если t была перечислена то t достижима и выдаем REJECT, иначе ACCEPT
   REJECT
 else
   ACCEPT 

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

Таким образом показано, что STNONCON ∈ NL.