Using Saffron to solve the N Queens Puzzle

package showcase.nqueenspuzzle;

import java.util.ArrayList;
import bits.BooleanLiteral;
import bits.Conjunction;
import bits.INaturalNumber;
import bits.IProblem;
import bits.IProblemMessage;
import bits.Problem;
import naturalnumbers.NaturalNumber;
import naturalnumbers.NaturalNumberAbsoluteDifferencer;
import naturalnumbers.NaturalNumberBounder;
import naturalnumbers.NaturalNumberPair;
import naturalnumbers.NaturalNumberUnequalizer;

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

        int N = 10; 

        /** 
         * Set globals:
         */

        NaturalNumber.setLargestNaturalNumber(N - 1);

        /**
         * Create Saffron objects and arrays:
         */

        NaturalNumberPair[] placement = new NaturalNumberPair[N];
        for (int i = 0; i < N; i++)
        {
             placement[i] = new NaturalNumberPair(new NaturalNumber(), new NaturalNumber());
        }    

        ArrayList parray = new ArrayList();  

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

        for (int i = 0; i < N; i++)
        {
            parray.add(new NaturalNumberBounder(placement[i].getFirst(), N - 1));
            parray.add(new NaturalNumberBounder(placement[i].getSecond(), N - 1));
        }

        for (int i = 0; i < N; i++)
            for (int j = i + 1; j < N; j++)
            {
                parray.add(notAttacking(placement[i], placement[j]));
            }

        /**
         * Create the Conjunction of all of these constraining problems:
         */

        IProblem problem = new Conjunction(parray);

        /**
         * Solve the Conjunction:
         */

        IProblemMessage s = problem.findModel(Problem.defaultSolver());
        if (s.getStatus() == IProblemMessage.SATISFIABLE)
        {
            BooleanLiteral.interpret(s.getLiterals());
            System.out.println("\n\tSOLUTION\n--------------------------");
            for (int i = 0; i < N; i++)
            {
                System.out.println("Queen on row " + placement[i].getSecond() + ", column " + placement[i].getFirst());
            }

            Object[][] board=new Object[N][N];
            for (int i = 0; i < N; i++)
                for (int j = 0; j < N; j++)
                {
                    board[i][j]=" .";
                }
            
            for (int i = 0; i < N; i++)
            {
                board[(int) placement[i].getFirst().getValue()][ (int) placement[i].getSecond().getValue()]=" Q";
            }
            
            for (int i = 0; i < N; i++)
            {
                System.out.print("\n");
                for (int j = 0; j < N; j++)
                {
                    System.out.print(board[j][i]);
                }
            }
            
        }
        else
            System.out.println("No solution.");

 

OUTPUT:


    SOLUTION
--------------------------
Queen on row 1, column 2
Queen on row 7, column 4
Queen on row 3, column 7
Queen on row 2, column 5
Queen on row 5, column 0
Queen on row 9, column 3
Queen on row 6, column 8
Queen on row 0, column 6
Queen on row 4, column 9
Queen on row 8, column 1

 . . . . . . Q . . .
 . . Q . . . . . . .
 . . . . . Q . . . .
 . . . . . . . Q . .
 . . . . . . . . . Q
 Q . . . . . . . . .
 . . . . . . . . Q .
 . . . . Q . . . . .
 . Q . . . . . . . .
 . . . Q . . . . . .

New location for future posts

This blog has been rehosted on Wordpress. From now on, posts will appear at http://www.kerrysoileau.com/saffronpreprocessor/

Using Saffron to solve the Set Atomic Basis Problem

Given a set U and a family C of subsets of U of equal size, does there exists a family B of sets (called atoms), not necessarily members of C, such that (1) the members of B are pairwise disjoint, (2) for every member c in C, there exists a subfamily of B whose union is exactly equal to c, and (3) the union of all members of B equals U?

As usual, we model sets as bit strings, where disjoint bit strings are those whose bitwise AND equals the bit string consisting of all zeroes, and unions of bit strings are the result of their bitwise OR.

BitStringBitAtomerDemo.java

package showcase.bitstringbitatom;

import java.util.ArrayList;

import utility.Bitstrings;
import bits.BooleanLiteral;
import bits.Conjunction;
import bits.IBitString;
import bits.IProblem;
import bits.IProblemMessage;
import bits.Problem;
import bitstrings.BitString;
import bitstrings.BitStringBitAtomer;
import bitstrings.BitStringFixer;

public class BitStringBitAtomerDemo extends Problem implements IProblem
{
public static void main(String[] args) throws Exception
{
IBitString[] C = new IBitString[5];
for (int i = 0; i < 5; i++)
{
String str = Bitstrings.randomBitstring(12);
C[i] = new BitString(str);
}

System.out.println("INPUT STRINGS:");
for (int i = 0; i < C.length; i++)
{
System.out.println(C[i].toBits());
}

IBitString atomBitString = new BitString(C[0].size());
ArrayList<String> atoms = new ArrayList<String>();
for (int pos = 0; pos < C[0].size(); pos++)
{
IProblemMessage s = new Conjunction(new BitStringFixer(C),
new BitStringBitAtomer(C, pos, atomBitString))
.findModel(Problem.defaultSolver());
if (s.getStatus() == IProblemMessage.SATISFIABLE
&& s.getLiterals().size() > 0)
{
BooleanLiteral.interpret(s.getLiterals());
String hsb = atomBitString.toBits();
if (!atoms.contains(hsb))
{
atoms.add(hsb);
}
}
else
System.out.println("No solution.");
}

System.out.println("\nOUTPUT ATOMS:");
for (int i = 0; i < atoms.size(); i++)
{
System.out.println(atoms.get(i));
}
}
}

BitStringBitAtomer.java

package bitstrings;

import bits.BitFixer;
import bits.Conjunction;
import bits.Disjunction;
import bits.IBitString;
import bits.IProblem;
import bits.Problem;
import bitstrings.BitString;
import bitstrings.BitStringAnder;
import bitstrings.BitStringEqualizer;
import bitstrings.BitStringNoter;
import exceptions.bitstrings.BitStringBitAtomerException;

public class BitStringBitAtomer extends Problem implements IProblem
{
public BitStringBitAtomer(IBitString[] bitStrings, int pos, IBitString atom)
throws Exception
{
if (bitStrings.length == 0)
throw (new BitStringBitAtomerException(
"IBitString or IBooleanVariable array of zero length was passed to constructor."));
if (atom == null)
throw (new BitStringBitAtomerException(
"A null conditionalResult variable was passed to constructor."));
if (atom.size() == 0)
throw (new BitStringBitAtomerException(
"A conditionalResult of size zero was passed to constructor."));

int stagingIndex = 0;
IProblem[] stagingArray = new IProblem[bitStrings.length + 2];

IBitString[] subTotal = new IBitString[bitStrings.length];
for (int i = 0; i < bitStrings.length; i++)
subTotal[i] = new BitString(bitStrings[0].size());

stagingArray[stagingIndex++] = stagingArray[stagingIndex++] = new Conjunction(
// if bitStrings[0][pos] then subTotal[0]=bitStrings[0]
new Disjunction(new BitFixer(
bitStrings[0].getBooleanVariable(pos), false),
new BitStringEqualizer(subTotal[0], bitStrings[0])),
// if !bitStrings[0][pos] then subTotal[0]=!bitStrings[0]
new Disjunction(new BitFixer(bitStrings[0]
.getBooleanVariable(pos), true), new BitStringNoter(
subTotal[0], bitStrings[0])));

for (int i = 1; i < bitStrings.length; i++)
{
IBitString notbits = new BitString(bitStrings[i].size());
stagingArray[stagingIndex++] = new Conjunction(
new Disjunction(new BitFixer(
bitStrings[i].getBooleanVariable(pos), false),
new BitStringAnder(subTotal[i - 1], bitStrings[i],
subTotal[i])),
new Disjunction(new BitFixer(bitStrings[i]
.getBooleanVariable(pos), true),
new BitStringAnder(subTotal[i - 1], notbits,
subTotal[i])), new BitStringNoter(
bitStrings[i], notbits));
}

stagingArray[stagingIndex++] = new BitStringEqualizer(atom,
subTotal[bitStrings.length - 1]);

this.setClauses(new Conjunction(stagingArray).getClauses());
}
}

OUTPUT:

INPUT STRINGS:
111000011110
101101101011
101010110010
011101011101
111000000111

OUTPUT ATOMS:
100000000010
010000000100
001000000000
000101000000
000010000000
000000100000
000000010000
000000001000
000000000001

Using Saffron to solve the Minimum Test Set problem

Let U be a nonempty set, S a nonempty family of subsets of U. Does there exist a sub family S' of K subsets in S which have the following property: For any distinct elements x and y in U, for every subset T in S', we have either x is in T and y is not, or vice versa.

This problem is clearly equivalent to the following: Given a set S of bit strings of equal length, does there exist a sub family S' of K bit strings in S such that for any distinct bit positions i and j, for every bit string T in S' we have T[i] !=T[j]? The following application solves this equivalent problem.

MinimumTestSetterDemo

package showcase.testset;

import bits.BooleanLiteral;
import bits.Conjunction;
import bits.IBitString;
import bits.IProblem;
import bits.IProblemMessage;
import bits.Problem;
import bitstrings.BitString;
import bitstrings.BitStringFixer;
import bitstrings.MinimumTestSetter;

public class MinimumTestSetterDemo
{
private static String cstring(int i, int j, char c)
{
char[] s = new char[j + 1];
for (int k = 0; k <= j; k++)
if (k == i || k == j)
s[k] = c;
else
s[k] = ' ';
return new String(s);
}

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

int K = 3;

/**
* Set globals:
*/

/**
* Create Saffron objects and arrays:
*/

IBitString[] S = new IBitString[]
{ new BitString("01000"), new BitString("01011"),
new BitString("10100"), new BitString("01100"),
new BitString("11010"), new BitString("10010"),
new BitString("01010") };

int cLength = S.length;
int cSize = S[0].size();

IBitString includedInTestSet = new BitString(cLength);

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

IProblem bsf = new BitStringFixer(S);
IProblem mts = new MinimumTestSetter(S, K, includedInTestSet);

/**
* Create the IProblem of satisfying all of these constraining problems:
*/

IProblem problem = new Conjunction(bsf, mts);

/**
* 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("PROBLEM");
for (int i = 0; i < cLength; i++)
System.out.println("C[" + i + "]=" + S[i].toBits());

System.out.println("\nSOLUTION");
for (int i = 0; i < cLength; i++)
if (includedInTestSet.getBooleanVariable(i).getValue())
System.out.println("C[" + i + "]=" + S[i].toBits());

System.out.println("\nVERIFICATION");
for (int i = 0; i < cSize; i++)
for (int j = i + 1; j < cSize; j++)
{
if (i == j)
continue;
for (int k = 0; k < cLength; k++)
{
boolean ci = S[k].getBooleanVariable(i).getValue();
boolean cj = S[k].getBooleanVariable(j).getValue();

boolean v1 = ci && !cj;
boolean v2 = !ci && cj;
boolean v3 = v1 || v2;
if (v3)
{

System.out.println(S[k].toBits());

System.out.println(cstring(i, j, '^'));
break;
}
}
}
}
else
System.out.println("No solution.");

}
}

MinimumTestSetter.java

package bitstrings;

import naturalnumbers.BitStringTotaler;
import naturalnumbers.NaturalNumber;
import naturalnumbers.NaturalNumberFixer;
import bits.BitFixer;
import bits.Conjunction;
import bits.Disjunction;
import bits.IBitString;
import bits.IBooleanVariable;
import bits.INaturalNumber;
import bits.IProblem;
import bits.Problem;

public class MinimumTestSetter extends Problem implements IProblem
{
public MinimumTestSetter(IBitString[] C, int K, IBitString includedInTestSet)
throws Exception
{
int cLength = C.length;
int cSize = C[0].size();

INaturalNumber NNK = new NaturalNumber(K);

int problemIndex = 0;
IProblem[] problemArray = new IProblem[cSize * cSize - cSize];

for (int i = 0; i < cSize; i++)
for (int j = 0; j < cSize; j++)
{
if (i == j)
continue;
IProblem[] parray = new IProblem[cLength];
for (int k = 0; k < cLength; k++)
{
// (C[k][i] && !C[k][j]) || (!C[k][i] && C[k][j])
IBooleanVariable ci = C[k].getBooleanVariable(i);
IBooleanVariable cj = C[k].getBooleanVariable(j);

parray[k] = new Disjunction(new Conjunction(new BitFixer(
ci, true), new BitFixer(cj, false)),
new Conjunction(new BitFixer(ci, false),
new BitFixer(cj, true)));
}
problemArray[problemIndex++] = new ConditionalDisjunction(
parray, includedInTestSet);
}

this.setClauses(new Conjunction(new BitStringTotaler(includedInTestSet,
NNK), new NaturalNumberFixer(NNK),
new Conjunction(problemArray)).getClauses());
}
}

OUTPUT:

PROBLEM
C[0]=01000
C[1]=01011
C[2]=10100
C[3]=01100
C[4]=11010
C[5]=10010
C[6]=01010

SOLUTION
C[3]=01100
C[5]=10010
C[6]=01010

VERIFICATION
01000
^^
01100
^ ^
01011
^  ^
01011
^   ^
01000
 ^^
01000
 ^ ^
01000
 ^  ^
01011
  ^^
01011
  ^ ^
11010
   ^^

Using Saffron to solve the Set Packing problem

The following is an example of how Saffron can be used to solve the Set Packing problem:  Let U be a nonempty set, S a family of subsets of U. Do there exist n subsets in S which are pairwise disjoint?

This problem is clearly equivalent to the following: Given a set S of bit strings of length len and c>1, do there exist c bit strings in S such that pairwise ORs of distinct bit strings all evaluate to the zero bit string of length len? The following application solves this equivalent problem.

JAVA CODE:

SetPackerDemo.java

package showcase.setpacker;

import naturalnumbers.BitStringPacker;
import naturalnumbers.NaturalNumber;
import bits.BooleanLiteral;
import bits.Conjunction;
import bits.IBitString;
import bits.INaturalNumber;
import bits.IProblem;
import bits.IProblemMessage;
import bits.Problem;
import bitstrings.BitString;
import bitstrings.BitStringFixer;

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

int c = 3;

/**
* Set globals:
*/

/**
* Create Saffron objects and arrays:
*/

IBitString[] S = new IBitString[]
{ new BitString("01001010"), new BitString("10101010"),
new BitString("10000000"), new BitString("00100000") };

IBitString membership = new BitString(S.length);
INaturalNumber K = new NaturalNumber(c);

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

IProblem p1 = Problem.newProblem();
for (int i = 0; i < S.length; i++)
p1 = new Conjunction(p1, new BitStringFixer(S[i]));

/**
* Create the IProblem of satisfying all of these constraining problems:
*/

IProblem problem = new Conjunction(p1, new BitStringFixer(K),
new BitStringPacker(S, K, membership));

/**
* 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("Source Data\n-----------");
for (int i = 0; i < S.length; i++)
System.out.println(S[i].toBits());
System.out.println("\nSolution\n--------");
for (int i = 0; i < S.length; i++)
if (membership.getBooleanVariable(i).getValue())
System.out.println(S[i].toBits());
}
else
System.out.println("No solution.");
}
}

OUTPUT:

Source Data ----------- 01001010 10101010 10000000 00100000 Solution -------- 01001010 10000000 00100000

BitStringPacker.java

package naturalnumbers;

import bits.BitFixer;
import bits.Conjunction;
import bits.Disjunction;
import bits.IBitString;
import bits.INaturalNumber;
import bits.IProblem;
import bits.Problem;
import bitstrings.BitStringDisjointer;

/**
 * A collection C of IBitStrings and a positive integer K: Does C include K mutually
 * "disjoint" IBitStrings?
 */

public class BitStringPacker extends Problem implements IProblem
{
public BitStringPacker(IBitString[] C, INaturalNumber K,
IBitString membership) throws Exception
{
int problemIndex = 0;
IProblem[] problemArray = new IProblem[(C.length - 1) * C.length / 2
+ 1];
problemArray[problemIndex++] = new BitStringTotaler(membership, K);
for (int i = 0; i < C.length - 1; i++)
for (int j = i + 1; j < C.length; j++)
problemArray[problemIndex++] = new Disjunction(new BitFixer(
membership.getBooleanVariable(i), false), new BitFixer(
membership.getBooleanVariable(j), false),
new BitStringDisjointer(C[i], C[j]));
this.setClauses(new Conjunction(problemArray).getClauses());
}
}

Using Saffron to solve the Subset Sum problem

The following is an example of how Saffron can be used to solve the Subset Sum problem: Given a set of nonnegative integers A and a nonnegative integer B, is there a subset A' ⊆ A such that the sum of the integers in A' equals exactly B?

JAVA CODE:

SubsetSumDemo.java

package showcase.subsetsum;

import java.util.ArrayList;
import naturalnumbers.ConditionalAdder;
import naturalnumbers.NaturalNumber;
import naturalnumbers.NaturalNumberFixer;
import bits.BooleanLiteral;
import bits.Conjunction;
import bits.IBitString;
import bits.INaturalNumber;
import bits.IProblem;
import bits.IProblemMessage;
import bits.Problem;
import bitstrings.BitString;

/**
 * Finds a subset of integers that sums to <code>desiredSum,</code> which in
 * this example is 171.
 */
public class SubsetSumDemo
{
public static void main(String[] args) throws Exception
{
/**
* Set Java variables:
*/

int B = 171;

Integer[] A = new Integer[]
{ 99, 92, 93, 85, 35, 27, 9, 2, 88, 90, 90, 1, 83, 45, 63, 83, 33, 21 };

int maxSum = 0;
for (int i = 0; i < A.length; i++)
maxSum += A[i];

/**
* Set globals:
*/

NaturalNumber.setLargestNaturalNumber(maxSum);

/**
* Create Saffron objects and arrays:
*/

INaturalNumber[] dataNNarry = new INaturalNumber[A.length];
IBitString membership = new BitString(A.length);
IProblem[] r = new IProblem[A.length];
INaturalNumber W = new NaturalNumber();
for (int i = 0; i < A.length; i++)
{
dataNNarry[i] = new NaturalNumber();
}

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

for (int i = 0; i < A.length; i++)
{
r[i] = new NaturalNumberFixer(dataNNarry[i], A[i]);
}
IProblem rArray = new Conjunction(r);
IProblem fixW = new NaturalNumberFixer(W, B);
IProblem cAdd = new ConditionalAdder(dataNNarry, membership, W);

/**
* Create the IProblem of satisfying all of these constraining problems:
*/

IProblem problem = new Conjunction(rArray, fixW, cAdd);

/**
* Solve the IProblem:
*/

IProblemMessage s = problem.findModel(Problem.defaultSolver());
if (s.getStatus() == IProblemMessage.SATISFIABLE
&& s.getLiterals().size() > 0)
{
BooleanLiteral.interpret(s.getLiterals());
ArrayList<Integer> Aprime = new ArrayList<Integer>();
for (int i = 0; i < membership.size() - 1; i++)
if (membership.getBooleanVariable(i).getValue())
Aprime.add(A[i]);
for (int i = 0; i < Aprime.size() - 1; i++)
System.out.print(Aprime.get(i) + " + ");
System.out.print(Aprime.get(Aprime.size() - 1) + " = "
+ B);
}
else
System.out.println("No solution.");
}
}

OUTPUT:

93 + 35 + 9 + 1 + 33 = 171

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());
}
}