Davenport, England, Griggio, Sturm, Tinelli, [2020] “Symbolic computation and satisfiability checking”
A short introduction to the (relatively) current state of the art in the interaction between SAT/SMT solvers and computer algebra systems.
The main direction, as I understand it, is to integrate CASs as domain solvers for SMT, but there is also a movement for algebraic SAT, such as Gröbner basis search in Boolean rings.