A closely related technique to SAT solvers is the "Constraint Satisfaction Problem" which I've been looking into recently.
Constraint Programming and SAT are BOTH NP-complete problems, and as such, they are mathematically equivalent. However, its sometimes more "obvious" to write problems in one form vs the other.
For example, Sudoku is simply written 27 constraints:
* All Different (X11, X12, X13, X14, X15, X16, X17, X18, X19)
* All Different (X21, X22, X23, X24, X25, X26, X27, X28, X29)
...
* All Different (X11, X21, X31, X41, X51, X61, X71, X81, X91)
...
* All Different (X11, X12, X13, X21, X22, X23, X31, X32, X34)
...
etc. etc.
Then define each "X" variable as "between 1 and 9" and bam, you're done with defining the problem in terms of "Constraints".
Representing Sudoku as a SAT problem is possible of course, but its just... harder. It just feels more humanly natural to represent Sudoku in terms of constraints. Or maybe not. Read "Part 1" if you want to see how the original blogger solved it in terms of 3-SAT (https://codingnest.com/modern-sat-solvers-fast-neat-underuse...)
Anyway, just plugging in a similarly fast, neat, and underused (and mathematically equivalent) solver to what the blogpost talks about. I personally don't know too much about SAT-solvers or their algorithms, aside from "They're same same, but different" to Constraint Programming.
For those having fun with the rabbit hole that is solving sudoku and similar problems with a computer, I highly recommend taking a look at Knuth's Dancing Links. I had fun with the idea here: http://taeric.github.io/Sudoku.html
His latest book which is due out this year goes into quite a lot of depth specifically on sudoku. The one he released last year using SAT solvers has a few fun exercises. In particular, he uses a SAT solver to construct sudoku boards that have a unique solution, but do not have any forced moves on the board.
PiCat seamlessly integrates with solvers. MiniZinc does need a solver capable of processing it, but it's fairly easy to do so. I just thought this kind of problem was a bit easier to describe more generally in a constraint form than SAT (which takes a bit of effort).
I see your point -- CNF as a modeling language leaves a lot to be desired. What I like about this article is that it uses CNF anyway and takes you through the hard work you'd have to do to express a problem that way. I didn't know about the Tseytin transformation, for instance, so I'd given up on using CNF because of the exponential blowup in my constraints. I probably still won't be using SAT solvers directly, but it's nice to learn how they work. It's like knowing an assembly language for constraint satisfaction.
I have been delving into Fstar [1] which has an SMT backend and provides a means of program verification. Fstar programs can then be code extracted to OCaml or Fsharp.
I think the combination of SAT solving, and a formal language like F* that can create executable OCaml or Fsharp code will be very useful in creating a pragmatic path to verified programs.
[1] https://www.fstar-lang.org/
Edit: I wanted to add that I prefer the Lisp syntax of SMT to the python, but that's based upon personal bias. However, a Lisp-like syntax was chosen due to the ease of parsing Lisp s-expressions.
