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.