Adakah formulasi SAT / SMT dari VRP / VRPTW (TSP, Penjadwalan Pekerjaan-Toko)?

saya bertanya-tanya apakah mereka merupakan pendekatan merumuskan Kendaraan-Routing-Masalah dengan Time-Windows ( VRPTW ) (sebagai masalah keputusan) sebagai contoh SAT / SMT? (alternatif: TSP)

Misalnya:
"Apakah ada solusi yang valid mengunjungi semua pelanggan dalam jendela waktu mereka dengan n = 10 kendaraan?"

Masalah keputusan ini bisa bermanfaat untuk langkah pertama meminimalkan jumlah kendaraan yang digunakan.

Saya tidak punya pengalaman dengan SMT, tetapi saya berharap itu perlu jika kita ingin menangani koordinat / kali sebagai bilangan real.

Biasanya semua formulasi TSP / VRP dilakukan dalam domain mixed-integer-programming, tetapi saya bertanya-tanya apakah formulasi sat / smt dapat bersaing (dalam hal memecahkan waktu dalam praktek) untuk masalah keputusan di atas.

Jadi apa yang Anda pikirkan:

• apakah Anda tahu referensi?
• Menurut Anda apakah pendekatan sat / smt bisa kompetitif?
• ada lagi yang ingin Anda sebutkan?

Terima kasih atas semua masukan Anda.

Sascha

Sunting : Seperti yang saya sebutkan TSP sebagai masalah yang lebih umum di TCS yang terkait dengan VRPTW, saya juga harus menyebutkan masalah Penjadwalan Job Shop , yang merupakan "masalah parsial" lainnya di VRPTW. Mungkin para peneliti di bidang ini mencoba sesuatu dengan SAT / SMT.

Masalah besar yang saya lihat dengan formulasi SAT untuk VRPTW adalah bahwa Anda harus menentukan waktu untuk menegakkan batasan jendela waktu (kecuali jika Anda menyandikan aritmatika sebagai sirkuit boolean yang belum pernah saya lihat selesai tetapi mungkin layak untuk dicoba). Ini berarti jumlah variabel menjadi jauh lebih besar karena jendela waktu meningkat mempengaruhi kinerja.

Formulasi SMT (Sat Modulo Theory) namun tidak akan memiliki masalah yang sama, saya pikir karena Anda memiliki propagator untuk batasan waktu yang akan mengembalikan kendala berlebihan ke pemecah SAT untuk dimasukkan ketika Anda bercabang.

Meskipun saya tidak tahu ada pekerjaan yang menggunakan formulasi SAT untuk VRPTW, saya tahu bahwa Peter Stuckey, dalam makalahnya tentang generasi Lazy Clause menggunakan pendekatan yang hampir persis seperti SMT untuk menyelesaikan Penjadwalan Toko Pekerjaan dan sepertinya mendapatkan hasil yang bagus untuk itu.