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.