random seeds in solvers

[algebravic]

Most (all?) of the solvers use randomness, and have a command option to set the random seed, for reproducibility. What does pysat do about that? It would be nice to be able to specify this.

[alexeyignatiev]

Currently, all the randomness is intentionally disabled in PySAT, to ensure deterministic behaviour of the solvers. It could be indeed helpful to have a way to set it in some particular cases, using additional functionality. Note that PRs are more than welcome.

[algebravic]

I've been using pysat (along with the package sacred, to run, and save experiments) to test various encodings in a class of combinatorial problems. The package sacred sets the seeds of the python random and numpy.random generators, to some "randomish" value if you don't specify it explicitly (but it records the setting in a file). I ran exactly the same problem with the same sat encodings a number of times with cadical. About 80% of the time, with the particular encoding it solved in about 2 seconds. However, about 20% of the time it took 120 seconds. So, clearly, the random seed has some significant effect. In those encodings I'm using the seqcounter cardinality encoding. I'm assuming (am I right?) that you don't use any randomness in the cardinality encodings.

[alexeyignatiev]

@algebravic, yes, you are right that CaDiCaL may still be using some of the randomness-tweaking parameters. In practice, I tend not to use CaDiCaL a lot because in incremental settings it is usually outperformed by MiniSat-like solvers. Regarding randomness in cardinality encodings, your assumption is correct that there should be none.

[lou1306]

I'm looking into this matter, although I am attacking Glucose first because I am more familiar with the MiniSat family of solvers. I actually seem to have a workable proof of concept, but before I submit a PR I would like to discuss the API with you.

The relevant members of the Solver class are:

    double    random_var_freq;
    double    random_seed;
    ...
    bool      rnd_pol;            // Use random polarities for branching heuristics.
    bool      rnd_init_act;       // Initialize variable activities with a small random value.
    bool      randomizeFirstDescent; // the first decisions (until first cnflict) are made randomly
                                     // Useful for syrup!

(This is Glucose 4.2.1 but other Glucoses and MiniSat are pretty similar).
These are all public, and I assume the solver support changing them on-the-fly, i.e., they need not be set at construction time. Therefore I suppose I can create new methods in Glucose421 and other classes to manipulate these members:

s = Glucose42(...)
s.set_rnd_pol(True)
s.set_random_seed(4.2)
s.set_random_freq(1)
s.solve()

In my proof of concept I instead added extra arguments to the __init__ method. If you'd rather have an API like the one above, I can do some (pretty quick) refactoring and send you a PR.

[alexeyignatiev]

Thanks, @lou1306. It would be preferable to implement this via a number of setters rather than a list of additional parameters to the initialiser. This way it would not complicate the generic solver's constructor.