同步代码

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 = []

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
 

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;

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;
+    int worker_procs = num_procs - 1;
-    if(rank == 0) {
+    if(worker_procs >= 8) {
-        S->last_node = S->next_node = 0;
+        // 分出一些 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

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

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);
+    int sol_thd = 0, intv_time = OPT(reset_time);// 初始化共享子句类
-
+    
-    // 初始化共享子句类
-    sharer* s;
     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();