i wonder if they are any approaches formulating a Vehicle-Routing-Problem with Time-Windows (VRPTW) (as a decision problem) as a SAT/SMT instance? (alternative: TSP)
"Is there a valid solution visiting all customers within their time-windows with n=10 vehicles?"
This decision problem could be useful for a first step minimizing the number of vehicles used.
I don't have any experience with SMT, but i expect it to be necessary if we want to handle coordinates/times as real numbers.
Usually all the TSP/VRP formulations are done in the mixed-integer-programming domain, but i wonder if a sat/smt formulation could be competitive (in terms of solving time in practice) for the decision problem above.
So what do you think:
- do you know any references?
- do you think a sat/smt approach could be competitive?
- anything else you want to mention?
Thanks for all your input.
Edit: As i mentioned the TSP as a more common problem in TCS which is related to the VRPTW, i should also mention the Job Shop Scheduling problem, which is the other "partial problem" in the VRPTW. Maybe the researchers in this field tried something with SAT/SMT.