diff --git a/src/light.hpp b/src/light.hpp index 9c6947a..2f5f715 100644 --- a/src/light.hpp +++ b/src/light.hpp @@ -46,7 +46,7 @@ public: sharer* s; std::vector> sharing_groups; - enum { SAT, UNSAT, DEFAULT } worker_type; + enum { UNSAT, DEFAULT } worker_type; MPI_Request terminal_request; diff --git a/src/sharer.cpp b/src/sharer.cpp index c6577c9..b608e4d 100644 --- a/src/sharer.cpp +++ b/src/sharer.cpp @@ -192,9 +192,9 @@ void sharer::do_clause_sharing() { std::vector> clauses; int transmitter; int from; + + int received_lits = 0; while((from = receive_clauses_from_other_node(clauses, transmitter)) != -1 &&clauses.size() > 0) { - printf("c node%d(%d) get %d exported clauses from node-%d\n", rank, S->worker_type, clauses.size(), transmitter); - // printf("c [node-%d] sharing unique reduce percentage: %.2f%%\n", rank, (double) num_skip_clauses_by_network / num_received_clauses_by_network * 100); for (int j = 0; j < consumers.size(); j++) { consumers[j]->import_clauses_from(clauses); @@ -202,12 +202,15 @@ void sharer::do_clause_sharing() { for (int k = 0; k < clauses.size(); k++) { clause_imported[clauses[k]->hash_code()] = true; + received_lits += clauses[k]->size; } // 传递外部网络传输的子句给下个节点 share_clauses_to_other_node(from, clauses); } + printf("c node%d(%d) get %d exported lits from network\n", rank, S->worker_type, received_lits); + for (int i = 0; i < producers.size(); i++) { cls.clear(); producers[i]->export_clauses_to(cls); @@ -232,13 +235,11 @@ void sharer::do_clause_sharing() { // 增加 lits 限制 int percent = sort_clauses(i); - if(S->worker_type == light::UNSAT) { - if (percent < 75) { - producers[i]->broaden_export_limit(); - } - else if (percent > 98) { - producers[i]->restrict_export_limit(); - } + if (percent < 75) { + producers[i]->broaden_export_limit(); + } + else if (percent > 98) { + producers[i]->restrict_export_limit(); } for (int j = 0; j < consumers.size(); j++) { @@ -317,36 +318,6 @@ int sharer::sort_clauses(int x) { return (OPT(share_lits) - space) * 100 / OPT(share_lits); } -// void light::share() { -// // printf("c sharing start\n"); -// if (OPT(DPS)) { -// sharer* s = new sharer(0, OPT(share_intv), OPT(share_lits), OPT(DPS)); -// s->margin = OPT(margin); -// for (int j = 0; j < OPT(threads); j++) { -// s->producers.push(workers[j]); -// workers[j]->in_sharer = s; -// } -// sharers.push(s); -// } -// else { -// int sharers_number = 1; -// for (int i = 0; i < sharers_number; i++) { -// sharer* s = new sharer(i, OPT(share_intv), OPT(share_lits), OPT(DPS)); -// for (int j = 0; j < OPT(threads); j++) { -// s->producers.push(workers[j]); -// s->consumers.push(workers[j]); -// workers[j]->in_sharer = s; -// } -// sharers.push(s); -// } - -// sharer_ptrs = new pthread_t[sharers_number]; -// for (int i = 0; i < sharers_number; i++) { -// pthread_create(&sharer_ptrs[i], NULL, share_worker, sharers[i]); -// } -// } -// } - void sharer::init_tree_transmission(std::vector> &sharing_groups) { srand(19260817); @@ -359,7 +330,6 @@ void sharer::init_tree_transmission(std::vector> &sharing_group } } - printf("c =========build tree=========\n"); for(int i=0; i> &sharing_group // build a tree from array for(int k=0; k> &sharing_groups) { - for(int i=0; irank) { diff --git a/src/solve.cpp b/src/solve.cpp index c936609..511bdf9 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -68,33 +68,33 @@ void light::init_workers() { } void light::diversity_workers() { - for (int i = 0; i < OPT(threads); i++) { + // if(worker_type == SAT) { - if (OPT(shuffle)) { - if (i) workers[i]->configure("order_reset", (rank - 1) * OPT(threads) + i); - } + // if (OPT(shuffle)) { + // if (i) workers[i]->configure("order_reset", (rank - 1) * OPT(threads) + i); + // } - if(worker_type == SAT) { + // workers[i]->configure("stable", 1); + // workers[i]->configure("target", 2); + // workers[i]->configure("phase", 1); + // // workers[i]->configure("heuristic", 0); - workers[i]->configure("stable", 1); - workers[i]->configure("target", 2); - workers[i]->configure("phase", 1); - // workers[i]->configure("heuristic", 0); + // if (i == 2) + // workers[i]->configure("stable", 0); + // else if (i == 6) + // workers[i]->configure("stable", 2); - if (i == 2) - workers[i]->configure("stable", 0); - else if (i == 6) - workers[i]->configure("stable", 2); - - if (i == 7) - workers[i]->configure("target", 0); - else if (i == 0 || i == 2 || i == 3 || i == 6) - workers[i]->configure("target", 1); + // if (i == 7) + // workers[i]->configure("target", 0); + // else if (i == 0 || i == 2 || i == 3 || i == 6) + // workers[i]->configure("target", 1); - if (i == 3 || i == 11 || i == 12 || i == 13 || i == 15) - workers[i]->configure("phase", 0); - } else if(worker_type == UNSAT) { + // if (i == 3 || i == 11 || i == 12 || i == 13 || i == 15) + // workers[i]->configure("phase", 0); + // } else + + if(worker_type == UNSAT) { OPT(share_lits) = 3000; @@ -120,42 +120,42 @@ void light::diversity_workers() { else if (i == 14) workers[i]->configure("target", 2); } else { - - if (OPT(pakis)) { - if (i == 13 || i == 14 || i == 9) - workers[i]->configure("tier1", 3); - else - workers[i]->configure("tier1", 2); - - if (i == 3 || i == 6 || i == 8 || i == 11 || i == 12 || i == 13 || i == 14 || i == 15) - workers[i]->configure("chrono", 0); - else - workers[i]->configure("chrono", 1); - - if (i == 2 || i == 15) - workers[i]->configure("stable", 0); - else if (i == 6 || i == 14) - workers[i]->configure("stable", 2); - else - workers[i]->configure("stable", 1); - - if (i == 10) - workers[i]->configure("walkinitially", 1); - else - workers[i]->configure("walkinitially", 0); - - if (i == 7 || i == 8 || i == 9 || i == 11) - workers[i]->configure("target", 0); - else if (i == 0 || i == 2 || i == 3 || i == 4 || i == 5 || i == 6 || i == 10) - workers[i]->configure("target", 1); - else - workers[i]->configure("target", 2); - - if (i == 4 || i == 5 || i == 8 || i == 9 || i == 12 || i == 13 || i == 15) - workers[i]->configure("phase", 0); - else - workers[i]->configure("phase", 1); + if (OPT(shuffle)) { + if (i) workers[i]->configure("order_reset", (rank - 1) * OPT(threads) + i); } + if (i == 13 || i == 14 || i == 9) + workers[i]->configure("tier1", 3); + else + workers[i]->configure("tier1", 2); + + if (i == 3 || i == 6 || i == 8 || i == 11 || i == 12 || i == 13 || i == 14 || i == 15) + workers[i]->configure("chrono", 0); + else + workers[i]->configure("chrono", 1); + + if (i == 2 || i == 15) + workers[i]->configure("stable", 0); + else if (i == 6 || i == 14) + workers[i]->configure("stable", 2); + else + workers[i]->configure("stable", 1); + + if (i == 10) + workers[i]->configure("walkinitially", 1); + else + workers[i]->configure("walkinitially", 0); + + if (i == 7 || i == 8 || i == 9 || i == 11) + workers[i]->configure("target", 0); + else if (i == 0 || i == 2 || i == 3 || i == 4 || i == 5 || i == 6 || i == 10) + workers[i]->configure("target", 1); + else + workers[i]->configure("target", 2); + + if (i == 4 || i == 5 || i == 8 || i == 9 || i == 12 || i == 13 || i == 15) + workers[i]->configure("phase", 0); + else + workers[i]->configure("phase", 1); } for (int j = 0; j < configure_name[i].size(); j++) { @@ -258,7 +258,8 @@ int light::run() { seperate_groups(); init_workers(); - diversity_workers(); + + if(OPT(pakis)) diversity_workers(); parse_input(); @@ -272,38 +273,26 @@ void light::seperate_groups() { int worker_procs = num_procs - 1; if(worker_procs >= 8) { - int sat_procs = worker_procs / 8; - int unsat_procs = sat_procs; - int default_procs = worker_procs - sat_procs - unsat_procs; - // [1, sat_procs] for sat - if(rank >= 1 && rank <= sat_procs) { - worker_type = light::SAT; + int unsat_procs = worker_procs / 4; + int default_procs = worker_procs - unsat_procs; + // [1, unsat_procs] for unsat + if(rank >= 1 && rank <= unsat_procs) { + worker_type = light::UNSAT; } std::vector tmp; - for(int i=1; i<=sat_procs; i++) { + for(int i=1; i<=unsat_procs; i++) { tmp.push_back(i); } sharing_groups.push_back(tmp); - // [sat_procs+1, sat_procs+unsat_procs] for unsat - 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++) { - 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) { + // [unsat_procs+1, worker_procs] + if(rank >= unsat_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=unsat_procs+1; i<=worker_procs; i++) { tmp.push_back(i); } sharing_groups.push_back(tmp);