[fheekgsn] Four color map algorithm?

Now that the four-color map theorem has been proved (Appel & Haken), what is an algorithm that will compute a 4-coloring of a given planar map?  Is it polynomial time?  Are there simple algorithms?  Open-source implementations?

Robertson et al, "Efficiently four coloring planar graphs".