Agreed; another useful technique is "Feed it to a heuristic solver". Heuristic solvers tend to be easier to program and reason about than a SAT solver, since you can use your existing domain model. Moreover, your scoring function look like a typical function that can call third party libraries (as heuristic solvers see the function as a black box usually). Heuristic solvers beat SAT solvers in cases like VRP, whereas SAT solvers are usually better at bin packing.
If you want to try to implement one yourself, a simple one is Simulated Annealing [1]. The core algorithm shouldn't be more than 30 lines of code; it is simple to implement. If you want to try an existing library, you can try Timefold Solver [2] (disclosure: I work for Timefold).