TeamAmalgam / kodkod

Kodkod relational model finder
Other
3 stars 0 forks source link

OGIA: Exclusion constraints are "not dominated by X and does not dominate X" #47

Open mhyee opened 10 years ago

mhyee commented 10 years ago

This could be an enhancement to OGIA, or a new algorithm. This change makes it a lot more like PGIA.

When starting off our N threads, we find N different starting solutions and let the threads go from there. The constraints we use are "is not dominated by a starting solution." However, if we make the constraint "is not dominated by a starting solution and does not dominate a starting solution", this guarantees that each starting solution (thread) will yield a unique Pareto point.

We can do the same when a thread has finished and needs to find a new starting solution. This new starting solution cannot dominate any of the "current" solutions used by the other threads, and cannot be dominated by those other solutions.

(Each thread has a "current" solution it is trying to dominate. We can update this "current solution" each time we find a better one, and use that solution for our constraints.)

This idea is very similar to #44. However, we add an additional constraint.

This idea is also similar to PGIA (#32) in that we avoid overlap. Instead of partitioning the space up front, we partition it as needed. This way, we avoid the dependency issue, and we also avoid sending a thread into a partition that doesn't have solutions.

(I haven't given this idea much more thought than what I've described. In particular, I haven't spent too much time thinking about this in three or more dimensions.)

cpkleynhans commented 10 years ago

We may even want to use these new exclusion constraints with the pareto-points. Currently we only exclude the area that the pareto-point dominates, however we could exclude the area dominated by the pareto-point as well. This could allow the SAT solver to more quickly set some bits to 0 since it will have an upper bound on some of the metrics.