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 10:55:41 +00:00
parent 5637f3d0c4
commit cd8127789d
6 changed files with 26 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
docker/common.dockerfile
View File

@ -4,7 +4,7 @@ USER root
RUN sed -i s@/archive.ubuntu.com/@/mirrors.bfsu.edu.cn/@g /etc/apt/sources.list
RUN apt update
RUN DEBIAN_FRONTEND=noninteractive apt install -y cmake build-essential zlib1g-dev libopenmpi-dev wget unzip python3 gfortran curl
RUN DEBIAN_FRONTEND=noninteractive apt install -y vim cmake build-essential zlib1g-dev libopenmpi-dev wget unzip python3 gfortran curl
RUN apt install -y libboost-all-dev

BIN
docker/light
View File

Binary file not shown.

2
docker/run_solver.sh
View File

@ -1,3 +1,3 @@
#!/bin/bash
mpirun --host localhost,worker1,worker2,worker3 /light -i ./files/class_1_easy_10_0.cnf
mpirun --host localhost,worker1,worker2,worker3 /light -i ./files/class_1_easy_10_0.cnf --share=1

2
makefile
View File

@ -6,7 +6,7 @@ OBJECTS := $(addprefix build/,$(SOURCES:%=%.o))
# 声明编译器和编译选项
CXX := mpicxx
CXXFLAGS := -O0 -Wall -Wextra -MMD -MP
CXXFLAGS := -O0 -Wall -Wextra -MMD -MP -g
LIBS := -Wl,-Bstatic -lkissat -L kissat-inc/build -I kissat-inc/ \
-lm4ri -L m4ri-20140914/.libs -I m4ri-20140914/ \

6
run.sh
View File

@ -1,3 +1,7 @@
#!/bin/bash
make -j 16 && mpirun -np 4 --allow-run-as-root ./light -i data/class_1_easy_10_0.cnf --share=1 --threads=4 --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
#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

40
src/workers/sharer.cpp
View File

@ -21,7 +21,7 @@ void share_clauses_to_next_node(std::vector<std::pair<MPI_Request, int*>> &send_
}
// 与数组最后一个交换，然后 pop_back;
std::swap(send_data_struct[0], send_data_struct[send_data_struct.size()-1]);
std::swap(send_data_struct[i], send_data_struct[send_data_struct.size()-1]);
send_data_struct.pop_back();
}
@ -64,13 +64,11 @@ 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;
const int BUF_SIZE = 1024 * 1024 * 1024;
bool receive_clauses_from_last_node(MPI_Request &receive_request, int *buf, vec<clause_store*> &clauses) {
clauses.clear();
int flag;
MPI_Status status;
@ -81,7 +79,6 @@ bool receive_clauses_from_last_node(MPI_Request &receive_request, int *buf, vec<
int count;
MPI_Get_count(&status, MPI_INT, &count);
while(index < count) {
clause_store* cl = new clause_store(buf[index++]);
cl->lbd = buf[index++];
@ -148,28 +145,27 @@ void * share_worker(void *arg) {
LOGGER->info("thread-%v: get %v exported clauses", i, number);
// 分享当前节点产生的子句
share_clauses_to_next_node(send_data_struct, sq->cls);
// //分享当前节点产生的子句
// share_clauses_to_next_node(send_data_struct, sq->cls);
// 导入外部网络传输的子句
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);
}
// // 导入外部网络传输的子句
// 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);
// }
// 传递外部网络传输的子句给下个节点
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();
// }
// }
// 导入当前节点产生的子句
int percent = sq->sort_clauses(i);
if (percent < 75) {