diff --git a/docker/light b/docker/light index d3df25c..c8247fd 100755 Binary files a/docker/light and b/docker/light differ diff --git a/run.sh b/run.sh index ae7b210..41960fa 100755 --- a/run.sh +++ b/run.sh @@ -1,3 +1,3 @@ #!/bin/bash -make -j 16 && mpirun -q -np 4 --allow-run-as-root ./light -i data/class_1_easy_10_0.cnf --share=1 --threads=4 --times=60 \ No newline at end of file +make -j 16 && mpirun -np 4 --allow-run-as-root ./light -i data/class_1_easy_10_0.cnf --share=1 --threads=4 --times=60 \ No newline at end of file diff --git a/src/distributed/clause_pack.hpp b/src/distributed/clause_pack.hpp new file mode 100644 index 0000000..e19edb5 --- /dev/null +++ b/src/distributed/clause_pack.hpp @@ -0,0 +1,9 @@ +#include "../utils/vec.hpp" +#include "../workers/clause.hpp" + + +class ClausePack { + + + +}; \ No newline at end of file diff --git a/src/distributed/comm_tag.h b/src/distributed/comm_tag.h index 7d66d3d..dfd40d1 100644 --- a/src/distributed/comm_tag.h +++ b/src/distributed/comm_tag.h @@ -4,4 +4,5 @@ const int TERMINATE_TAG = 0; const int SOLVED_REPORT_TAG = 1; const int MODEL_REPORT_TAG = 2; -const int START_TAG = 3; \ No newline at end of file +const int START_TAG = 3; +const int SHARE_CLAUSES_TAG = 4; \ No newline at end of file diff --git a/src/distributed/leader.hpp b/src/distributed/leader.hpp index f54b45d..dbdd0bb 100644 --- a/src/distributed/leader.hpp +++ b/src/distributed/leader.hpp @@ -12,8 +12,6 @@ #include "../paras.hpp" #include "heartbeat.h" - - void leader_main(light* S, int num_procs, int rank) { auto clk_st = std::chrono::high_resolution_clock::now(); @@ -129,11 +127,6 @@ void leader_main(light* S, int num_procs, int rank) { if(res == 10) { printf("s SAT\n"); - for(int i=0; ivars; i++) { - printf("%d ", sol[i]); - } - printf("\n"); - for (int i = 1; i <= pre->orivars; i++) if (pre->mapto[i]) pre->mapval[i] = (sol[abs(pre->mapto[i])-1] > 0 ? 1 : -1) * (pre->mapto[i] > 0 ? 1 : -1); diff --git a/src/workers/basekissat.cpp b/src/workers/basekissat.cpp index a7db2cd..f2ff149 100644 --- a/src/workers/basekissat.cpp +++ b/src/workers/basekissat.cpp @@ -93,7 +93,7 @@ int call_back_in(void *solver, int *lbd, cvec *c) { } if (!res) return -10; return 1; -} +} basekissat::basekissat(int id, light* light) : basesolver(id, light) { solver = kissat_init(); diff --git a/src/workers/clause.hpp b/src/workers/clause.hpp index 010accd..27a36b9 100644 --- a/src/workers/clause.hpp +++ b/src/workers/clause.hpp @@ -19,6 +19,7 @@ struct clause_store { bool free_clause() { int ref = refs.fetch_sub(1); if (ref <= 1) { + // printf("c free clause: "); // for (int i = 0; i < size; i++) // printf("%d ", data[i]); // puts(""); diff --git a/src/workers/sharer.cpp b/src/workers/sharer.cpp index 7122cb3..2a6c122 100644 --- a/src/workers/sharer.cpp +++ b/src/workers/sharer.cpp @@ -3,13 +3,134 @@ #include "sharer.hpp" #include "clause.hpp" #include +#include "../distributed/comm_tag.h" #include +void share_clauses_to_next_node(std::vector> &send_data_struct, const vec &cls) { + + // 清理 send_data_struct,把发送完毕的发送数据结构清理掉 + for(int i=0; isize + 2); + } + + send_buf = new int[send_length]; + int index = 0; + + for(int i=0; isize; + send_buf[index++] = c->lbd; + for(int j=0; jsize; j++) { + send_buf[index++] = c->data[j]; + } + } + + assert(index == send_length); + + // 调用 MPI 发送共享子句 + + int num_procs, rank; + MPI_Comm_size(MPI_COMM_WORLD, &num_procs); + MPI_Comm_rank(MPI_COMM_WORLD, &rank); + + int target = rank % (num_procs - 1) + 1; + + MPI_Isend(send_buf, send_length, MPI_INT, target, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, &send_request); + + send_data_struct.push_back(std::make_pair(send_request, send_buf)); + + LOGGER->info("send clauses: %v", send_length); +} + + +const int BUF_SIZE = 1024 * 1024; + +bool receive_clauses_from_last_node(MPI_Request &receive_request, int *buf, vec &clauses) { + clauses.clear(); + + + int flag; + MPI_Status status; + + int index = 0; + + // 已接收完数据 + if(MPI_Test(&receive_request, &flag, &status) == MPI_SUCCESS && flag == 1) { + int count; + MPI_Get_count(&status, MPI_INT, &count); + + + while(index < count) { + clause_store* cl = new clause_store(buf[index++]); + cl->lbd = buf[index++]; + for(int i=0; isize; i++) { + cl->data[i] = buf[index++]; + } + clauses.push(cl); + } + + assert(index == count); + + // 进行下一步接收数据 + + int num_procs, rank; + MPI_Comm_size(MPI_COMM_WORLD, &num_procs); + MPI_Comm_rank(MPI_COMM_WORLD, &rank); + + int from = (rank - 2 + num_procs - 1) % (num_procs - 1) + 1; + + LOGGER->info("receive clauses: %v", count); + + MPI_Irecv(buf, BUF_SIZE, MPI_INT, from, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, &receive_request); + + return true; + } + + return false; + +} + void * share_worker(void *arg) { int nums = 0; sharer * sq = (sharer *)arg; auto clk_st = std::chrono::high_resolution_clock::now(); double share_time = 0; + + std::vector> send_data_struct; + + MPI_Request receive_request; + + int buf[BUF_SIZE]; + + int num_procs, rank; + MPI_Comm_size(MPI_COMM_WORLD, &num_procs); + MPI_Comm_rank(MPI_COMM_WORLD, &rank); + + int from = (rank - 2 + num_procs - 1) % (num_procs - 1) + 1; + MPI_Irecv(buf, BUF_SIZE, MPI_INT, from, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, &receive_request); + while (true) { ++nums; usleep(sq->share_intv); @@ -23,7 +144,33 @@ void * share_worker(void *arg) { sq->producers[i]->export_clauses_to(sq->cls); // printf("c size %d\n", sq->cls.size()); int number = sq->cls.size(); - // printf("get %d exported clauses\n", number); + + LOGGER->info("thread-%v: get %v exported clauses", i, number); + + + // 分享当前节点产生的子句 + share_clauses_to_next_node(send_data_struct, sq->cls); + + + // 导入外部网络传输的子句 + vec clauses; + if(receive_clauses_from_last_node(receive_request, buf, clauses)) { + for (int j = 0; j < sq->consumers.size(); j++) { + for (int k = 0; k < clauses.size(); k++) + clauses[k]->increase_refs(1); + sq->consumers[j]->import_clauses_from(clauses); + } + + // 传递外部网络传输的子句给下个节点 + share_clauses_to_next_node(send_data_struct, clauses); + + for (int k = 0; k < clauses.size(); k++) { + clauses[k]->free_clause(); + } + } + + + // 导入当前节点产生的子句 int percent = sq->sort_clauses(i); if (percent < 75) { sq->producers[i]->broaden_export_limit(); diff --git a/src/workers/sharer.hpp b/src/workers/sharer.hpp index 233864a..bcbd0f9 100644 --- a/src/workers/sharer.hpp +++ b/src/workers/sharer.hpp @@ -2,6 +2,8 @@ #define _sharer_hpp_INCLUDED #include "../paras.hpp" #include +#include "../utils/vec.hpp" +#include "clause.hpp" class basesolver; class sharer {