add RS/pakis switch

solve.cpp

@@ -55,7 +55,44 @@ void light::init_workers() {
 
 void light::diversity_workers() {
     for (int i = 0; i < OPT(threads); i++) {
-        if (i) workers[i]->configure("order_reset", i);
+        if (OPT(shuffle)) {
+            if (i) workers[i]->configure("order_reset", i);
+        }
+        if (OPT(pakis)) {
+            if (i == 13 || i == 14 || i == 20 || i == 21)
+                workers[i]->configure("tier1", 3);
+            else
+                workers[i]->configure("tier1", 2);
+
+            if (i == 3 || i == 4 || i == 6 || i == 8 || i == 11 || i == 12 || i == 13 || i == 14 || i == 16 || i == 18 || i == 23)
+                workers[i]->configure("chrono", 0);
+            else
+                workers[i]->configure("chrono", 1);    
+
+            if (i == 2 || i == 23)
+                workers[i]->configure("stable", 0);
+            else if (i == 6 || i == 16)
+                workers[i]->configure("stable", 2);
+            else
+                workers[i]->configure("stable", 1);
+
+            if (i == 10 || i == 22)
+                workers[i]->configure("walkinitially", 1);
+            else
+                workers[i]->configure("walkinitially", 0);
+
+            if (i == 7 || i == 8 || i == 9 || i == 17 || i == 18 || i == 19 || i == 20)
+                workers[i]->configure("target", 0);
+            else if (i == 0 || i == 2 || i == 3 || i == 4 || i == 5 || i == 6 || i == 10 || i == 23)
+                workers[i]->configure("target", 1);
+            else
+                workers[i]->configure("target", 2);
+            
+            if (i == 4 || i == 5 || i == 8 || i == 9 || i == 12 || i == 13 || i == 15 || i == 18 || i == 19)
+                workers[i]->configure("phase", 0);
+            else
+                workers[i]->configure("phase", 1);
+        }
     }
 }
 
@@ -119,7 +156,14 @@ int light::solve() {
 
     for (int i = 0; i < OPT(threads); i++) {
         pthread_join(ptr[i], NULL);
-    }    
+    }
+    auto clk_now = std::chrono::high_resolution_clock::now();
+    double solve_time = std::chrono::duration_cast<std::chrono::milliseconds>(clk_now - clk_sol_st).count();
+    solve_time = 0.001 * solve_time;
+    printf("c solve time: %.2lf\n", solve_time);
+    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;
 }

testLight/cal_solver.py

@@ -268,15 +268,18 @@ if __name__ == "__main__":
     solvers = []
 
 
-    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v3--1-preprocess","preprocess"))
-    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-nps","sharing-nps"))
-    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-dps","sharing-dps"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/p-mcomsps","p-mcomsps"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/treengeling","treengeling"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v3--1-preprocess","preprocess"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-1-preprocess","pre"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-1-nps","sharing-nps"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-dps","sharing-dps"))
 
     # append_all_solvers_in_dir(solvers, "/pub/data/chenzh/res/light/")
     samples = []
     samples.append(["/pub/data/chenzh/data/sat2020/vbs.txt", "vbs"])
     samples.append(["/pub/data/chenzh/data/sat2021/vbs.txt", "vbs"])
-    samples.append(["/pub/data/chenzh/data/sat2022/all.txt", "all"])
+    # samples.append(["/pub/data/chenzh/data/sat2022/all.txt", "all"])
     clt = calculater(solvers, samples)
     clt.cal_and_show()
 

testLight/run4-1.sh

@@ -0,0 +1,132 @@
+#!/bin/bash
+
+SEND_THREAD_NUM=4
+tmp_fifofile="/tmp/$$.fifo" # 脚本运行的当前进程ID号作为文件名
+mkfifo "$tmp_fifofile" # 新建一个随机fifo管道文件
+exec 6<>"$tmp_fifofile" # 定义文件描述符6指向这个fifo管道文件
+rm $tmp_fifofile
+for i in $(seq 1 $SEND_THREAD_NUM)
+do
+	echo # for循环 往 fifo管道文件中写入 $SEND_THREAD_NUM 个空行
+done >&6
+
+# CUTOFF_TIME=3600
+instance_20="/pub/data/chenzh/data/sat2020"
+instance_21="/pub/data/chenzh/data/sat2021"
+instance_22="/pub/data/chenzh/data/sat2022"
+
+
+res1="/pub/data/chenzh/res/light/v1-origin"
+res2="/pub/data/chenzh/res/light/v4-1-preprocess"
+res3="/pub/data/chenzh/res/light/v1-1-origin"
+res4="/pub/data/chenzh/res/light/v2-preprocess"
+res5="/pub/data/chenzh/res/light/v3--1-preprocess"
+res_no="/pub/data/chenzh/res/unused"
+#####################################################
+
+all_datas=($instance_21)
+for((i=0;i<${#all_datas[*]};i++))
+do
+	instance=${all_datas[$i]}
+
+	# res_solver_ins=$res5
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v3--1 $instance/$file --share=1 --threads=31
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+	# res_solver_ins=$res4
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v2 $instance/$file --share=1 --threads=31
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+
+	# res_solver_ins=$res3
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v1-1 $instance/$file --simplify=0 --reset=1
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+
+	res_solver_ins=$res2
+	if [ ! -d "$res_solver_ins" ]; then
+		mkdir -p $res_solver_ins
+	fi
+	for dir_file in `cat $instance/vbs111.txt`
+	do
+		file=$dir_file
+		echo $file
+		touch $res_solver_ins/$file
+		read -u 6
+		{
+			cd /home/chenzh/solvers/Light
+			time ./light-v4-1 $instance/$file --simplify=1
+			echo >&6
+		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	done
+
+	# res_solver_ins=$res1
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v1 $instance/$file --simplify=0
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+done
+
+res_solver_ins=$res_no
+if [ ! -d "$res_solver_ins" ]; then
+	mkdir -p $res_solver_ins
+fi
+for((i=0;i<4;i++))
+do
+	read -u 6
+	{
+		cd /home/chenzh/solvers/Light
+		time ./light-v1 /home/chenzh/data/hard_cnfs/49.cnf
+		echo >&6
+	} >$res_solver_ins/$i  2>>$res_solver_ins/$i &
+done
+
+
+exit 0

testLight/run4-2.sh

@@ -0,0 +1,132 @@
+#!/bin/bash
+
+SEND_THREAD_NUM=4
+tmp_fifofile="/tmp/$$.fifo" # 脚本运行的当前进程ID号作为文件名
+mkfifo "$tmp_fifofile" # 新建一个随机fifo管道文件
+exec 6<>"$tmp_fifofile" # 定义文件描述符6指向这个fifo管道文件
+rm $tmp_fifofile
+for i in $(seq 1 $SEND_THREAD_NUM)
+do
+	echo # for循环 往 fifo管道文件中写入 $SEND_THREAD_NUM 个空行
+done >&6
+
+# CUTOFF_TIME=3600
+instance_20="/pub/data/chenzh/data/sat2020"
+instance_21="/pub/data/chenzh/data/sat2021"
+instance_22="/pub/data/chenzh/data/sat2022"
+
+
+res1="/pub/data/chenzh/res/light/v1-origin"
+res2="/pub/data/chenzh/res/light/v4-1-preprocess"
+res3="/pub/data/chenzh/res/light/v1-1-origin"
+res4="/pub/data/chenzh/res/light/v2-preprocess"
+res5="/pub/data/chenzh/res/light/v3--1-preprocess"
+res_no="/pub/data/chenzh/res/unused"
+#####################################################
+
+all_datas=($instance_20)
+for((i=0;i<${#all_datas[*]};i++))
+do
+	instance=${all_datas[$i]}
+
+	# res_solver_ins=$res5
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v3--1 $instance/$file --share=1 --threads=31
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+	# res_solver_ins=$res4
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v2 $instance/$file --share=1 --threads=31
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+
+	# res_solver_ins=$res3
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v1-1 $instance/$file --simplify=0 --reset=1
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+
+	res_solver_ins=$res2
+	if [ ! -d "$res_solver_ins" ]; then
+		mkdir -p $res_solver_ins
+	fi
+	for dir_file in `cat $instance/vbs.txt`
+	do
+		file=$dir_file
+		echo $file
+		touch $res_solver_ins/$file
+		read -u 6
+		{
+			cd /home/chenzh/solvers/Light
+			time ./light-v4-1 $instance/$file --simplify=1
+			echo >&6
+		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	done
+
+	# res_solver_ins=$res1
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v1 $instance/$file --simplify=0
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+done
+
+res_solver_ins=$res_no
+if [ ! -d "$res_solver_ins" ]; then
+	mkdir -p $res_solver_ins
+fi
+for((i=0;i<4;i++))
+do
+	read -u 6
+	{
+		cd /home/chenzh/solvers/Light
+		time ./light-v1 /home/chenzh/data/hard_cnfs/49.cnf
+		echo >&6
+	} >$res_solver_ins/$i  2>>$res_solver_ins/$i &
+done
+
+
+exit 0

testLight/run4-3.sh

@@ -17,7 +17,7 @@ instance_22="/pub/data/chenzh/data/sat2022"
 
 
 res1="/pub/data/chenzh/res/light/v1-origin"
-res2="/pub/data/chenzh/res/light/v1-preprocess"
+res2="/pub/data/chenzh/res/light/v4-1-preprocess"
 res3="/pub/data/chenzh/res/light/v1-1-origin"
 res4="/pub/data/chenzh/res/light/v2-preprocess"
 res5="/pub/data/chenzh/res/light/v3--1-preprocess"
@@ -91,7 +91,7 @@ do
 		read -u 6
 		{
 			cd /home/chenzh/solvers/Light
-			time ./light-v1 $instance/$file --simplify=1
+			time ./light-v4-1 $instance/$file --simplify=1
 			echo >&6
 		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
 	done

testLight/run5-1.sh

@@ -21,11 +21,11 @@ res2="/pub/data/chenzh/res/light/v1-preprocess-2"
 res3="/pub/data/chenzh/res/light/v1-1-origin"
 res4="/pub/data/chenzh/res/light/v2-preprocess"
 res5="/pub/data/chenzh/res/light/v3--1-preprocess"
-res6="/pub/data/chenzh/res/light/v4-nps"
+res6="/pub/data/chenzh/res/light/v4-1-nps"
 res_no="/pub/data/chenzh/res/unused"
 #####################################################
 
-all_datas=($instance_21 $instance_20 $instance_22)
+all_datas=($instance_21)
 for((i=0;i<${#all_datas[*]};i++))
 do
 	instance=${all_datas[$i]}
@@ -42,7 +42,7 @@ do
 		read -u 6
 		{
 			cd /home/chenzh/solvers/Light
-			time ./light-v4 $instance/$file --share=1
+			time ./light-v4-1 $instance/$file --share=1
 			echo >&6
 		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
 	done

testLight/run5-2.sh

@@ -0,0 +1,151 @@
+#!/bin/bash
+
+SEND_THREAD_NUM=4
+tmp_fifofile="/tmp/$$.fifo" # 脚本运行的当前进程ID号作为文件名
+mkfifo "$tmp_fifofile" # 新建一个随机fifo管道文件
+exec 6<>"$tmp_fifofile" # 定义文件描述符6指向这个fifo管道文件
+rm $tmp_fifofile
+for i in $(seq 1 $SEND_THREAD_NUM)
+do
+	echo # for循环 往 fifo管道文件中写入 $SEND_THREAD_NUM 个空行
+done >&6
+
+# CUTOFF_TIME=3600
+instance_20="/pub/data/chenzh/data/sat2020"
+instance_21="/pub/data/chenzh/data/sat2021"
+instance_22="/pub/data/chenzh/data/sat2022"
+
+
+res1="/pub/data/chenzh/res/light/v1-origin"
+res2="/pub/data/chenzh/res/light/v1-preprocess-2"
+res3="/pub/data/chenzh/res/light/v1-1-origin"
+res4="/pub/data/chenzh/res/light/v2-preprocess"
+res5="/pub/data/chenzh/res/light/v3--1-preprocess"
+res6="/pub/data/chenzh/res/light/v4-1-nps"
+res_no="/pub/data/chenzh/res/unused"
+#####################################################
+
+all_datas=($instance_20)
+for((i=0;i<${#all_datas[*]};i++))
+do
+	instance=${all_datas[$i]}
+	
+	res_solver_ins=$res6
+	if [ ! -d "$res_solver_ins" ]; then
+		mkdir -p $res_solver_ins
+	fi
+	for dir_file in `cat $instance/vbs.txt`
+	do
+		file=$dir_file
+		echo $file
+		touch $res_solver_ins/$file
+		read -u 6
+		{
+			cd /home/chenzh/solvers/Light
+			time ./light-v4-1 $instance/$file --share=1
+			echo >&6
+		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	done
+
+
+	# res_solver_ins=$res5
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v3--1 $instance/$file --share=1 --threads=31
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+	# res_solver_ins=$res4
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v2 $instance/$file --share=1 --threads=31
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+
+	# res_solver_ins=$res3
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v1-1 $instance/$file --simplify=0 --reset=1
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+
+	# res_solver_ins=$res2
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light $instance/$file --simplify=1
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+
+	# res_solver_ins=$res1
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v1 $instance/$file --simplify=0
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+done
+
+res_solver_ins=$res_no
+if [ ! -d "$res_solver_ins" ]; then
+	mkdir -p $res_solver_ins
+fi
+for((i=0;i<4;i++))
+do
+	read -u 6
+	{
+		cd /home/chenzh/solvers/Light
+		time ./light-v1 /home/chenzh/data/hard_cnfs/49.cnf
+		echo >&6
+	} >$res_solver_ins/$i  2>>$res_solver_ins/$i &
+done
+
+
+exit 0

testLight/run5-3.sh

@@ -0,0 +1,151 @@
+#!/bin/bash
+
+SEND_THREAD_NUM=4
+tmp_fifofile="/tmp/$$.fifo" # 脚本运行的当前进程ID号作为文件名
+mkfifo "$tmp_fifofile" # 新建一个随机fifo管道文件
+exec 6<>"$tmp_fifofile" # 定义文件描述符6指向这个fifo管道文件
+rm $tmp_fifofile
+for i in $(seq 1 $SEND_THREAD_NUM)
+do
+	echo # for循环 往 fifo管道文件中写入 $SEND_THREAD_NUM 个空行
+done >&6
+
+# CUTOFF_TIME=3600
+instance_20="/pub/data/chenzh/data/sat2020"
+instance_21="/pub/data/chenzh/data/sat2021"
+instance_22="/pub/data/chenzh/data/sat2022"
+
+
+res1="/pub/data/chenzh/res/light/v1-origin"
+res2="/pub/data/chenzh/res/light/v1-preprocess-2"
+res3="/pub/data/chenzh/res/light/v1-1-origin"
+res4="/pub/data/chenzh/res/light/v2-preprocess"
+res5="/pub/data/chenzh/res/light/v3--1-preprocess"
+res6="/pub/data/chenzh/res/light/v4-1-nps"
+res_no="/pub/data/chenzh/res/unused"
+#####################################################
+
+all_datas=($instance_22)
+for((i=0;i<${#all_datas[*]};i++))
+do
+	instance=${all_datas[$i]}
+	
+	res_solver_ins=$res6
+	if [ ! -d "$res_solver_ins" ]; then
+		mkdir -p $res_solver_ins
+	fi
+	for dir_file in `cat $instance/all.txt`
+	do
+		file=$dir_file
+		echo $file
+		touch $res_solver_ins/$file
+		read -u 6
+		{
+			cd /home/chenzh/solvers/Light
+			time ./light-v4-1 $instance/$file --share=1
+			echo >&6
+		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	done
+
+
+	# res_solver_ins=$res5
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v3--1 $instance/$file --share=1 --threads=31
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+	# res_solver_ins=$res4
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v2 $instance/$file --share=1 --threads=31
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+
+	# res_solver_ins=$res3
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v1-1 $instance/$file --simplify=0 --reset=1
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+
+	# res_solver_ins=$res2
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light $instance/$file --simplify=1
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+
+	# res_solver_ins=$res1
+	# if [ ! -d "$res_solver_ins" ]; then
+	# 	mkdir -p $res_solver_ins
+	# fi
+	# for dir_file in `cat $instance/vbs.txt`
+	# do
+	# 	file=$dir_file
+	# 	echo $file
+	# 	touch $res_solver_ins/$file
+	# 	read -u 6
+	# 	{
+	# 		cd /home/chenzh/solvers/Light
+	# 		time ./light-v1 $instance/$file --simplify=0
+	# 		echo >&6
+	# 	} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
+	# done
+done
+
+res_solver_ins=$res_no
+if [ ! -d "$res_solver_ins" ]; then
+	mkdir -p $res_solver_ins
+fi
+for((i=0;i<4;i++))
+do
+	read -u 6
+	{
+		cd /home/chenzh/solvers/Light
+		time ./light-v1 /home/chenzh/data/hard_cnfs/49.cnf
+		echo >&6
+	} >$res_solver_ins/$i  2>>$res_solver_ins/$i &
+done
+
+
+exit 0

utils/paras.hpp

@@ -9,11 +9,13 @@
     PARA( DPS        , int    , 0     , 0  , 1   , "DPS/NPS") \
     PARA( DPS_period , int    , 10000 , 1  , 1e6 , "DPS sharing period") \
     PARA( mode       , int    , 0     , 0  , 2   , "SAT=1, UNSAT=2") \
+    PARA( pakis      , int    , 0     , 0  , 1   , "Use pakis diversity") \
     PARA( reset      , int    , 0     , 0  , 1   , "Dynamically reseting") \
     PARA( reset_time , int    , 10    , 1  , 1e5 , "Reseting base interval (seconds)") \
     PARA( share      , int    , 0     , 0  , 1   , "Sharing learnt clauses") \
     PARA( share_intv , int    , 500000, 0  , 1e9 , "Sharing interval (microseconds)") \
     PARA( share_lits , int    , 1500  , 0  , 1e6 , "Sharing lits (per every #share_intv seconds)") \
+    PARA( shuffle    , int    , 1     , 0  , 1   , "Use random shuffle") \
     PARA( simplify   , int    , 1     , 0  , 1   , "Use Simplify (only preprocess)") \
     PARA( times      , double , 5000  , 0  , 1e8 , "Cutoff time") \
     PARA( threads    , int    , 32    , 1  , 128 , "Thread number") \

workers/basekissat.cpp

@@ -15,7 +15,7 @@ void basekissat::add(int l) {
     kissat_add(solver, l);
 }
 
-void basekissat::configure(char* name, int id) {
+void basekissat::configure(const char* name, int id) {
     kissat_set_option(solver, name, id);
 }
 
@@ -100,18 +100,21 @@ void kissat_wait_sharing(void *solver) {
         // printf("c %d start wait with number %d\n", S->id, s->waitings);
     }
     if (s->should_sharing()) s->cond.notify_one(); 
-    
     boost::mutex::scoped_lock lock(s->mtx);
     while (s->waitings > 0) {
         s->cond.wait(lock);
     }
-    
-    // auto clk_now = std::chrono::high_resolution_clock::now();
-    // int solve_time = std::chrono::duration_cast<std::chrono::milliseconds>(clk_now - clk_st).count();
+    auto clk_now = std::chrono::high_resolution_clock::now();
+    int solve_time = std::chrono::duration_cast<std::chrono::milliseconds>(clk_now - clk_st).count();
+    S->waiting_time += 0.001 * solve_time;
     // printf("c %d wait for %d.%03ds\n", S->id, solve_time / 1000, solve_time % 1000);
     // printf("c %d finish sharing\n", S->id);
 }
 
+double basekissat::get_waiting_time() {
+    return waiting_time;
+}
+
 basekissat::basekissat(int id, light* light) : basesolver(id, light) {
     good_clause_lbd = 2;
     // outexport.open("export.txt");

workers/basekissat.hpp

@@ -9,7 +9,7 @@ public:
     void add(int l);
     int  solve();
     int  val(int l);
-    void configure(char* name, int id);
+    void configure(const char* name, int id);
     // int  get_reset_data();
     // void reset();
     int  get_conflicts();
@@ -22,10 +22,12 @@ public:
     void import_clauses_from(vec<clause_store *> &clauses);
     void broaden_export_limit();
     void restrict_export_limit();
+    double get_waiting_time();
 
     basekissat(int id, light *light);
     ~basekissat();
     int x1 = 0, x2 = 0;
+    double waiting_time = 0;
     kissat* solver;
     int good_clause_lbd = 0;
     

workers/basesolver.hpp

@@ -15,7 +15,7 @@ public:
     virtual int  solve() = 0;
     virtual int  val(int l) = 0;
     virtual void terminate() = 0;
-    virtual void configure(char* name, int id) = 0;
+    virtual void configure(const char* name, int id) = 0;
     virtual int  get_conflicts() = 0;
 
     virtual void parse_from_CNF(char* filename) = 0;
@@ -27,6 +27,7 @@ public:
     virtual void import_clauses_from(vec<clause_store *> &clauses) = 0;
     virtual void broaden_export_limit() = 0;
     virtual void restrict_export_limit() = 0;
+    virtual double get_waiting_time() = 0;
     light * controller;
     int id;
     sharer* in_sharer;

workers/sharer.cpp

@@ -9,6 +9,7 @@ void * share_worker(void *arg) {
     int nums = 0;
     sharer * sq = (sharer *)arg;
     auto clk_st = std::chrono::high_resolution_clock::now();
+    double share_time = 0;
     while (true) {
         ++nums;
         if (sq->dps) {
@@ -55,11 +56,14 @@ void * share_worker(void *arg) {
                 sq->cls[k]->free_clause();
             }
         }
+        auto clk_ed = std::chrono::high_resolution_clock::now();
+        share_time += 0.001 * std::chrono::duration_cast<std::chrono::milliseconds>(clk_ed - clk_now).count();
+        
         if (sq->dps) {
             sq->sharing_finish();
         }
     }
-    printf("c sharing nums: %d\n", nums);
+    printf("c sharing nums: %d\nc sharing time: %.2lf\n", nums, share_time);
     // if (terminated) puts("terminated set to 1");
     return NULL;
 }