Finding Graph Counterexamples with Alloy

I recently answered this question on Quora: “Can you draw 2 non-isomorphic graphs with five vertexes and five edges simple graphs with each vertex carrying the same degree sequence?” It seems like questions of this sort, asking for a specific counterexample, could be addressed through a constraint solver or model checker. So I decided to see if I could re-solve the problem using Alloy.

So, what’s a graph? It’s got nodes and edges:

sig Node {
}
sig Graph {
   nodes : set Node,
   edges : Node -> Node
} {
   edges = ~edges
   no Node <: iden & edges
   Node.edges in nodes
   edges.Node in nodes
}

We want undirected graphs, so the first constraint (“fact”) is that the edge relation is equal to its transpose. If there’s an edge (x,y) there must be an edge (y,x) as well.

The second constraint was a bit harder to write. It expresses anti-reflexivity; there should be no self-loops in the graph. iden is the identity relation on all atoms in the model. The <: operator picks just those elements of the relation whose first element is in Node, so that is the identity relation on nodes.

The last two constraints state that every edge in the graph must have endpoints in the graph. This model is a little strange in that two graphs can share Nodes, or Nodes can even exist not in any graph. But the former is probably OK as long as we’re careful (it might help keep the satisfiability instances smaller) and the second makes the visualizations a little weird but that’s OK. We could write a constraint to eliminate that as a possibility.

When are two graphs isomoprhic? When there’s a bijection between their nodes that preserves edge relationships:

pred isomorphic_graphs( a : Graph, b : Graph ) {
  some f : a.nodes one -> one b.nodes {
    (~f).(a.edges).f = b.edges
  }
}

This is simple, elegant, and totally useless for use in the model checker because it depends on a higher-order quantification. The some f is an existential quantifier over relations, and there are a lot of possible relations. We can use this predicate in some cases, but not others. For example, this works:

pred has_isomorphism {
  some disj a, b : Graph {
     isomorphic_graphs[a, b]
     no a.nodes & b.nodes 
  }
}
run has_isomorphism for 6 but exactly 2 Graph

Visualization of two isomorphic graphs

But this won’t:

two_nonisomorphic: run {
 some a, b: Graph {
 same_degree_sequence[a,b]
 not isomorphic_graphs[a,b]
 }
} for 5 but exactly 2 Graph

Starting over

How can we rewrite the model to make it feasible to solve?

The definition above allows two degrees of freedom that are unnecessary for this problem: it allows graphs with arbitrary numbers of nodes, and it allows the nodes to be arbitrary atoms in the model. But we can instead just fix what nodes a graph has, tailored to the problem we want to solve:

enum Node { n_1, n_2, n_3, n_4, n_5 }
sig Graph {
   edges : Node -> Node
} {
   edges = ~edges
   no Node <: iden & edges
}

Now every graph has five vertices. We keep undirected edges, and the prohibition on self-loops, but the other two constraints are now trivially satisfied. Every graph has the same five nodes.

For isomorphism, we can use the same idea but quantify over the values of the bijection instead of over bijections:

pred isomorphic_graphs_5( g1 : Graph, g2 : Graph ) {
  some disj a, b, c, d, e : Node {
    let f = n_1->a + n_2->b + n_3->c + n_4->d + n_5->e {
      (~f).(g1.edges).f = g2.edges
    }
  }  
}

Same for matching degrees, although I did this in a cruder fashion:

fun degree( g : Graph, n : Node ) : Int {
 #(g.edges[n])
}
pred same_degree_sequence_5( g1 : Graph, g2 : Graph ) {
  some disj a, b, c, d, e : Node {
    degree[g1,n_1] = degree[g2,a]
    degree[g1,n_2] = degree[g2,b]
    degree[g1,n_3] = degree[g2,c]
    degree[g1,n_4] = degree[g2,d]
    degree[g1,n_5] = degree[g2,e]
  }
}

Now, let’s solve the original problem. We have to increase the bitwidth of the integers to get the desired number of edges— otherwise the model is trivially unsatisfiable because it can’t express “10”.

two_nonisomorphic: run {
   some a, b: Graph {
      same_degree_sequence_5[a,b]
      not isomorphic_graphs_5[a,b]
      #a.edges = 10
   }
} for 10 but 5 Int, exactly 2 Graph

The resulting model is fairly big (18,000 variables?) but quickly solved:

And here are the two examples I showed, as visualized by Alloy (projected over graphs):

Another benefit of using the same set of nodes is that each example is clearly visible by itself, rather than the visualization including all nodes, whether they are in the graph or not. (I wish, in addition to projecting by a particular object, we could filter the visualization as well.)

From the visualizer, we can open the interactive “Evaluator” and query the relations:

or write expressions in the Alloy language, like this comprehension expression mapping nodes to degrees:

Conclusion

Alloy works pretty well for finding small examples, but the need to tailor each model to the size of the (counter)-example is undesirable. It might be possible to write a macro that allows us to easily create graphs of different sizes, but that’s advanced-level usage of Alloy that’s beyond me right now. It’s hard to make the recommendation for students looking for such graph counterexamples to “just use Alloy” if they have to carefully understand the limitations of the model checker — a common problem when building models.

It might be interesting to build a domain-specific language specialized for such graph examples. Under the hood, it could make the translation from statements in second-order logic (about isomorphisms or colorings) to first-order logic in a variety of different graph sizes.