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

同步代码

Browse Source
This commit is contained in:
YuhangQ 2023-04-06 11:57:08 +00:00
parent 1c60672abf
commit a3a2596713
5 changed files with 30 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
run.sh
View File

@ -4,4 +4,4 @@
#valgrind
make -j 16 && mpirun -np 4 --allow-run-as-root ./light -i data/class_1_easy_10_0.cnf --share=1 --threads=32 --times=60
make -j 16 && mpirun -np 4 --allow-run-as-root valgrind ./light -i data/class_1_easy_10_0.cnf --share=1 --threads=32 --times=60

4
src/distributed/leader.hpp
View File

@ -135,11 +135,13 @@ void leader_main(light* S, int num_procs, int rank) {
printf("%d ", i * pre->mapval[i]);
}
printf("\n");
delete []sol;
} else if(res == 20) {
printf("s UNSAT\n");
} else {
printf("s UNKNOWN\n");
}
delete []sol;
}

1
src/workers/basesolver.cpp
View File

@ -44,6 +44,7 @@ double basesolver::get_waiting_time() {
void basesolver::export_clauses_to(vec<clause_store *> &clauses) {
clause_store *cls;
while (export_clause.pop(cls)) {
clauses.push(cls);
}

4
src/workers/basesolver.hpp
View File

@ -55,8 +55,8 @@ public:
vec<vec<clause_store *>> bucket;
vec<int> unfree;
boost::lockfree::spsc_queue<clause_store*, boost::lockfree::capacity<1024000>> import_clause;
boost::lockfree::spsc_queue<clause_store*, boost::lockfree::capacity<1024000>> export_clause;
boost::lockfree::spsc_queue<clause_store*, boost::lockfree::capacity<10240000>> import_clause;
boost::lockfree::spsc_queue<clause_store*, boost::lockfree::capacity<10240000>> export_clause;
basesolver(int sid, light* light) : id(sid), controller(light) {
good_clause_lbd = 2;

46
src/workers/sharer.cpp
View File

@ -64,7 +64,7 @@ void share_clauses_to_next_node(std::vector<std::pair<MPI_Request, int*>> &send_
LOGGER->info("send clauses: %v", send_length);
}
const int BUF_SIZE = 1024 * 1024 * 1024;
const int BUF_SIZE = 1024 * 1024;
bool receive_clauses_from_last_node(MPI_Request &receive_request, int *buf, vec<clause_store*> &clauses) {
clauses.clear();
@ -139,31 +139,31 @@ void * share_worker(void *arg) {
for (int i = 0; i < sq->producers.size(); i++) {
sq->cls.clear();
sq->producers[i]->export_clauses_to(sq->cls);
// printf("c size %d\n", sq->cls.size());
printf("c size %d\n", sq->cls.size());
int number = sq->cls.size();
LOGGER->info("thread-%v: get %v exported clauses", i, number);
// //分享当前节点产生的子句
// share_clauses_to_next_node(send_data_struct, sq->cls);
//分享当前节点产生的子句
//if(sq->cls.size() > 0) share_clauses_to_next_node(send_data_struct, sq->cls);
// // 导入外部网络传输的子句
// vec<clause_store*> clauses;
// 导入外部网络传输的子句
//vec<clause_store*> 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);
// }
// // 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);
// // // 传递外部网络传输的子句给下个节点
// // share_clauses_to_next_node(send_data_struct, clauses);
// for (int k = 0; k < clauses.size(); k++) {
// clauses[k]->free_clause();
// }
// // for (int k = 0; k < clauses.size(); k++) {
// // clauses[k]->free_clause();
// // }
// }
// 导入当前节点产生的子句
@ -172,15 +172,15 @@ void * share_worker(void *arg) {
sq->producers[i]->broaden_export_limit();
}
else if (percent > 98) {
sq->producers[i]->restrict_export_limit();
//sq->producers[i]->restrict_export_limit();
}
for (int j = 0; j < sq->consumers.size(); j++) {
if (sq->producers[i]->id == sq->consumers[j]->id) continue;
for (int k = 0; k < sq->cls.size(); k++)
sq->cls[k]->increase_refs(1);
sq->consumers[j]->import_clauses_from(sq->cls);
}
// for (int j = 0; j < sq->consumers.size(); j++) {
// if (sq->producers[i]->id == sq->consumers[j]->id) continue;
// for (int k = 0; k < sq->cls.size(); k++)
// sq->cls[k]->increase_refs(1);
// sq->consumers[j]->import_clauses_from(sq->cls);
// }
for (int k = 0; k < sq->cls.size(); k++) {
sq->cls[k]->free_clause();
}