Skip to content

CNF Encodings for the Min-Max Multiple Traveling Salesmen Problem

Notifications You must be signed in to change notification settings

ReprodSuplem/MTSP

Repository files navigation

This is an instruction for reproducing the experiments described in our submission. 

===== Part A =====
Usage of instance generator ->
We implemented four instance generators as the following ruby scripts: 
(1) instGen_arithmetic.rb
(2) instGen_guide.rb
(3) instGen_acyclic.rb
(4) instGen_relative.rb
They are used in the same way, so here we only introduce one of them in detail. 
Make sure the TSP problem (e.g., burma14.tsp file) you want to solve 
is in the same directory as instance generator (e.g., instGen_guide.rb). 
Determine the number of salesmen to respond to this problem, such as 3 salesmen, 
and run
 $ ruby ./instGen_guide.rb ./burma14.tsp m=3
Then two files will be generated in the same directory: 
one is "burma14_m3.lp" and another one is "burma14_m3.wcnf", 
where the former corresponds to the IP formulation that can be solved by CPLEX optimizer; 
while the latter corresponds to CNF encoding based on guiding potential. 
Note that this instruction does NOT include the usage of CPLEX optimizer, and
please refer to its official manual. 

===== Part B =====
Usage of group MaxSAT sovler ->
We modified QMaxSAT solver (version submitted into MaxSAT Evaluation 2018) to 
six group MaxSAT solvers as follows. 
(1) QMaxSAT_arithmetic
(2) QMaxSAT_arithmetic_heuristic
(3) QMaxSAT_potential
(4) QMaxSAT_potential_heuristic
(5) QMaxSAT_relative
(6) QMaxSAT_relative_heuristic
where
(1) and (2) are the solvers used for the instance generated by instGen_arithmetic.rb; 
(3) and (4) are the solvers used for the instance generated by instGen_guide.rb or instGen_acyclic.rb; 
(5) and (6) are the solvers used for the instance generated by instGen_relative.rb. 
They are used in the same way, so here we only introduce one of them in detail. 
For example, we want to solve the instance "burma14_m3.wcnf" generated by instGen_guide.rb 
by (3). Then we should run 
 $ ./QMaxSAT_potential/code/qmaxsat_g3 -card=mrwto -pmodel=0 -narr=14 -mct=3 ./burma14_m3.wcnf ./solution.txt
Note that -narr=$x indicates that the number of cities is $x, 
and -mct=$y indicates that the number of salesmen is $y. 
Please do not pay attention to the last argument file "solution.txt", 
it does NOT play any role in reproducing our experiment, 
but please keep this argument, otherwise you will get an error. 

About

CNF Encodings for the Min-Max Multiple Traveling Salesmen Problem

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published