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

Проблема

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

Начиная обход в узле A на приведенном выше графике, мы посетим узлы в порядке B, D и E или B, E и D перед посещением C и еще не посещенными узлами, доступными из C. Если обход начался в узле C и посетили F перед D, то мы посетили бы узлы F, D, E, A и B по порядку.

Ограничения

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

  1. Каждый узел должен быть посещен ровно один раз. Другими словами, каждый узел должен встречаться в выходной последовательности ровно один раз.
  2. На каждом этапе обхода можно посетить только один узел. Так как будет N шагов (позиций в выводе) и из-за ограничения 1 шаг посетит хотя бы один узел. Итак, нам нужно учитывать только каждый шаг посещает не более одного узла.
  3. После посещения узла m на шаге g, если один из узлов-преемников m m посещается на шаге h›g, то все узлы, посещенные с g по h (за исключением g), должны быть не посещены при посещении m и достижимый из m.
    Если узел, достижимый из m, был посещен до посещения m, то он не будет посещен после посещения m из-за ограничения 1; следовательно, нам нужно рассмотреть только вторую часть ограничения.
    Предположим, что q посещается на шаге j после посещения m и до посещения n, т. е. g‹j‹h. Если q достижимо из m, то должно быть ребро (p, q) такое, что вершина p достижима из m и посещается на шаге i после посещения m и до посещения q, т. е. g≤i‹j. Поскольку p достижимо из m, это наблюдение должно быть выполнено и для p. Следовательно, для всех узлов, посещенных на шагах i от g+1 до h.
    Другими словами, для каждого ребра (m, n), если m посещается на шаге g, n посещается на шаге h, и q на шаге g‹j‹h, то существует ребро (p, q), такое что p встречается на шаге g≤i‹j.

Кодирование

Используйте одну переменную vNxPy для представления появления узла Nx на шаге Py. Поскольку у нас есть N узлов и N шагов, у нас будет N * N переменных.

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

  • Используйте сложный шаблон X7 для кодирования ограничения 1.
  • Используйте сложный шаблон X6 для кодирования ограничения 2.
  • Используйте простой шаблон S6 для кодирования каждого ребра (m, n, q) и шага g‹j‹h,часть ограничения 3. Используйте простой шаблон S3 для кодирования если m встречается на шаге g, n встречается на шаге h, а q — на шаге g‹j‹h, тогда часть ограничения. Используйте простой шаблон S5 для кодирования существует ребро (p, q), такое что p встречается на шаге g≤i‹j.

Решение

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

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

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

Исследуйте размер формулы, сгенерированной приведенным выше решением, на графиках разного размера.