Any SAT/SMT formulations of the VRP/VRPTW (TSP, Job-Shop-Scheduling)?

Question

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)

For example:
"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.

Sascha

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.

Answer 1

The big problem I see with a SAT formulation for VRPTW is that you have to discretize time to enforce the time window constraints (unless you encode arithmetic as boolean circuits which I've never seen done but might be worth trying). This means the number of variables becomes much larger as the time window increases affecting performance.

An SMT (Sat Modulo Theory) formulation however wouldn't have a similar issue, I think since you have a propagator for the time window constraints which would return redundant constraints to the SAT solver to incorporate when you branch.

While I don't know of any work using SAT formulations for VRPTW, I know that Peter Stuckey, in his paper on Lazy Clause generation used an approach almost exactly like SMT to solve Job Shop Scheduling and seemed to get good results for that.