diff --git a/kissat-inc/makefile b/kissat-inc/makefile index 8e4ab81..37626dd 100644 --- a/kissat-inc/makefile +++ b/kissat-inc/makefile @@ -1,17 +1,17 @@ all: - $(MAKE) -C "/home/chenzh/solvers/cloud-nobug/cloud-sat/kissat-inc/build" + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" kissat: - $(MAKE) -C "/home/chenzh/solvers/cloud-nobug/cloud-sat/kissat-inc/build" kissat + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" kissat tissat: - $(MAKE) -C "/home/chenzh/solvers/cloud-nobug/cloud-sat/kissat-inc/build" tissat + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" tissat clean: - rm -f "/home/chenzh/solvers/cloud-nobug/cloud-sat/kissat-inc"/makefile - -$(MAKE) -C "/home/chenzh/solvers/cloud-nobug/cloud-sat/kissat-inc/build" clean - rm -rf "/home/chenzh/solvers/cloud-nobug/cloud-sat/kissat-inc/build" + rm -f "/pub/netdisk1/qianyh/Light/kissat-inc"/makefile + -$(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" clean + rm -rf "/pub/netdisk1/qianyh/Light/kissat-inc/build" coverage: - $(MAKE) -C "/home/chenzh/solvers/cloud-nobug/cloud-sat/kissat-inc/build" coverage + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" coverage indent: - $(MAKE) -C "/home/chenzh/solvers/cloud-nobug/cloud-sat/kissat-inc/build" indent + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" indent test: - $(MAKE) -C "/home/chenzh/solvers/cloud-nobug/cloud-sat/kissat-inc/build" test + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" test .PHONY: all clean coverage indent kissat test tissat diff --git a/run.sh b/run.sh index 9188bcf..84ce1f8 100755 --- a/run.sh +++ b/run.sh @@ -1,5 +1,26 @@ #!/bin/bash -$INSTANCE=$1 +cd kissat-inc +make clean +./configure +make -j 64 +cd .. +make clean -mpirun --bind-to none -np 4 --allow-run-as-root ./light -i $INSTANCE --share=1 --threads=4 --times=10 --share_method=0 \ No newline at end of file +# buglist +# - fe96b630b3e761821308b544368dd521-GP_100_950_34.cnf +# - 0d4970edf84353e5a5798bca3f7f270e-SAT_H_instances_childsnack_p10.hddl_2.cnf + + +# 退出慢 +# - 00aefd1fc30c425075166ca051e57218-barman-pfile10-038.sas.ex.15.cnf +# - 23e61c50ee2ac5cad1d337572abdebcf-aws-encryption-sdk-c:aws_cryptosdk_priv_hdr_parse_edks.cnf + +# 这个存在问题 +DIR=/pub/data/chenzh/data/sat2022 +INSTANCE=23e61c50ee2ac5cad1d337572abdebcf-aws-encryption-sdk-c:aws_cryptosdk_priv_hdr_parse_edks.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 + +make -j 16 && mpirun --mca btl_tcp_if_include 192.168.100.0/24 --hostfile ./experiment/hostfile --bind-to none -np 65 --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/light.hpp b/src/light.hpp index 3b597e3..2a9612a 100644 --- a/src/light.hpp +++ b/src/light.hpp @@ -57,6 +57,7 @@ public: int finalResult; int winner_id; mutable boost::mutex winner_mtx; + int maxtime; void update_winner(int id, int period) { boost::mutex::scoped_lock lock(winner_mtx); diff --git a/src/sharer.cpp b/src/sharer.cpp index 1f1ab52..a1548cf 100644 --- a/src/sharer.cpp +++ b/src/sharer.cpp @@ -100,6 +100,7 @@ void sharer::share_clauses_to_other_node(int from, const std::vector> &clauses, int &transmitter) { + clauses.clear(); int flag; diff --git a/src/solve.cpp b/src/solve.cpp index 659e412..8310d24 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -12,10 +12,11 @@ auto clk_st = std::chrono::high_resolution_clock::now(); char* worker_sign = ""; -std::atomic terminated; int result = 0; int winner_conf; +std::atomic terminated; + void * read_worker(void *arg) { basesolver * sq = (basesolver *)arg; sq->parse_from_MEM(sq->controller->instance); @@ -37,7 +38,6 @@ void * solve_worker(void *arg) { if (res == 10) sq->get_model(sq->model); } //printf("get result %d with res %d\n", sq->id, res); - } return NULL; } @@ -161,7 +161,6 @@ void light::terminate_workers() { } void light::parse_input() { - pthread_t *ptr = new pthread_t[OPT(threads)]; for (int i = 0; i < OPT(threads); i++) { pthread_create(&ptr[i], NULL, read_worker, workers[i]); @@ -170,7 +169,6 @@ void light::parse_input() { pthread_join(ptr[i], NULL); } delete []ptr; - } int light::solve() { @@ -204,8 +202,10 @@ int light::solve() { int flag; // when getting terminate signal if(MPI_Test(&terminal_request, &flag, MPI_STATUS_IGNORE) == MPI_SUCCESS && flag == 1) { + // printf("terminate: worker-%d\n", rank); terminated = 1; terminate_workers(); + break; } auto clk_now = std::chrono::high_resolution_clock::now(); @@ -213,6 +213,7 @@ int light::solve() { if (solve_time >= OPT(times)) { terminated = 1; terminate_workers(); + break; } } @@ -221,11 +222,14 @@ int light::solve() { // printf("ending solve\n"); // terminate_workers(); //important, need combine nps/dps !!!!!!!!!!!!!!!! - for (int i = 0; i < OPT(threads); i++) { - pthread_join(ptr[i], NULL); - } + // for (int i = 0; i < OPT(threads); i++) { + // pthread_join(ptr[i], NULL); + // } + + // printf("pthread_join: worker-%d\n", rank); // printf("ending join\n"); + if (result == 10) workers[winner_id]->model.copyTo(model); auto clk_now = std::chrono::high_resolution_clock::now(); @@ -234,7 +238,7 @@ int light::solve() { // printf("c solve time: %.2lf\nwinner is %d, period is %d\n", solve_time, winner_id, winner_period); // for (int i = 0; i < OPT(threads); i++) { // printf("c thread %d waiting time: %.2lf\n", i, workers[i]->get_waiting_time()); - // } + // } delete []ptr; return result; } @@ -307,7 +311,6 @@ void light::seperate_groups() { } } - void print_model(vec &model) { printf("v"); for (int i = 0; i < model.size(); i++) {