I'm looking at the world of proof assistants and SMT solvers because I have a very hard constraint satisfaction problem, and I'm hitting the limits of what I ca

I'm looking at the world of proof assistants and SMT solvers because I have a very hard constraint satisfaction problem, and I'm hitting the limits of what I can do with a backtracking binary search. This is a new area for me, and it seems like most of the work in this area is being done by academics. I've been reading up on Coq, Lean, Rosette, Z3 and Prolog CLP/FD, but I still don't have a good mental model for this space, so I'm not even sure I've identified the right potential tools for the job.