We at Imandra just open sourced minisat-ml , a reimplementation of Minisat 2.2 in OCaml. The goal is to experiment with the performance difference between C++ and (low level) OCaml that stays as close as possible to the original.
The report provides more detailed explanations on the porting process, as well as some experimental results. Personally I think it’d also be an interesting sample point for flambda and other performance tools of the ecosystem, since minisat 2.2 is a fixed target in a field known to require very high performance.