Pass options to solver

[ChrisJefferson]

I want to be able to set the random seed of the solver -- now I could add a special option for this, but it might be nicer to just be able to call parseOptions for every solver, maybe on construction of solver?

I was going to try this myself, but it would require turning a python string (or list of strings) into a C-like argv (so a list of strings, null terminated), and I'm not positive how to do that.

[alexeyignatiev]

Hi @ChrisJefferson, well, it would be nice to have this kind of control of the solver and be able to set any available parameter. Currently, this is not supported. Unfortunately, I can't do this now but I may look into this when I there is time (not sure when though).

If you want to do it yourself, it should not be too hard. Here is a simple example showing how to pass a string into a C/C++ extension.

[ChrisJefferson]

I started doing this, but it turned out to be messier than I would like.

The problem is the options have to be set per-solver. I added an argument to the constructor to set them, but then realised once you set an option it is set forever and can't be revoked.

So now I'm wondering about something like pysat.set_commandline("g4", "-rnd-init"), but wanted to check if that's OK.

Also, if someone starts playing with all the options they can probably make pysat very upset, but I think we just have to put a warning on.

[alexeyignatiev]

I am not sure this is the best solution. I would rather prefer to have something like solver.set_option('rnd-init', True) where solver is a concrete object of class Solver.

[ChrisJefferson]

If one wants to hook into the parseOptions function most of the solvers implement, that requires you call it before you construct the solver, and then it changes the value forever.

You could of course manually write wrappers around all the various values solvers provide, but I'm not sure which ones you can change in advance -- 'rnd-init' for example (the one I care about) I think needs setting before the constructor of the solver is called.

[alexeyignatiev]

No, I meant to set the options after the solver is created. Something like:

g = Solver(name='g3')
g.set_option('rnd-init', True)
g.set_option('rnd-init', False)
g.delete()

[alexeyignatiev]

Regarding "which ones you can change in advance", this is indeed unclear. Dealing with all the possible solver options is complicated and messy and this is the reason for it to be missing now.

[ChrisJefferson]

Just in case anyone reads this and really wants it, I have a horrible example at:

https://github.com/ChrisJefferson/pysat/tree/glucose-set-arguments , which adds a function pysolvers.glucose41_set_argc, which takes a list of strings. However, this function has various issues (some options make pysat crash, passing ["--help"] makes python exit), so it's probably too unsafe as present.

[alexeyignatiev]

Well, it should have nothing to do with Glucose's command line. We should pick a set of parameters that may be worth accessing for changing the behavior of the solver and have methods to set them. The set of parameters varies for various solvers.