diff --git a/src/solve.cpp b/src/solve.cpp index 6ecbb5a..5446396 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -61,14 +61,23 @@ void light::init_workers() { } void light::diversity_workers() { - printf("c num %d\n", num_procs); + // printf("c num %d\n", num_procs); for (int i = 0; i < OPT(threads); i++) { + if(solver_type == LSTECH) { + workers[i]->configure("worker_seed", 0); + workers[i]->configure("worker_index", i); + workers[i]->configure("worker_number", OPT(threads)); + continue; + } + + assert(solver_type == KISSAT); + if(worker_type == SAT) { if (OPT(shuffle)) { workers[i]->configure("worker_index", i); workers[i]->configure("worker_number", OPT(threads)); - if(rank == 1 || solver_type = LSTECH) { + if(rank == 1) { workers[i]->configure("worker_seed", 0); } else { workers[i]->configure("worker_seed", rank); @@ -113,7 +122,7 @@ void light::diversity_workers() { if (OPT(shuffle)) { workers[i]->configure("worker_index", i); workers[i]->configure("worker_number", OPT(threads)); - if(rank == num_procs - 1 || solver_type = LSTECH) { + if(rank == num_procs - 1) { workers[i]->configure("worker_seed", 0); } else { workers[i]->configure("worker_seed", rank); @@ -270,10 +279,9 @@ void light::seperate_groups() { if(worker_procs >= 8) { int sat_procs = worker_procs / 8; int unsat_procs = worker_procs / 4; - int default_procs = worker_procs - sat_procs - unsat_procs; + int lstech_procs = 3; + int default_procs = worker_procs - sat_procs - unsat_procs - lstech_procs; - if (rank == 2 || rank == sat_procs + 2 || rank == sat_procs + unsat_procs + 2) - solver_type == LSTECH; std::vector tmp; // [1, sat_procs] for sat @@ -289,6 +297,7 @@ void light::seperate_groups() { if(rank >= sat_procs+1 && rank <= sat_procs+unsat_procs) { worker_type = light::UNSAT; } + tmp.clear(); for(int i=sat_procs+1; i<=sat_procs+unsat_procs; i++) { @@ -296,13 +305,26 @@ void light::seperate_groups() { } sharing_groups.push_back(tmp); - // [sat_procs+unsat_procs+1, worker_procs] - if(rank >= sat_procs+unsat_procs+1 && rank <= worker_procs) { + + // [sat_procs+unsat_procs+1, sat_procs+unsat_procs+lstech_procs] for ls-tech + if(rank >= sat_procs+unsat_procs+1 && rank <= sat_procs+unsat_procs+lstech_procs) { + solver_type = LSTECH; + OPT(share) = 0; + } + + tmp.clear(); + for(int i=sat_procs+unsat_procs+1; i<=sat_procs+unsat_procs+lstech_procs; i++) { + tmp.push_back(i); + } + sharing_groups.push_back(tmp); + + // [sat_procs+unsat_procs+lstech_procs+1, worker_procs] + if(rank >= sat_procs+unsat_procs+lstech_procs+1 && rank <= worker_procs) { worker_type = light::DEFAULT; } tmp.clear(); - for(int i=sat_procs+unsat_procs+1; i<=worker_procs; i++) { + for(int i=sat_procs+unsat_procs+lstech_procs+1; i<=worker_procs; i++) { tmp.push_back(i); } sharing_groups.push_back(tmp);