Last time we had a look at a very crude model for growing graphs for the Travelling Salesman Problem (TSP). I neglected to actually visualize what the solutions looked like, so here is a rendering of a couple:

Not very complex indeed... So what seems to be the problem here? Well, the model itself is very exhaustive, so it will generate any conceivable graph on the input domain. The single model rule is generic on the full input domain:

config Grid20x20: Main

{

action abstract static void TravelingSalesman.InsertVertex(int x, int y)

where x in {0..19}, y in {0..19};

}

This means that for each state Spec Explorer will try X * Y rules, so for larger input domains like 20x20, it takes forever to explore a state fully. What we are interested in with the TSP is not to construct a plethora of simple graphs, but to generate high complexity graphs (because they are much harder to solve). So what we need is a depth-first search (DFS), luckily Spec Explorer allows us to do just that using a config switch:

config Main

{

...

switch DepthFirst = true;

...

}

Unfortunately it turns out that the DFS exploration uses an “optimized” version of DFS, causing it to always fully explore each state it visits, instead of immediately exploring from newly discovered states. Not that it’s going to show the extra states that got explored, they are simply hidden away until they get fully explored much later in the process (sorry, guys but that’s just silly). Anyway, that is exactly what we wanted to avoid, because even when using DFS exploration on a 10x10 grid it will take hours to generate graphs with 10 vertices.

The combination of a large input domain coupled with the design of the exploration engine of Spec Explorer, makes it infeasible to find larger graphs this way.

Let’s investigate a different approach. The underlying problem is that we are giving the model too much freedom. Instead of allowing it to add a vertex at any grid point, we can turn the picture around, and instead model the splicing of an edge directly. The process goes like follows:

a) Select any existing edge

b) Splice it by two parameters

a. Alpha determines where to insert a splicing point along the edge

b. Beta determines the perpendicular distance from the splicing point to the new point

c) Take the nearest grid point to the decimal point

d) Grow the graph by trying to insert a vertex at that point

The implementation of splicing goes as follows:

public class Edge

{

public Vertex P1;

public Vertex P2;

public Vertex Splice(double alpha, double beta)

{

// Find splicing point

double spx = (P1.X + P2.X) * alpha;

double spy = (P1.Y + P2.Y) * alpha;

// Project perpendicularly

double ex = -(P2.Y - P1.Y);

double ey = P2.X - P1.X;

double px = spx + beta * ex;

double py = spy + beta * ey;

return new Vertex((int)Math.Round(px), (int)Math.Round(py));

}

}

The signature of the model rule looks like:

action static void TravelingSalesman.SpliceEdge(int index, double alpha, double beta);

A clear benefit of this implementation is that the complexity of the rule is independent on the grid size, thus we can extend our grid to be very large and still be able to explore the full state-space within reasonable time.

A down-side is that now we have an infinite number of possible inputs on the alpha and beta variables, but we can fix those in the configuration.

Of course, just using the SpliceEdge rule will not work, because we require one edge to start with, but we can easily construct an initial edge using our InsertVertex rule. Thus the machine we explore looks like this:

machine FixedTriangle() : Main where ForExploration = true

{

InsertVertex(3,3) ; InsertVertex(16,7) ; InsertVertex(8,16)

}

machine Splicing() : Main where ForExploration = true

{

(FixedTriangle ; SpliceEdge(_,0.5,0.35)* ; Solve) || TravelingSalesManModel

}

Notice how this machine obtains the desired result using model slicing, to both limit the input domain for SpliceEdge as well as construct a fixed starting triangle to splice from. The starting triangle looks like:

Exploring this on a 20x20 grid yields:

Using this approach we can easily generate graphs containing 10 vertices. A subset of the constructed graphs can be seen here (the starting triangle is shown in gray):

Some interesting things can be seen from these graphs. Only two of the edges are ever spliced, the left-most edge cannot be spliced as the resulting vertex is invalid under the InsertVertex rule. Also, the top-most edge is always spliced in-wards, whereas the right-most edge is spliced out-wards. The first problem stems from the magnitude of the b parameter which is too large to produce valid slices, it would be beneficial to vary the magnitude of the input value. The second problem is that b > 0, thus the algorithm will always splice in a fixed direction, again we should allow negative values as well.

Lifting our first limitation we allow b to be either 0.35 or -0.35:

config Config20x20: Main

{

action static void TravelingSalesman.InsertVertex(int x, int y)

where x in {0..19}, y in {0..19};

action static void TravelingSalesman.SpliceEdge(int index, double alpha, double beta)

where alpha in {0.5}, beta in {0.35,-0.35};

}

And using the following machine definition:

machine Splicing() : Main where ForExploration = true

{

(FixedTriangle ; SpliceEdge(_,0.5,_){2} ; Solve) || TravelingSalesManModel

}

We generate much more diverse graphs:

This is already much better! Let’s see how far we can drive this:

This is a partial explore using DFS on the machine. The produced graphs have up to 16 vertices in them:

One short-fall of this approach is that the model splices the edges into finer and finer pieces without adding much complexity to the graph. The problem arises when we get close to the boundaries of the grid, and when the rounding of the computed point causes it to snap back on the edge that we are splicing. Of course, we can lift this constraint by expanding the size of the grid, but another approach could be to work on having a floating-point value grid, which we will explore in the next post, where I still owe you the proof for the splicing algorithm.

**Conclusion**

We saw how the design of Spec Explorer makes it infeasible to grow our original implementation to larger size grids because the number of valid inputs for any given state grows with the number of grid points. This limitation was lifted by changing the model to start out from three fixed points (using model slicing) and then expanding it by splicing only existing edges. The number of inputs using this approach grows by one for each successful model rule. We were able to generate graphs of higher complexity with this approach within reasonable time (minutes).

[1] Traveling Salesman Re-model

[1] Traveling Salesman Re-model

## No comments:

## Post a Comment