树形传播初版已实现
This commit is contained in:
parent
64aeac80f1
commit
11449eca3b
2
makefile
2
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/ \
|
||||
|
||||
4
run.sh
4
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
|
||||
|
||||
114
src/sharer.cpp
114
src/sharer.cpp
@ -23,13 +23,12 @@ int num_skip_clauses_by_network = 0;
|
||||
|
||||
std::unordered_map<int, bool> clause_imported;
|
||||
|
||||
void sharer::share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_store>> &cls) {
|
||||
void sharer::share_clauses_to_other_node(int from, const std::vector<shared_ptr<clause_store>> &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::vector<shared_ptr<c
|
||||
send_length += (cls[i]->size + 2);
|
||||
}
|
||||
|
||||
shared_ptr<int[]> send_buf = std::make_shared<int[]>(send_length);
|
||||
shared_ptr<int[]> send_buf(new int[send_length]());
|
||||
|
||||
for(int i=0; i<send_length; i++) {
|
||||
send_buf[i] = i;
|
||||
}
|
||||
|
||||
int index = 0;
|
||||
|
||||
@ -57,20 +60,28 @@ void sharer::share_clauses_to_next_node(int from, const std::vector<shared_ptr<c
|
||||
// 调用 MPI 发送共享子句
|
||||
|
||||
if(OPT(share_method)) {
|
||||
|
||||
// printf("MPI_SEND: %d %d from: %d rank: %d\n", son[from][rank][0], son[from][rank][1], from, rank);
|
||||
|
||||
// 树形传递
|
||||
if(son[from][rank][0] != -1) {
|
||||
MPI_Request *send_request = new MPI_Request();
|
||||
MPI_Isend(send_buf.get(), send_length, MPI_INT, son[from][rank][0], SHARE_CLAUSES_TAG, MPI_COMM_WORLD, send_request);
|
||||
send_data_struct.push_back(std::make_pair(send_request, send_buf));
|
||||
}
|
||||
if(son[from][rank][1] != -1) {
|
||||
MPI_Request *send_request = new MPI_Request();
|
||||
MPI_Isend(send_buf.get(), send_length, MPI_INT, son[from][rank][1], SHARE_CLAUSES_TAG, MPI_COMM_WORLD, send_request);
|
||||
send_data_struct.push_back(std::make_pair(send_request, send_buf));
|
||||
}
|
||||
|
||||
} else {
|
||||
MPI_Request *send_request = new MPI_Request();
|
||||
// 环形传递
|
||||
MPI_Isend(send_buf.get(), send_length, MPI_INT, next_node, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, send_request);
|
||||
send_data_struct.push_back(std::make_pair(send_request, send_buf));
|
||||
}
|
||||
|
||||
send_data_struct.push_back(std::make_pair(send_request, send_buf));
|
||||
|
||||
// printf("c [worker] send clauses: %d\n", send_length);
|
||||
|
||||
// 清理 send_data_struct，把发送完毕的发送数据结构清理掉
|
||||
@ -82,59 +93,56 @@ void sharer::share_clauses_to_next_node(int from, const std::vector<shared_ptr<c
|
||||
// 与数组最后一个交换，然后 pop_back;
|
||||
std::swap(send_data_struct[i], send_data_struct[send_data_struct.size()-1]);
|
||||
send_data_struct.pop_back();
|
||||
// printf("c [worker] free send request, now: %d\n", send_data_struct.size());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
int sharer::receive_clauses_from_last_node(std::vector<shared_ptr<clause_store>> &clauses, int &transmitter) {
|
||||
int sharer::receive_clauses_from_other_node(std::vector<shared_ptr<clause_store>> &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<clause_store> cl = std::make_shared<clause_store>(buf[index++]);
|
||||
|
||||
cl->lbd = buf[index++];
|
||||
for(int i=0; i<cl->size; 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<clause_store> cl = std::make_shared<clause_store>(buf[index++]);
|
||||
|
||||
cl->lbd = buf[index++];
|
||||
for(int i=0; i<cl->size; 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<shared_ptr<clause_store>> 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<std::vector<int>> &sharing_groups) {
|
||||
|
||||
srand(19260817);
|
||||
@ -352,8 +357,9 @@ void sharer::init_tree_transmission(std::vector<std::vector<int>> &sharing_group
|
||||
}
|
||||
}
|
||||
|
||||
for(int i=0; i<sharing_groups.size(); i++) {
|
||||
|
||||
printf("c =========build tree=========\n");
|
||||
for(int i=0; i<sharing_groups.size(); i++) {
|
||||
// create binary trees for every group;
|
||||
std::vector<int> &group = sharing_groups[i];
|
||||
|
||||
@ -363,7 +369,7 @@ void sharer::init_tree_transmission(std::vector<std::vector<int>> &sharing_group
|
||||
// radom shuffle
|
||||
std::vector<int> 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<rs.size(); k++) {
|
||||
std::swap(rs[k], rs[rand()%(rs.size()-1)+1]);
|
||||
}
|
||||
@ -373,9 +379,11 @@ void sharer::init_tree_transmission(std::vector<std::vector<int>> &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]);
|
||||
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
@ -32,8 +32,8 @@ public:
|
||||
void init_circular_transmission(std::vector<std::vector<int>> &sharing_groups);
|
||||
void init_tree_transmission(std::vector<std::vector<int>> &sharing_groups);
|
||||
|
||||
void share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_store>> &cls);
|
||||
int receive_clauses_from_last_node(std::vector<shared_ptr<clause_store>> &clauses, int &transmitter);
|
||||
void share_clauses_to_other_node(int from, const std::vector<shared_ptr<clause_store>> &cls);
|
||||
int receive_clauses_from_other_node(std::vector<shared_ptr<clause_store>> &clauses, int &transmitter);
|
||||
|
||||
int sort_clauses(int x);
|
||||
int import_clauses(int id);
|
||||
|
||||
@ -286,7 +286,6 @@ void light::seperate_groups() {
|
||||
}
|
||||
sharing_groups.push_back(tmp);
|
||||
|
||||
|
||||
// [sat_procs+1, sat_procs+unsat_procs] for unsat
|
||||
if(rank >= sat_procs+1 && rank <= sat_procs+unsat_procs) {
|
||||
worker_type = light::UNSAT;
|
||||
@ -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<int> &model) {
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user