I just learned about DPLL(T) and the DPLL algorithm in relation to SMT solvers. I have seen z3 referenced in a few places regarding SMT solvers as well.
Wondering what the z3 uses for its algorithms at a high level for implementing the SMT solving. If it is DPLL algorithms, a variation, something custom, a bunch of things, etc. Hoping to learn about the different types of algorithms a modern SMT solver uses.
SMT solvers come from a long line of research in automated reasoning, both in computer-based theorem-proving communities and in traditional mathematical logic. It's impossible to summarize all the algorithms/research in a stack-overflow answer. However, the book http://www.decision-procedures.org/ is an excellent read, and have many references that can help you guide into the literature. (The first edition is already 10 years old, but I see now that they have a second edition that came out in 2016.)