\myheading{Which SAT/SMT solver I should use?}

Unfortunately, the whole field is still in its infancy.
Solvers are continuously evolving and nothing stable yet.

A good idea is just try them all.
Before using their \ac{API}s, first try to encode your problem in \ac{CNF} or SMT-LIB format and just try all the solvers.