While developing an algorithm for fast distributed computation of a graph diameter and radius, some of my colleagues had a conjecture about graph topology that, if true, would enable an aggressive optimization of the algorithm.

In order to understand the conjecture we must first recall some (more or less) standard graph theory definitions:

- The
**distance**between two nodes is the length of the shortest path between them; - The
**eccentricity**of a node is the greatest distance between that node and all others; - The
**diameter**of a graph is the maximum eccentricity found in the graph; - A node is
**peripheral**if its eccentricity is equal to the diameter; - The
**antipode**of a node is the set of nodes at distance equal to its eccentricity.

Given a non-directed connected graph the initial conjecture was:

*For every node, all nodes in its antipode are peripheral.*

They quickly found a counter-example to this conjecture and relaxed it to the following:

*For every node, some node in its antipode is peripheral.*

For a long time they were not able to prove or refute this conjecture. At some point I was involved in the discussion and decided to model-check it using Alloy before attempting any proof.

Modeling a non-directed connected graph using Alloy is fairly trivial (assuming some basic knowledge of Alloy):

sig Node { adj : set Node -- adjacency relation } fact { adj = ~adj -- the adjacency relation is symmetrical no iden & adj -- no loops all n : Node | Node in n.*adj -- the graph is connected }

To model distances I used a ternary relation between pairs of nodes and a natural number. Natural numbers are easily modeled with a total ordering, which is axiomatized in one of Alloy’s standard modules:

open util/ordering[Nat] sig Nat {}

The distance relation can be declared in the node signature and axiomatized as follows:

sig Node { adj : set Node, dist : Node -> one Nat } fact { all n : Node | n.dist[n] = first all disj n,m : Node | n.dist[m] = min[n.adj.dist[m]].next }

The two facts just state that, for every node:

- The distance to itself is 0.
- The distance to another node is 1 plus the minimum distance between its neighbors and that node.

We can now compute the eccentricity relation by direct transcription of the above definition, using a higher-order function without parameter (i.e. a constant):

fun ecc [] : Node -> one Nat { { n : Node, d : Nat | d = max[n.dist[Node]] } }

Given this relation, the diameter, periphery and antipode relation can be trivially defined:

fun diam [] : one Nat { max[Node.ecc] } pred peripheral [n : Node] { n.ecc = diam } fun antipode [] : Node -> Node { { n, m : Node | n.dist[m] = n.ecc } }

Following this approach, other graph concepts, such as radius or centrality, could also be trivially defined:

fun radius [] : one Nat { min[Node.ecc] } pred central [n : Node] { n.ecc = radius }

The conjecture can now be directly transcribed into the following assertion:

check { all n : Node | some m : antipode[n] | peripheral[m] }

Unfortunately, when the scope was increased to 7 we had several counter-examples. Here is one of them:

The diameter of this graph is 4. The antipode of node 6 is node 3, but this node is not peripheral, since it has eccentricity 3.

Bummer 😦 At least we can now easily model-check other similar properties before indulging in pointless discussions.