From 3a310fe9ffe980ffb2addb342df8dbc04bd9b94c Mon Sep 17 00:00:00 2001 From: YuhangQ Date: Wed, 19 Apr 2023 06:05:55 +0000 Subject: [PATCH] =?UTF-8?q?=E5=A2=9E=E5=8A=A0sat-unsat=E6=A8=A1=E5=BC=8F?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- run.sh | 4 +- src/main.cpp | 8 +-- src/sharer.cpp | 18 ++++--- src/sharer.hpp | 4 +- src/solve.cpp | 131 ++++++++++++++++++++++++++++++++----------------- 5 files changed, 104 insertions(+), 61 deletions(-) diff --git a/run.sh b/run.sh index 3aaba04..20065cf 100755 --- a/run.sh +++ b/run.sh @@ -22,8 +22,8 @@ DIR=/pub/data/chenzh/data/sat2022 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 +# 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 +make -j 16 && mpirun --bind-to none -np 4 --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 diff --git a/src/main.cpp b/src/main.cpp index e04d279..922ba8c 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -36,21 +36,21 @@ int main(int argc, char **argv) { // [1, sat_procs] for sat if(rank >= 1 && rank <= sat_procs) { - S->worker_type = Light::SAT; + 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; + 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; + S->worker_type = light::DEFAULT; if(S->next_node > worker_procs) { S->next_node = sat_procs+unsat_procs+1; } @@ -58,7 +58,7 @@ int main(int argc, char **argv) { } else { // 总线程太小就跑默认策略 - S->worker_type = Light::DEFAULT; + S->worker_type = light::DEFAULT; S->next_node = rank + 1; if(S->next_node > worker_procs) { S->next_node = 1; diff --git a/src/sharer.cpp b/src/sharer.cpp index 7b48bcb..4d13d96 100644 --- a/src/sharer.cpp +++ b/src/sharer.cpp @@ -160,14 +160,14 @@ void sharer::do_clause_sharing() { auto clk_now = std::chrono::high_resolution_clock::now(); int solve_time = std::chrono::duration_cast(clk_now - clk_st).count(); - printf("c [node-%d] round %d, time: %d.%d\n", rank, nums, solve_time / 1000, solve_time % 1000); + printf("c node%d(%d)round %d, time: %d.%d\n", rank, S->worker_type, nums, solve_time / 1000, solve_time % 1000); // 导入外部网络传输的子句 std::vector> clauses; int transmitter; 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(%d) get %d exported clauses from node-%d\n", rank, S->worker_type, 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++) { @@ -205,12 +205,14 @@ void sharer::do_clause_sharing() { // 增加 lits 限制 int percent = sort_clauses(i); - // if (percent < 75) { - // producers[i]->broaden_export_limit(); - // } - // else if (percent > 98) { - // producers[i]->restrict_export_limit(); - // } + if(S->worker_type == light::UNSAT) { + if (percent < 75) { + producers[i]->broaden_export_limit(); + } + else if (percent > 98) { + producers[i]->restrict_export_limit(); + } + } for (int j = 0; j < consumers.size(); j++) { if (producers[i]->id == consumers[j]->id) continue; diff --git a/src/sharer.hpp b/src/sharer.hpp index d2f0a64..b61ec2d 100644 --- a/src/sharer.hpp +++ b/src/sharer.hpp @@ -12,7 +12,7 @@ public: vec producers, consumers; std::vector> cls; - sharer(int next_node):next_node(next_node) {} + sharer(light *S):S(S) {} void do_clause_sharing(); void clause_sharing_init(); @@ -22,7 +22,7 @@ public: int import_clauses(int id); private: - int next_node; + light* S; }; #endif \ No newline at end of file diff --git a/src/solve.cpp b/src/solve.cpp index 7680f6a..44c44f5 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -74,58 +74,99 @@ void light::diversity_workers() { 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(worker_type == SAT) { - // 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); + } - if (OPT(shuffle)) { - if (i) workers[i]->configure("order_reset", i); - } - if (OPT(pakis)) { - if (i == 13 || i == 14 || i == 9) - workers[i]->configure("tier1", 3); - else - workers[i]->configure("tier1", 2); + workers[i]->configure("stable", 1); + workers[i]->configure("target", 2); + workers[i]->configure("phase", 1); + workers[i]->configure("heuristic", 0); - if (i == 3 || i == 6 || i == 8 || i == 11 || i == 12 || i == 13 || i == 14 || i == 15) - workers[i]->configure("chrono", 0); - else - workers[i]->configure("chrono", 1); + if (i == 2) + workers[i]->configure("stable", 0); + else if (i == 6) + workers[i]->configure("stable", 2); - if (i == 2 || i == 15) - workers[i]->configure("stable", 0); - else if (i == 6 || i == 14) - workers[i]->configure("stable", 2); - else - workers[i]->configure("stable", 1); - - if (i == 10) - workers[i]->configure("walkinitially", 1); - else - workers[i]->configure("walkinitially", 0); - - if (i == 7 || i == 8 || i == 9 || i == 11) + if (i == 7) workers[i]->configure("target", 0); - else if (i == 0 || i == 2 || i == 3 || i == 4 || i == 5 || i == 6 || i == 10) + else if (i == 0 || i == 2 || i == 3 || i == 6) workers[i]->configure("target", 1); - else - workers[i]->configure("target", 2); - - if (i == 4 || i == 5 || i == 8 || i == 9 || i == 12 || i == 13 || i == 15) + + if (i == 3 || i == 11 || i == 12 || i == 13 || i == 15) workers[i]->configure("phase", 0); - else - workers[i]->configure("phase", 1); + } else if(worker_type == UNSAT) { + + OPT(share_lits) = 3000; + + workers[i]->configure("chrono", 1); + workers[i]->configure("stable", 0); + // workers[i]->configure("walkinitially", 0); + workers[i]->configure("target", 1); + // workers[i]->configure("phase", 1); + workers[i]->configure("heuristic", 0); + // workers[i]->configure("margin", 1)0; + + if (i == 0 || i == 1 || i == 7 || i == 8 || i == 11 || i == 15) + workers[i]->configure("heuristic", 1); + + if (i == 3 || i == 6 || i == 8 || i == 11 || i == 12 || i == 13) + workers[i]->configure("chrono", 0); + + if (i == 2) + workers[i]->configure("stable", 1); + + if (i == 9) + workers[i]->configure("target", 0); + else if (i == 14) + workers[i]->configure("target", 2); + } else { + + if (OPT(shuffle)) { + if (i) workers[i]->configure("order_reset", i); + } + + if (OPT(pakis)) { + if (i == 13 || i == 14 || i == 9) + workers[i]->configure("tier1", 3); + else + workers[i]->configure("tier1", 2); + + if (i == 3 || i == 6 || i == 8 || i == 11 || i == 12 || i == 13 || i == 14 || i == 15) + workers[i]->configure("chrono", 0); + else + workers[i]->configure("chrono", 1); + + if (i == 2 || i == 15) + workers[i]->configure("stable", 0); + else if (i == 6 || i == 14) + workers[i]->configure("stable", 2); + else + workers[i]->configure("stable", 1); + + if (i == 10) + workers[i]->configure("walkinitially", 1); + else + workers[i]->configure("walkinitially", 0); + + if (i == 7 || i == 8 || i == 9 || i == 11) + workers[i]->configure("target", 0); + else if (i == 0 || i == 2 || i == 3 || i == 4 || i == 5 || i == 6 || i == 10) + workers[i]->configure("target", 1); + else + workers[i]->configure("target", 2); + + if (i == 4 || i == 5 || i == 8 || i == 9 || i == 12 || i == 13 || i == 15) + workers[i]->configure("phase", 0); + else + workers[i]->configure("phase", 1); + } + } + + for (int j = 0; j < configure_name[i].size(); j++) { workers[i]->configure(configure_name[i][j], configure_val[i][j]); } @@ -169,7 +210,7 @@ int light::solve() { int sol_thd = 0, intv_time = OPT(reset_time);// 初始化共享子句类 if(OPT(share)) { - s = new sharer(); + s = new sharer(this); for (int j = 0; j < OPT(threads); j++) { s->producers.push(workers[j]); s->consumers.push(workers[j]);