YuhangQ/cloud-sat
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

增加lstech模式

Browse Source
This commit is contained in:
YuhangQ 2023-05-05 06:16:05 +00:00
parent e8466070ec
commit c7b82c2ad9
1 changed files with 31 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
src/solve.cpp
View File

@ -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<int> tmp;
// [1, sat_procs] for sat
@ -290,19 +298,33 @@ void light::seperate_groups() {
worker_type = light::UNSAT;
}
tmp.clear();
for(int i=sat_procs+1; i<=sat_procs+unsat_procs; i++) {
tmp.push_back(i);
}
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);