子句改为双模哈希

run.sh

@@ -13,7 +13,7 @@
 # 04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf
 
 DIR=/pub/data/chenzh/data/sat2022
-INSTANCE=eede03732955f620b5291f9dcf9f95df-tseitin_n200_d3.cnf
+INSTANCE=03bb7baaa45980753a0e7050ae44755d-atco_enc3_opt1_03_53.cnf
 
 make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600
 

src/utils/hashmap.hpp

@@ -4,7 +4,7 @@ typedef long long ll;
 
 struct DataType{
 	ll key;  
-	int val;  
+	int val;
 };
 
 struct HashNode{

src/workers/clause.hpp

@@ -21,11 +21,7 @@ struct clause_store {
         refs += inc;
     }
 
-    int hash_code() {
-
-        const int B = 31;
-        const int MOD = 10000007;
-        
+    ll __hash(int B, int MOD) {
         ll res = 0;
         ll b = 1;
 
@@ -34,8 +30,12 @@ struct clause_store {
             res = (res + d * b) % MOD;
             b = (b * B) % MOD;
         }
+    }
 
-        return res;
+    int hash_code() {
+        const int B = 31;
+        const int MOD = 10000007;
+        return __hash(31, 1000000007) ^ __hash(17, 1000000009);
     }
 
     bool free_clause() {

src/workers/sharer.cpp

@@ -1,6 +1,7 @@
 #include "../light.hpp"
 #include "basesolver.hpp"
 #include "sharer.hpp"
+#include "unordered_map"
 #include "clause.hpp"
 #include <unistd.h>
 #include "../distributed/comm_tag.h"
@@ -19,7 +20,8 @@ int num_received_clauses_by_network = 0;
 int num_skip_clauses_by_network = 0;
 
 // 记录子句是否已经导入过
-int *clause_imported;
+
+std::unordered_map<int, bool> clause_imported;
 
 void share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_store>> &cls) {
 
@@ -127,8 +129,6 @@ 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() {
@@ -136,7 +136,6 @@ void sharer::clause_sharing_end() {
     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() {