В этом посте я опишу, как кодировать обход в ширину (поиск) (BFT/BFS) ориентированного графа как задачу SAT. Он будет следовать тому же потоку, что и пост, описывающий как решить простую версию судоку, закодировав ее как задачу SAT.

Проблема

Учитывая ориентированный граф и узел n в графе, обход в ширину графа посещает узлы, достижимые из n в порядке возрастания уровней, где уровень i состоит из всех узлов, которые являются i переходами и не менее чем я прыгаю от n.

Начиная обход с узла A на уровне 0 на приведенном выше графике, мы посетим узлы B и C на уровне 1 и узлы D, E и F на уровне 2 (обозначены скобками на диаграмме). На том же графе, начиная обход с узла B (уровень 0), мы посетим узлы D и E на уровне 1, узел A на уровне 2, узел C на уровне 3 и узел F на уровне 4.

Как это связано с БФС?

Учитывая обход с точки зрения того, какие узлы были посещены на каком уровне, может быть несколько порядков обхода, потому что существует множество порядков посещения узлов на уровне, например, ACBDEF и ABCDEF оба являются допустимыми порядками BFT/BFS.

Если вы думаете, что оба эти порядка не будут генерироваться алгоритмом BFS на основе очередей, то вы правы. Причина этого в том, что выбор схемы в алгоритме на основе очереди не учитывает все возможные порядки.

Ограничения

Вход представляет собой граф с N узлами и E направленными ребрами. На выходе будет набор пар узлов в соответствии с порядком посещения BFT.

  1. Так как узлов N, не более N уровней (в случае графа путей).
  2. Поскольку каждый узел нужно посетить ровно один раз, каждый узел встречается ровно на одном уровне.
  3. Когда узел m посещается на уровне g, для каждого последующего узла n узла m есть три возможности: а) узел n уже был посещен ранее, так как у него есть предшественник, посещенный на уровне h ‹ g, б) узел n будет посещен на уровне g поскольку его предшественник посещается на уровне g-1, или c) n будет посещен на уровне g+1, так как m является его первым посещаемым предшественником.
    Другими словами, для каждого ребра (m , n), если узел m встречается на уровне g, то n не встречается на уровне h › g+1.
  4. Рассмотрим мутацию G приведенного выше графа без ребра (E, A). На графе G, если мы начнем обход с узла B. Обход завершится после посещения узлов D и E. Чтобы убедиться, что все узлы посещены, обход должен быть «перезапущен» с непосещенного узла. Такие перезапуски могут быть разрешены путем связывания следующего уровня с узлом перезапуска. [Примечание. Эта ассоциация не согласуется с определением уровня, указанным ранее, но ее можно модифицировать, вычитая уровень узла перезапуска из уровня посещенных узлов из узел перезапуска.] Таким образом, в графе мутаций G (B)(DE)(A)(C)(F) следует признать действительным BFT с перезапуском, происходящим в A на уровне 3, в то время как обход (B) (DEA)(C )(F) следует отклонить. Основываясь на разнице между этими обходами, мы видим, что узел перезапуска должен быть единственным узлом на своем уровне.
    Кроме того, ограничения 1–3 можно тривиально удовлетворить, назначив один и тот же уровень всем узлам. Мы хотим запретить такие присваивания, потребовав, чтобы узлы на уровне имели предшественников на предыдущем уровне.
    Оба эти ограничения могут быть зафиксированы следующим образом: для каждой пары различных узлов m и n, встречающихся на уровне g, существуют два ребра (p, m) и (q, n), такие что p и q встречаются на уровне g-1.
  5. Мы хотим, чтобы уровни начинались с 1. Другими словами, по крайней мере один узел находится на уровне 1.
  6. В номерах уровней не должно быть пробелов, т. е. мы не хотим, чтобы узел A находился на уровне 1, а узлы B и C — на уровне 3. Другими словами,
    a) если существует узел на уровне g , то существует узел на уровне g-1, и
    b)если нет узла на уровне g, то нет узлов на уровне g+1.

Кодирование

Мы используем одну переменную vNxLy для представления появления узла Nx на уровне Ly. Поскольку у нас есть N узлов и N уровней, у нас будет N*N переменных.

Используя общие шаблоны ограничений, мы можем механически перевести ограничения в формулы КНФ следующим образом.

  • Примените ограничение 1, контролируя количество переменных, связанных с уровнями.
  • Используйте сложный шаблон X7 для кодирования ограничения 2.
  • Используйте простой шаблон S6 для кодирования для каждого ребра (m, n)части ограничения 3. Для каждого ребра используйте составной шаблон C6 для кодирования, если узел m встречается на уровне g, то n не встречается на уровне h › g+1, так как это эквивалентно, если узел m встречается на уровне g, тогда для всех h › g+1 n не встречается на уровне h.
  • Используйте простой шаблон S6 для кодирования каждой пары различных узлов m и n, встречающихся на уровне g,часть ограничения 4. Используйте простой шаблон S3 для кодирования существующих ребер (p, m) и (q, n) части. Используйте преобразование Цейтина для кодирования p и q на уровне g-1 части.
  • Используйте простой шаблон S5 для кодирования ограничения 5.
  • Используйте простой шаблон S6 для кодирования части уровня g и C5 для кодирования если ..., то существует узловаячасть ограничения 6a. Используйте простой шаблон S6 для кодирования для части уровня g и C6 для кодирования если…, то нет узловчасть ограничения 6b (поскольку узлов нет можно указать как для всех узлов).

Устранение избыточности

Приведенная выше схема кодирования имеет некоторую избыточность. Например, при кодировании каждой пары различных узлов m и n в ограничении 4 предложения, созданные для (m, n), будут такими же, как предложения, созданные для (n, m). Этой избыточности можно избежать во время кодирования или отфильтровать после кодирования, удалив дубликаты.

Решение

Теперь мы объединяем формулы из кодирования ограничений в одну формулу CNF и передаем ее решателю SAT. Если решатель предоставляет модель, то мы интерпретируем каждую переменную vNxLy, которая является истинной в модели, как посещение узла x на уровне y. Используя эту информацию, мы можем легко определить допустимый порядок BFT/BFS, расположив узлы в порядке возрастания уровней и выбрав любой порядок узлов на одном уровне. Вот и все :)

Вот скрипт Groovy, который воплощает эту кодировку и использует решатель Z3 для решения проблемы.

Для вас сделать

В приведенном выше коде порядок BFT/BFS идентифицируется в коде Groovy без использования решателя SAT. Расширьте ограничения и кодировку, чтобы определить порядок с помощью решателя SAT.

Что дальше?

В следующем блоге я опишу как закодировать обход в глубину (поиск) ориентированного графа как задачу SAT.

Обновления

04/15/2018

Вот фрагмент кода решает ту же проблему, 1) вычисляя порядок без вычисления уровней и 2) используя решатель для определения порядка. Однако это решение допускает только те заказы, которые являются результатом BFT/BFS на основе очередей.