TeamAmalgam / kodkod

Kodkod relational model finder
Other
3 stars 0 forks source link

OGIA: Add exclusion constraints for non-pareto points to global exclusion constraints variable #44

Open joseph39 opened 10 years ago

joseph39 commented 10 years ago

Currently, for OGIA, exclusion constraints for only the Pareto points are being stored in the global variable that is used to find a new starting point. However, this has resulted in different threads using the same exclusion constraints and thus doing exactly the same work, because the thread that initially found the original Pareto point is unable to add new exclusion constraints until it finds a new Pareto point. The algorithm should be changed so that the global variable holding the exclusion constraints be updated as soon as the threads find new non-pareto solutions, allowing other threads to use the most up-to-date exclusion constraints.

In order to minimize the number of clauses that the global variable holds, it should also actively remove exclusion constraints that are dominated by another.