Using Saffron to solve the Map Coloring problem

The following is an example of how Saffron can be used to color a map. The application finds a valid coloring of the states Florida, Alabama, Georgia, Tennessee, South Carolina, Arkansas, Missouri, Kentucky, Virginia and North Carolina. Available colors are designated with the integers 0, 1 and 2.

JAVA CODE:

MapColorerDemo.java

package showcase.mapcoloring;

import java.util.Arrays;
import java.util.HashMap;
import java.util.HashSet;

import naturalnumbers.NaturalNumber;
import bits.BooleanLiteral;
import bits.INaturalNumber;
import bits.IProblem;
import bits.IProblemMessage;
import bits.Problem;
import bitstringgraphs.BitStringGraph;
import bitstringgraphs.IBitStringGraph;
import bitstringgraphs.MapColorer;

public class MapColorerDemo
{
public static void main(String[] args) throws Exception
{
/**
* Set Java variables:
*/

int numberOfColors = 3;

HashMap<String, String[]> map = new HashMap<String, String[]>();
map.put("Florida", new String[]
{ "Alabama", "Georgia" });
map.put("Alabama", new String[]
{ "Tennessee", "Mississippi" });
map.put("Georgia", new String[]
{ "Alabama", "Tennessee", "South Carolina" });
map.put("Tennessee", new String[]
{ "Arkansas", "Missouri", "Kentucky", "Virginia", "North Carolina" });

HashMap<String, Integer> directory = new HashMap<String, Integer>();
HashMap<Integer, String> yrotcerid = new HashMap<Integer, String>();

HashSet<String> regions = new HashSet<String>(map.keySet());

for (String[] ar : map.values())
{
regions.addAll(Arrays.asList(ar));
}

int numberOfRegions = regions.size();

int index = 0;
for (String s : regions)
{
directory.put(s, index);
yrotcerid.put(index, s);
index++;
}

/**
* Set globals:
*/
NaturalNumber.setLargestNaturalNumber(numberOfColors - 1);

/**
* Create Saffron objects and arrays:
*/
IBitStringGraph skeleton = new BitStringGraph(numberOfRegions);
INaturalNumber[] coloring = new INaturalNumber[skeleton.size()];

/**
* Create problems which constrain the values of these Saffron objects:
*/

for (String s : map.keySet())
{
Integer left = directory.get(s);
for (String currRight : map.get(s))
{
skeleton.connect(left, directory.get(currRight));
}
}

IProblem mapColoringConstraint = new MapColorer(skeleton,
numberOfColors, coloring);

/**
* Create the IProblem of satisfying all of these constraining problems:
*/
IProblem problem = mapColoringConstraint;

/**
* Solve the IProblem:
*/
IProblemMessage s = problem.findModel(Problem.defaultSolver());
if (s.getStatus() == IProblemMessage.SATISFIABLE
&& s.getLiterals().size() > 0)
{
BooleanLiteral.interpret(s.getLiterals());

System.out.println("\tSOLUTION");
System.out.println("----------------+-----");
System.out.println("State   \t|Color");
System.out.println("----------------+-----");
for (int i = 0; i < skeleton.size(); i++)
System.out.println(yrotcerid.get(i) + " \t|  " + coloring[i]);
}
else
System.out.println("No solution.");
}
}

OUTPUT:

SOLUTION
----------------+-----
State           |Color
----------------+-----
North Carolina |  2
Mississippi     |  1
Tennessee       |  0
Missouri        |  2
Kentucky        |  1
Georgia         |  1
Florida         |  0
Alabama         |  2
Arkansas        |  2
Virginia        |  2
South Carolina |  2


MapColorer.java

package bitstringgraphs;

import java.util.ArrayList;

import naturalnumbers.NaturalNumber;
import naturalnumbers.NaturalNumberFixer;
import naturalnumbers.NaturalNumberOrderer;
import naturalnumbers.NaturalNumberUnequalizer;
import bits.Conjunction;
import bits.INaturalNumber;
import bits.IProblem;
import bits.Problem;
import exceptions.bitstringgraphs.MapColorerException;

public class MapColorer extends Problem implements IProblem
{
public MapColorer(IBitStringGraph skeleton, int numberOfColors,
INaturalNumber[] coloring) throws Exception
{
if (skeleton == null)
throw new MapColorerException(
"Null IBitStringGraph passed to constructor.");
if (numberOfColors < 1)
throw new MapColorerException("Bad int passed to constructor.");
if (coloring == null)
throw new MapColorerException(
"Null INaturalNumber[] passed to constructor.");
if (skeleton.size() != coloring.length)
throw new MapColorerException(
"In constructor, the length of the INaturalNumber[] does "
+ "not match the size of the IBitStringGraph.");

IProblem graphProblem = new BitStringGraphFixer(skeleton);

for (int i = 0; i < skeleton.size(); i++)
coloring[i] = new NaturalNumber("coloring-" + i);

INaturalNumber pens = new NaturalNumber();
IProblem pensFix = new NaturalNumberFixer(pens, numberOfColors - 1);

IProblem[] pfix = new IProblem[skeleton.size()];
for (int i = 0; i < skeleton.size(); i++)
{
pfix[i] = new NaturalNumberOrderer(coloring[i], pens);
}
IProblem paletteProblem = new Conjunction(pfix);

ArrayList<IProblem> pList = new ArrayList<IProblem>();
for (int i = 0; i < skeleton.size(); i++)
for (int j = 0; j < skeleton.size(); j++)
{
if (i == j)
continue;
if (skeleton.areConnected(i, j))
{
pList.add(new NaturalNumberUnequalizer(coloring[i],
coloring[j]));
}
}
IProblem coloringProblem = new Conjunction(pList);

IProblem problem = new Conjunction(graphProblem, pensFix,
paletteProblem, coloringProblem);

this.setClauses(problem.getClauses());
}
}