[balddenimhero]

SAT/SMT solving is indeed a much more structured approach and I agree that the analogy does not work too well for the backtracking part. I think that it rather applies to the well-established incorporation of "restarts" of the search. Even thogh SAT/SMT solving is deterministic it still tries to avoid local maxima via such pseudo-random heuristics.