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

competition mode

Browse Source
This commit is contained in:
ihan-o 2023-05-15 14:02:35 +08:00
parent ae0516eb9c
commit 14634be021
11 changed files with 117 additions and 47 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
res.txt Normal file
View File

File diff suppressed because one or more lines are too long

45
result.txt Normal file
View File

File diff suppressed because one or more lines are too long

7
run.sh
View File

@ -21,9 +21,10 @@
# - 367c25ad50259a685a25b86d6dd171b2-GP_100_950_33.cnf
# 这个存在问题
DIR=/pub/data/chenzh/data/sat2020
INSTANCE=tseitingrid7x165_shuffled.cnf
# INSTANCE=a4bffff28417d6b4d72f7b9122988ba5-reconf10_68_queen15_2.configure
# DIR=/pub/data/chenzh/data/sat2020
DIR=/home/chenzh/data/benchmark_single
# INSTANCE=tseitingrid7x165_shuffled.cnf
INSTANCE=10_0.cnf
make -j && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --shuffle=1 --share=1 --threads=16 --times=3600 --share_method=0

22
src/leader.hpp
View File

@ -14,9 +14,9 @@ void leader_main(light* S, int num_procs, int rank) {
auto clk_st = std::chrono::high_resolution_clock::now();
__global_paras.print_change();
// __global_paras.print_change();
printf("c [leader] preprocess(simplify) input data\n");
// printf("c [leader] preprocess(simplify) input data\n");
// 进行化简
auto pre = new preprocess();
@ -31,7 +31,7 @@ void leader_main(light* S, int num_procs, int rank) {
// preprocess 证明了UNSAT 则不需要启动云计算
if(!start) {
MPI_Barrier(MPI_COMM_WORLD);
printf("c [leader] UNSAT!!!!!! by preprocess\n");
// printf("c [leader] UNSAT!!!!!! by preprocess\n");
printf("s UNSATISFIABLE\n");
return;
}
@ -51,9 +51,9 @@ void leader_main(light* S, int num_procs, int rank) {
int cnf_length = str_ref.size() + 1;
printf("c [leader] length of cnf (bytes): %lld\n", cnf_length);
// printf("c [leader] length of cnf (bytes): %lld\n", cnf_length);
printf("c [leader] hand out length of cnf instance to all nodes\n");
// printf("c [leader] hand out length of cnf instance to all nodes\n");
MPI_Barrier(MPI_COMM_WORLD);
@ -61,13 +61,13 @@ void leader_main(light* S, int num_procs, int rank) {
MPI_Barrier(MPI_COMM_WORLD);
printf("c [leader] hand out cnf instance to all nodes\n");
// printf("c [leader] hand out cnf instance to all nodes\n");
MPI_Bcast(cstr, cnf_length, MPI_CHAR, 0, MPI_COMM_WORLD);
MPI_Barrier(MPI_COMM_WORLD);
printf("c [leader] hand out done!\n");
// printf("c [leader] hand out done!\n");
int is_sat;
MPI_Request solved;
@ -84,7 +84,7 @@ void leader_main(light* S, int num_procs, int rank) {
auto clk_now = std::chrono::high_resolution_clock::now();
int solve_time = std::chrono::duration_cast<std::chrono::seconds>(clk_now - clk_st).count();
if (solve_time >= OPT(times)) {
printf("c [leader] solve time out\n");
// printf("c [leader] solve time out\n");
break;
}
@ -105,7 +105,7 @@ void leader_main(light* S, int num_procs, int rank) {
if(is_sat) {
res = 10;
printf("c [leader] received model size: %d\n", pre->vars);
// printf("c [leader] received model size: %d\n", pre->vars);
// printf("c SAT!!!!!!\n");
MPI_Send(NULL, 0, MPI_INT, status.MPI_SOURCE, MODEL_REPORT_TAG, MPI_COMM_WORLD);
@ -131,7 +131,7 @@ void leader_main(light* S, int num_procs, int rank) {
for (int i = 1; i <= pre->orivars; i++) {
printf("%d ", i * pre->mapval[i]);
}
printf("\n");
printf("0\n");
delete []sol;
} else if(res == 20) {
printf("s UNSATISFIABLE\n");
@ -141,6 +141,6 @@ void leader_main(light* S, int num_procs, int rank) {
auto clk_now = std::chrono::high_resolution_clock::now();
double solve_time = std::chrono::duration_cast<std::chrono::milliseconds>(clk_now - clk_st).count();
printf("c time: %.3f\n", solve_time / 1000);
// printf("c time: %.3f\n", solve_time / 1000);
}

4
src/preprocess/binary.cpp
View File

@ -17,7 +17,7 @@ bool preprocess::preprocess_binary() {
clause[i][j] = tolit(clause[i][j]);
}
}
printf("c sz %d\n", clause[1].size());
// printf("c sz %d\n", clause[1].size());
nlit = (vars << 1) + 2;
for (int i = 1; i <= vars; i++) f[i] = i, val[i] = 1, varval[i] = color[i] = resseen[tolit(i)] = resseen[tolit(-i)] = 0;
for (int i = 1; i <= clauses; i++) clause_delete[i] = 0;
@ -192,7 +192,7 @@ bool preprocess::preprocess_binary() {
else varval[i] = varval[f[i]] * val[i];
}
}
printf("c turns: %d\n", turn);
// printf("c turns: %d\n", turn);
for (int i = 1; i <= clauses; i++) {
if (clause_delete[i]) continue;

2
src/preprocess/card.cpp
View File

@ -310,7 +310,7 @@ int preprocess::card_elimination() {
int preprocess::preprocess_card() {
int sone = search_almost_one();
printf("c [CE] almost one cons: %d\n", sone);
// printf("c [CE] almost one cons: %d\n", sone);
if (!sone) return 1;
int scc = scc_almost_one();
int sz = card_one.size();

4
src/preprocess/preprocess.cpp
View File

@ -83,7 +83,7 @@ void preprocess::update_var_clause_label() {
for (int j = 0; j < l; j++)
clause[id].push(color[abs(clause[i][j])] * pnsign(clause[i][j]));
}
printf("c After preprocess: vars: %d -> %d , clauses: %d -> %d ,\n", vars, remain_var, clauses, id);
// printf("c After preprocess: vars: %d -> %d , clauses: %d -> %d ,\n", vars, remain_var, clauses, id);
for (int i = id + 1; i <= clauses; i++)
clause[i].clear(true);
for (int i = remain_var + 1; i <= vars; i++)
@ -183,7 +183,7 @@ int preprocess::do_preprocess(char* filename) {
if (vars <= 1e5 && clauses <= 1e6) {
res = preprocess_card();
if (!res) {
printf("c solved by card elimination\n");
// printf("c solved by card elimination\n");
release();
delete []mapto;
delete []mapval;

2
src/preprocess/resolution.cpp
View File

@ -51,7 +51,7 @@ bool preprocess::preprocess_resolution() {
q[++r] = i, clean[i] = 1;
}
}
printf("c len %d\n", r);
// printf("c len %d\n", r);
int now_turn = 0, seen_flag = 0;
vec<int> vars;

34
src/sharer.cpp
View File

@ -154,15 +154,15 @@ void sharer::clause_sharing_init(std::vector<std::vector<int>> &sharing_groups)
MPI_Comm_size(MPI_COMM_WORLD, &num_procs);
MPI_Comm_rank(MPI_COMM_WORLD, &rank);
printf("c sharing groups: ");
for(int i=0; i<sharing_groups.size(); i++) {
printf(" [ ");
for(int j=0; j<sharing_groups[i].size(); j++) {
printf("%d ", sharing_groups[i][j]);
}
printf("]");
}
printf("\n");
// printf("c sharing groups: ");
// for(int i=0; i<sharing_groups.size(); i++) {
// printf(" [ ");
// for(int j=0; j<sharing_groups[i].size(); j++) {
// printf("%d ", sharing_groups[i][j]);
// }
// printf("]");
// }
// printf("\n");
if(OPT(share_method)) {
init_tree_transmission(sharing_groups);
@ -175,10 +175,10 @@ void sharer::clause_sharing_init(std::vector<std::vector<int>> &sharing_groups)
}
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() {
@ -189,7 +189,7 @@ void sharer::do_clause_sharing() {
auto clk_now = std::chrono::high_resolution_clock::now();
int solve_time = std::chrono::duration_cast<std::chrono::milliseconds>(clk_now - clk_st).count();
printf("c node%d(%d)round %d, time: %d.%d\n", rank, S->worker_type, nums, solve_time / 1000, solve_time % 1000);
// printf("c node%d(%d)round %d, time: %d.%d\n", rank, S->worker_type, nums, solve_time / 1000, solve_time % 1000);
// 导入外部网络传输的子句
std::vector<shared_ptr<clause_store>> clauses;
@ -212,7 +212,7 @@ void sharer::do_clause_sharing() {
share_clauses_to_other_node(from, clauses);
}
printf("c node%d(%d) get %d exported lits from network\n", rank, S->worker_type, received_lits);
// printf("c node%d(%d) get %d exported lits from network\n", rank, S->worker_type, received_lits);
for (int i = 0; i < producers.size(); i++) {
cls.clear();
@ -307,7 +307,7 @@ void sharer::init_tree_transmission(std::vector<std::vector<int>> &sharing_group
}
}
printf("c =========build tree=========\n");
// printf("c =========build tree=========\n");
for(int i=0; i<sharing_groups.size(); i++) {
// create binary trees for every group;
std::vector<int> &group = sharing_groups[i];
@ -328,7 +328,7 @@ void sharer::init_tree_transmission(std::vector<std::vector<int>> &sharing_group
son[rs[0]][rs[k]][0] = ( 2 * k + 1 < rs.size() ) ? rs[ 2 * k + 1 ] : -1;
son[rs[0]][rs[k]][1] = ( 2 * k + 2 < rs.size() ) ? rs[ 2 * k + 2 ] : -1;
printf("c son[%d][%d][%d]=%d\tson[%d][%d][%d]=%d\n", rs[0], rs[k], 0, son[rs[0]][rs[k]][0], rs[0], rs[k], 1, son[rs[0]][rs[k]][1]);
// printf("c son[%d][%d][%d]=%d\tson[%d][%d][%d]=%d\n", rs[0], rs[k], 0, son[rs[0]][rs[k]][0], rs[0], rs[k], 1, son[rs[0]][rs[k]][1]);
}
}
}

4
src/solver_api/basemaple.hpp
View File

@ -18,10 +18,10 @@ public:
int get_conflicts();
void parse_from_MEM(char* instance);
void exp_clause(void *cl, int lbd) {
puts("wrong");
// puts("wrong");
}
bool imp_clause(shared_ptr<clause_store>cls, void *cl) {
puts("wrong");
// puts("wrong");
}
basemaple(int id, light *light);

16
src/worker.hpp
View File

@ -18,7 +18,7 @@ void worker_main(light* S, int num_procs, int rank) {
int start;
MPI_Recv(&start, 1, MPI_INT, 0, START_TAG, MPI_COMM_WORLD, MPI_STATUS_IGNORE);
if(!start) {
printf("c [worker%d] I have no need to start\n", rank);
// printf("c [worker%d] I have no need to start\n", rank);
MPI_Barrier(MPI_COMM_WORLD);
return;
}
@ -55,16 +55,16 @@ void worker_main(light* S, int num_procs, int rank) {
// printf("threads: %lf\n", threads);
if(threads > 16) {
printf("c [worker%d] threads per worker were set %d by default : %d\n", rank, OPT(threads));
// printf("c [worker%d] threads per worker were set %d by default : %d\n", rank, OPT(threads));
} else {
OPT(threads) = floor(threads);
printf("c [worker%d] too big instance %lld\n", rank, cnf_length);
printf("c [worker%d] threads per worker were set %d by memcheck %d\n", rank, OPT(threads));
// printf("c [worker%d] too big instance %lld\n", rank, cnf_length);
// printf("c [worker%d] threads per worker were set %d by memcheck %d\n", rank, OPT(threads));
}
int res = S->run();
printf("c [worker%d] kissat exit with result: %d\n", rank, res);
// printf("c [worker%d] kissat exit with result: %d\n", rank, res);
MPI_Request *solved_request = new MPI_Request();
MPI_Request *model_request = new MPI_Request();
@ -82,20 +82,20 @@ void worker_main(light* S, int num_procs, int rank) {
auto clk_now = std::chrono::high_resolution_clock::now();
int solve_time = std::chrono::duration_cast<std::chrono::seconds>(clk_now - clk_st).count();
if (solve_time >= OPT(times)) {
printf("c [worker%d] solve time out\n", rank);
// printf("c [worker%d] solve time out\n", rank);
break;
}
// when getting terminate signal
if(MPI_Test(&S->terminal_request, &flag, MPI_STATUS_IGNORE) == MPI_SUCCESS && flag == 1) {
printf("c [worker%d] getting terminate signal\n", rank);
// printf("c [worker%d] getting terminate signal\n", rank);
break;
}
// when getting model signal
if(MPI_Test(model_request, &flag, MPI_STATUS_IGNORE) == MPI_SUCCESS && flag == 1) {
printf("c [worker%d] getting send model signal\n", rank);
// printf("c [worker%d] getting send model signal\n", rank);
// send model and break;
MPI_Send(S->model.data, S->model.size(), MPI_INT, 0, MODEL_REPORT_TAG, MPI_COMM_WORLD);