Target Phase (non-inverted) + Luby restarts + glues

[msooseth]

This may help. I'll hack it a bit more.

[msoos]

This seems to give a lot of speedup. But maybe there is a bug...

[msoos]

Yep, there is a bug :)

[aehyvari]

Sure! I'll wait for the previous results (cluster's busy...) and then give this one a go!

[msoos]

I think this may be OK now, so when you have time and the cluster is not too busy, it'd be nice to see the performance :)

[aehyvari]

After running all the benchmarks, this starts to look really good. However, I left one question that puzzled me. I have a version that I'm cleaning for opensmt master, we can continue the discussion there once I manage to make the PR.

[msooseth]

I'm super-happy to see that this has improved performance! By the way, with in-line distillation, I am pretty sure we could make the solver about 1.5x faster. Maybe I'll have a go at it sometime later today, see if you like it :) It basically tries to simplify the learnt clauses once in a while. It's super effective. I have been hacking my SAT solver to bits lately and it's helped a lot with the performance of my counting tool... I'm back in the game again :)

[aehyvari]

I'm super-happy to see that this has improved performance! By the way, with in-line distillation, I am pretty sure we could make the solver about 1.5x faster. Maybe I'll have a go at it sometime later today, see if you like it :) It basically tries to simplify the learnt clauses once in a while. It's super effective. I have been hacking my SAT solver to bits lately and it's helped a lot with the performance of my counting tool... I'm back in the game again :)

We should absolutely try it out, sounds great!