diff --git a/run.sh b/run.sh index 84ce1f8..c783cc6 100755 --- a/run.sh +++ b/run.sh @@ -1,11 +1,11 @@ #!/bin/bash -cd kissat-inc -make clean -./configure -make -j 64 -cd .. -make clean +# cd kissat-inc +# make clean +# ./configure +# make -j 64 +# cd .. +# make clean # buglist # - fe96b630b3e761821308b544368dd521-GP_100_950_34.cnf @@ -16,9 +16,13 @@ make clean # - 00aefd1fc30c425075166ca051e57218-barman-pfile10-038.sas.ex.15.cnf # - 23e61c50ee2ac5cad1d337572abdebcf-aws-encryption-sdk-c:aws_cryptosdk_priv_hdr_parse_edks.cnf +# 解不出来 +# - 72329bc80f5f55dcc356a22f3f11ebec-GP_200_313_5.cnf +# - 367c25ad50259a685a25b86d6dd171b2-GP_100_950_33.cnf + # 这个存在问题 DIR=/pub/data/chenzh/data/sat2022 -INSTANCE=23e61c50ee2ac5cad1d337572abdebcf-aws-encryption-sdk-c:aws_cryptosdk_priv_hdr_parse_edks.cnf +INSTANCE=72329bc80f5f55dcc356a22f3f11ebec-GP_200_313_5.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 diff --git a/src/solve.cpp b/src/solve.cpp index 8310d24..366f37d 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -27,15 +27,19 @@ void * solve_worker(void *arg) { basesolver * sq = (basesolver *)arg; while (!terminated) { int res = sq->solve(); - if (res && !terminated) { //printf("c result: %d, winner is %d, winner run %d confs\n", res, sq->id, sq->get_conflicts()); - terminated = 1; - sq->controller->terminate_workers(); + + // terminated = 1; + // sq->controller->terminate_workers(); + result = res; sq->controller->update_winner(sq->id, 0); winner_conf = sq->get_conflicts(); if (res == 10) sq->get_model(sq->model); + + terminated = 1; + sq->controller->terminate_workers(); } //printf("get result %d with res %d\n", sq->id, res); } @@ -229,7 +233,7 @@ int light::solve() { // 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();