diff --git a/experiment/cal.py b/experiment/cal.py index 02893bf..21f697e 100755 --- a/experiment/cal.py +++ b/experiment/cal.py @@ -273,19 +273,21 @@ def gen_samples(dir): if __name__ == "__main__": solvers = [] + + solvers.append(solver_SAT_standard_gnomon("./cloud-sat","cloud-sat-circle-new")) # solvers.append(solver_SAT_standard_gnomon("/pub/netdisk1/qianyh/aws-batch-comp-infrastructure-sample/docker/runner/exp-result","mallob")) - solvers.append(solver_SAT_standard_gnomon("./light-3m-v3-tree","light-3m-v3-tree")) - solvers.append(solver_SAT_standard_gnomon("./light-3m-v3-circle","light-3m-v3-circle")) - solvers.append(solver_SAT_standard_gnomon("./light-3m-v2-tree","light-3m-v2-tree")) - solvers.append(solver_SAT_standard_gnomon("./light-3m-v2-circle","light-3m-v2-circle")) + solvers.append(solver_SAT_standard_gnomon("./light-3m-v4-tree","light-3m-v4-tree")) + solvers.append(solver_SAT_standard_gnomon("./light-3m-v4-circle","light-3m-v4-circle")) + # solvers.append(solver_SAT_standard_gnomon("./light-3m-v2-tree","light-3m-v2-tree")) + # solvers.append(solver_SAT_standard_gnomon("./light-3m-v2-circle","light-3m-v2-circle")) # solvers.append(solver_SAT_standard_gnomon("./light-3m-new-tree","light-3m-new-tree")) # solvers.append(solver_SAT_standard_gnomon("./light-3m-new-circle","light-3m-new-circle")) - solvers.append(solver_SAT_standard_gnomon("./light-3m-no-pre","light-3m-no-pre")) - solvers.append(solver_SAT_standard_gnomon("./light-3m","light-3m")) - solvers.append(solver_SAT_standard_gnomon("./light-no-bug","light-no-bug")) - solvers.append(solver_SAT_standard_gnomon("./light-circle","light-circle")) - solvers.append(solver_SAT_standard_gnomon("./light-circle-unique","light-circle-unique")) - solvers.append(solver_SAT_standard_gnomon("./first_version","bug-cloud")) + # solvers.append(solver_SAT_standard_gnomon("./light-3m-no-pre","light-3m-no-pre")) + # solvers.append(solver_SAT_standard_gnomon("./light-3m","light-3m")) + # solvers.append(solver_SAT_standard_gnomon("./light-no-bug","light-no-bug")) + # solvers.append(solver_SAT_standard_gnomon("./light-circle","light-circle")) + # solvers.append(solver_SAT_standard_gnomon("./light-circle-unique","light-circle-unique")) + # solvers.append(solver_SAT_standard_gnomon("./first_version","bug-cloud")) # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/huawei_sat/kissat-mab","origin-mab")) # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/huawei_simp/kissat-mab","preprocess-mab")) diff --git a/run.sh b/run.sh index fd90dde..7d5068b 100755 --- a/run.sh +++ b/run.sh @@ -1,26 +1,5 @@ #!/bin/bash -#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 --bind-to none -np 9 --allow-run-as-root ./light -i /pub/data/chenzh/data/sat2022/0205e0724a8a912dde9ad7dfba2aee0b-003-23-80.cnf --share=1 --threads=32 --times=3600 - -# 这个200s 退出了 -# 03bb7baaa45980753a0e7050ae44755d-atco_enc3_opt1_03_53.cnf - -# preprocess 占了特别大内存 - - - -# 有BUG -# 04157f716c1e9606c6a530657bf8f957-Kakuro-easy-125-ext.xml.hg_4.cnf - - -#每次都有BUG -# 3d2a6e5c2f8f58dee79fd50444009625-cfi-rigid-z2-0088-03-or_2_shuffle_all.cnf - - # cd kissat-inc # make clean # ./configure @@ -28,12 +7,24 @@ # cd .. # make clean + + +# buglist +# - fe96b630b3e761821308b544368dd521-GP_100_950_34.cnf +# - 0d4970edf84353e5a5798bca3f7f270e-SAT_H_instances_childsnack_p10.hddl_2.cnf + + # 这个存在问题 DIR=/pub/data/chenzh/data/sat2022 -INSTANCE=3d2a6e5c2f8f58dee79fd50444009625-cfi-rigid-z2-0088-03-or_2_shuffle_all.cnf +INSTANCE=51e4929accfa3a0e68bff09974c7f0f4-SAT_MS_sat_nurikabe_p16.pddl_166.cnf + + + + + # make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --shuffle=1 --share=1 --threads=16 --times=3600 --share_method=1 -make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i ./data/hard1.cnf --share=1 --threads=16 --times=10 +make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 --share_method=0 #./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 diff --git a/src/sharer.cpp b/src/sharer.cpp index d974aad..de6d4c5 100644 --- a/src/sharer.cpp +++ b/src/sharer.cpp @@ -196,15 +196,15 @@ void sharer::do_clause_sharing() { int received_lits = 0; while((from = receive_clauses_from_other_node(clauses, transmitter)) != -1 &&clauses.size() > 0) { - for (int j = 0; j < consumers.size(); j++) { - consumers[j]->import_clauses_from(clauses); - } - for (int k = 0; k < clauses.size(); k++) { clause_imported[clauses[k]->hash_code()] = true; received_lits += clauses[k]->size; } + for (int j = 0; j < consumers.size(); j++) { + consumers[j]->import_clauses_from(clauses); + } + // 传递外部网络传输的子句给下个节点 share_clauses_to_other_node(from, clauses); } @@ -243,14 +243,16 @@ void sharer::do_clause_sharing() { producers[i]->restrict_export_limit(); } } + + for (int k = 0; k < cls.size(); k++) { + clause_imported[cls[k]->hash_code()] = true; + } for (int j = 0; j < consumers.size(); j++) { if (producers[i]->id == consumers[j]->id) continue; consumers[j]->import_clauses_from(cls); } - for (int k = 0; k < cls.size(); k++) { - clause_imported[cls[k]->hash_code()] = true; - } + } auto clk_ed = std::chrono::high_resolution_clock::now(); diff --git a/src/solve.cpp b/src/solve.cpp index 782766d..ca07c33 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -191,9 +191,7 @@ int light::solve() { s->producers.push(workers[j]); s->consumers.push(workers[j]); } - printf("==============run1============\n"); s->clause_sharing_init(sharing_groups); - printf("==============run2============\n"); } while (!terminated) {