增加哈希

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

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);

src/workers/clause.hpp

@@ -11,7 +11,6 @@ struct clause_store {
     int *data;
     std::atomic<int> 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) {

src/workers/sharer.cpp

@@ -15,6 +15,12 @@ std::vector<std::pair<MPI_Request*, int*>> 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<shared_ptr<clause_store>> &cls) {
 
     int target = rank % (num_procs - 1) + 1;
@@ -29,6 +35,7 @@ void share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_st
 
     // 初始化发送数据
     for(int i=0; i<cls.size(); i++) {
+        if(clause_imported[cls[i]->hash_code()]) continue;
         send_length += (cls[i]->size + 2);
     }
 
@@ -39,6 +46,7 @@ void share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_st
     send_buf[index++] = from;
 
     for(int i=0; i<cls.size(); i++) {
+        if(clause_imported[cls[i]->hash_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<shared_ptr<clause_store>> &claus
 
         from = buf[index++];
         while(index < count) {
+            num_received_clauses_by_network++;
+
             shared_ptr<clause_store> cl = std::make_shared<clause_store>(buf[index++]);
             cl->lbd = buf[index++];
             for(int i=0; i<cl->size; 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<shared_ptr<clause_store>> &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();
         }
     }