SAT Encoding: Depth First Traversal of Directed Graph

In this post, I will describe how to encode the problem of depth-first traversal (search) (DFT/DFS) of a directed graph as a SAT problem. It will follow the same flow of the post describing how to encode breadth-first traversal (search) (BFT/BFS) of a directed graph as a SAT problem.

Problem

Image for post
Image for post

Starting the traversal at node A in the above graph, we will visit nodes the order of B, D, and E or B, E, and D before visiting C and the yet unvisited nodes reachable from C. If the traversal started at node C and visited F before D, then we would visit nodes F, D, E, A, and B in order.

Constraints

  1. Each node should be visited exactly once. In other words, each node should occur in the output sequence exactly one.
  2. Only one node can be visited in each step during the traversal. Since there will be N steps (positions in the output) and due to constraint 1, a step will visit at least one node. So, we only need to consider each step visits at most one node.
  3. After visiting node m at step g, if one of m’s successor node n is visited at step h>g, then all nodes visited from g thru h (excluding g) should be unvisited when m was visited and reachable from m.
    If a node reachable from m was visited before visiting m, then it will not be visited after visiting m due to constraint 1; hence, we need to consider only the second part of the constraint.
    Suppose q is visited in step j after visiting m and before visiting n, i.e., g<j<h. If q is reachable from m, then there should be an edge (p, q) such that node p is reachable from m and is visited at step i after visiting m and before visiting q, i.e., g≤i<j. Since p is reachable from m, this observation should also hold for p. Hence, for all nodes visited in steps i from g+1 thru h.
    In other words, for each edge (m, n), if m is visited at step g, n visited at step h, and q at step g<j<h, then there exists an edge (p, q) such that p occurs at step g≤i<j.

Encoding

Using the common constraint patterns, we can mechanically translate the constraints into CNF formulae as follows.

  • Use complex pattern X7 to encode constraint 1.
  • Use complex pattern X6 to encode constraint 2.
  • Use simple pattern S6 to encode for every edge (m, n, q) and step g<j<h, part of constraint 3. Use simple pattern S3 to encode if m occurs at step g, n occurs at step h, and q at step g<j<h, then part of the constraint. Use simple pattern S5 to encode there exists an edge (p, q) such that p occurs at step g≤i<j.

Solving

Here’s a Groovy script that embodies this encoding and uses Z3 solver to solve the problem.

For You To Do

Written by

Programming, experimenting, writing | Past: SWE, Researcher, Professor | Present: SWE

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store