From 227d700b5390d838aa246ee6e4dddbdc7208dcde Mon Sep 17 00:00:00 2001 From: YuhangQ Date: Thu, 13 Apr 2023 07:09:41 +0000 Subject: [PATCH] =?UTF-8?q?=E5=A2=9E=E5=8A=A0=E5=93=88=E5=B8=8C?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/paras.hpp | 3 ++- src/solve.cpp | 16 ++++++++-------- src/workers/clause.hpp | 19 ++++++++++++++++++- src/workers/sharer.cpp | 26 +++++++++++++++++++++++--- 4 files changed, 51 insertions(+), 13 deletions(-) diff --git a/src/paras.hpp b/src/paras.hpp index 8659e25..973ea34 100644 --- a/src/paras.hpp +++ b/src/paras.hpp @@ -19,7 +19,8 @@ PARA( shuffle , int , '\0' , false , 1 , 0 , 1 , "Use random shuffle") \ PARA( simplify , int , '\0' , false , 1 , 0 , 1 , "Use Simplify (only preprocess)") \ PARA( threads , int , '\0' , false , 32 , 1 , 128 , "Thread number") \ - PARA( times , double , '\0' , false , 5000 , 0 , 1e8 , "Cutoff time") + PARA( times , double , '\0' , false , 5000 , 0 , 1e8 , "Cutoff time") \ + PARA( unique , int , '\0' , false , 1 , 0 , 1 , "Whether perform unique checking when receiving clauses from other nodes") // name, short-name, must-need, default, comments diff --git a/src/solve.cpp b/src/solve.cpp index 5962171..1baffb4 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -73,36 +73,36 @@ void light::diversity_workers() { if (i) workers[i]->configure("order_reset", i); } if (OPT(pakis)) { - if (i == 13 || i == 14 || i == 20 || i == 21) + if (i == 13 || i == 14 || i == 9) workers[i]->configure("tier1", 3); else workers[i]->configure("tier1", 2); - if (i == 3 || i == 4 || i == 6 || i == 8 || i == 11 || i == 12 || i == 13 || i == 14 || i == 16 || i == 18 || i == 23) + 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 == 23) + if (i == 2 || i == 15) workers[i]->configure("stable", 0); - else if (i == 6 || i == 16) + else if (i == 6 || i == 14) workers[i]->configure("stable", 2); else workers[i]->configure("stable", 1); - if (i == 10 || i == 22) + if (i == 10) workers[i]->configure("walkinitially", 1); else workers[i]->configure("walkinitially", 0); - if (i == 7 || i == 8 || i == 9 || i == 17 || i == 18 || i == 19 || i == 20) + 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 || i == 23) + 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 || i == 18 || i == 19) + 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); diff --git a/src/workers/clause.hpp b/src/workers/clause.hpp index 3286a5f..4d83c6d 100644 --- a/src/workers/clause.hpp +++ b/src/workers/clause.hpp @@ -11,7 +11,6 @@ struct clause_store { int *data; std::atomic refs; clause_store(int sz) { - //printf("c new clause_store\n"); size = sz; data = (int*) malloc(sizeof(int) * sz); @@ -21,6 +20,24 @@ struct clause_store { void increase_refs(int inc) { refs += inc; } + + int hash_code() { + + const int B = 31; + const int MOD = 10000007; + + ll res = 0; + ll b = 1; + + for (int i=0; i < size; i++) { + int d = (data[i] % MOD + MOD) % MOD; + res = (res + d * b) % MOD; + b = (b * B) % MOD; + } + + return res; + } + bool free_clause() { // int ref = refs.fetch_sub(1); // if (ref <= 1) { diff --git a/src/workers/sharer.cpp b/src/workers/sharer.cpp index c0f7610..2bd5b17 100644 --- a/src/workers/sharer.cpp +++ b/src/workers/sharer.cpp @@ -15,6 +15,12 @@ std::vector> send_data_struct; MPI_Request receive_request; int buf[BUF_SIZE]; +int num_received_clauses_by_network = 0; +int num_skip_clauses_by_network = 0; + +// 记录子句是否已经导入过 +int *clause_imported; + void share_clauses_to_next_node(int from, const std::vector> &cls) { int target = rank % (num_procs - 1) + 1; @@ -29,6 +35,7 @@ void share_clauses_to_next_node(int from, const std::vectorhash_code()]) continue; send_length += (cls[i]->size + 2); } @@ -39,6 +46,7 @@ void share_clauses_to_next_node(int from, const std::vectorhash_code()]) continue; auto& c = cls[i]; send_buf[index++] = c->size; send_buf[index++] = c->lbd; @@ -88,11 +96,17 @@ bool receive_clauses_from_last_node(std::vector> &claus from = buf[index++]; while(index < count) { + num_received_clauses_by_network++; + shared_ptr cl = std::make_shared(buf[index++]); cl->lbd = buf[index++]; for(int i=0; isize; i++) { cl->data[i] = buf[index++]; } + if(clause_imported[cl->hash_code()]) { + num_skip_clauses_by_network++; + continue; + } clauses.push_back(cl); } @@ -102,8 +116,6 @@ bool receive_clauses_from_last_node(std::vector> &claus int from = (rank - 2 + num_procs - 1) % (num_procs - 1) + 1; - //LOGGER->info("receive clauses: %v", count); - MPI_Irecv(buf, BUF_SIZE, MPI_INT, from, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, &receive_request); } @@ -115,10 +127,16 @@ void sharer::clause_sharing_init() { MPI_Comm_rank(MPI_COMM_WORLD, &rank); int from = (rank - 2 + num_procs - 1) % (num_procs - 1) + 1; MPI_Irecv(buf, BUF_SIZE, MPI_INT, from, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, &receive_request); + + clause_imported = new int[10000007]; } void sharer::clause_sharing_end() { printf("c sharing nums: %d\nc sharing time: %.2lf\n", nums, share_time); + printf("c sharing received_num_by_network: %d\n", num_received_clauses_by_network); + printf("c sharing skip_num_by_network: %d\n", num_skip_clauses_by_network); + printf("c sharing unique reduce percentage: %.2f%%\n", (double) num_skip_clauses_by_network / num_received_clauses_by_network * 100); + delete []clause_imported; } void sharer::do_clause_sharing() { @@ -158,6 +176,7 @@ void sharer::do_clause_sharing() { share_clauses_to_next_node(from, clauses); for (int k = 0; k < clauses.size(); k++) { + clause_imported[clauses[k]->hash_code()] = true; clauses[k]->free_clause(); } } @@ -178,7 +197,8 @@ void sharer::do_clause_sharing() { consumers[j]->import_clauses_from(cls); } for (int k = 0; k < cls.size(); k++) { - int res = cls[k]->free_clause(); + clause_imported[cls[k]->hash_code()] = true; + cls[k]->free_clause(); } }