search

msoos / cryptominisat

An advanced SAT solver
https://www.msoos.org
Other
825 stars 184 forks source link

"greedy unbound" for speeding up finding solutions in bulk #421

Closed egri-nagy closed 5 years ago

egri-nagy commented 7 years ago

Following an off-site discussion, this issue is about the possibility of trying to unbind variables (make them Undef/) such that the solution is still valid, in the context of obtaining a large number of solutions.

msoos commented 7 years ago

The expected timeline is possibly next week, most likely the week starting Sept 11. I'm sorry, I'll be on holidays in the coming days! I hope it's not too late until then.

egri-nagy commented 7 years ago

No worries. I got very busy (accepted talk for clojure/conj), so it will be some time before I can return to this problem. best @

On Fri, Aug 25, 2017 at 5:18 AM, Mate Soos notifications@github.com wrote:

The expected timeline is possibly next week, most likely the week starting Sept 11. I'm sorry, I'll be on holidays in the coming days! I hope it's not too late until then.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/msoos/cryptominisat/issues/421#issuecomment-324745533, or mute the thread https://github.com/notifications/unsubscribe-auth/AGiektjo8zjZFTYPvCeFb7EYYmsz7ALJks5sbdqbgaJpZM4O9_tM .

msoos commented 6 years ago

I can't do this... I tried a few times but every time it's a mess because of variable elimination and solution extension. I don't know what to do... I would really need to think about how solution extension can be done with this in mind :S Breaking variable elimination is essentially not an option as it's super-important for speed.

egri-nagy commented 6 years ago

I see. Thanks for the effort! Do you think it is generally true that finding a solution and finding all solutions cannot be optimized at the same time?

msoos commented 6 years ago

Well, there are exact counters out there, e.g. sharpSAT if you want to do that :) Or, much-much more interestingly, there is approxMC which is using an old CryptoMiniSat :)

msoos commented 5 years ago

I am closing this because exact counters have been improving over the years, for example, we just published work into IJCAI to improve exact counting with SharpSAT. Furthermore, approximate counting has significantly improved over the years. Getting "GreedyUnbound" right is very-very messy and currently I am not even sure it's possible. Hence, I'd rather not attempt doing it. Instead, I'll let exact counters such as SharpSAT and approximate counters such as ApproxMC do the heavy lifting.

I hope this is not too big of a disappointment and I hope you will enjoy using ApproxMC or our improved SharpSAT :) Let me know if you need any help! Cheers,

Mate