Dear all, I am releasing a preliminary version of "satchmo", a monadic library for encoding boolean and integral number constraints to CNF-SAT. It uses minisat (http://minisat.se/) as a backend solver. http://dfa.imn.htwk-leipzig.de/satchmo/ http://hackage.haskell.org/cgi-bin/hackage-scripts/package/satchmo Enjoy - J.W. PS: what would be the proper top level hackage module name for this? I guess it could be Constraint.SAT.Encoding ...