Z3 is an SMT solver, which means it combines a boolean SAT solver, which is used to solve the boolean structure of the problem, with theory-specific solvers, e.g. bit vectors, or linear equations.
Modern SAT solvers use the DPLL algorithm, which has in turn influenced modern CSP solvers. Wikipedia has a great page on DPLL:
Modern SAT solvers use the DPLL algorithm, which has in turn influenced modern CSP solvers. Wikipedia has a great page on DPLL:
https://en.m.wikipedia.org/wiki/DPLL_algorithm