I've used Google's ORTools and Microsoft Z3. If you need to input a lot of variables, I found Z3 to be better since it took SMTLIB formatted text as one big chunk- rather than numerous API calls which each suffer native binding overhead. Z3 can also iteratively solve, where you can append additional constraints and rerun the solver from its current position- I don't think ORTools had this feature.