From de434abbfbbce64fe932fd04cf8c417c40f79624 Mon Sep 17 00:00:00 2001
From: YuhangQ <i@yuhangq.com>
Date: Fri, 28 Apr 2023 07:43:11 +0000
Subject: [PATCH] =?UTF-8?q?=E6=9B=B4=E6=96=B0RS=EF=BC=8C=E7=AC=AC=E4=B8=80?=
=?UTF-8?q?=E4=B8=AAnode=E5=92=8C=E6=9C=80=E5=90=8E=E4=B8=80=E4=B8=AAnode?=
=?UTF-8?q?=E5=88=9D=E5=A7=8B=E6=8E=92=E5=88=97=E4=B8=BA=201~n?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
kissat-inc/makefile | 18 +++++++++---------
kissat-inc/src/bump.c | 15 +++++++++------
run.sh | 20 ++++++++------------
src/light.hpp | 1 +
src/solve.cpp | 8 +++++++-
5 files changed, 34 insertions(+), 28 deletions(-)
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<std::vector<int>> 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);
}