From 94feff698a7cfc849e06d10d07c6666477e1596a Mon Sep 17 00:00:00 2001
From: YuhangQ <i@yuhangq.com>
Date: Fri, 28 Apr 2023 08:56:18 +0000
Subject: [PATCH] =?UTF-8?q?=E4=BF=AE=E6=94=B9=E4=B8=80=E4=BA=9B=E9=97=AE?=
 =?UTF-8?q?=E9=A2=98=EF=BC=8C=E5=86=85=E5=AD=98=E6=94=B9=E4=B8=BA5.5?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 run.sh         | 16 ++++++++--------
 src/solve.cpp  |  9 +++++++--
 src/worker.hpp |  2 +-
 3 files changed, 16 insertions(+), 11 deletions(-)

diff --git a/run.sh b/run.sh
index 95c5a45..bb7c348 100755
--- a/run.sh
+++ b/run.sh
@@ -1,11 +1,11 @@
 #!/bin/bash
 
-cd kissat-inc
-make clean
-./configure
-make -j 64
-cd ..
-make clean
+# cd kissat-inc
+# make clean
+# ./configure
+# make -j 64
+# cd ..
+# make clean
 
 # buglist
 # - fe96b630b3e761821308b544368dd521-GP_100_950_34.cnf
@@ -13,11 +13,11 @@ make clean
 
 # 这个存在问题
 DIR=/pub/data/chenzh/data/sat2022
-INSTANCE=30ca21da9753263cc8cda020802b58ce-GP_500_200_20.cnf
+INSTANCE=0d4970edf84353e5a5798bca3f7f270e-SAT_H_instances_childsnack_p10.hddl_2.cnf
 
 
 # make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --shuffle=1 --share=1 --threads=16 --times=3600 --share_method=1
 
-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 --share_method=0
+make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 --share_method=0
 
 #./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600
diff --git a/src/solve.cpp b/src/solve.cpp
index 327410b..82fdc88 100644
--- a/src/solve.cpp
+++ b/src/solve.cpp
@@ -62,7 +62,7 @@ void light::diversity_workers() {
                 workers[i]->configure("worker_index", i);
                 workers[i]->configure("worker_number", OPT(threads));
 
-                if(rank == 1 || rank == num_procs - 1) {
+                if(rank == 1) {
                     workers[i]->configure("worker_seed", 0);
                 } else {
                     workers[i]->configure("worker_seed", rank);
@@ -117,6 +117,12 @@ void light::diversity_workers() {
             if (OPT(shuffle)) {
                 workers[i]->configure("worker_index", i);
                 workers[i]->configure("worker_number", OPT(threads));
+
+                if(rank == num_procs - 1) {
+                    workers[i]->configure("worker_seed", 0);
+                } else {
+                    workers[i]->configure("worker_seed", rank);
+                }
                 workers[i]->configure("worker_seed", rank);
             // printf("r1: %d, r2: %d, r3: %d\n", r1, r2, r3);
             }
@@ -311,7 +317,6 @@ void light::seperate_groups() {
     }
 }
 
-
 void print_model(vec<int> &model) {
     printf("v");
     for (int i = 0; i < model.size(); i++) {
diff --git a/src/worker.hpp b/src/worker.hpp
index e159b6f..3e103e9 100644
--- a/src/worker.hpp
+++ b/src/worker.hpp
@@ -43,7 +43,7 @@ void worker_main(light* S, int num_procs, int rank) {
     MPI_Barrier(MPI_COMM_WORLD);
 
     // mem_usage per thread per G input file (GB)
-    double mem_ptpg = 20.4;
+    double mem_ptpg = 5.5;
 
     // mem_usage per thread (GB)
     double mem_pt = (double)cnf_length / 1073741824 * mem_ptpg;