Jakieś sformułowania SAT / SMT VRP / VRPTW (TSP, Job-Shop-Scheduling)?

zastanawiam się, czy są jakieś podejścia do formułowania problemu trasy pojazdu z systemem Windows-Time ( VRPTW ) (jako problemem decyzyjnym) jako instancji SAT / SMT? (alternatywnie: TSP)

Na przykład:
„Czy istnieje prawidłowe rozwiązanie odwiedzające wszystkich klientów w ich ramach czasowych przy n = 10 pojazdach?”

Ten problem decyzyjny może być przydatny w pierwszym etapie minimalizacji liczby używanych pojazdów.

Nie mam żadnego doświadczenia z SMT, ale spodziewam się, że będzie to konieczne, jeśli chcemy traktować współrzędne / czasy jako liczby rzeczywiste.

Zwykle wszystkie formuły TSP / VRP są wykonywane w domenie programowania mieszanych liczb całkowitych, ale zastanawiam się, czy formuła sat / smt mogłaby być konkurencyjna (pod względem czasu rozwiązania w praktyce) w odniesieniu do powyższego problemu decyzyjnego.

Więc co o tym myślisz:

• znasz jakieś referencje?
• czy uważasz, że podejście sat / smt może być konkurencyjne?
• coś jeszcze chcesz wspomnieć?

Dziękuję za cały Twój wkład.

Sascha

Edycja : Jak wspomniałem TSP jako bardziej powszechny problem w TCS, który jest związany z VRPTW, powinienem również wspomnieć o problemie planowania pracy , który jest drugim „częściowym problemem” w VRPTW. Być może badacze w tej dziedzinie próbowali czegoś z SAT / SMT.

Duży problem, jaki widzę w sformułowaniu SAT dla VRPTW, polega na tym, że musisz dyskretyzować czas, aby wymusić ograniczenia okna czasowego (chyba że kodujesz arytmetykę jako obwody boolowskie, których nigdy wcześniej nie widziałem, ale warto spróbować). Oznacza to, że liczba zmiennych staje się znacznie większa, gdy zwiększa się okno czasowe wpływające na wydajność.

Myślę jednak, że sformułowanie SMT (Sat Modulo Theory) nie miałoby podobnego problemu, ponieważ masz propagator ograniczeń okna czasowego, które zwracałyby nadmiarowe ograniczenia do solvera SAT, aby uwzględnić je podczas rozgałęzienia.

Chociaż nie znam żadnej pracy wykorzystującej formuły SAT dla VRPTW, wiem, że Peter Stuckey w swoim artykule na temat generowania Lazy Clause zastosował podejście prawie dokładnie takie jak SMT do rozwiązania harmonogramu zleceń i wydawało się, że osiąga dobre wyniki.