diff --git a/run.sh b/run.sh index 190051d..9ec83d3 100755 --- a/run.sh +++ b/run.sh @@ -13,10 +13,10 @@ # 04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf DIR=/pub/data/chenzh/data/sat2022 -INSTANCE=00aefd1fc30c425075166ca051e57218-barman-pfile10-038.sas.ex.15.cnf +INSTANCE=0d209cb420326994f9c4898eb10228ab-008-80-8.cnf 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/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 diff --git a/src/sharer.cpp b/src/sharer.cpp index 74ddb7f..1607b7e 100644 --- a/src/sharer.cpp +++ b/src/sharer.cpp @@ -25,7 +25,14 @@ std::unordered_map clause_imported; void share_clauses_to_next_node(int from, const std::vector> &cls) { - int target = rank % (num_procs - 1) + 1; + /** + * sat_group [1, num_procs/2] + * unsat_group [num_procs/2+1, num_procs-1] + */ + + int target = rank + 1; + if(target == num_procs / 2 + 1) target = 1; + if(target == num_procs) target = num_procs/2+1; // 环形传递，数据来源如果是目的地，说明数据已轮转一圈，停止发送。 if(from == target) return; @@ -80,12 +87,14 @@ void share_clauses_to_next_node(int from, const std::vector> &clauses) { +int receive_clauses_from_last_node(std::vector> &clauses, int &transmitter) { clauses.clear(); int flag; MPI_Status status; + transmitter = -1; + int from = -1; // 已接收完数据 @@ -94,6 +103,11 @@ bool receive_clauses_from_last_node(std::vector> &claus int count; MPI_Get_count(&status, MPI_INT, &count); + if(transmitter == -1) { + transmitter = status.MPI_SOURCE; + } + assert(transmitter == status.MPI_SOURCE); + from = buf[index++]; while(index < count) { @@ -117,11 +131,7 @@ bool receive_clauses_from_last_node(std::vector> &claus assert(index == count); - // 进行下一步接收数据 - - 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); + MPI_Irecv(buf, BUF_SIZE, MPI_INT, MPI_ANY_SOURCE, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, &receive_request); } return from; @@ -130,15 +140,14 @@ bool receive_clauses_from_last_node(std::vector> &claus void sharer::clause_sharing_init() { 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); + MPI_Irecv(buf, BUF_SIZE, MPI_INT, MPI_ANY_SOURCE, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, &receive_request); } void sharer::clause_sharing_end() { - printf("c sharing nums: %d\nc sharing time: %.2lf\n", nums, share_time); - printf("c sharing received_num_by_network: %d\n", num_received_clauses_by_network); - printf("c sharing skip_num_by_network: %d\n", num_skip_clauses_by_network); - printf("c sharing unique reduce percentage: %.2f%%\n", (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() { @@ -153,9 +162,11 @@ void sharer::do_clause_sharing() { // 导入外部网络传输的子句 std::vector> clauses; - int from = receive_clauses_from_last_node(clauses); + int transmitter; + int from = receive_clauses_from_last_node(clauses, transmitter); if(from != -1 && clauses.size() > 0) { - printf("c [worker] get %d exported clauses from network\n", clauses.size()); + printf("c [node-%d] get %d exported clauses from node-%d\n", rank, 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++) { consumers[j]->import_clauses_from(clauses); diff --git a/src/solve.cpp b/src/solve.cpp index 64f1ebf..a7dc376 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -68,7 +68,24 @@ void light::init_workers() { } void light::diversity_workers() { + + int num_procs, rank; + MPI_Comm_size(MPI_COMM_WORLD, &num_procs); + MPI_Comm_rank(MPI_COMM_WORLD, &rank); + for (int i = 0; i < OPT(threads); i++) { + + /** + * sat_group [1, num_procs/2] + * unsat_group [num_procs/2+1, num_procs-1] + */ + + if(rank <= num_procs / 2) { + workers[i]->configure("sat", 1); + } else { + workers[i]->configure("unsat", 1); + } + if (OPT(shuffle)) { if (i) workers[i]->configure("order_reset", i); } diff --git a/src/workers/basekissat.cpp b/src/workers/basekissat.cpp index 8db8be1..20deedf 100644 --- a/src/workers/basekissat.cpp +++ b/src/workers/basekissat.cpp @@ -70,8 +70,12 @@ bool basekissat::imp_clause(shared_ptrcls, void *cl) { for (int i = 0; i < cls->size; i++) { // S->outimport << cls->data[i] << std::endl; int eidx = abs(cls->data[i]); - if (eidx >= SIZE_STACK(solver->import)) printf("c wrong %d\n", eidx); + + assert(eidx > 0); + + if (eidx >= SIZE_STACK(solver->import)) printf("c wrong %d sizeo_stack %d\n", eidx, SIZE_STACK(solver->import)); import *import = &PEEK_STACK (solver->import, eidx); + if (import->eliminated) return false; else { int ilit = import->lit;