search

ekmett / ersatz

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

add function to call depqbf with extra arguments #90

Closed jwaldmann closed 4 months ago

jwaldmann commented 4 months ago

fixes #89

RyanGlScott commented 4 months ago

Thanks! This is a welcome addition.

Part of me wonders if we should also change depqbfPath to always pass --no-dynamic-nenofex, for the sake of having better defaults. Are there any downsides to doing this? You mention in the Haddocks that depqbf 6.03 or later require this argument—do older versions of depqbf break if you pass this as an argument?

jwaldmann commented 4 months ago

do older versions of depqbf break if you pass this as an argument

experiments show that the argument appeared in depqbf version 6.02 (release date: Mar 27, 2017) and is required to extract a model. older versions don't accept it (they core dump).

My patch is just an easy stop-gap measure. Perhaps we should orient for a different default solver, see https://www.qbflib.org/qbfeval2022_results.php (caqe-bloqqer-qdo).

Ideally, code in ersatz should not depend on specific solvers at all, because they will adhere to the specification of the respective competititons (https://www.qbflib.org/qdimacs.html#output already linked in ersatz source code)