From 76470817cff75916078f1190c300ed7c47502f23 Mon Sep 17 00:00:00 2001 From: YuhangQ Date: Tue, 18 Apr 2023 12:45:22 +0000 Subject: [PATCH] =?UTF-8?q?=E4=BF=AE=E5=A4=8D=E9=97=AE=E9=A2=98=EF=BC=8Cba?= =?UTF-8?q?se=E7=89=88=E6=9C=AC?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- run.sh | 9 ++++++--- src/paras.hpp | 2 -- src/sharer.cpp | 12 +++++++----- src/solve.cpp | 12 +++++++----- 4 files changed, 20 insertions(+), 15 deletions(-) diff --git a/run.sh b/run.sh index 9ec83d3..f208001 100755 --- a/run.sh +++ b/run.sh @@ -12,10 +12,13 @@ # preprocess 占了特别大内存 # 04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf -DIR=/pub/data/chenzh/data/sat2022 -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 + +# 这个存在问题 +DIR=/pub/data/chenzh/data/sat2022 +INSTANCE=3d2a6e5c2f8f58dee79fd50444009625-cfi-rigid-z2-0088-03-or_2_shuffle_all.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 ./data/hard1.cnf --share=1 --threads=16 --times=3600 diff --git a/src/paras.hpp b/src/paras.hpp index da153a9..a233f9f 100644 --- a/src/paras.hpp +++ b/src/paras.hpp @@ -22,8 +22,6 @@ PARA( threads , int , '\0' , false , 32 , 1 , 128 , "Thread number") \ PARA( times , double , '\0' , false , 5000 , 0 , 1e8 , "Cutoff time") \ PARA( unique , int , '\0' , false , 1 , 0 , 1 , "Whether perform unique checking when receiving clauses from other nodes") - - // name, short-name, must-need, default, comments #define STR_PARAS \ diff --git a/src/sharer.cpp b/src/sharer.cpp index 1607b7e..7b48bcb 100644 --- a/src/sharer.cpp +++ b/src/sharer.cpp @@ -30,9 +30,11 @@ void share_clauses_to_next_node(int from, const std::vector(clk_now - clk_st).count(); - printf("c [worker] round %d, time: %d.%d\n", nums, solve_time / 1000, solve_time % 1000); + printf("c [node-%d] round %d, time: %d.%d\n", rank, nums, solve_time / 1000, solve_time % 1000); // 导入外部网络传输的子句 std::vector> clauses; @@ -166,7 +168,7 @@ void sharer::do_clause_sharing() { int from = receive_clauses_from_last_node(clauses, transmitter); if(from != -1 && clauses.size() > 0) { 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); + // 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); diff --git a/src/solve.cpp b/src/solve.cpp index a7dc376..72e8bc3 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -80,11 +80,13 @@ void light::diversity_workers() { * 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(rank <= num_procs / 2) { + // workers[i]->configure("sat", 1); + // OPT(share_lits) = 1500; + // } else { + // workers[i]->configure("unsat", 1); + // OPT(share_lits) = 3000; + // } if (OPT(shuffle)) { if (i) workers[i]->configure("order_reset", i);