From 11449eca3bebbfff98ba6f963e1029326cc2452c Mon Sep 17 00:00:00 2001 From: YuhangQ Date: Thu, 20 Apr 2023 14:49:05 +0800 Subject: [PATCH] =?UTF-8?q?=E6=A0=91=E5=BD=A2=E4=BC=A0=E6=92=AD=E5=88=9D?= =?UTF-8?q?=E7=89=88=E5=B7=B2=E5=AE=9E=E7=8E=B0?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- makefile | 2 +- run.sh | 4 +- src/sharer.cpp | 116 ++++++++++++++++++++++++++----------------------- src/sharer.hpp | 6 +-- src/solve.cpp | 3 -- 5 files changed, 68 insertions(+), 63 deletions(-) diff --git a/makefile b/makefile index 1c195e9..f438f11 100644 --- a/makefile +++ b/makefile @@ -6,7 +6,7 @@ OBJECTS := $(addprefix build/,$(SOURCES:%=%.o)) # 声明编译器和编译选项 CXX := mpicxx -CXXFLAGS := -O3 -Wall -Wextra -MMD -MP -march=native -mtune=native -g +CXXFLAGS := -std=c++17 -O3 -Wall -Wextra -MMD -MP -march=native -mtune=native -g LIBS := -Wl,-Bstatic -lkissat -L kissat-inc/build -I kissat-inc/ \ -lm4ri -L m4ri-20140914/.libs -I m4ri-20140914/ \ diff --git a/run.sh b/run.sh index 2ff9c54..846df2f 100755 --- a/run.sh +++ b/run.sh @@ -25,8 +25,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 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 -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 +make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i ./data/WS_500_16_70_10.apx_0.cnf --share=1 --threads=16 --times=3600 #./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 diff --git a/src/sharer.cpp b/src/sharer.cpp index 0f4dcb0..696759f 100644 --- a/src/sharer.cpp +++ b/src/sharer.cpp @@ -23,13 +23,12 @@ int num_skip_clauses_by_network = 0; std::unordered_map clause_imported; -void sharer::share_clauses_to_next_node(int from, const std::vector> &cls) { +void sharer::share_clauses_to_other_node(int from, const std::vector> &cls) { // 环形传递，数据来源如果是目的地，说明数据已轮转一圈，停止发送。 if(OPT(share_method) == 0 && from == next_node) return; // 定义发送数据 - MPI_Request *send_request = new MPI_Request(); int send_length = 1; // 初始化发送数据 @@ -37,7 +36,11 @@ void sharer::share_clauses_to_next_node(int from, const std::vectorsize + 2); } - shared_ptr send_buf = std::make_shared(send_length); + shared_ptr send_buf(new int[send_length]()); + + for(int i=0; i> &clauses, int &transmitter) { +int sharer::receive_clauses_from_other_node(std::vector> &clauses, int &transmitter) { clauses.clear(); int flag; MPI_Status status; transmitter = -1; - int from = -1; - // 已接收完数据 - while(MPI_Test(&receive_request, &flag, &status) == MPI_SUCCESS && flag == 1) { - int index = 0; - int count; - MPI_Get_count(&status, MPI_INT, &count); + MPI_Test(&receive_request, &flag, &status); - if(transmitter == -1) { - transmitter = status.MPI_SOURCE; - } - - //assert(transmitter == status.MPI_SOURCE); - - from = buf[index++]; - - while(index < count) { - num_received_clauses_by_network++; - - shared_ptr cl = std::make_shared(buf[index++]); - - cl->lbd = buf[index++]; - for(int i=0; isize; i++) { - cl->data[i] = buf[index++]; - } - - if(clause_imported[cl->hash_code()]) { - - num_skip_clauses_by_network++; - continue; - } - - clauses.push_back(cl); - } - - assert(index == count); - - MPI_Irecv(buf, BUF_SIZE, MPI_INT, MPI_ANY_SOURCE, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, &receive_request); + // 没有数据需要接收 + if(flag == 0) { + return -1; } + int index = 0; + int count; + MPI_Get_count(&status, MPI_INT, &count); + + transmitter = status.MPI_SOURCE; + + from = buf[index++]; + + while(index < count) { + num_received_clauses_by_network++; + + shared_ptr cl = std::make_shared(buf[index++]); + + cl->lbd = buf[index++]; + for(int i=0; isize; i++) { + cl->data[i] = buf[index++]; + } + + if(clause_imported[cl->hash_code()]) { + num_skip_clauses_by_network++; + continue; + } + + clauses.push_back(cl); + } + + assert(index == count); + + MPI_Irecv(buf, BUF_SIZE, MPI_INT, MPI_ANY_SOURCE, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, &receive_request); + return from; } @@ -183,8 +191,8 @@ void sharer::do_clause_sharing() { // 导入外部网络传输的子句 std::vector> clauses; int transmitter; - int from = receive_clauses_from_last_node(clauses, transmitter); - if(from != -1 && clauses.size() > 0) { + int from; + while((from = receive_clauses_from_other_node(clauses, transmitter)) != -1 &&clauses.size() > 0) { 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); @@ -197,10 +205,9 @@ void sharer::do_clause_sharing() { } // 传递外部网络传输的子句给下个节点 - share_clauses_to_next_node(from, clauses); + share_clauses_to_other_node(from, clauses); } - // printf("start sharing %d\n", sq->share_intv); for (int i = 0; i < producers.size(); i++) { cls.clear(); producers[i]->export_clauses_to(cls); @@ -216,7 +223,7 @@ void sharer::do_clause_sharing() { cls.resize(t_size); //分享当前节点产生的子句 - if(cls.size() > 0) share_clauses_to_next_node(rank, cls); + if(cls.size() > 0) share_clauses_to_other_node(rank, cls); //printf("c [worker] thread-%d: get %d exported clauses\n", i, t_size); @@ -338,8 +345,6 @@ int sharer::sort_clauses(int x) { // } // } - - void sharer::init_tree_transmission(std::vector> &sharing_groups) { srand(19260817); @@ -352,8 +357,9 @@ void sharer::init_tree_transmission(std::vector> &sharing_group } } - for(int i=0; i &group = sharing_groups[i]; @@ -363,7 +369,7 @@ void sharer::init_tree_transmission(std::vector> &sharing_group // radom shuffle std::vector rs = group; // keep group[j] as the first - std::swap(group[j], group[0]); + std::swap(rs[j], rs[0]); for(int k=1; k> &sharing_group // printf("son[%d] [%d]\n", rs[0], rs[k]); // son[1][1][0] =213; - son[rs[0]][rs[k]][0] = ( 2 * k + 1 < rs.size() ) ? rs[ 2 * k + 1 ] : -1; son[rs[0]][rs[k]][1] = ( 2 * k + 2 < rs.size() ) ? rs[ 2 * k + 2 ] : -1; + + printf("c son[%d][%d][%d]=%d\tson[%d][%d][%d]=%d\n", rs[0], rs[k], 0, son[rs[0]][rs[k]][0], rs[0], rs[k], 1, son[rs[0]][rs[k]][1]); + } } diff --git a/src/sharer.hpp b/src/sharer.hpp index 7742f0e..1f90ca8 100644 --- a/src/sharer.hpp +++ b/src/sharer.hpp @@ -32,14 +32,14 @@ public: void init_circular_transmission(std::vector> &sharing_groups); void init_tree_transmission(std::vector> &sharing_groups); - void share_clauses_to_next_node(int from, const std::vector> &cls); - int receive_clauses_from_last_node(std::vector> &clauses, int &transmitter); + void share_clauses_to_other_node(int from, const std::vector> &cls); + int receive_clauses_from_other_node(std::vector> &clauses, int &transmitter); int sort_clauses(int x); int import_clauses(int id); private: - light* S; + light* S; }; #endif \ No newline at end of file diff --git a/src/solve.cpp b/src/solve.cpp index 977517e..42843fe 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -285,7 +285,6 @@ void light::seperate_groups() { tmp.push_back(i); } sharing_groups.push_back(tmp); - // [sat_procs+1, sat_procs+unsat_procs] for unsat if(rank >= sat_procs+1 && rank <= sat_procs+unsat_procs) { @@ -318,8 +317,6 @@ void light::seperate_groups() { } sharing_groups.push_back(tmp); } - - printf("sg: %d\n", sharing_groups[0].size()); } void print_model(vec &model) {