Irgendwelche SAT / SMT-Formulierungen des VRP / VRPTW (TSP, Job-Shop-Scheduling)?

Ich frage mich, ob es irgendwelche Ansätze gibt, die ein Fahrzeugroutenproblem mit Zeitfenstern ( VRPTW ) (als Entscheidungsproblem) als SAT / SMT-Instanz formulieren . (Alternative: TSP)

Zum Beispiel:
"Gibt es eine gültige Lösung, die alle Kunden innerhalb ihrer Zeitfenster mit n = 10 Fahrzeugen besucht?"

Dieses Entscheidungsproblem könnte für einen ersten Schritt nützlich sein, um die Anzahl der verwendeten Fahrzeuge zu minimieren.

Ich habe keine Erfahrung mit SMT, aber ich erwarte, dass es notwendig ist, wenn wir Koordinaten / Zeiten als reelle Zahlen behandeln wollen.

Normalerweise werden alle TSP / VRP-Formulierungen im Bereich der gemischten Ganzzahlprogrammierung durchgeführt, aber ich frage mich, ob eine Sat / SMT-Formulierung (in Bezug auf die Lösungszeit in der Praxis) für das obige Entscheidungsproblem wettbewerbsfähig sein könnte.

Also was denkst du:

• Kennen Sie Referenzen?
• Denken Sie, dass ein Sat / SMT-Ansatz wettbewerbsfähig sein könnte?
• Möchten Sie noch etwas erwähnen?

Vielen Dank für all Ihre Beiträge.

Sascha

Bearbeiten : Da ich den TSP als ein häufigeres Problem in TCS erwähnt habe, das mit dem VRPTW zusammenhängt, sollte ich auch das Job Shop Scheduling-Problem erwähnen , das das andere "Teilproblem" im VRPTW ist. Vielleicht haben die Forscher auf diesem Gebiet etwas mit SAT / SMT versucht.

Das große Problem, das ich bei einer SAT-Formulierung für VRPTW sehe, ist, dass Sie die Zeit diskretisieren müssen, um die Zeitfenstereinschränkungen durchzusetzen (es sei denn, Sie codieren Arithmetik als boolesche Schaltungen, die ich noch nie gesehen habe, die es aber möglicherweise wert sind, ausprobiert zu werden). Dies bedeutet, dass die Anzahl der Variablen mit zunehmendem Zeitfenster viel größer wird, was sich auf die Leistung auswirkt.

Eine SMT-Formulierung (Sat Modulo Theory) hätte jedoch kein ähnliches Problem. Ich denke, da Sie einen Propagator für die Zeitfenster-Einschränkungen haben, der redundante Einschränkungen an den SAT-Solver zurückgibt, die beim Verzweigen berücksichtigt werden sollen.

Obwohl ich keine Arbeit mit SAT-Formulierungen für VRPTW kenne, weiß ich, dass Peter Stuckey in seinem Artikel über die Generierung von Lazy Clause einen Ansatz verwendet hat, der fast genau dem von SMT entspricht, um Job Shop Scheduling zu lösen, und dafür gute Ergebnisse zu erzielen schien.