diff --git a/run.sh b/run.sh index 8171648..81f4a5b 100755 --- a/run.sh +++ b/run.sh @@ -13,7 +13,7 @@ # 这个存在问题 DIR=/pub/data/chenzh/data/sat2022 -INSTANCE=30ca21da9753263cc8cda020802b58ce-GP_500_200_20.cnf +INSTANCE=0d4970edf84353e5a5798bca3f7f270e-SAT_H_instances_childsnack_p10.hddl_2.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 diff --git a/src/sharer.cpp b/src/sharer.cpp index b08b1bc..1f1ab52 100644 --- a/src/sharer.cpp +++ b/src/sharer.cpp @@ -77,7 +77,7 @@ void sharer::share_clauses_to_other_node(int from, const std::vectorworker_type, send_length); + // printf("c node%d(%d) to %d exported lits from network\n", rank, S->worker_type, send_length); MPI_Request *send_request = new MPI_Request(); // 环形传递 MPI_Isend(send_buf.get(), send_length, MPI_INT, next_node, SHARE_CLAUSES_TAG, MPI_COMM_WORLD, send_request); diff --git a/src/solve.cpp b/src/solve.cpp index c8bf8dd..659e412 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -255,12 +255,12 @@ int light::run() { } void light::seperate_groups() { - solver_type = light::LSTECH; + solver_type = light::KISSAT; // split distribute nodes to groups(SAT MODE、UNSAT MODE、DEFAULT MODE) int worker_procs = num_procs - 1; if(worker_procs >= 8) { - int sat_procs = worker_procs / 4; + int sat_procs = worker_procs / 8; int unsat_procs = worker_procs / 4; int default_procs = worker_procs - sat_procs - unsat_procs; diff --git a/src/worker.hpp b/src/worker.hpp index e159b6f..0b3512b 100644 --- a/src/worker.hpp +++ b/src/worker.hpp @@ -43,7 +43,7 @@ void worker_main(light* S, int num_procs, int rank) { MPI_Barrier(MPI_COMM_WORLD); // mem_usage per thread per G input file (GB) - double mem_ptpg = 20.4; + double mem_ptpg = 8.0; // mem_usage per thread (GB) double mem_pt = (double)cnf_length / 1073741824 * mem_ptpg;