分为SAT和UNSAT两个环

run.sh

@@ -13,10 +13,10 @@
 # 04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf
 
 DIR=/pub/data/chenzh/data/sat2022
-INSTANCE=00aefd1fc30c425075166ca051e57218-barman-pfile10-038.sas.ex.15.cnf
+INSTANCE=0d209cb420326994f9c4898eb10228ab-008-80-8.cnf
 
 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/hard1.cnf --share=1 --threads=16 --times=3600
+#make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i ./data/hard1.cnf --share=1 --threads=16 --times=3600
 
 #./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600

src/sharer.cpp

@@ -25,7 +25,14 @@ std::unordered_map<int, bool> 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;
+    /**
+    * sat_group    [1, num_procs/2]
+    * unsat_group  [num_procs/2+1, num_procs-1]
+    */
+
+    int target = rank + 1;
+    if(target == num_procs / 2 + 1) target = 1;
+    if(target == num_procs) target = num_procs/2+1;
 
     // 环形传递，数据来源如果是目的地，说明数据已轮转一圈，停止发送。
     if(from == target) return;
@@ -80,12 +87,14 @@ void share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_st
     }
 }
 
-bool receive_clauses_from_last_node(std::vector<shared_ptr<clause_store>> &clauses) {
+int receive_clauses_from_last_node(std::vector<shared_ptr<clause_store>> &clauses, int &transmitter) {
     clauses.clear();
 
     int flag;
     MPI_Status status;
 
+    transmitter = -1;
+
     int from = -1;
 
     // 已接收完数据
@@ -94,6 +103,11 @@ bool receive_clauses_from_last_node(std::vector<shared_ptr<clause_store>> &claus
         int count;
         MPI_Get_count(&status, MPI_INT, &count);
 
+        if(transmitter == -1) {
+            transmitter = status.MPI_SOURCE;
+        }
+        assert(transmitter == status.MPI_SOURCE);
+
         from = buf[index++];
 
         while(index < count) {
@@ -117,11 +131,7 @@ bool receive_clauses_from_last_node(std::vector<shared_ptr<clause_store>> &claus
 
         assert(index == count);
 
-        // 进行下一步接收数据
+        MPI_Irecv(buf, BUF_SIZE, MPI_INT, MPI_ANY_SOURCE, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, &receive_request);
-
-        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);
     }
 
     return from;
@@ -130,15 +140,14 @@ bool receive_clauses_from_last_node(std::vector<shared_ptr<clause_store>> &claus
 void sharer::clause_sharing_init() {
     MPI_Comm_size(MPI_COMM_WORLD, &num_procs);
     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, MPI_ANY_SOURCE, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, &receive_request);
-    MPI_Irecv(buf, BUF_SIZE, MPI_INT, from, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, &receive_request);
 }
 
 void sharer::clause_sharing_end() {
-    printf("c sharing nums: %d\nc sharing time: %.2lf\n", nums, share_time);
+    printf("c [node-%d] sharing nums: %d\nc sharing time: %.2lf\n", rank, nums, share_time);
-    printf("c sharing received_num_by_network: %d\n", num_received_clauses_by_network);
+    printf("c [node-%d] sharing received_num_by_network: %d\n", rank, num_received_clauses_by_network);
-    printf("c sharing skip_num_by_network: %d\n", num_skip_clauses_by_network);
+    printf("c [node-%d] sharing skip_num_by_network: %d\n", rank, 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);
+    printf("c [node-%d] sharing unique reduce percentage: %.2f%%\n", rank, (double) num_skip_clauses_by_network / num_received_clauses_by_network * 100);
 }
 
 void sharer::do_clause_sharing() {
@@ -153,9 +162,11 @@ void sharer::do_clause_sharing() {
 
     // 导入外部网络传输的子句
     std::vector<shared_ptr<clause_store>> clauses;
-    int from = receive_clauses_from_last_node(clauses);
+    int transmitter;
+    int from = receive_clauses_from_last_node(clauses, transmitter);
     if(from != -1 && clauses.size() > 0) {
-        printf("c [worker] get %d exported clauses from network\n", clauses.size());
+        printf("c [node-%d] get %d exported clauses from node-%d\n", rank, 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);

src/solve.cpp

@@ -68,7 +68,24 @@ void light::init_workers() {
 }
 
 void light::diversity_workers() {
+
+    int num_procs, rank;
+    MPI_Comm_size(MPI_COMM_WORLD, &num_procs);
+    MPI_Comm_rank(MPI_COMM_WORLD, &rank);
+
     for (int i = 0; i < OPT(threads); i++) {
+        
+        /**
+         * sat_group    [1, num_procs/2]
+         * unsat_group  [num_procs/2+1, num_procs-1]
+        */
+
+        if(rank <= num_procs / 2) {
+            workers[i]->configure("sat", 1);
+        } else {
+            workers[i]->configure("unsat", 1);
+        }
+
         if (OPT(shuffle)) {
             if (i) workers[i]->configure("order_reset", i);
         }

src/workers/basekissat.cpp

@@ -70,8 +70,12 @@ bool basekissat::imp_clause(shared_ptr<clause_store>cls, void *cl) {
     for (int i = 0; i < cls->size; i++) {
         // S->outimport << cls->data[i] << std::endl;
         int eidx = abs(cls->data[i]);
-        if (eidx >= SIZE_STACK(solver->import)) printf("c wrong %d\n", eidx);
+
+        assert(eidx > 0);
+
+        if (eidx >= SIZE_STACK(solver->import)) printf("c wrong %d   sizeo_stack %d\n", eidx, SIZE_STACK(solver->import));
         import *import = &PEEK_STACK (solver->import, eidx);
+
         if (import->eliminated) return false;
         else {
             int ilit = import->lit;