search

ekmett / ersatz

A monad for interfacing with external SAT solvers
Other
62 stars 15 forks source link

more flexible way of calling other solvers #44

Open jwaldmann opened 4 years ago

jwaldmann commented 4 years ago

We have minisatPath and cryptominisat5Path but that does not allow me to call, e.g., glucose, because it needs an extra option to print the model.

I am thinking of

solverPathOptions :: MonadIO m => FilePath -> [String] -> Solver SAT m

cryptominisat5 = solverPathOptions "cryptominisat5" []
glucose = solverPathOptions "glucose" [ "-model" ]
glueminisat = solverPathOptions "glueminisat" [ "-show-model" ]

for solvers that write to stdout, and print the model in "v ..." lines.

glguy commented 4 years ago

That seems reasonable; would you care to make a PR?

jwaldmann commented 4 years ago

Yes.

Any thoughts on the name (solverPathOptions) and the module (currently, Ersatz.Solver.Minisat)?

The semantics is "a solver that respects SAT-Comp specification"? (cf. http://www.satcompetition.org/2009/format-solvers2009.html) But strictly speaking, "glucose" does not, only "glucose -model" does.

And the "execution environment" (that is, the command line) is not even specified exactly.

emeinhardt commented 6 months ago 
solverPathOptions :: MonadIO m => FilePath -> [String] -> Solver SAT m

One downside is that this requires the user to understand how command line arguments are expected to be tokenized and passed to the solver executable by ersatz for any solver where solver option identifiers and arguments are sometimes/always separated by whitespace instead of (usually) =.

I'd prefer ersatz users be insulated from having to know about or for anything they write to depend on an implementation detail like this that's easy to get wrong, but I'm not sure there's an alternative way to support passing options to solvers besides a proposal that includes or allows for solver-specific configuration details for command-line arguments.

However, I'd like to add support for a more recent QBF solver sometime soon (caqe) and eventually (not soon) support for {exact/projected/approximate/weighted} model counters, so whatever the solution, I'd like something that gracefully permits different solvers to have different behavior while not affecting the usability or maintenance burdens of other solvers.