Alloy Practice Problem: Undirected Acyclic Graphs

While learning Alloy this was one of the exercises in the book I was reading. It’s kinda weird to combine “acyclic” and “undirected” for graphs but there is a way to formalize the intuition about what it means for an undirected graph to be acyclic.

For everything that follows I’m going to assume that you understand the Alloy syntax and semantics. If not then I recommend some posts I wrote for beginners to get started over at dev.to: 1, 2, 3, 4, 5.

The graph structure is expressed in terms of nodes. The node signature is pretty simple and just says a node can be connected to 0 or more other nodes

Next we need to specify the conditions for making the graph undirected and we do that by forcing the adjs to be symmetric

If that’s all we did we’d get a lot more than just “acyclic” undirected graphs so we need to set up a few more restrictions. We don’t want any self loops so we make sure that’s the case

We also want to rule out trivial graphs

The above fact forces all nodes to participate in the adjs relation because we don’t want disconnected graphs with nodes just hanging out. If you run the model at this point you’ll get some interesting results We want to rule out those cases but it is not obvious how to do that. If you stare at the above “cyclic” undirected graphs a thought might occur to you: why not treat the graph as a directed graph and then try to figure out what the acyclicity condition would look like?

If you look at the smallest example with 3 nodes you’ll notice there is a cycle starting at Node\$0 and the cycle is Node\$0 -> Node\$1 -> Node\$2 -> Node\$0 and we want to rule that out. There is an obvious way to break the cycle and it’s removing one of the edges. We are going to build our definition of acyclicity on this intuition.

If you look at any node and remove the edge connecting that node to it’s neighbor then the cycle is broken. Another way of specifying the condition is to say if we look at any two nodes that are connected then if we remove one of the edges going back then we should not be able to get back to where we started

Running the model with the above conditions will give the correct results

If you find a better way then let me know.