From 9038ce048b74f78327d0f6fff82c68d087b3dfa8 Mon Sep 17 00:00:00 2001
From: YuhangQ <i@yuhangq.com>
Date: Wed, 19 Apr 2023 13:49:18 +0800
Subject: [PATCH] =?UTF-8?q?=E5=90=8C=E6=AD=A5=E4=BB=A3=E7=A0=81?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 experiment/cal.py |  3 +++
 run.sh            |  6 +++++-
 src/light.hpp     |  6 ++++--
 src/main.cpp      | 46 +++++++++++++++++++++++++++++++++++++++-------
 src/sharer.hpp    |  5 +++++
 src/solve.cpp     |  8 +++-----
 6 files changed, 59 insertions(+), 15 deletions(-)

diff --git a/experiment/cal.py b/experiment/cal.py
index d0c105c..25624a8 100755
--- a/experiment/cal.py
+++ b/experiment/cal.py
@@ -273,9 +273,12 @@ def gen_samples(dir):
 
 if __name__ == "__main__":
     solvers = []
+    # solvers.append(solver_SAT_standard_gnomon("/pub/netdisk1/qianyh/aws-batch-comp-infrastructure-sample/docker/runner/exp-result","mallob"))
+    solvers.append(solver_SAT_standard_gnomon("./exp-result","light-new"))
     solvers.append(solver_SAT_standard_gnomon("./light-circle","light-circle"))
     solvers.append(solver_SAT_standard_gnomon("./light-circle-unique","light-circle-unique"))
     solvers.append(solver_SAT_standard_gnomon("./first_version","bug-cloud"))
+    
     # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/huawei_sat/kissat-mab","origin-mab"))
     # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/huawei_simp/kissat-mab","preprocess-mab"))
     samples = []
diff --git a/run.sh b/run.sh
index f208001..3aaba04 100755
--- a/run.sh
+++ b/run.sh
@@ -10,13 +10,17 @@
 # 03bb7baaa45980753a0e7050ae44755d-atco_enc3_opt1_03_53.cnf
 
 # preprocess 占了特别大内存
+
+
+
+# 有BUG
 # 04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf
 
 
 
 # 这个存在问题
 DIR=/pub/data/chenzh/data/sat2022
-INSTANCE=3d2a6e5c2f8f58dee79fd50444009625-cfi-rigid-z2-0088-03-or_2_shuffle_all.cnf
+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
 
diff --git a/src/light.hpp b/src/light.hpp
index fb4ed6a..cefe3bd 100644
--- a/src/light.hpp
+++ b/src/light.hpp
@@ -44,12 +44,14 @@ public:
     pthread_t *sharer_ptrs;
     vec<int> model;
 
+    sharer* s;
+    enum { SAT, UNSAT, DEFAULT } worker_type;
+    int next_node;
+
     MPI_Request terminal_request;
 
     int num_procs;
     int rank;
-    int next_node;
-    int last_node;
 
     char* filename;
     char* instance;
diff --git a/src/main.cpp b/src/main.cpp
index 2d3bf73..e04d279 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -23,14 +23,46 @@ int main(int argc, char **argv) {
     light* S = new light();
     S->arg_parse(argc, argv);
 
-    // 初始化环形节点关系
-    S->rank = rank;
-    S->num_procs = num_procs;
-    if(rank == 0) {
-        S->last_node = S->next_node = 0;
+    // 初始化环形数据结构
+
+    int worker_procs = num_procs - 1;
+    if(worker_procs >= 8) {
+        // 分出一些 worker 跑其他策略
+        int sat_procs = worker_procs / 8;
+        int unsat_procs = sat_procs;
+        int default_procs = worker_procs - sat_procs - unsat_procs;
+
+        S->next_node = rank + 1;
+
+        // [1, sat_procs] for sat
+        if(rank >= 1 && rank <= sat_procs) {
+            S->worker_type = Light::SAT;
+            if(S->next_node > sat_procs) {
+                S->next_node = 1;
+            }
+        }
+        // [sat_procs+1, sat_procs+unsat_procs] for unsat
+        if(rank >= sat_procs+1 && rank <= sat_procs+unsat_procs) {
+            S->worker_type = Light::UNSAT;
+            if(S->next_node > sat_procs+unsat_procs) {
+                S->next_node = sat_procs+1;
+            }
+        }
+        // [sat_procs+unsat_procs+1, worker_procs]
+        if(rank >= sat_procs+unsat_procs+1 && rank <= worker_procs) {
+            S->worker_type = Light::DEFAULT;
+            if(S->next_node > worker_procs) {
+                S->next_node = sat_procs+unsat_procs+1;
+            }
+        }
+
     } else {
-        S->last_node = (rank - 2 + num_procs - 1) % (num_procs - 1) + 1;
-        S->next_node = rank % (num_procs - 1) + 1;
+        // 总线程太小就跑默认策略
+        S->worker_type = Light::DEFAULT;
+        S->next_node = rank + 1;
+        if(S->next_node > worker_procs) {
+            S->next_node = 1;
+        }
     }
 
     // leader
diff --git a/src/sharer.hpp b/src/sharer.hpp
index a4050f1..d2f0a64 100644
--- a/src/sharer.hpp
+++ b/src/sharer.hpp
@@ -12,12 +12,17 @@ public:
     vec<basesolver *> producers, consumers;
     std::vector<shared_ptr<clause_store>> cls;
 
+    sharer(int next_node):next_node(next_node) {}
+
     void do_clause_sharing();
     void clause_sharing_init();
     void clause_sharing_end();
 
     int sort_clauses(int x);
     int import_clauses(int id);
+
+private:
+    int next_node;
 };
 
 #endif
\ No newline at end of file
diff --git a/src/solve.cpp b/src/solve.cpp
index 72e8bc3..7680f6a 100644
--- a/src/solve.cpp
+++ b/src/solve.cpp
@@ -166,10 +166,8 @@ int light::solve() {
     thread_inf unimprove[OPT(threads)];
     auto clk_sol_st = std::chrono::high_resolution_clock::now();
     int pre_time = std::chrono::duration_cast<std::chrono::seconds>(clk_sol_st - clk_st).count();
-    int sol_thd = 0, intv_time = OPT(reset_time);
-
-    // 初始化共享子句类
-    sharer* s;
+    int sol_thd = 0, intv_time = OPT(reset_time);// 初始化共享子句类
+    
     if(OPT(share)) {
         s = new sharer();
         for (int j = 0; j < OPT(threads); j++) {
@@ -226,7 +224,7 @@ int light::solve() {
 int light::run() {
 
     init_workers();
-    diversity_workers();    
+    diversity_workers();
 
     parse_input();