I wrote a language some time ago exploring the use of SAT solvers for these types of problems, trying to make writing solvers easy to reason about, never quite took off, but here's what the minesweeper solution looked like: http://sabrlang.org/mine/.

It basically translates the somewhat more complex rules into the simpler SAT rules using minisat. However sometimes needed a generator in python to make the rules :/. But still kinda nice to see it more visually, language looks like this in the end: http://sabrlang.org/code/mine/source.txt. It basically lists the requirements for middle, edge and corner blocks, than says where those blocks are on the "board."

Kinda fun, though arguably somewhat restrictive. One of the more fun ones I think is the rubiks cube: http://sabrlang.org/rubik/.