树形传播初版已实现

makefile

@@ -6,7 +6,7 @@ OBJECTS := $(addprefix build/,$(SOURCES:%=%.o))
 
 # 声明编译器和编译选项
 CXX := mpicxx
-CXXFLAGS := -O3 -Wall -Wextra -MMD -MP -march=native -mtune=native -g 
+CXXFLAGS := -std=c++17 -O3 -Wall -Wextra -MMD -MP -march=native -mtune=native -g 
 
 LIBS := -Wl,-Bstatic -lkissat -L kissat-inc/build -I kissat-inc/ \
 	    -lm4ri -L m4ri-20140914/.libs -I m4ri-20140914/ \

run.sh

@@ -25,8 +25,8 @@
 DIR=/pub/data/chenzh/data/sat2022
 INSTANCE=04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf
 
-# make -j 16 && mpirun --bind-to none -np 5 --allow-run-as-root ./light -i $DIR/$INSTANCE --share=1 --threads=4 --times=3600
+# make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600
 
-make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i ./data/class_1_easy_10_0.cnf --share=1 --threads=16 --times=3600
+make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i ./data/WS_500_16_70_10.apx_0.cnf --share=1 --threads=16 --times=3600
 
 #./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600

src/sharer.cpp

@@ -23,13 +23,12 @@ int num_skip_clauses_by_network = 0;
 
 std::unordered_map<int, bool> clause_imported;
 
-void sharer::share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_store>> &cls) {
+void sharer::share_clauses_to_other_node(int from, const std::vector<shared_ptr<clause_store>> &cls) {
 
     // 环形传递，数据来源如果是目的地，说明数据已轮转一圈，停止发送。
     if(OPT(share_method) == 0 && from == next_node) return;
 
     // 定义发送数据
-    MPI_Request *send_request = new MPI_Request();
     int send_length = 1;
 
     // 初始化发送数据
@@ -37,7 +36,11 @@ void sharer::share_clauses_to_next_node(int from, const std::vector<shared_ptr<c
         send_length += (cls[i]->size + 2);
     }
 
-    shared_ptr<int[]> send_buf = std::make_shared<int[]>(send_length);
+    shared_ptr<int[]> send_buf(new int[send_length]());
+
+    for(int i=0; i<send_length; i++) {
+        send_buf[i] = i;
+    }
 
     int index = 0;
 
@@ -57,19 +60,27 @@ void sharer::share_clauses_to_next_node(int from, const std::vector<shared_ptr<c
     // 调用 MPI 发送共享子句
 
     if(OPT(share_method)) {
+
+        // printf("MPI_SEND: %d %d   from: %d rank: %d\n", son[from][rank][0], son[from][rank][1], from, rank);
+        
         // 树形传递
         if(son[from][rank][0] != -1) {
+            MPI_Request *send_request = new MPI_Request();
             MPI_Isend(send_buf.get(), send_length, MPI_INT, son[from][rank][0], SHARE_CLAUSES_TAG, MPI_COMM_WORLD, send_request);
+            send_data_struct.push_back(std::make_pair(send_request, send_buf));
         }
         if(son[from][rank][1] != -1) {
+            MPI_Request *send_request = new MPI_Request();
             MPI_Isend(send_buf.get(), send_length, MPI_INT, son[from][rank][1], SHARE_CLAUSES_TAG, MPI_COMM_WORLD, send_request);
+            send_data_struct.push_back(std::make_pair(send_request, send_buf));
         }
+
     } else {
+        MPI_Request *send_request = new MPI_Request();
         // 环形传递
         MPI_Isend(send_buf.get(), send_length, MPI_INT, next_node, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, send_request);
-    }
+        send_data_struct.push_back(std::make_pair(send_request, send_buf));
-
+    }    
-    send_data_struct.push_back(std::make_pair(send_request, send_buf));
 
     // printf("c [worker] send clauses: %d\n", send_length);
 
@@ -82,59 +93,56 @@ void sharer::share_clauses_to_next_node(int from, const std::vector<shared_ptr<c
             // 与数组最后一个交换，然后 pop_back;
             std::swap(send_data_struct[i], send_data_struct[send_data_struct.size()-1]);
             send_data_struct.pop_back();
-            // printf("c [worker] free send request, now: %d\n", send_data_struct.size());
         }
     }
 }
 
-int sharer::receive_clauses_from_last_node(std::vector<shared_ptr<clause_store>> &clauses, int &transmitter) {
+int sharer::receive_clauses_from_other_node(std::vector<shared_ptr<clause_store>> &clauses, int &transmitter) {
     clauses.clear();
 
     int flag;
     MPI_Status status;
 
     transmitter = -1;
-
     int from = -1;
 
-    // 已接收完数据
+    MPI_Test(&receive_request, &flag, &status);
-    while(MPI_Test(&receive_request, &flag, &status) == MPI_SUCCESS && flag == 1) {
-        int index = 0;
-        int count;
-        MPI_Get_count(&status, MPI_INT, &count);
 
-        if(transmitter == -1) {
+    // 没有数据需要接收
-            transmitter = status.MPI_SOURCE;
+    if(flag == 0) {
-        }
+        return -1;
-
-        //assert(transmitter == status.MPI_SOURCE);
-
-        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);
-        }
-
-        assert(index == count);
-
-        MPI_Irecv(buf, BUF_SIZE, MPI_INT, MPI_ANY_SOURCE, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, &receive_request);
     }
 
+    int index = 0;
+    int count;
+    MPI_Get_count(&status, MPI_INT, &count);
+
+    transmitter = status.MPI_SOURCE;
+
+    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);
+    }
+
+    assert(index == count);
+
+    MPI_Irecv(buf, BUF_SIZE, MPI_INT, MPI_ANY_SOURCE, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, &receive_request);
+
     return from;
 }
 
@@ -183,8 +191,8 @@ void sharer::do_clause_sharing() {
     // 导入外部网络传输的子句
     std::vector<shared_ptr<clause_store>> clauses;
     int transmitter;
-    int from = receive_clauses_from_last_node(clauses, transmitter);
+    int from;
-    if(from != -1 && clauses.size() > 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);
 
@@ -197,10 +205,9 @@ void sharer::do_clause_sharing() {
         }
 
         // 传递外部网络传输的子句给下个节点
-        share_clauses_to_next_node(from, clauses);
+        share_clauses_to_other_node(from, clauses);
     }
 
-    // printf("start sharing %d\n", sq->share_intv);
     for (int i = 0; i < producers.size(); i++) {
         cls.clear();
         producers[i]->export_clauses_to(cls);
@@ -216,7 +223,7 @@ void sharer::do_clause_sharing() {
         cls.resize(t_size);
 
         //分享当前节点产生的子句
-        if(cls.size() > 0) share_clauses_to_next_node(rank, cls);
+        if(cls.size() > 0) share_clauses_to_other_node(rank, cls);
 
         //printf("c [worker] thread-%d: get %d exported clauses\n", i, t_size);
             
@@ -338,8 +345,6 @@ int sharer::sort_clauses(int x) {
 //     }   
 // }
 
-
-
 void sharer::init_tree_transmission(std::vector<std::vector<int>> &sharing_groups) {
 
     srand(19260817);
@@ -352,8 +357,9 @@ void sharer::init_tree_transmission(std::vector<std::vector<int>> &sharing_group
         }
     }
     
-    for(int i=0; i<sharing_groups.size(); i++) {
 
+    printf("c =========build tree=========\n");
+    for(int i=0; i<sharing_groups.size(); i++) {
         // create binary trees for every group;
         std::vector<int> &group = sharing_groups[i];
 
@@ -363,7 +369,7 @@ void sharer::init_tree_transmission(std::vector<std::vector<int>> &sharing_group
             // radom shuffle
             std::vector<int> rs = group;
             // keep group[j] as the first
-            std::swap(group[j], group[0]);
+            std::swap(rs[j], rs[0]);
             for(int k=1; k<rs.size(); k++) {
                 std::swap(rs[k], rs[rand()%(rs.size()-1)+1]);
             }
@@ -373,9 +379,11 @@ void sharer::init_tree_transmission(std::vector<std::vector<int>> &sharing_group
                 // printf("son[%d] [%d]\n", rs[0], rs[k]);
 
                 // son[1][1][0] =213;
-
                 son[rs[0]][rs[k]][0] = ( 2 * k + 1 < rs.size() ) ? rs[ 2 * k + 1 ] : -1;
                 son[rs[0]][rs[k]][1] = ( 2 * k + 2 < rs.size() ) ? rs[ 2 * k + 2 ] : -1;
+                
+                printf("c son[%d][%d][%d]=%d\tson[%d][%d][%d]=%d\n", rs[0], rs[k], 0, son[rs[0]][rs[k]][0], rs[0], rs[k], 1, son[rs[0]][rs[k]][1]);
+                
             }
 
         }

src/sharer.hpp

@@ -32,14 +32,14 @@ public:
     void init_circular_transmission(std::vector<std::vector<int>> &sharing_groups);
     void init_tree_transmission(std::vector<std::vector<int>> &sharing_groups);
 
-    void share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_store>> &cls);
+    void share_clauses_to_other_node(int from, const std::vector<shared_ptr<clause_store>> &cls);
-    int receive_clauses_from_last_node(std::vector<shared_ptr<clause_store>> &clauses, int &transmitter);
+    int receive_clauses_from_other_node(std::vector<shared_ptr<clause_store>> &clauses, int &transmitter);
     
     int sort_clauses(int x);
     int import_clauses(int id);
 
 private:
-    light* S;    
+    light* S;
 };
 
 #endif

src/solve.cpp

@@ -285,7 +285,6 @@ void light::seperate_groups() {
             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) {
@@ -318,8 +317,6 @@ void light::seperate_groups() {
         }
         sharing_groups.push_back(tmp);
     }
-
-    printf("sg: %d\n", sharing_groups[0].size());
 }
 
 void print_model(vec<int> &model) {