YuhangQ/cloud-sat
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

三模式SAT,UNSAT,DEFAULT分布求解

Browse Source
This commit is contained in:
YuhangQ 2023-04-19 14:15:14 +08:00
parent 3a310fe9ff
commit d36e3e6975
3 changed files with 16 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
run.sh
View File

@ -24,6 +24,6 @@ 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 4 --allow-run-as-root ./light -i ./data/hard1.cnf --share=1 --threads=16 --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
#./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600

29
src/sharer.cpp
View File

@ -23,21 +23,10 @@ int num_skip_clauses_by_network = 0;
std::unordered_map<int, bool> clause_imported;
void share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_store>> &cls) {
/**
* sat_group [1, num_procs/2]
* unsat_group [num_procs/2+1, num_procs-1]
*/
int target = rank % (num_procs - 1) + 1;
// int target = rank + 1;
// if(target == num_procs / 2 + 1) target = 1;
// if(target == num_procs) target = num_procs/2+1;
void sharer::share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_store>> &cls) {
// 环形传递，数据来源如果是目的地，说明数据已轮转一圈，停止发送。
if(from == target) return;
if(from == S->next_node) return;
// 定义发送数据
MPI_Request *send_request = new MPI_Request();
@ -68,7 +57,7 @@ void share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_st
// 调用 MPI 发送共享子句
MPI_Isend(send_buf, send_length, MPI_INT, target, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, send_request);
MPI_Isend(send_buf, send_length, MPI_INT, S->next_node, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, send_request);
send_data_struct.push_back(std::make_pair(send_request, send_buf));
@ -89,7 +78,7 @@ void share_clauses_to_next_node(int from, const std::vector<shared_ptr<clause_st
}
}
int receive_clauses_from_last_node(std::vector<shared_ptr<clause_store>> &clauses, int &transmitter) {
int sharer::receive_clauses_from_last_node(std::vector<shared_ptr<clause_store>> &clauses, int &transmitter) {
clauses.clear();
int flag;
@ -146,10 +135,10 @@ void sharer::clause_sharing_init() {
}
void sharer::clause_sharing_end() {
printf("c [node-%d] sharing nums: %d\nc sharing time: %.2lf\n", rank, nums, share_time);
printf("c [node-%d] sharing received_num_by_network: %d\n", rank, num_received_clauses_by_network);
printf("c [node-%d] sharing skip_num_by_network: %d\n", rank, num_skip_clauses_by_network);
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 nums: %d\nc sharing time: %.2lf\n", rank, nums, share_time);
printf("c node%d sharing received_num_by_network: %d\n", rank, num_received_clauses_by_network);
printf("c node%d sharing skip_num_by_network: %d\n", rank, num_skip_clauses_by_network);
printf("c node%d sharing unique reduce percentage: %.2f%%\n", rank, (double) num_skip_clauses_by_network / num_received_clauses_by_network * 100);
}
void sharer::do_clause_sharing() {
@ -167,7 +156,7 @@ void sharer::do_clause_sharing() {
int transmitter;
int from = receive_clauses_from_last_node(clauses, transmitter);
if(from != -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(%d)->%d get %d exported clauses from node-%d\n", rank, S->worker_type, S->next_node, 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++) {

6
src/sharer.hpp
View File

@ -18,11 +18,17 @@ public:
void clause_sharing_init();
void clause_sharing_end();
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);
int sort_clauses(int x);
int import_clauses(int id);
private:
light* S;
};
#endif