diff --git a/run.sh b/run.sh index 44650f2..7124bd0 100755 --- a/run.sh +++ b/run.sh @@ -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 \ No newline at end of file +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 \ No newline at end of file diff --git a/src/distributed/leader.hpp b/src/distributed/leader.hpp index dbdd0bb..ed44dc2 100644 --- a/src/distributed/leader.hpp +++ b/src/distributed/leader.hpp @@ -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; + + } \ No newline at end of file diff --git a/src/workers/basesolver.cpp b/src/workers/basesolver.cpp index c561744..ff05b46 100644 --- a/src/workers/basesolver.cpp +++ b/src/workers/basesolver.cpp @@ -44,6 +44,7 @@ double basesolver::get_waiting_time() { void basesolver::export_clauses_to(vec &clauses) { clause_store *cls; + while (export_clause.pop(cls)) { clauses.push(cls); } diff --git a/src/workers/basesolver.hpp b/src/workers/basesolver.hpp index f015cf9..4be5e8e 100644 --- a/src/workers/basesolver.hpp +++ b/src/workers/basesolver.hpp @@ -55,8 +55,8 @@ public: vec> bucket; vec unfree; - boost::lockfree::spsc_queue> import_clause; - boost::lockfree::spsc_queue> export_clause; + boost::lockfree::spsc_queue> import_clause; + boost::lockfree::spsc_queue> export_clause; basesolver(int sid, light* light) : id(sid), controller(light) { good_clause_lbd = 2; diff --git a/src/workers/sharer.cpp b/src/workers/sharer.cpp index 235e344..b4cf0df 100644 --- a/src/workers/sharer.cpp +++ b/src/workers/sharer.cpp @@ -64,7 +64,7 @@ void share_clauses_to_next_node(std::vector> &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 &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 clauses; + // 导入外部网络传输的子句 + //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); - // } + // // 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(); }