How a SMT / SAT Solver Generates Valuations for this Example

Question

First, an example of a set of constraints which turned out not to be solvable (I don't think):

b < 3 && c + a > 5 && a - b > 2 && c > 1 && b - c > 3

My procedure for solving this is roughly: Okay b is less than 3, and c > 1. 1 + a > 5, so a > 4 in that case. Try 4 - 2 > 2, no that doesn't work, so maybe a is 5, 5 - 2 > 2. Then b - c > 3. 2 - 2 > 3. No, so b must b greater than 3, but we know b is less than 3, so it can't be solved.

Then a simpler example that can be solved.

b < 3 && c + a > 5 && a - b > 2

So say b is 2. Then a - 2 > 2, so say a is 5. Then c + 5 > 5, so say c is 1 as well. Then a = 5, b = 2, c = 1 solves the problem.

In that example, I picked numbers that were close to the boundary, in that they were "just above" the lower bound in the > part. But you could say that a is 100 and c is 100. This is a particularly easy example as well.

My question is, how a constraint solver solves this problem. I have been reading about SAT and SMT, and have yet to read the book on decision procedures. However, I understand that SAT solvers solve systems of boolean equations in two ways: (1) by returning yes/no that the system can be solved, or (2) by assigning valuations to each variable in the system so that it satisfies the constraints. I don't know how they do this though. I also understand that SMT solvers are basically a light layer on top of SAT solvers. They allow you to have richer boolean formulas using different "theories" (such as theory of equality, theory of reals, of integers, of lists, etc.). Then you can optionally define how to merge these theories so you can apply the SAT solver on a complicated expression involving e.g. the reals, integers, equality, booleans, and lists or arrays all at once. To me this seems obvious, why wouldn't the constraint solver just work over arbitrary functions and variables, but I'm probably missing something.

I would like to know how to implement something like z3. I assume that each specific theory (such as the theory of strings) is quite complicated, so I didn't want to ask about how to generically solve all the different kinds of constraints. Instead I wanted to ask a simplified down question using basic integer constraints so I can learn the fundamentals of how an SMT / SAT solver works.

As such, the question is basically just that, how a constraint solver solves the second example above. One or two of the algorithms it might use to do so. Specifically, I would like to know how to give some function a set of constraints, and have it give me back valuations for all of the variables. In that regard, the question also entails how the constraint solver picks or decides on the set of values. I have seen it said that it is random, but I would like to avoid that approach if possible. But either way, when it picks a value, wondering how it knows it got a valid one. If it has to recompute all the constraints every time it makes a guess, or can do some sort of optimization. Basically, just how the SAT / SMT solver works.

To keep it simple, I am not looking for a complete explanation of how all aspects of solving the problem work. Just more a high level introduction to the algorithms and how they go about selecting the values and returning the valuation. Once I understand that then I figure understanding the more complicated theories like the theory of strings will make more sense.

I am asking because I can't tell based on my reading so far if it all really just boils down to apply constraints into a SAT solver, and there are maybe 1 or 2 SAT solving algorithms (DPLL and CDCL I am getting familiar with) for Boolean constraints (plus maybe a few more for generating the test data to solve the constraints). Or am I wrong there, and there is an entire layer of research on top of that (on SMT solvers) where custom decision procedures are the algorithms you want to use, and there are hundreds of them and there's no standard pattern to them. In which case I keep having difficulty imaging how it is possible to solve a constraint system like the one above, or something more complicated with string constraints (matches regex) and other constraints that require complex functions (like something is the reverse or sorted version of something else). If there's that much variability then the idea of solving any constraints seems hard.

Basically what I am looking for is a description of an implementation. I have read many papers so far but they have mostly been too high level to apply it.