Bounded GIA

[mhyee]

First step to one of our parallelization approaches. I will be working in this branch.

The idea is to optimize each of the metrics individually, to "bound" the metric space. For a problem with two objectives, this basically means drawing a rectangle boundary and only searching within it.

There may be more efficient ways of computing these bounds.

Things to think about:

• If we optimize metric m1 and get value v1, that point may not be a Pareto point. Do we care about this, or should we try to find a Pareto point with value v1?
  • Probably not. This would require extra computation (which scales up with the number of dimensions) and probably won't help. The algorithm will take care of this later on, so there's no point trying to compute the solution in advance.
• How can we gracefully handle single-objective problems?
  • Finding the boundary is (roughly) equivalent to finding the (single) Pareto point. (Roughly because there's 1 extra Sat and 1 extra Unsat call.)
• Do we want to use an incremental solver to find the boundaries?
  • Yes, an incremental solver later seems to help in the handful of tests I ran.
• This method seems like it'll work for higher-dimension problems, but there might be gotchas worth watching out for.
• If there's only one Pareto point, this strategy may waste work.
  • We'll worry about this later.
• This could probably be easily multithreaded. One thread per dimension.
• It may be worthwhile to find lower bounds as well as upper bounds.
• How can we find inexact bounds instead of exact bounds? Will inexact bounds be cheaper to find but still helpful?

[mhyee]

I've made a first attempt at implementing this. See commit 4d3072160f92ff6d6fe38c12b5d6900dee0aad28.

I still need to add unit tests. For the four or five small problems I've tried, things seem to be working. The time between finding all the boundaries and then finding all the Pareto points seems to have improved slightly, but is outweighed by the overhead of finding the boundaries. So Moolloy actually got worse for smaller problems. I don't know if it'll even improve for larger problems.

Finding the boundaries could probably be improved. Right now I'm using a GIA-like approach where I throw a dart, and then I improve it in each of the dimensions. (One quick fix is to use an incremental solver for this.) Once I find a boundary, I do not confirm whether the solution there is a Pareto point, as the difficulty increases exponentially as we add more dimensions. The Pareto point will be found anyway, by the rest of the algorithm.

Single-objective problems seem to be handled fine, as well as single Pareto point problems. However, there's still the overhead of initially finding the boundaries.

I want to play around with this some more before sending a pull request. (In the meantime, I might create a moolloy branch to run some tests on our workers.)

[mhyee]

Commit https://github.com/TeamAmalgam/kodkod/commit/1bb0287bb81400f1a6cb9ecb532ba48dec8c1b07 uses an incremental solver, which really helps.

Commit https://github.com/TeamAmalgam/kodkod/commit/bdf31912b607a3513ce15b5dc8c3376c6d386645 makes the boundary finding multithreaded.

I create a thread pool and pass it to an ExecutorCompletionService. The ECS allows me to add tasks to a work queue, and then consume results from a result queue. I queue up a BoundaryFinder task for each objective (dimension).

This reduces the overhead for finding boundaries. However, in the handful of tests I've tried, the boundaries sometimes improve the overall runtime and sometimes worsen it. Even if you account for the overhead for finding the boundaries.

So by itself, this strategy probably isn't too helpful. (EDIT: Not worthwhile to look at inexact bounds.)