diff --git a/kissat-inc/makefile b/kissat-inc/makefile index 01f20c5..37626dd 100644 --- a/kissat-inc/makefile +++ b/kissat-inc/makefile @@ -1,17 +1,17 @@ all: - $(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" kissat: - $(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" kissat + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" kissat tissat: - $(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" tissat + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" tissat clean: - rm -f "/home/chenzh/solvers/cloud-sat/kissat-inc"/makefile - -$(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" clean - rm -rf "/home/chenzh/solvers/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-sat/kissat-inc/build" coverage + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" coverage indent: - $(MAKE) -C "/home/chenzh/solvers/cloud-sat/kissat-inc/build" indent + $(MAKE) -C "/pub/netdisk1/qianyh/Light/kissat-inc/build" indent test: - $(MAKE) -C "/home/chenzh/solvers/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/kissat-inc/src/bump.c b/kissat-inc/src/bump.c index fc2a0e3..00ed113 100644 --- a/kissat-inc/src/bump.c +++ b/kissat-inc/src/bump.c @@ -67,12 +67,15 @@ void kissat_init_shuffle(kissat * solver, int maxvar) { id = (int *)malloc(sizeof(int) * (maxvar + 1)); for (int i = 1; i <= maxvar; i++) id[i] = i; - for (int i = 1; i <= maxvar; i++) - { - int j = (rand_r(&seed) % maxvar) + 1; - int x = id[i]; - id[i] = id[j]; - id[j] = x; + + if(seed != 0) { + for (int i = 1; i <= maxvar; i++) + { + int j = (rand_r(&seed) % maxvar) + 1; + int x = id[i]; + id[i] = id[j]; + id[j] = x; + } } int block_size = maxvar / number; diff --git a/run.sh b/run.sh index e402289..95c5a45 100755 --- a/run.sh +++ b/run.sh @@ -1,27 +1,23 @@ #!/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 # - 0d4970edf84353e5a5798bca3f7f270e-SAT_H_instances_childsnack_p10.hddl_2.cnf - - # 这个存在问题 DIR=/pub/data/chenzh/data/sat2022 -INSTANCE=0d4970edf84353e5a5798bca3f7f270e-SAT_H_instances_childsnack_p10.hddl_2.cnf +INSTANCE=30ca21da9753263cc8cda020802b58ce-GP_500_200_20.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 $DIR/$INSTANCE --share=1 --threads=16 --times=3600 --share_method=0 +make -j 16 && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i data/class_1_easy_10_0.cnf --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 ac1c590..7ddcabd 100644 --- a/src/light.hpp +++ b/src/light.hpp @@ -47,6 +47,7 @@ public: sharer* s; std::vector> sharing_groups; enum { SAT, UNSAT, DEFAULT } worker_type; + int worker_rs; MPI_Request terminal_request; diff --git a/src/solve.cpp b/src/solve.cpp index 87bf28b..327410b 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -54,13 +54,19 @@ void light::init_workers() { } void light::diversity_workers() { + for (int i = 0; i < OPT(threads); i++) { if(worker_type == SAT) { if (OPT(shuffle)) { workers[i]->configure("worker_index", i); workers[i]->configure("worker_number", OPT(threads)); - workers[i]->configure("worker_seed", rank); + + if(rank == 1 || rank == num_procs - 1) { + workers[i]->configure("worker_seed", 0); + } else { + workers[i]->configure("worker_seed", rank); + } // printf("r1: %d, r2: %d, r3: %d\n", r1, r2, r3); }