Also if you have thousands of variables, you probably shouldn't be writing SMT statements directly. Usually you have some sort of script for your problem domain that emits SMT then invokes the solver. E.g. the popular SMT solver Z3 has a very simple lisp-like syntax that's easy to emit from a script.
As for changing costs, you might be able to use simple expressions like: costOfShippingXusingZ = 100 - numOfXusingZ * 2
Or you might use "soft constraints" that let you add weights to optional constraints.
It's important to note that with SMT/SAT solvers you generally want to keep your formulas linear or "first-order" which means don't multiply variables together if you can help it.
This might be useful: https://rise4fun.com/Z3/tutorial/optimization
the follow on is that the same program should also process the model (answer) that Z3 produces and render it in a domain-appropriate fashion.
this is easiest if you use something like the python interface to Z3, instead of actually generating SMT-LIB sexps and feeding them to Z3.
The hardest part is getting the model back at the end (well, and making problems that don't scale too badly with N).
However large graphs might not fit in memory.
A* also allows you to find a solution faster by overestimating your heuristic: For example if you multiply your heurisitic with 1.1 you are guaranteed to find a path whose length is within 10% of the shortest path, requiring less CPU time and memory for the search.
If you’re minimizing the cost, shouldn’t this be formulated as an optimization problem?
I've only recently learned about SAT type solvers as MILP/LP problems are very fast and globally optimal, unlike things like A* or Genetic Algorithms. I think GA's are cool because you can write one in less than 1/2 page of Python, where MIP solvers are usually large black-box C codesets (Ex: GLPK, CPLEX, GUROBI, XPRESS, Open-Solver).
Fun to code though!
My only issue with LP and MILP solvers is scalibility. You have none! Multicore doesn't really seem to help any.
My favorite MILP is commercial and perhaps somewhat obscure for general population - Mosek. Any recommendations in regards to other good options? perhaps open source that might be in same or better league.
For more information, see this page: http://plato.asu.edu/guide.html
Any ideas on how to switch to an SAT solver? How would I even write such a large SAT Boolean expression, and how would I tell the SAT solver that the costs will change for each choice depending on business rules and other choices made? It seemed impossible with a SAT system but I assume I’m not familiar enough with the concepts.