I used Picat which provides a uniform API for many different flavour of solvers (e.g. smt module uses z3 underneath): https://gist.github.com/natrys/c19be79ac93578674540cdfa7a0df...

I get instantaneous answer with apparently zero backtrack with both SAT and SMT module. Though I don't know how reliable this statistics is.