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.