search

TeamAmalgam / kodkod

Kodkod relational model finder
Other
3 stars 0 forks source link

Finding first Pareto point in PartitionedGIA #29

Closed mhyee closed 10 years ago

mhyee commented 10 years ago

Another step in the "PartitionedGIA" approach.

The idea is that if we have a Pareto point, we can easily partition the search space. However, if we have no Pareto points, what do we do?

We could simply find the first Pareto point the "usual" way, but we might be able to make this faster. Also, we would ideally find a Pareto point that is close to the "centre" of the search space, and would equally partition the space.

One idea is to start, say, three threads with different constraints (better than 0%, better than 30%, better than 60%) and let them search for a Pareto point. When one of them returns with a Pareto point, kill the other two threads. Then use that Pareto point to partition the space.

25 is a prerequisite, but enough of it has been completed. @mhyee will continue working on that (in its own branch, to be merged into this one later) to make the boundary finding more efficient.

The provided "interface" is essentially the boundaryConstraints variable.

mhyee commented 10 years ago

It might be better to branch off off amalgam-partitioned-gia.

Java's ExecutorCompletionService seems to provide a way to start a bunch of threads with tasks, take the first result, and then cancel the remaining threads. We'll need to be careful to make sure the SAT solvers can actually be cancelled.

joseph39 commented 10 years ago

From our OGIA experience, all threads will find same initial Pareto point. This idea wouldn't work unless we can make the SAT solvers truly non-deterministic.