Testing the optimality of algorithms using Alloy - Part 3

Continuing from part 2...
http://feels-good-to-ramble.blogspot.in/2012/11/testing-optimality-of-algorithms-using_30.html
 , we are not done yet concluding that a BFS-based coloring algorithm is suboptimal. We now need to modify the algorithm to run BFS for every vertex as starting vertex in turn, and then check whether the least number of colors used in all those sub-runs is still suboptimal. This complicates things quite a lot, because we now need to store results for every BFS sub-run. It is not now enough to continue to store with Node, the fields that we stored with it in part 2. This is because, the field values are liable to change for each sub-run of the BFS. We solve this problem in a simple way by introducing another signature called Run, to denote a sub-run. We store fields, 'colormap', 'ordermap', 'levelmap' and 'snapshot', to denote maps between a Node and respectively its BFS 'color', its order of discovery during this sub-run of the BFS, its level in this sub-run of the BFS and finally, the  set of Nodes that include itself and the ones discovered before it in this sub-run. We need to introduce one more signature called Order which is the order of discovery of a Node for a sub-run. Only, the fields 'adjacency' and 'optcolor' remain with the Node, since they do not change from sub-run to sub-run. Finally, the predicate 'bfs_suboptimal' changes to assert the following:

all r:Run |  bfs[r] and #Node.optcolor < #r.colormap[Node]

which means that for every sub-run, the coloring found by Alloy (in 'optcolor') uses fewer colors than the coloring obtained by BFS in that sub-run.
  With these changes to our Alloy source,  it was found that no suboptimal coloring is obtained for vertices (Nodes)  up to 5 in number. The smallest graphs where BFS-based coloring is suboptimal has 6 or more vertices. All the test results in the figures below show only the 'optcolor' arrows and not the colors obtained through BFS. Also, the double-arrowed, red edges between any two Nodes (blue boxes) are the adjacency edges between the nodes.

Fig 1

Fig 2

Fig 3

 Some more results found after tweaking the source to constrain the number of 'optcolor's required to more than 3, then we get no 'suboptimal' coloring for 6 nodes, but we do get some for 7 nodes, one of which is shown in fig 4.

Fig 4

 This means that for 6 nodes the BFS based coloring does not use more than 4 colors in any case.

Fig 5

 It was also found similarly, that for 7 nodes the BFS based coloring does not exceed 5 colors, but for 8 nodes it does, as shown in Fig 5.
 The Alloy source listing is given below :

open util/graph[Node] as GR
open util/ordering[Order] as OR
open util/ordering[Color] as CO
open util/ordering[Level] as LV


sig Color {}

sig Run {
   start_node: one Node,
  private colormap: Node->one Color,
  private ordermap: Node one ->one Order,
  private levelmap: Node->one Level,
  private snapshot: Node  -> set Node
}

sig Order{}

sig Node{
    adjacency: set Node,
    optcolor: one Color
}

sig Level {}

pred  undirected_graph() {
    GR/undirected[adjacency]
    GR/noSelfLoops[adjacency]
       GR/stronglyConnected[adjacency]
}

pred init (r:Run) {
    let i=OR/first | let n= r.start_node | r.ordermap[n]=i and
    r.levelmap[n]=LV/first and r.snapshot[n] = n and r.colormap[n]=CO/first
}

fun done_nodes(r:Run, n:Node): set Node {
   r.snapshot[n]
}

fun next_level (r:Run, n:Node) : Level {
   LV/next[r.levelmap[n]]
}

fun prev_level (r:Run, n:Node) : Level {
   LV/prev[r.levelmap[n]]
}

fun level(r:Run, n:Node):Level {
   r.levelmap[n]
}

fun next_order(r:Run, n:Node): Order {
  OR/next[r.ordermap[n]]
}

fun prev_order(r:Run, n:Node): Order {
  OR/prev[r.ordermap[n]]
}

fun order(r:Run, n:Node) :Order {
  r.ordermap[n]
}

fun nodes_at_same_level(r:Run, n:Node) : set Node {
  (r.levelmap). (r::level[n])
}

fun node_at_order (r:Run, o:Order) : one Node {
  (r.ordermap). o
}

fun nodes_at_level (r:Run, l:Level) : set Node {
  (r.levelmap). l
}

fun next_siblings(r:Run, n:Node): set Node
{
  let parent_nodes= r::nodes_at_level [r::prev_level[n] ]   |
     some parent_nodes implies
      {
       let siblings = parent_nodes.adjacency -  r::done_nodes[n] |
         some siblings  implies
            siblings
         else
            none
     }
      else
            none
}


fun  children_at_next_level(r:Run, last_upper_node:Node) : set Node
{
    let n=last_upper_node |
           let peers= (r::nodes_at_same_level[n].adjacency - r::done_nodes[n]) |
           some peers implies
             peers
           else
             none
}

pred bfs(r:Run) {
    init[r]  
    all ord:Order - OR/last | step[r, ord ]
   correctness [r]
}

pred correctness [r:Run] {
   all n:Node | r.colormap[n] not in r.colormap[n.adjacency]
}

fact {
  some Node
  undirected_graph 
  no disj r1,r2:Run | r1.start_node=r2.start_node
  no disj n1,n2:Node | start_node.n1 = start_node.n2
  Run.start_node = Node
  coloring_prob
}

pred coloring_prob  { (no n,m:Node | (m in n.adjacency and n.optcolor= m.optcolor) ) }

pred set_color(r:Run, n:Node)
{
 let prevn = r::node_at_order[r::prev_order[n]] | let cols=Color - r.colormap[(n.adjacency & r::done_nodes[prevn])] |
   r.colormap[n] = CO/min[cols]
}

--This creates the next level from the current level. It is based on traversing the adjacencies
pred step (r:Run, i : Order) {
     let n= r::node_at_order[i] | 
     {
       let sibs=r::next_siblings[n] |
        some sibs implies
        {
         one m:sibs | r::order[m] = r:: next_order[n]  and
              r::level[m] = r::level[n] and
              r::done_nodes[m] = r::done_nodes[n] + m
       }
      else
      {
         let  children=r::children_at_next_level[n] |
         some children implies
         {
           one m: children |
               r::order[m] = r::next_order[ n ] and
              r::level[m] = r::next_level[n] and
              r::done_nodes[m] = r::done_nodes[n] + m
        }
      }
     let m= r::node_at_order[ r::next_order[n] ] |  r::set_color[m]
   }
}

pred bfs_suboptimal()
{
   all r:Run |  bfs[r] and #Node.optcolor < #r.colormap[Node]
}

run bfs_suboptimal for 6 but  4 Color

To conclude, in this set of 3 posts we saw how Alloy can be employed to test our understanding of problems, especially when we are learning about or exploring a subject. Specifically, we demonstrated how a simple (class-P) BFS-based algorithm is unable give optimal results for the vertex coloring problem, for many graph instances, shattering any intuition that this problem may have this algorithm as a solution. Of course, it does not demonstrate that there is no exact solution for the vertex-coloring problem in P, simply that our BFS-based algorithm is not the one.
 Of course, the world knows the vertex-coloring problem is NP-complete, and that there is perhaps (note the 'perhaps') little sense in pursuing an exact solution in P for this problem. These posts simply illustrate a larger point about how we can use approaches and tools to test the efficacy of any approximate algorithms that we may rig up for such problems. For example in future it may be interesting to find out the bounds on the suboptimality of the BFS-based algorithm, that is, how far from the optimal solution can it get, and whether there are bounds on this distance from optimality. This requires theoretical proof, but tools like Alloy can suggest directions and check hunches.