v4.3 fixed bug

preprocess/binary.cpp

@@ -17,8 +17,9 @@ bool preprocess::preprocess_binary() {
             clause[i][j] = tolit(clause[i][j]);
         }
     }
+    printf("c sz %d\n", clause[1].size());
     nlit = (vars << 1) + 2;
-    for (int i = 1; i <= vars; i++) f[i] = i, val[i] = 1, varval[i] = color[i] = 0;
+    for (int i = 1; i <= vars; i++) f[i] = i, val[i] = 1, varval[i] = color[i] = resseen[tolit(i)] = resseen[tolit(-i)] = 0;
     for (int i = 1; i <= clauses; i++) clause_delete[i] = 0;
     int len = 0;
     for (int i = 1; i <= clauses; i++) {
@@ -131,6 +132,7 @@ bool preprocess::preprocess_binary() {
             }
             if (t == 0) return false;
             if (t != l) simplify = 1, l = t;
+            
             t = 0;
             for (int j = 0; j < l; j++) {
                 if (resseen[a[j]] == i) continue;
@@ -141,7 +143,6 @@ bool preprocess::preprocess_binary() {
                 if (resseen[negative(a[j])] == i && !clause_delete[i]) {
                     clause_delete[i] = 1, simplify = 1;
                 }
-            
             for (int j = 0; j < l; j++) resseen[a[j]] = 0;
                 
             if (l == 1) {
@@ -171,7 +172,7 @@ bool preprocess::preprocess_binary() {
             for (int j = 0; j < l; j++)
                 clause[i].push(a[j]);
         }
-
+        
         for (int i = 1; i <= vars; i++) {
             int x = find(i);
             if (varval[i] && x != i) {
@@ -190,9 +191,8 @@ bool preprocess::preprocess_binary() {
                 }
                 else varval[i] = varval[f[i]] * val[i];
             }
-        break;
     }
-    // printf("c turns: %d\n", turn);
+    printf("c turns: %d\n", turn);
 
     for (int i = 1; i <= clauses; i++) {
         if (clause_delete[i]) continue;

preprocess/preprocess.cpp

@@ -161,15 +161,6 @@ void preprocess::get_complete_model() {
     }  
 }
 
-void preprocess::write_cnf() {
-    for (int i = 1; i <= clauses; i++) {
-        int l = clause[i].size();
-        for (int j = 0; j < l; j++)
-            printf("%d ", clause[i][j]);
-        puts("0");
-    }
-}
-
 int preprocess::do_preprocess(char* filename) {
     readfile(filename);
     preprocess_init();
@@ -190,6 +181,8 @@ int preprocess::do_preprocess(char* filename) {
         clause.clear(true);
         return 0;
     }
+
+
     if (vars <= 1e5 && clauses <= 1e6) {
         res = preprocess_card();
         if (!res) {
@@ -213,6 +206,8 @@ int preprocess::do_preprocess(char* filename) {
         resolution.clear(true);
         return 0;
     }
+
+
     res = preprocess_binary();
     if (!res) {
         release();

preprocess/preprocess.hpp

@@ -43,13 +43,14 @@ public:
     int clauses;
     vec<vec<int>> clause, res_clause;
     void readfile(const char *file);
+    void write_cnf();
     void release();
     
     int maxlen, orivars, oriclauses, res_clauses, resolutions;
     int *f, nlit, *a, *val, *color, *varval, *q, *seen, *resseen, *clean, *mapto, *mapfrom, *mapval;
     // HashMap* C;
     vec<int> *occurp, *occurn, clause_delete, nxtc, resolution;
-
+    
     int find(int x);    
     bool res_is_empty(int var);
     void update_var_clause_label();
@@ -64,7 +65,6 @@ public:
     vec<vec<double>> mat;
     vec<int> *occur;
     vec<int> cdel;
-    void write_cnf();
     int  check_card(int id);
     int  preprocess_card();
     int  search_almost_one();    

testLight/cal_solver.py

@@ -268,11 +268,17 @@ if __name__ == "__main__":
     solvers = []
 
 
-    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/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/sota/pakis","pakis"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/pakis22","pakis22"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/NPS","NPS"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/sota/pakis-mab","pakis-mab"))
     # 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-2-nps-rp","sharing-nps-rp"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-2-nps-p","sharing-nps-p"))
     # 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/")

testLight/run4-1.sh

@@ -21,6 +21,7 @@ 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"
+res6="/pub/data/chenzh/res/light/v4-2-nps-rp"
 res_no="/pub/data/chenzh/res/unused"
 #####################################################
 
@@ -29,6 +30,23 @@ 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-2 $instance/$file --share=1 --pakis=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
@@ -79,22 +97,22 @@ do
 	# 	} >$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=$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

testLight/run4-2.sh

@@ -21,6 +21,7 @@ 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"
+res6="/pub/data/chenzh/res/light/v4-2-nps-rp"
 res_no="/pub/data/chenzh/res/unused"
 #####################################################
 
@@ -29,6 +30,23 @@ 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-2 $instance/$file --share=1 --pakis=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
@@ -79,22 +97,22 @@ do
 	# 	} >$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=$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

testLight/run5-1.sh

@@ -22,6 +22,7 @@ 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"
+res7="/pub/data/chenzh/res/light/v4-2-nps-p2"
 res_no="/pub/data/chenzh/res/unused"
 #####################################################
 
@@ -30,7 +31,7 @@ for((i=0;i<${#all_datas[*]};i++))
 do
 	instance=${all_datas[$i]}
 	
-	res_solver_ins=$res6
+	res_solver_ins=$res7
 	if [ ! -d "$res_solver_ins" ]; then
 		mkdir -p $res_solver_ins
 	fi
@@ -42,12 +43,30 @@ do
 		read -u 6
 		{
 			cd /home/chenzh/solvers/Light
-			time ./light-v4-1 $instance/$file --share=1
+			time ./light-v4-2 $instance/$file --share=1 --shuffle=0 --pakis=1
 			echo >&6
 		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
 	done
 
 
+	# 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

testLight/run5-2.sh

@@ -22,19 +22,20 @@ 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"
+res7="/pub/data/chenzh/res/light/v4-2-nps-p2"
 res_no="/pub/data/chenzh/res/unused"
 #####################################################
 
-all_datas=($instance_20)
+all_datas=($instance_22)
 for((i=0;i<${#all_datas[*]};i++))
 do
 	instance=${all_datas[$i]}
 	
-	res_solver_ins=$res6
+	res_solver_ins=$res7
 	if [ ! -d "$res_solver_ins" ]; then
 		mkdir -p $res_solver_ins
 	fi
-	for dir_file in `cat $instance/vbs.txt`
+	for dir_file in `cat $instance/all.txt`
 	do
 		file=$dir_file
 		echo $file
@@ -42,12 +43,30 @@ do
 		read -u 6
 		{
 			cd /home/chenzh/solvers/Light
-			time ./light-v4-1 $instance/$file --share=1
+			time ./light-v4-2 $instance/$file --share=1 --shuffle=0 --pakis=1
 			echo >&6
 		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
 	done
 
 
+	# 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

testLight/run6-1.sh

@@ -0,0 +1,150 @@
+#!/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"
+res6="/pub/data/chenzh/res/light/v4-2-dps-r"
+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=$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-2 $instance/$file --share=1 --DPS=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-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/run6-2.sh

@@ -0,0 +1,150 @@
+#!/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"
+res6="/pub/data/chenzh/res/light/v4-2-dps-r"
+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-2 $instance/$file --share=1 --DPS=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-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/run7-1.sh

@@ -0,0 +1,150 @@
+#!/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"
+res6="/pub/data/chenzh/res/light/v4-2-dps2-r"
+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=$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-2 $instance/$file --share=1 --DPS=1 --DPS_period=20000 --share_lits=3000
+			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-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/run7-2.sh

@@ -0,0 +1,150 @@
+#!/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"
+res6="/pub/data/chenzh/res/light/v4-2-dps2-r"
+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-2 $instance/$file --share=1 --DPS=1 --DPS_period=20000 --share_lits=3000
+			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-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/run8-1.sh

@@ -21,9 +21,7 @@ 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"
-res7="/pub/data/chenzh/res/light/v4-dps"
-res8="/pub/data/chenzh/res/light/v4-dps-2w"
+res6="/pub/data/chenzh/res/light/v4-1-nps2"
 res_no="/pub/data/chenzh/res/unused"
 #####################################################
 
@@ -31,8 +29,9 @@ all_datas=($instance_21 $instance_20)
 for((i=0;i<${#all_datas[*]};i++))
 do
 	instance=${all_datas[$i]}
-	
-	res_solver_ins=$res8
+
+
+	res_solver_ins=$res6
 	if [ ! -d "$res_solver_ins" ]; then
 		mkdir -p $res_solver_ins
 	fi
@@ -44,7 +43,7 @@ do
 		read -u 6
 		{
 			cd /home/chenzh/solvers/Light
-			time ./light-v4 $instance/$file --share=1 --DPS=1 --DPS_period=20000
+			time ./light-v4-2 $instance/$file --share=1
 			echo >&6
 		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
 	done

testLight/run8-2.sh

@@ -21,9 +21,7 @@ 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"
-res7="/pub/data/chenzh/res/light/v4-dps"
-res8="/pub/data/chenzh/res/light/v4-dps-2w"
+res6="/pub/data/chenzh/res/light/v4-1-nps2"
 res_no="/pub/data/chenzh/res/unused"
 #####################################################
 
@@ -31,12 +29,13 @@ all_datas=($instance_22)
 for((i=0;i<${#all_datas[*]};i++))
 do
 	instance=${all_datas[$i]}
-	
-	res_solver_ins=$res8
+
+
+	res_solver_ins=$res6
 	if [ ! -d "$res_solver_ins" ]; then
 		mkdir -p $res_solver_ins
 	fi
-	for dir_file in `cat $instance/vbs.txt`
+	for dir_file in `cat $instance/all.txt`
 	do
 		file=$dir_file
 		echo $file
@@ -44,7 +43,7 @@ do
 		read -u 6
 		{
 			cd /home/chenzh/solvers/Light
-			time ./light-v4 $instance/$file --share=1 --DPS=1 --DPS_period=20000
+			time ./light-v4-2 $instance/$file --share=1
 			echo >&6
 		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
 	done

utils/parse.cpp

@@ -87,3 +87,14 @@ void preprocess::readfile(const char *file) {
     }
     delete []data;
 }
+
+void preprocess::write_cnf() {
+    printf("p cnf %d %d\n", vars, clauses);
+    for (int i = 1; i <= clauses; i++) {
+        int l = clause[i].size();
+        for (int j = 0; j < l; j++) {
+            printf("%d ", clause[i][j]);
+        }
+        puts("0");
+    }
+}