Solver version information

[algebravic]

I've been using pysat to do some systematic exploration on the effect of encodings for a particular class of combinatorial problems. I've run a bunch of solvers with all combinations of the various problem generation options for the CNF. For one particular instance I've found that cadical is best. However, I just ran the cnf generated by that, written out with the to_file option on the current version of cadical on github, and found a big difference: the version in pysat takes 12 seconds and the version on github takes 68 seconds. Upon further investigation, I found that the version of cadical on github is 1.3.1, but (and this was a bit tedious -- I had to download the source code tar ball for cadical from the pysathq/pysat github) I found that the version that pysat was using was 1.0.3. It would be nice if each solver could return its versin information from a method call. Could this be put in as an enhancement. This would be a great help for people reporting the results from using pysat

I'm still mystified why the later version of cadical did so much worse. Also, Armin Biere mentioned his recent talks at the Simons Institute that he's written a new solver called satch -- meant to be something like minisat was -- a clean small version which one can fiddle with. It's at https://github.com/arminbiere/satch . When I ran the CNF I described above on satch it took only 1.2 seconds! That might be a good solver to add to pysat.

[alexeyignatiev]

It would be indeed nice to have the version information available on request. I will consider adding it. Thanks for the suggestion.

Regarding the newer version of CaDiCaL, you can never be sure that the newer version of a solver will always be better than the older version. We are dealing with NP-complete problems here and rely on heuristics, which may (or may not) work well in some particular cases.

As for satch, I am not sure it supports any incrementally. If not, it does not make much sense to me to include it in PySAT.

[algebravic]

@alex, Thanks. I think that the best way (if possible) would be for each solver (in C or C++) have a VERSION external symbol which you could access. Absent that, of course you can add a python method by hand. As far as satch, it appears that it doesn't yet have full incrementality, but, according to the README, they intend to add it. Also, is there a way to pass options to solvers? I found, running the standalone cadical with my example, that passing the --sat option to it decreased its run time to 2.9 seconds. That was a big difference, and it would be nice to be able to do that from within pysat.