I finally wrote a post on how to write SMT solvers in #OCaml with mSAT: here, a SAT-powered Sudoku solver in 260 lines, with an in-browser demo.
https://blag.cedeela.fr/sudoku-msat/ . (Also my first usage of typescript.)
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!