Mathmeth.com

A first experiment in algorithmic graph theory A graph is called “properly (2-)colorable” if there is a red/blue coloring of the nodes such that each of the edges is “mixed” : that is, such that the endnodes of each edge have different colors. Note that this is an existential graph property; as algorithmic graphtheorists, we are therefore compelled to investigate this property by writing a program toestablish it by witness.
We design this program from its specifications, namely: This phrasing of the specification is the simplest I can come up with, but note that it hidesthe fact that evaluation of (1) depends on the truth of (0) : the mixedness of an edge depends on the colors of its endnodes, and hence on those nodesbeing colored in the first place! Should we change the definition of ‘mixed’ to accomodateuncolored nodes? And if so, how? To try to answer these questions or even investigatethem would commit us to premature design decisions. Indeed, we must resolve the tensionbetween ‘colored’ and ‘mixed’ , but the best way to do this is to let the design of ourprogram resolve it for us, for only then can we be sure that our decisions will point us inthe direction of our goal, the completed program. That the specification is noncommitalat this stage in our design is in fact a merit! And so we turn to the design of a program establishing (0) ∧ (1) . A standard first question of program construction is: “Does our program require a loop?” .
I can see, the answer is clearly yes, since we have in general no way of concluding (1)without checking it for every edge; indeed, we are designing this program in the hopes offinding a static condition that will allow us to establish (1) . Now that we have decidedour program will contain a loop, our next task is to find an invariant, guard, and variantfunction for this loop.
The most common strategy for picking an invariant is to pick a generalization of the postcondition (or a conjunct thereof) that is easily established by a simple initialization.
This consideration, alongside the considerations above about the tension between ‘colored’and ‘mixed’ , make it clear that (0) should be included in the invariant: First, (0) iseasily established, for example by the nondeterministic initialization: and even easily maintained by thereafter restricting our program to “color flips” : that is,the change of a node’s color from red to blue, or vice versa. And second, by maintaining(0) as an invariant, the predicate ‘mixed’ automatically becomes well-defined for all edgesof our graph. Note how simply following standard program construction techniques hasprovided a simple, elegant, and (most importantly!) constructive solution to the definitionaltension discussed above.
Furthermore, this decision simplifies issues of data management considerably. Though linguistically there is a distinction between ‘colored’ and ‘uncolored’ , mathematicallythere is no difference: “uncolored” is simply a third color to worry about; worse yet, acolor which must be changed in the course of the program. By maintaining (0) , theoperations of coloring and uncoloring nodes drop out of the heart of our program, leavingus with the sole, simple operation of “color flip” ; indeed, for some nodes, such a flipwill never be necessary. To summarize: Good design decisions bring far-reaching andlong-lasting rewards! With (0) now in our invariant, the question becomes: “Should (1) be in our invariant as well?” . Unlike with (0) , opting to maintain (1) is by no means a clear-cut decision,but it is certainly a move worth investigating, for three reasons: First, our only remainingdesign task will then be to prove the invariance of (1) ; second, it may help us by furtherconstraining our design, for instance by leading us to a guard and variant function; andthird, there is a certain elegance (and virtuosity?) to a program which maintains the entirepostcondition throughout.
We begin our investigation by asking how we can establish (1) with a simple ini- tialization. Note that (1) is a universal quantification, and there is a standard way totruthify a universal quantification initially: namely, by making the its range empty. In thecase of (1) , this would mean initializing the program with no edges. Since finally, alledges are present, this suggests a program shape where each iteration of the loop replacesan arbitrary edge of the graph; thus the guard and variant function have come by design,since the graph has finitely many edges. To encode this idea of “replacing edges” , ourprogram will maintain a subgraph H of the entire graph G . And so summarizing allof the above, the shape of the program is now: { Invariant: (1’) : all edges of H are mixed } “possibly using color flips, establish that x and y have different colors, while maintaining (1’) ” The last step of our design is to refine the operation: “possibly using color flips, establish that x and y have different colors, while maintaining (1’) ” in the above program sketch. Towards this end, let us abstract away from the edge xy ,and investigate more generally how we can maintain (1’) under a color flip of an arbitrarynode n . By definition, an edge is mixed precisely when its endnodes have different colors,so flipping n ’s color unmixes precisely the edges incident with n .
(1’) , we therefore have to flip the colors of the neighbors of n as well. Repeating thisargument, we conclude that if we wish to maintain (1 ) under a color flip of a node, wemust swap that node’s connected component. And as the reader can check, swapping anentire connected component indeed maintains (1 ) .
Proving this depends on your definition of connected component; at best it is completelytrivial, at worst it involves showing that if there is a path P from i to j , and an edgefrom j to k , then there is a path from i to k .
If k is a node of P , then there is a subpath of P followed by the edge jk is a path from i to k .
So far so good: the operation of “component color flip” has been forced upon us by choosing (1’) as an invariant. (Again, good design decisions bring far-reaching andlong-lasting rewards!) We now come to the final stage of the design, where we have torefine (∗) and show that the colors of x and y can be changed using this operationso that they are different.
But here we run into our first problem, because as we now know, if x and y have the same color and are connected, then our operation of “component color flip” changeseither both or neither of x and y , and that is no good! Were we to be faced with sucha scenario, we would have to scrap the entire strategy embodied by our program: it justwouldn’t work.
Since so much of the design thus far has been so elegant and forced, I propose to not scrap the design, and instead strengthen the invariant so as ensure this scenario does notarise. Remembering that edge xy is an arbitrary edge of G , I propose to strengthenthe invariant with: ( x and y differ in color) ∨ ( x and y are not connected in H ) Provided we can maintain (2) , we can straightforwardly refine (∗) : { (2) , hence x and y are not connected in H } “swap either x or y ’s connected component” and our program is complete. Note that in all of the above, we have barely made use of(1’) .
Our attention now turns to the maintenance of (2) .
property, and on the other, connectivity , which is not necessarily local at all. We needsome way of relating the two. So we turn, with hope, to the as-yet unexploited invariant(1’) , and we find we are in luck: (1’) relates colors to edges, and edges are indeed the To make this relation precise: since by (1’) each edge of H nodes alternate along paths. Thus we have (for instance): ( x and y differ in color) ∨ ( x and y are not connected in H ) I have formulated the observation in this way, because via (3) , we can now opportunis-tically strengthen (2) into a property independent of color, and indeed, of H : ( x and y differ in color) ∨ ( x and y are not connected in H ) The conclusion of this calculation is that thanks to the invariant, (2) follows from: for all xy in G , all x – y paths in G have odd length (An equivalent formulation sometimes seen in the literature is: “ G has no odd cycles” ,or “all cycles of G are even” .) We showed above that if the invariant could be strengthened with (2) , our program would be correct. We have now shown that under the invariant, (2) follows from (4) ,which, being a property of G , is never falsified. Hence taking (4) as precondition tothe entire program establishes the program’s correctness.
And thus we have proved that a graph satisfying (4) is properly colorable; indeed, the above program will exhibit a proper coloring of that graph.
Three comments on the preceding. First, one might ask if my formulation of (3) is a little bit of a rabbit. Well, that is a fair question, but honestly, I don’t know what tosay. The simple observation that in a properly colored graph, colors alternate along apath, suffices to establish a plethora of little theorems like (3) , all relating the followingbooleans: there exists an x - y path with even (odd) length Property (3) was specifically chosen from among these theorems to allow us to strengthenthe term of (2) . Perhaps someone can synthesize a sort of “symbol dynamics” for thesetheorems, which would streamline the “invention” of (3) . Reader: your help has beensolicited! Second, note that one of these theorems is (4) ! That is, the converse of our theorem holds: if a graph is properly colorable, then equivalence: a graph is properly colorable precisely when (4) holds. This observation issomewhat reassuring, in that by strengthening (2) to (4) decision— , we did not strengthen “too much” ; we strengthened “just right” ! Third and finally, a reader familiar with the calculational style will understandably be annoyed at the verbosity of the above, wondering why I resisted formalizing many of thenotions of the above, even to the extent that I rendered universal quantifications in English!Again, that concern is entirely fair, but again I don’t know what to say. I have attemptedseveral formalizations of the above, and not once have I reaped the benefits. On the onehand, the above proof does not involve much calculation; on the other, I found that themore I tried to formalize, the more notational issues arose. For instance, to cast something like “for all edges e of H ” in formal notation, for the range of that quantification Iwould have to decide whether to allow myself to write something like “ e ∈ H ” , or tointroduce an ad-hoc notation, like “ e ∈ edge(H) ” .
option, because H is changed in the course of the program.) The sad lesson here is that we have not quite reached the point in the theory of graphs where our notation can carry arguments for us. The happy lesson here is that there isclearly a lot to be gained from a constructive, algorithmic approach to graph theory.
Jeremy Weissmann11260 Overland Ave. #21ACulver City, CA 90230USA

Source: http://www.mathmeth.com/jaw/main/jaw0xx/jaw17.pdf