search

TeamAmalgam / kodkod

Kodkod relational model finder
Other
3 stars 0 forks source link

Incremental SAT solver support #7

Closed mhyee closed 11 years ago

mhyee commented 11 years ago

Kodkod 2.0 provides access to incremental SAT solvers. Based on the nature of GIA, this should immediately give us significant performance improvements.

Some (but not all) of the Kodkod SAT solvers support incremental adding of constraints. We'll need to investigate, and try to get this working with GIA.

mhyee commented 11 years ago

It looks like Sat4J supports incremental solving. This is good enough for now.

We'll also need to make sure we can select IGIA instead of GIA. Possibly through some argument to Alloy.

mhyee commented 11 years ago

Right now we see up to 4x speedup, but for some models it actually slows down.

We think this is because of garbage collection, but we need to investigate. It might also be worth trying to use MiniSat instead of Sat4J.