Designing the proof of Vizing’s Theorem (with J.R. Rao)

Designing the proof of Vizing's Theorem

by Josyula R.Rao & Edsger W.Dgkstra

We shall design the proof of the following theorem, due to V.G. Vizing.

Theorem For a finite undirected graph without autoloops and without multiple edges, at any vertex of which fewer than N edges meet, N colours suffice for an edge colouring such that edges incident on the same vertex are of different colour.

The graph being adcpably coloured is ex-pressed by

(0) $\left( {{AV} : {acc}.V}\right)$

where predicate acc on vertices is given by acc. $V \equiv$ (no two edges incident on vertex

V have the same colour)

We shall prove Vizing's Theorem constructively by showing how the entire graph can be acceptably coloured. To this end it suffices to design a procedure that, given an acceptably coloured graph with one uncoloured edge, construct an acceptable colouring in which this last edge is coloured as well. Repeated applica

tion of this procedure, starting with a graph consisting of vertices only (whose colouring is trivially acceptable) and adding one uncoloured edge at a time, colours the whole graph acceptably. We shall design the procedure for colouring the next uncoloured edge.

In the rest of this note, we confine ourselves to acceptably coloured graphs. In order not to interrupt the subsequent development of the procedure too much, we first introduce a concept, the need of which will emerge, viz. the alternating path. An alternating path is a maximal path of at most two given colours. Because the colouring of the graph is acceptable, those two colours alternate along such a path; hence the name. One can show the following:

(i) an alternating path is either a cycle (i.e. without end points) or a simple path with two end points. (In order to avoid case analysis, we allow the end points to coincide, in which case the alter-. nating path has length O.) (ii) a pair of colours and a vertex determine a unique alternating path of those colours and through that vertex. (We allow the two given colours to be equal, in which case the length of the alternating path is at most 1 edge.) (iii) swapping the colours of the edges of an

alternating path leaves the colouring acceptable (because alternating paths are maximal, i.e. have no end points where they can be extended); its significance is that it provides a way for changing the sets of colours at the end points while leaving the colouring acceptable.

Before the procedure starts, we define for each vertex $V$ a colour $c.V$ , in terms of which we define predicate $f$ given by $p.V \equiv (\text{no edge incident on } V \text{ has colour } c.V)$ .

The fact that the number of colours is higher than the number of edges meeting at any vertex is exploited by choosing $c$ in such a way that initially (A V: f.v) holds.

In the following algorithm for the procedure, $X, Y$ , and $Z$ are variables of type vertex. The procedure's functional specification in terms of pre- and postcondition is given in full; intermediate assertions are only named and will be determined later. Explanation and missing definitions will be given afterwards, when we design the algorithm. (We give this text now for future reference. At this stage, the reader should not try to understand this program fragment.)

$\left{ {\begin{array}{l} \left( {A \vee : a + c \cdot V}\right) \land \left( {A \vee : f \cdot V}\right) \land \ \left( {XY\text{ is the only uncoloured edge }}\right) 3 \end{array}} }\right.$ $\left{ {{Po} : \text{invariant}}\right}$

do the c.Y-path ends in Y → {P1} determine Z so that edge XZ has colour c.Y {P2}; give edge XY colour c.Y and uncolour edge XZ {P3}; Y: Z {Po}

od {P4} swap the colours along the c.Y-path ${$ P5 $}$ ; give edge XY colour c.Y ${$ (AV: acc.V) A (all edges are coloured) $}$ .

The term

(0) $\left( {A{V}_{1} : {acc}.V}\right)$

is a conjunct of all intermediate assertions; the term

(1) (XY is the only uncoloured edge)

is a conjunct of all, except P3. Note that, in view of the absence of autoloops, (1) implies that $X$ and $Y$ are different vertices.

We shall now show how the above algorithm can be designed. The leading principle is to keep things as simple as possible and not to introduce complications unless forced to do so. In particular: the simplest way, if possible, of asserting a term

that has been asserted before is to maintain it in between.

We now start the design of the algorithm, beginning with its last statement. Because (o) - i.e. (A V: acc. V)- occurs in both pre- and postcondition, we decide - see previous paragraph- to maintain (0) all through the algorithm. Consequently, the final act of the algorithm is to colour the uncoloured edge with an acceptable colour. Let, as initially, the uncoloured edge be XY ; colouring it while main-. taining (0) means that has to be coloured with a colour that is incident on neither X nor Y . Initially, since P.X. f.Y holds, c.X is not incident on X and c.Y is not incident on Y . Somewhat asymmetrically we decide to give edge XY the colour c.y . This choice of last statement yields - note that in view of the definition of $f$

$$ f. Y \equiv (c. Y n o t i n c i d e n t o n Y) - $$

for its precondition P5;

P5: (0) A (1) A (c.y not incident on X) A P.Y.

We now consider $P5$ as the postcondition to be established. Because (0) $\land$ (1) $\land$ $P.Y$ is implied by the precondition, we concentrate our

attention on establishing P5 's conjunct

(c.y not incident on $X$ )

while maintaining its three other conjuncts. If an edge incident on X has colour c.y , its colour has to be replaced by a colour not incident on X . Since initially f.x holds, (i.e. colour c.x not incident on X), we propose, in view of (iii), to swap the colours c.x and c.y along the alternating path through X that has those colours. This ensures that c.y is no longer incident on X .

Since we need the concept a number of times, we define, for graphs satisfying (A V: a c. V) and f.x and for any colour $p$ ,the $p$ -path to be the alternating path through X with colours $p$ and c.x . Due to f.x , i.e. c.x not incident on X,

• the $p$ -path with $p = c.x$ is empty
• a non-empty p-path starts at $X$ with an edge of colour $p$ and ends at a vertex different from $X$ .

In the above terminology, we propose to establish (c.y not incident on X) by swapping the colours along the c.Y-path; this maintains (0) $\land$ (1), but maintains f.Y only provided the c.Y-path does not end in Y. (Because of f.Y, a c.Y-path ending at Y does so with

an edge of colour c.x ; changing that colour into c.y would falsify f.Y.) Collecting our requirements, we get as precondition $P$ for the colour swap along the c.y- path

${P}_{4} : \;$ (0) $\land \;$ (1) $\land \;f.x \land f.y \land$

(the c. Y - path does not end in $Y$ )

We now consider $\mathbb{P}\mathbb{R}$ as the postcondition to be established. Observing that the first four conjuncts of $\mathbb{P}\mathbb{R}$ are implied by the pre-condition, we apply the same heuristic principle as before and decide to look for a statement that establishes the last conjunct of $\mathbb{P}\mathbb{R}$ while maintaining the others. The following methodological interlude explains why we look for a statement of the form of a repetition.

Methodological InteRlude Suppose we look for a program $S$ that satisfies for some $P, Q$

[\left{ {P}\right} \sim \left{ {P \land Q}\right} ]

In those initial states in which Q holds, S may act as a skip. Sometimes this requires no explicit measures. (We saw an example of this in the statement we derived earlier: swapping the colours along an alternating path automatically reduces to a skip if the path is empty.) Otherwise we need an explicit guard in order

to distinguish between the cases Q and IQ . Unless an S of the form

$$ i f Q \rightarrow s k i p \quad I \quad \neg Q \rightarrow D \quad f _ {i} $$

obviously does the job, it is wiser to begin looking for an $S$ of the form

$$ \underline {{d o}} \mapsto Q \rightarrow D \quad \underline {{o d}} $$

since this allows us to separate the concerns far partial correctness and termination. If, while studying termination, we learn that D is executed at most once because it establishes Q , we are still free to replace the repetition by the alternative construct. (End of Methodological Interlude.)

The repeatable statement we are looking for should have the potential of falsifying the guard (the c.y-path ends in $Y$ )

Because of an example in which it is impossible to falsify this guard by only changing C and not changing the colouring of the edges, and because, for simplicity's sake, we would not like to change both, we decide to try to keep c constant and let the repeatable statement affect the edge colouring only.

The next constraint we adopt is that the

repeatable statement is confined to the combination of colouring the uncoloured edge and uncolouring a coloured one. This is inspired by the observation that this is the simplest transformation whose repeated application can transform a colouring with one uncoloured edge into any other such colouring. It is a constraint - and therefore not adopted without optimism - because, in addition, we intend to maintain at each step

(0) $\land \;\left( 1\right) \land f \cdot X \land f \cdot Y$

As asymmetrically as before, we decide to give the uncoloured edge the colour c.y; on account of the initial validity of p.y, this colouring act maintains acc.y. In order to maintain acc.x as well, the first edge of the c.y-path is uncoloured. Thus we have designed the repeatable statement given above. (The variable Z has primarily been introduced to ease the discussion.) Our gamble is that we can prove invariance and termination. Let us concentrate on the invariance first.

As we shall see shortly, all is available for the invariance of (0) $\wedge$ (1) $\wedge$ f.x ; the invariance of f.y ,however, poses a problem. The invariance of p.y requires the conjunct p.z

in $P_{3}$ , and the simplest way of justifying it there is by requiring $f. Z$ as conjunct in $P_{2}$ . (Besides this being the simplest way, our termination argument, as we shall see later, relies on the fact that no false value is truthfied.) In order to justify $f. Z$ in $P_{2}$ the invariant has to be strengthened with a new conjunct; $(\underline{A} V::f.V)$ would justify $f. Z$ but is too strong to be maintained. We could also justify $f. Z$ from

for any colour $p$ such that the $p$ -path is not empty:

where $S$ is the second vertex on the $p$ -path This, however, is also too strong: the repeatable statement transforms the $p$ -path X2...Y into the $p$ -path XY...Z with XY of colour c.y, so if.S for $p = c.y$ . The following slightly weaker conjunct does the job:

(2) for any colour $p$ such that the $p$ -path is not empty: $P.S \vee c.l \neq p.$ where $S$ is the second vertex of the $p$ -path and $L$ its last vertex.

Now the time has come to list and justify assertions $P0$ through $P3$ .

${P}_{0} : \;\left( 0\right) \land \left( 1\right) \land \left( 2\right) \land f.x \land f.y \land x \neq y$

Assertion ${PO}$ is implied by the precondition of the procedure: its first two conjuncts occur in the precondition, the next three follow from (A V : f.v), and $X \neq Y$ follows from (1) and the absence of autoloops. We return later to the re-establishment of ${PO}$ at the end of the repeatable statement.

P1: PO A (the c.y-path ends in Y) A (the c.y-path starts at X with an edge of colour c.y)

The first two conjuncts follow from the topology of the program; the last conjunct is a property of nonempty p-paths and the c.Y-path is nonempty because it connects the different vertices X and Y .

${P}{2} : \;{P}{1} \land \left( {{XZ}\text{ has colour }c.Y}\right) \land X \neq Z \land$ $f.2 \land c.2 \neq c.Y \land Y \neq Z.$

The first conjunct $P_{1}$ , which does not refer to $Z$ , is maintained and implies the existence of a unique vertex $Z$ such that $XZ$ has colour $c_{Y}$ ; $XZ$ is an edge and not an autoloop, hence $X \neq Z$ ; the conjunct $f_{Z}$ follows from (2) with the instantiation $p, S, L := c_{Y}, Z, Y$ ; from $f_{Z}$ and the fact that $XZ$ has colour $c_{Y}$ , we conclude $c_{Z} \neq c_{Y}$ , from which

with Leibniz's Principle, $Y \neq Z$ follows.

P3: (X2 is the only uncoloured edge) A

(XY has colour C.Y) A (0) A

${f}^{2}x \mid {7f}^{2}y \mid {52}$ (2)

Since $X,Y,Z$ are three distinct vertices, XY and XZ are distinct edges and the (un)colouring statement is well-defined; with (1) it establishes the first two conjuncts. For (0) and the next three conjuncts we need only consider vertices $X,Y,Z$ since they are the only vertices with incident edges changing colour; acc.X and f.x are maintained because the bag of colours incident on X remains the same; to the bag of colours incident on Y the colour c.y is added and, because of p.y in P2, this main-tains acc.y and falsifies p.y; acc.z and f.z are maintained because the bag of colours incident on Z decreases. For the invariance of (2), we distinguish two cases.

In the case $p \neq c.Y$ , we observe that the (un)colouring statement leaves the $p$ -path unchanged; in particular, if the $p$ -path is not empty, its vertices $S$ and $L$ remain the same. The constancy of $L$ ensures the constancy of $c.L \neq p$ ; for the constancy of $f.S$ we observe that $Y$ is the only vertex whose $f$ -value changes, while $S \neq Y$ because $XS$ has colour $p$ and $XY$ was uncoloured.

(Here we have used the absence of multiple edges.)

In the case $p = c.Y$ we observe that the $p$ -path $XZ \ldots Y$ is replaced by the $p$ -path $XY \ldots Z$ , i.e. we have to demonstrate (2) for the instantiation $p, S, L := c.Y, Y, Z$ , i.e.

$$ f: Y \vee c. Z \neq c. Y, $$

which follows from ${P}{2}$ . Hence ${P}{3}$ is justified.

The axiom of assignment tells us that ${P}{3}$ is for $Y = Z$ a precondition strong enough for the re-establishment of ${P}{0}$ .

For the termination argument we observe that, the function $c$ not being changed, $f$ -values can only be changed by changing edge colours, i.e. by the (un)colouring statement. Comparison of $P2$ and $P3$ shows that it decreases $(\underline{NV} : f.V)$ by 1 (by falsifying $f.Y$ ); hence the repetition terminates.

And this concludes our design of the proof of Vizing's Theorem.

Acknowledgements We thank R.E. Tarjan for having drawn our attention to the ugliness of the existing proofs; for constructive criticism we thank the ATAC - in particular K.L. Calvert and J. Misra - and the ETAC - in particular W.H. J.

Feijen - ; for their active assistance we thank A.J.M. van Gasteren and David Gries.

In retrospect

The above is our nth explanation of the second algorithm we designed to prove Vizing's Theorem. (This algorithm is much better than our first one, which was probably still too much influenced by the published proofs.)

We are very pleased by the modesty of what we needed: the function C, the predicates acc and f , the notion of the p-path , and three variables X,Y,Z of type vertex (of which $x$ is a constant and Z really only a local variable of the repeatable statement).

We also have reservations, for the algo- rithm is probably more subtle than our heuristic explanation suggests. The conclusion that in the repeatable statement the uncoloured edge should be allowed to migrate over the graph is not surprising; the decision to restrict that migration by keeping X constant (and confining Y to range over the neighbours of $X$ ) is much less obvious. (Note that at the beginning of the repeatable statement, the

situation is symmetric in $X$ and $Y$ : they are connected by a path of even length along which the edge colours c.y and c.x alterate.) The only justification we can think of for the optimistic decision to keep $X$ constant is that thus, independently of the size of the graph, the number of possible values of XY is bounded by N. The underlying hope was obviously to prevent the shape of the graph from generating a case analysis.

Moreover it is only fair to say that we worked very hard on our definitions. The a priori restriction to acceptably coloured graphs simplified the introduction of the alternating path; the restriction to graphs with $p \times {X}^{2}$ as well simplified the introduction of the p-path; the formulation of (2) in terms of universal quanhification over the clummy $p$ of type colour simplified its proof of invariance. (It is straightforward predicate calculus to eliminate $p$ from (2). "For each L such that the nonempty cL-path ends at L,etc.,"; in the case $p = c.y$ we have to compare XZ...Y with XY...Z : the end points differ, the colour that alternates with c.x remains the same. Hence the colour p, and not the end point L,should be the dummy in (2).)

We are pleased that we needed only one case analysis and no pictures; we are glad that we could avoid notations such as ${\mu }_{\beta \gamma ,}\left\lbrack {a,z}\right\rbrack$ -used by Claude Berge-, but we would like to master a more calculational style of reasoning about graphs.

Austin, 22 September 1990

Josyula R. Rao prof. dr. Edsger W. Dýkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188 USA