A wide range of practical problems can easily be solved by SMT solvers such as z3, cvc5, and STP. The idea is to write out the problem as a system of equations and let the solver automatically find a solution (or prove that no solution exists). Amazon Web Services is currently solving a billion SMT queries per day.
