You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I want to use mSAT to solve (a lot of) quite small CNFs (~40 variables), but I want to get non-deterministic solutions (e.g. a uniform pick from the set of solutions). Could I (easily) do that with this library? I appreciate all suggestions :).
The text was updated successfully, but these errors were encountered:
I haven't yet thought about this use-case.
Currently, I'd say you can get some amount of non-determinism by randomizing the order in which you add clauses to the solver (which will in turn randomize the order in which the variables are added to the heap, and thus which variables are decided on when there is a tie in the activity score, which is what should happen for all the first decisions, which is likely to significantly influence how the solver will explore the clauses, and thus the solution returned), but I haven't tried it before, so it'd probably be best to try it on some small hand-crafted examples and see whether it works.
I want to use mSAT to solve (a lot of) quite small CNFs (~40 variables), but I want to get non-deterministic solutions (e.g. a uniform pick from the set of solutions). Could I (easily) do that with this library? I appreciate all suggestions :).
The text was updated successfully, but these errors were encountered: