Add functions for writing *SAT problems to a dimacs file

[emeinhardt]

This PR adds functions to facilitate writing a problem to a *dimacs file. The intended use cases include experimentation with command-line options to solvers with existing ersatz support +/- experimentation with solvers that don't have explicit ersatz support.

[RyanGlScott]

Thanks, these look reasonable to me. It might also make sense to use writeDimacs' and friends in the implementation of some of the solvers:

• https://github.com/ekmett/ersatz/blob/d12434c98e08f8dc180c99f155e1e9d92c96c1cc/src/Ersatz/Solver/Z3.hs#L33-L34
• https://github.com/ekmett/ersatz/blob/d12434c98e08f8dc180c99f155e1e9d92c96c1cc/src/Ersatz/Solver/DepQBF.hs#L53-L54
• https://github.com/ekmett/ersatz/blob/d12434c98e08f8dc180c99f155e1e9d92c96c1cc/src/Ersatz/Solver/Minisat.hs#L54-L55
• https://github.com/ekmett/ersatz/blob/d12434c98e08f8dc180c99f155e1e9d92c96c1cc/src/Ersatz/Solver/Minisat.hs#L90-L91

[jwaldmann]

looks useful. for calling other solvers,see also https://github.com/ekmett/ersatz/issues/44 . Currently, I am writing solveWith (cryptominisat5Path "kissat") $ do ... which looks strange, and there's no way to set options.

[emeinhardt]

I've updated the Solver modules as well, per suggestions.

With respect to passing options to solvers from within ersatz, I'd like that feature (and would like to call Kissat from ersatz) and could submit a PR, but would expect that to need an appropriate error type and some decision or statement of preference (as minimal as "use mtl/transformers"?) about error handling types.

Right now I see error in the transitive-closure PR for array shape mismatches and an IOError in Ersatz.Solver.Common when no solver is found — not much to rewrite if the goal is to move towards something else.