search

ekmett / ersatz

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

support cryptominisat5[try again] #26

Closed cutsea110 closed 5 years ago

cutsea110 commented 7 years ago

Hi.

I've fail to parse cryptominisat5's output solution file. This patch fix it.

jwaldmann commented 7 years ago

I support the idea. But can we make this in a more general way, and name it appropriately. What you implemented does work for any solver that adhers to the recent SAT competition specification (e.g., lingeling).

So I expect to be able to call solveWith (solver "lingeling") $ do ..., instead of, or in addition to, hard-coding solver names in the Ersatz API, and this solver should not live in ...Minisat.

The competition spec actually says that there is one argument (the CNF file name) and output goes to stdout (so we could read it with System.Process.Bytestring from process-extras). Or does it not? It's implied in http://baldur.iti.kit.edu/sat-competition-2016/index.php?cat=submission (outputting proofs).

glguy commented 5 years ago

32daf1252458a6ab96b24e4ae59373f18c43dc5f adds cryptominisat5 support. I believe that makes this PR redundant