[nanolith]

Start with this.

https://smt.st/SAT_SMT_by_example.pdf

The algorithms behind SAT / SMT are actually pretty straight-forward. One of these days, I'll get around to publishing an article to demystify them.