diff --git a/light-v4-4 b/light-v4-4
new file mode 100755
index 0000000..0e2c971
Binary files /dev/null and b/light-v4-4 differ
diff --git a/light-v5-0 b/light-v5-0
new file mode 100755
index 0000000..a2423ea
Binary files /dev/null and b/light-v5-0 differ
diff --git a/light-v5-1 b/light-v5-1
new file mode 100755
index 0000000..4b6bb8d
Binary files /dev/null and b/light-v5-1 differ
diff --git a/light-v5-2 b/light-v5-2
new file mode 100755
index 0000000..49eb8e1
Binary files /dev/null and b/light-v5-2 differ
diff --git a/light-v5-3 b/light-v5-3
new file mode 100755
index 0000000..6b9987e
Binary files /dev/null and b/light-v5-3 differ
diff --git a/light-v5-4 b/light-v5-4
new file mode 100755
index 0000000..d86e227
Binary files /dev/null and b/light-v5-4 differ
diff --git a/light-v5-5 b/light-v5-5
new file mode 100755
index 0000000..8882d62
Binary files /dev/null and b/light-v5-5 differ
diff --git a/light-v5-6 b/light-v5-6
new file mode 100755
index 0000000..acaa3ae
Binary files /dev/null and b/light-v5-6 differ
diff --git a/light-v5-7 b/light-v5-7
new file mode 100755
index 0000000..5c4e255
Binary files /dev/null and b/light-v5-7 differ
diff --git a/light.cpp b/light.cpp
index 75380a5..e4f3ecb 100644
--- a/light.cpp
+++ b/light.cpp
@@ -5,9 +5,9 @@
 
 light::light():
   finalResult           (0),
-  winner                (0),
-  maxtime               (5000),
-  globalEnding          (false)
+  winner_period         (1e9),
+  winner_id             (-1),
+  maxtime               (5000)
 {
     opt = new paras();
     opt->init_paras();
diff --git a/light.hpp b/light.hpp
index 5eaf212..ebed728 100644
--- a/light.hpp
+++ b/light.hpp
@@ -5,7 +5,9 @@
 #include "preprocess/preprocess.hpp"
 #include <atomic>
 #include <iostream>
-#include <mutex>
+#include <boost/thread.hpp>
+#include <boost/thread/thread.hpp>
+#include <boost/lockfree/spsc_queue.hpp>
 typedef long long ll;
 
 class basesolver;
@@ -35,10 +37,20 @@ public:
     vec<sharer *> sharers;
 
     int finalResult;
-    int winner;
+    int winner_period, winner_id;
+    mutable boost::mutex winner_mtx;
     int maxtime;
-    std::atomic<bool> globalEnding;
-
+    void update_winner(int id, int period) {
+        boost::mutex::scoped_lock lock(winner_mtx);
+        if (period < winner_period || (period == winner_period && id < winner_id)) {
+            winner_period = period;
+            winner_id = id;
+        }
+    }
+    int  get_winner_period() {
+        boost::mutex::scoped_lock lock(winner_mtx);
+        return winner_period;
+    }
     void arg_parse(int argc, char **argv);
     void init_workers();
     void diversity_workers();
diff --git a/solve.cpp b/solve.cpp
index 32c3212..7d983cc 100644
--- a/solve.cpp
+++ b/solve.cpp
@@ -7,7 +7,7 @@
 #include <mutex>
 auto clk_st = std::chrono::high_resolution_clock::now();
 char* worker_sign = "";
-std::mutex mtx;
+
 std::atomic<int> terminated;
 int result = 0;
 int winner, winner_conf;
@@ -26,21 +26,37 @@ void * solve_worker(void *arg) {
    basesolver * sq = (basesolver *)arg;
    while (!terminated) {
         int res = sq->solve();
-        vec<int> seq_model;
-        if (res == 10) {
-            sq->get_model(seq_model);
+        if (sq->controller->opt->DPS == 2) {
+            printf("c %d solved, res is %d\n", sq->id, res);
+            if (res) {
+                terminated = 1;
+                result = res; 
+                printf("c %d solved 1\n", sq->id);
+                sq->set_winner_period();
+                printf("c %d solved 2\n", sq->id);
+                sq->controller->update_winner(sq->id, sq->period);
+                printf("c %d solved 3\n", sq->id);
+                if (res == 10) sq->get_model(sq->model);
+            }
+            printf("c %d really solved, period is %d\n", sq->id, sq->period);
         }
-        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();
-            result = res;
-            winner = sq->id;
-            winner_conf = sq->get_conflicts();
-            if (res == 10) seq_model.copyTo(model);
+        else {
+            vec<int> seq_model;
+            if (res == 10) {
+                sq->get_model(seq_model);
+            }
+            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();
+                result = res;
+                winner = sq->id;
+                winner_conf = sq->get_conflicts();
+                if (res == 10) seq_model.copyTo(model);
+            }
+            seq_model.clear();
+            printf("get result %d with res %d\n", sq->id, res);
         }
-        seq_model.clear();
-        // printf("get result %d with res %d\n", sq->id, res);
    }
    return NULL;
 }
@@ -97,8 +113,12 @@ void light::diversity_workers() {
 }
 
 void light::terminate_workers() {
+    printf("c controller reach limit\n");
     for (int i = 0; i < OPT(threads); i++) {
-        workers[i]->terminate();
+        if (OPT(share) == 1 && OPT(DPS) == 2) 
+            workers[i]->dps_terminate();
+        else 
+            workers[i]->terminate();
     }
     for (int i = 0; i < sharers.size(); i++) {
         sharers[i]->set_terminated();
@@ -152,15 +172,19 @@ int light::solve() {
         // }
     }
     // printf("ending solve\n");
-    terminate_workers();
+    // terminate_workers(); //important, need combine nps/dps !!!!!!!!!!!!!!!!
 
     for (int i = 0; i < OPT(threads); i++) {
         pthread_join(ptr[i], NULL);
     }
+    
+    printf("ending join\n");
+    if (result == 10)
+        workers[winner_id]->model.copyTo(model);
     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);
+    printf("c solve time: %.2lf\nwinner is %d, period is %d\n", solve_time, winner_id, winner_period);
     for (int i = 0; i < OPT(threads); i++) {
         printf("c thread %d waiting time: %.2lf\n", i, workers[i]->get_waiting_time());
     }   
@@ -206,7 +230,7 @@ void solve(int argc, char **argv) {
     int res = S->run();
     if (res == 10) {
         printf("s SATISFIABLE\n");
-        print_model(model);
+        // print_model(model);
     }
     else if (res == 20) {
         printf("s UNSATISFIABLE\n");
diff --git a/solvers/kissat-inc/build/analyze.o b/solvers/kissat-inc/build/analyze.o
index 78299ea..e3edf97 100644
Binary files a/solvers/kissat-inc/build/analyze.o and b/solvers/kissat-inc/build/analyze.o differ
diff --git a/solvers/kissat-inc/build/ands.o b/solvers/kissat-inc/build/ands.o
index e4d94dd..26ea00b 100644
Binary files a/solvers/kissat-inc/build/ands.o and b/solvers/kissat-inc/build/ands.o differ
diff --git a/solvers/kissat-inc/build/application.o b/solvers/kissat-inc/build/application.o
index 7bfc775..936946f 100644
Binary files a/solvers/kissat-inc/build/application.o and b/solvers/kissat-inc/build/application.o differ
diff --git a/solvers/kissat-inc/build/arena.o b/solvers/kissat-inc/build/arena.o
index 526d141..a1e8d93 100644
Binary files a/solvers/kissat-inc/build/arena.o and b/solvers/kissat-inc/build/arena.o differ
diff --git a/solvers/kissat-inc/build/assign.o b/solvers/kissat-inc/build/assign.o
index e81b424..8889857 100644
Binary files a/solvers/kissat-inc/build/assign.o and b/solvers/kissat-inc/build/assign.o differ
diff --git a/solvers/kissat-inc/build/autarky.o b/solvers/kissat-inc/build/autarky.o
index d776ada..62ce415 100644
Binary files a/solvers/kissat-inc/build/autarky.o and b/solvers/kissat-inc/build/autarky.o differ
diff --git a/solvers/kissat-inc/build/averages.o b/solvers/kissat-inc/build/averages.o
index 596fe2d..2682c08 100644
Binary files a/solvers/kissat-inc/build/averages.o and b/solvers/kissat-inc/build/averages.o differ
diff --git a/solvers/kissat-inc/build/backtrack.o b/solvers/kissat-inc/build/backtrack.o
index 6cd8818..d74565b 100644
Binary files a/solvers/kissat-inc/build/backtrack.o and b/solvers/kissat-inc/build/backtrack.o differ
diff --git a/solvers/kissat-inc/build/backward.o b/solvers/kissat-inc/build/backward.o
index ee51e16..8879543 100644
Binary files a/solvers/kissat-inc/build/backward.o and b/solvers/kissat-inc/build/backward.o differ
diff --git a/solvers/kissat-inc/build/build.h b/solvers/kissat-inc/build/build.h
index ddb7273..4332a3f 100644
--- a/solvers/kissat-inc/build/build.h
+++ b/solvers/kissat-inc/build/build.h
@@ -1,5 +1,5 @@
 #define VERSION "1.0.3"
 #define COMPILER "gcc (Ubuntu 9.4.0-1ubuntu1~20.04.1) 9.4.0 -W -Wall -O3 -DNEMBEDDED -DNDEBUG -DNMETRICS -DNSTATISTICS"
 #define ID "79d8d8f20465e71fd2b0f193b468898cd803a59a"
-#define BUILD "Mon Feb 27 07:44:55 UTC 2023 Linux seed4 5.4.0-125-generic x86_64"
+#define BUILD "Mon Mar 13 18:39:10 CST 2023 Linux seed1 5.4.0-139-generic x86_64"
 #define DIR "/home/chenzh/solvers/Light/solvers/kissat-inc/build"
diff --git a/solvers/kissat-inc/build/build.o b/solvers/kissat-inc/build/build.o
index f90b7a0..b83612a 100644
Binary files a/solvers/kissat-inc/build/build.o and b/solvers/kissat-inc/build/build.o differ
diff --git a/solvers/kissat-inc/build/bump.o b/solvers/kissat-inc/build/bump.o
index 918b958..3671e1e 100644
Binary files a/solvers/kissat-inc/build/bump.o and b/solvers/kissat-inc/build/bump.o differ
diff --git a/solvers/kissat-inc/build/clause.o b/solvers/kissat-inc/build/clause.o
index fe567e6..bc97cbc 100644
Binary files a/solvers/kissat-inc/build/clause.o and b/solvers/kissat-inc/build/clause.o differ
diff --git a/solvers/kissat-inc/build/clueue.o b/solvers/kissat-inc/build/clueue.o
index bc7de95..e815807 100644
Binary files a/solvers/kissat-inc/build/clueue.o and b/solvers/kissat-inc/build/clueue.o differ
diff --git a/solvers/kissat-inc/build/collect.o b/solvers/kissat-inc/build/collect.o
index 59f1a4c..f35aa7b 100644
Binary files a/solvers/kissat-inc/build/collect.o and b/solvers/kissat-inc/build/collect.o differ
diff --git a/solvers/kissat-inc/build/compact.o b/solvers/kissat-inc/build/compact.o
index 11d0f37..9ae4923 100644
Binary files a/solvers/kissat-inc/build/compact.o and b/solvers/kissat-inc/build/compact.o differ
diff --git a/solvers/kissat-inc/build/decide.o b/solvers/kissat-inc/build/decide.o
index 6b43679..13b2bf3 100644
Binary files a/solvers/kissat-inc/build/decide.o and b/solvers/kissat-inc/build/decide.o differ
diff --git a/solvers/kissat-inc/build/deduce.o b/solvers/kissat-inc/build/deduce.o
index 42800c1..e4c5083 100644
Binary files a/solvers/kissat-inc/build/deduce.o and b/solvers/kissat-inc/build/deduce.o differ
diff --git a/solvers/kissat-inc/build/dense.o b/solvers/kissat-inc/build/dense.o
index 2b22678..b62bddf 100644
Binary files a/solvers/kissat-inc/build/dense.o and b/solvers/kissat-inc/build/dense.o differ
diff --git a/solvers/kissat-inc/build/dominate.o b/solvers/kissat-inc/build/dominate.o
index cce757d..d26e628 100644
Binary files a/solvers/kissat-inc/build/dominate.o and b/solvers/kissat-inc/build/dominate.o differ
diff --git a/solvers/kissat-inc/build/eliminate.o b/solvers/kissat-inc/build/eliminate.o
index 5cca1af..1856a68 100644
Binary files a/solvers/kissat-inc/build/eliminate.o and b/solvers/kissat-inc/build/eliminate.o differ
diff --git a/solvers/kissat-inc/build/equivalences.o b/solvers/kissat-inc/build/equivalences.o
index 12e24ec..465992a 100644
Binary files a/solvers/kissat-inc/build/equivalences.o and b/solvers/kissat-inc/build/equivalences.o differ
diff --git a/solvers/kissat-inc/build/extend.o b/solvers/kissat-inc/build/extend.o
index 837aaad..e37d6f7 100644
Binary files a/solvers/kissat-inc/build/extend.o and b/solvers/kissat-inc/build/extend.o differ
diff --git a/solvers/kissat-inc/build/failed.o b/solvers/kissat-inc/build/failed.o
index dbd62e0..0f027ca 100644
Binary files a/solvers/kissat-inc/build/failed.o and b/solvers/kissat-inc/build/failed.o differ
diff --git a/solvers/kissat-inc/build/flags.o b/solvers/kissat-inc/build/flags.o
index 7aa6dc7..8811db5 100644
Binary files a/solvers/kissat-inc/build/flags.o and b/solvers/kissat-inc/build/flags.o differ
diff --git a/solvers/kissat-inc/build/forward.o b/solvers/kissat-inc/build/forward.o
index 4069774..f2ef269 100644
Binary files a/solvers/kissat-inc/build/forward.o and b/solvers/kissat-inc/build/forward.o differ
diff --git a/solvers/kissat-inc/build/frames.o b/solvers/kissat-inc/build/frames.o
index 7acff15..49ae0de 100644
Binary files a/solvers/kissat-inc/build/frames.o and b/solvers/kissat-inc/build/frames.o differ
diff --git a/solvers/kissat-inc/build/gates.o b/solvers/kissat-inc/build/gates.o
index 2f4ba95..d5634da 100644
Binary files a/solvers/kissat-inc/build/gates.o and b/solvers/kissat-inc/build/gates.o differ
diff --git a/solvers/kissat-inc/build/ifthenelse.o b/solvers/kissat-inc/build/ifthenelse.o
index 71b3180..87570fc 100644
Binary files a/solvers/kissat-inc/build/ifthenelse.o and b/solvers/kissat-inc/build/ifthenelse.o differ
diff --git a/solvers/kissat-inc/build/import.o b/solvers/kissat-inc/build/import.o
index c22e7fb..f8a0e84 100644
Binary files a/solvers/kissat-inc/build/import.o and b/solvers/kissat-inc/build/import.o differ
diff --git a/solvers/kissat-inc/build/internal.o b/solvers/kissat-inc/build/internal.o
index b61d4aa..4e0c4b6 100644
Binary files a/solvers/kissat-inc/build/internal.o and b/solvers/kissat-inc/build/internal.o differ
diff --git a/solvers/kissat-inc/build/kissat b/solvers/kissat-inc/build/kissat
index 43c2d21..e1f4f00 100755
Binary files a/solvers/kissat-inc/build/kissat and b/solvers/kissat-inc/build/kissat differ
diff --git a/solvers/kissat-inc/build/learn.o b/solvers/kissat-inc/build/learn.o
index 4d8813b..d14e592 100644
Binary files a/solvers/kissat-inc/build/learn.o and b/solvers/kissat-inc/build/learn.o differ
diff --git a/solvers/kissat-inc/build/libkissat.a b/solvers/kissat-inc/build/libkissat.a
index 855eb09..795bfb2 100644
Binary files a/solvers/kissat-inc/build/libkissat.a and b/solvers/kissat-inc/build/libkissat.a differ
diff --git a/solvers/kissat-inc/build/limits.o b/solvers/kissat-inc/build/limits.o
index 1c435ca..101d154 100644
Binary files a/solvers/kissat-inc/build/limits.o and b/solvers/kissat-inc/build/limits.o differ
diff --git a/solvers/kissat-inc/build/minimize.o b/solvers/kissat-inc/build/minimize.o
index 0aca901..5a06613 100644
Binary files a/solvers/kissat-inc/build/minimize.o and b/solvers/kissat-inc/build/minimize.o differ
diff --git a/solvers/kissat-inc/build/mode.o b/solvers/kissat-inc/build/mode.o
index c297fa5..13c79d4 100644
Binary files a/solvers/kissat-inc/build/mode.o and b/solvers/kissat-inc/build/mode.o differ
diff --git a/solvers/kissat-inc/build/parse.o b/solvers/kissat-inc/build/parse.o
index 83da2c0..7c928a3 100644
Binary files a/solvers/kissat-inc/build/parse.o and b/solvers/kissat-inc/build/parse.o differ
diff --git a/solvers/kissat-inc/build/phases.o b/solvers/kissat-inc/build/phases.o
index f50a106..061d11e 100644
Binary files a/solvers/kissat-inc/build/phases.o and b/solvers/kissat-inc/build/phases.o differ
diff --git a/solvers/kissat-inc/build/print.o b/solvers/kissat-inc/build/print.o
index 6e145e7..59e41e6 100644
Binary files a/solvers/kissat-inc/build/print.o and b/solvers/kissat-inc/build/print.o differ
diff --git a/solvers/kissat-inc/build/probe.o b/solvers/kissat-inc/build/probe.o
index 5915217..a321961 100644
Binary files a/solvers/kissat-inc/build/probe.o and b/solvers/kissat-inc/build/probe.o differ
diff --git a/solvers/kissat-inc/build/profile.o b/solvers/kissat-inc/build/profile.o
index b471860..2466e95 100644
Binary files a/solvers/kissat-inc/build/profile.o and b/solvers/kissat-inc/build/profile.o differ
diff --git a/solvers/kissat-inc/build/promote.o b/solvers/kissat-inc/build/promote.o
index d6f4eea..9248cff 100644
Binary files a/solvers/kissat-inc/build/promote.o and b/solvers/kissat-inc/build/promote.o differ
diff --git a/solvers/kissat-inc/build/proof.o b/solvers/kissat-inc/build/proof.o
index df7fef3..e7519d6 100644
Binary files a/solvers/kissat-inc/build/proof.o and b/solvers/kissat-inc/build/proof.o differ
diff --git a/solvers/kissat-inc/build/propdense.o b/solvers/kissat-inc/build/propdense.o
index 95d84a1..8a9292c 100644
Binary files a/solvers/kissat-inc/build/propdense.o and b/solvers/kissat-inc/build/propdense.o differ
diff --git a/solvers/kissat-inc/build/prophyper.o b/solvers/kissat-inc/build/prophyper.o
index 55ec5a8..b3aa71a 100644
Binary files a/solvers/kissat-inc/build/prophyper.o and b/solvers/kissat-inc/build/prophyper.o differ
diff --git a/solvers/kissat-inc/build/proprobe.o b/solvers/kissat-inc/build/proprobe.o
index fe3d596..f8e5d53 100644
Binary files a/solvers/kissat-inc/build/proprobe.o and b/solvers/kissat-inc/build/proprobe.o differ
diff --git a/solvers/kissat-inc/build/propsearch.o b/solvers/kissat-inc/build/propsearch.o
index 4a64bfa..d023da6 100644
Binary files a/solvers/kissat-inc/build/propsearch.o and b/solvers/kissat-inc/build/propsearch.o differ
diff --git a/solvers/kissat-inc/build/queue.o b/solvers/kissat-inc/build/queue.o
index fabe247..3a07400 100644
Binary files a/solvers/kissat-inc/build/queue.o and b/solvers/kissat-inc/build/queue.o differ
diff --git a/solvers/kissat-inc/build/reduce.o b/solvers/kissat-inc/build/reduce.o
index d09c36a..188b8c2 100644
Binary files a/solvers/kissat-inc/build/reduce.o and b/solvers/kissat-inc/build/reduce.o differ
diff --git a/solvers/kissat-inc/build/reluctant.o b/solvers/kissat-inc/build/reluctant.o
index 164891e..f993a97 100644
Binary files a/solvers/kissat-inc/build/reluctant.o and b/solvers/kissat-inc/build/reluctant.o differ
diff --git a/solvers/kissat-inc/build/rephase.o b/solvers/kissat-inc/build/rephase.o
index 1d0ffaf..cf006cd 100644
Binary files a/solvers/kissat-inc/build/rephase.o and b/solvers/kissat-inc/build/rephase.o differ
diff --git a/solvers/kissat-inc/build/resize.o b/solvers/kissat-inc/build/resize.o
index 56f25fe..ca5f4c9 100644
Binary files a/solvers/kissat-inc/build/resize.o and b/solvers/kissat-inc/build/resize.o differ
diff --git a/solvers/kissat-inc/build/resolve.o b/solvers/kissat-inc/build/resolve.o
index d0f5328..e82bd91 100644
Binary files a/solvers/kissat-inc/build/resolve.o and b/solvers/kissat-inc/build/resolve.o differ
diff --git a/solvers/kissat-inc/build/resources.o b/solvers/kissat-inc/build/resources.o
index 04265e0..b1ffd6e 100644
Binary files a/solvers/kissat-inc/build/resources.o and b/solvers/kissat-inc/build/resources.o differ
diff --git a/solvers/kissat-inc/build/restart.o b/solvers/kissat-inc/build/restart.o
index adbac54..abd545f 100644
Binary files a/solvers/kissat-inc/build/restart.o and b/solvers/kissat-inc/build/restart.o differ
diff --git a/solvers/kissat-inc/build/search.o b/solvers/kissat-inc/build/search.o
index 45c009d..40663b0 100644
Binary files a/solvers/kissat-inc/build/search.o and b/solvers/kissat-inc/build/search.o differ
diff --git a/solvers/kissat-inc/build/sort.o b/solvers/kissat-inc/build/sort.o
index e516e53..edbc54e 100644
Binary files a/solvers/kissat-inc/build/sort.o and b/solvers/kissat-inc/build/sort.o differ
diff --git a/solvers/kissat-inc/build/statistics.o b/solvers/kissat-inc/build/statistics.o
index 687fc08..47b0400 100644
Binary files a/solvers/kissat-inc/build/statistics.o and b/solvers/kissat-inc/build/statistics.o differ
diff --git a/solvers/kissat-inc/build/strengthen.o b/solvers/kissat-inc/build/strengthen.o
index 60b8718..e199077 100644
Binary files a/solvers/kissat-inc/build/strengthen.o and b/solvers/kissat-inc/build/strengthen.o differ
diff --git a/solvers/kissat-inc/build/substitute.o b/solvers/kissat-inc/build/substitute.o
index 7992d03..4b29752 100644
Binary files a/solvers/kissat-inc/build/substitute.o and b/solvers/kissat-inc/build/substitute.o differ
diff --git a/solvers/kissat-inc/build/ternary.o b/solvers/kissat-inc/build/ternary.o
index 1988311..37e9358 100644
Binary files a/solvers/kissat-inc/build/ternary.o and b/solvers/kissat-inc/build/ternary.o differ
diff --git a/solvers/kissat-inc/build/trail.o b/solvers/kissat-inc/build/trail.o
index 5f25454..186a5cb 100644
Binary files a/solvers/kissat-inc/build/trail.o and b/solvers/kissat-inc/build/trail.o differ
diff --git a/solvers/kissat-inc/build/transitive.o b/solvers/kissat-inc/build/transitive.o
index ff6839c..c9185bc 100644
Binary files a/solvers/kissat-inc/build/transitive.o and b/solvers/kissat-inc/build/transitive.o differ
diff --git a/solvers/kissat-inc/build/vector.o b/solvers/kissat-inc/build/vector.o
index bb1dc01..8475313 100644
Binary files a/solvers/kissat-inc/build/vector.o and b/solvers/kissat-inc/build/vector.o differ
diff --git a/solvers/kissat-inc/build/vivify.o b/solvers/kissat-inc/build/vivify.o
index 0c97b85..881bb95 100644
Binary files a/solvers/kissat-inc/build/vivify.o and b/solvers/kissat-inc/build/vivify.o differ
diff --git a/solvers/kissat-inc/build/walk.o b/solvers/kissat-inc/build/walk.o
index 8a89c5b..e3b43b9 100644
Binary files a/solvers/kissat-inc/build/walk.o and b/solvers/kissat-inc/build/walk.o differ
diff --git a/solvers/kissat-inc/build/watch.o b/solvers/kissat-inc/build/watch.o
index cfc4d3e..cdfd11b 100644
Binary files a/solvers/kissat-inc/build/watch.o and b/solvers/kissat-inc/build/watch.o differ
diff --git a/solvers/kissat-inc/build/weaken.o b/solvers/kissat-inc/build/weaken.o
index 44d4884..c2a0e7c 100644
Binary files a/solvers/kissat-inc/build/weaken.o and b/solvers/kissat-inc/build/weaken.o differ
diff --git a/solvers/kissat-inc/build/xors.o b/solvers/kissat-inc/build/xors.o
index 779e5c6..119ac40 100644
Binary files a/solvers/kissat-inc/build/xors.o and b/solvers/kissat-inc/build/xors.o differ
diff --git a/solvers/kissat-inc/src/analyze.c b/solvers/kissat-inc/src/analyze.c
index 0958077..fe52fa3 100644
--- a/solvers/kissat-inc/src/analyze.c
+++ b/solvers/kissat-inc/src/analyze.c
@@ -168,6 +168,7 @@ analyze_reason_side_literals(kissat *solver)
     {
       assert(a->reason < SIZE_STACK(solver->arena));
       clause *c = (clause *)(arena + a->reason);
+      solver->dps_ticks++;
       for (all_literals_in_clause(lit, c))
         if (IDX(lit) != idx)
           mark_literal_as_analyzed(solver, all_assigned, lit,
diff --git a/solvers/kissat-inc/src/eliminate.c b/solvers/kissat-inc/src/eliminate.c
index dd1881d..92f2323 100644
--- a/solvers/kissat-inc/src/eliminate.c
+++ b/solvers/kissat-inc/src/eliminate.c
@@ -315,6 +315,7 @@ weaken_clauses (kissat * solver, unsigned lit)
 	    kissat_weaken_clause (solver, lit, c);
 	  LOGCLS (c, "removing %s", LOGLIT (lit));
 	  kissat_eliminate_clause (solver, c, lit);
+    solver->dps_ticks++;
 	}
     }
   RELEASE_WATCHES (*pos_watches);
@@ -351,7 +352,8 @@ weaken_clauses (kissat * solver, unsigned lit)
 	  if (!optimize && !satisfied)
 	    kissat_weaken_clause (solver, not_lit, d);
 	  LOGCLS (d, "removing %s", LOGLIT (not_lit));
-	  kissat_eliminate_clause (solver, d, not_lit);
+	  kissat_eliminate_clause (solver, d, not_lit);   
+    solver->dps_ticks++;
 	}
     }
   if (optimize && neg_watches->size)
diff --git a/solvers/kissat-inc/src/forward.c b/solvers/kissat-inc/src/forward.c
index 019faef..b24058a 100644
--- a/solvers/kissat-inc/src/forward.c
+++ b/solvers/kissat-inc/src/forward.c
@@ -151,6 +151,7 @@ find_forward_subsumption_candidates (kissat * solver, references * candidates)
 	continue;
       assert (c->size > 2);
       unsigned subsume = 0;
+	  solver->dps_ticks++;
       for (all_literals_in_clause (lit, c))
 	{
 	  const unsigned idx = IDX (lit);
@@ -270,7 +271,11 @@ forward_literal (kissat * solver, unsigned lit, bool binaries,
 
 	  INC (subsumption_checks);
 
-	  subsume = true;
+	  subsume = true;	
+
+
+	  solver->dps_ticks++;
+
 
 	  unsigned candidate = INVALID_LIT;
 
@@ -605,6 +610,7 @@ forward_subsume_all_clauses (kissat * solver)
 #ifndef QUIET
 	checked++;
 #endif
+	solver->dps_ticks++;
 	bool removed = false;
 	if (forward_subsumed_clause (solver, c, &removed))
 	  subsumed++;
@@ -656,6 +662,7 @@ forward_subsume_all_clauses (kissat * solver)
 	if (c->subsume)
 	  remain++;
 #endif
+	solver->dps_ticks++;
 	for (all_literals_in_clause (lit, c))
 	  {
 	    const unsigned idx = IDX (lit);
diff --git a/solvers/kissat-inc/src/internal.c b/solvers/kissat-inc/src/internal.c
index c5af8d5..27614fc 100644
--- a/solvers/kissat-inc/src/internal.c
+++ b/solvers/kissat-inc/src/internal.c
@@ -39,6 +39,7 @@ kissat_init (void)
   solver->watching = true;
   solver->conflict.size = 2;
   solver->conflict.keep = true;
+  solver->dps_ticks=0;
   solver->scinc = 1.0;
   solver->first_reducible = INVALID_REF;
   solver->last_irredundant = INVALID_REF;
diff --git a/solvers/kissat-inc/src/internal.h b/solvers/kissat-inc/src/internal.h
index a8931b7..a6d1647 100644
--- a/solvers/kissat-inc/src/internal.h
+++ b/solvers/kissat-inc/src/internal.h
@@ -73,10 +73,12 @@ typedef STACK (watch *) patches;
 
 struct kissat
 {
+  int dps_ticks;
   int  (* cbkImportUnit)  (void *);
   int  (* cbkImportClause)(void *, int *, cvec *);
   void (* cbkExportClause)(void *, int, cvec *);	        
-  void (* cbkWaitSharing) (void *);           // callback for clause learning
+  int (* cbkWaitSharing) (void *);          
+  void (* cbkFreeClause)  (void *);           // callback for clause learning
   int share_dps;
   int share_dps_period;
   cvec *importedClause;
diff --git a/solvers/kissat-inc/src/minimize.c b/solvers/kissat-inc/src/minimize.c
index 151194a..017abde 100644
--- a/solvers/kissat-inc/src/minimize.c
+++ b/solvers/kissat-inc/src/minimize.c
@@ -9,6 +9,7 @@ minimize_reference (kissat * solver, assigned * assigned,
 {
   const unsigned not_lit = NOT (lit);
   clause *c = kissat_dereference_clause (solver, ref);
+  solver->dps_ticks++;
   for (all_literals_in_clause (other, c))
     if (other != not_lit &&
 	!minimize_literal (solver, assigned, other, depth))
diff --git a/solvers/kissat-inc/src/propdense.c b/solvers/kissat-inc/src/propdense.c
index 8a55871..0e55a4a 100644
--- a/solvers/kissat-inc/src/propdense.c
+++ b/solvers/kissat-inc/src/propdense.c
@@ -107,6 +107,7 @@ non_watching_propagate_literal (kissat * solver,
 
   ADD (ticks, ticks);
   ADD (dense_ticks, ticks);
+  solver->dps_ticks += ticks;
 
   return true;
 }
diff --git a/solvers/kissat-inc/src/prophyper.c b/solvers/kissat-inc/src/prophyper.c
index 055d7f1..099fc39 100644
--- a/solvers/kissat-inc/src/prophyper.c
+++ b/solvers/kissat-inc/src/prophyper.c
@@ -77,6 +77,8 @@ binary_propagate_literal (kissat * solver, unsigned lit)
   const watch *begin = BEGIN_WATCHES (*watches);
   const watch *end = END_WATCHES (*watches);
   const watch *p = begin;
+  int ticks =  kissat_cache_lines (watches->size, sizeof (watch));
+  solver->dps_ticks +=ticks;
 
   clause *res = 0;
 
diff --git a/solvers/kissat-inc/src/proplit.h b/solvers/kissat-inc/src/proplit.h
index 881ae07..32c307a 100644
--- a/solvers/kissat-inc/src/proplit.h
+++ b/solvers/kissat-inc/src/proplit.h
@@ -243,6 +243,7 @@ PROPAGATE_LITERAL (kissat * solver,
 	}
     }
   solver->ticks += ticks;
+  solver->dps_ticks += ticks;
 
   while (p != end_watches)
     *q++ = *p++;
diff --git a/solvers/kissat-inc/src/resolve.c b/solvers/kissat-inc/src/resolve.c
index 58669d5..e8348a4 100644
--- a/solvers/kissat-inc/src/resolve.c
+++ b/solvers/kissat-inc/src/resolve.c
@@ -213,6 +213,7 @@ generate_resolvents (kissat * solver, unsigned lit,
 	    }
 
 	  PUSH_STACK (solver->resolvents, INVALID_LIT);
+	  solver->dps_ticks++;
 	}
 
       for (all_literals_in_clause (other, c))
diff --git a/solvers/kissat-inc/src/search.c b/solvers/kissat-inc/src/search.c
index a30c2e5..5efbb73 100644
--- a/solvers/kissat-inc/src/search.c
+++ b/solvers/kissat-inc/src/search.c
@@ -171,12 +171,16 @@ int kissat_search(kissat *solver)
       solver->reseting = 0;
     }
     if (!solver->level) {
-      if (solver->share_dps == 1 && solver->nconflict >= solver->share_dps_period) {
-        solver->nconflict = 0;
-        solver->cbkWaitSharing(solver->issuer);
+      int should_free = 0;
+      if (solver->share_dps > 0 && solver->dps_ticks >= solver->share_dps_period) {
+        solver->dps_ticks -= solver->share_dps_period;
+        should_free = solver->cbkWaitSharing(solver->issuer);
+        if (should_free == -1) return 0;
       }
       if (!kissat_importUnitClauses(solver)) return 20;
       if (!kissat_importClauses(solver)) return 20;
+      if (should_free == 1 && solver->share_dps == 2)
+        solver->cbkFreeClause(solver->issuer);
     }
     clause *conflict = kissat_search_propagate(solver);
     if (conflict)
diff --git a/solvers/kissat-inc/src/substitute.c b/solvers/kissat-inc/src/substitute.c
index d65423b..b0da092 100644
--- a/solvers/kissat-inc/src/substitute.c
+++ b/solvers/kissat-inc/src/substitute.c
@@ -100,6 +100,10 @@ determine_representatives (kissat * solver, unsigned *repr)
 	      assert (reach_lit == mark_lit);
 	      assert (repr[lit] == INVALID_LIT);
 	      watches *watches = all_watches + not_lit;
+
+  		unsigned ticks = kissat_cache_lines (watches->size, sizeof (watch));
+		solver->dps_ticks += 1 + ticks;
+
 	      for (all_binary_blocking_watches (watch, *watches))
 		{
 		  if (!watch.type.binary)
@@ -199,6 +203,10 @@ determine_representatives (kissat * solver, unsigned *repr)
 	      LOG ("substitute mark[%s] = %u", LOGLIT (lit), reached);
 	      const unsigned not_lit = NOT (lit);
 	      watches *watches = all_watches + not_lit;
+		  
+			unsigned ticks = kissat_cache_lines (watches->size, sizeof (watch));
+			solver->dps_ticks += 1 + ticks;
+
 	      for (all_binary_blocking_watches (watch, *watches))
 		{
 		  if (!watch.type.binary)
diff --git a/solvers/kissat-inc/src/transitive.c b/solvers/kissat-inc/src/transitive.c
index 6debdcc..e6eb643 100644
--- a/solvers/kissat-inc/src/transitive.c
+++ b/solvers/kissat-inc/src/transitive.c
@@ -89,6 +89,7 @@ transitive_reduce (kissat * solver,
   watch *begin_src = BEGIN_WATCHES (*src_watches);
   unsigned ticks = kissat_cache_lines (src_watches->size, sizeof (watch));
   ADD (transitive_ticks, ticks + 1);
+  solver->dps_ticks += 1 + ticks;
   const unsigned not_src = NOT (src);
   unsigned reduced = 0;
   bool failed = false;
@@ -158,7 +159,7 @@ transitive_reduce (kissat * solver,
       ADD (propagations, propagated);
       ADD (probing_propagations, propagated);
       ADD (transitive_propagations, propagated);
-
+      solver->dps_ticks += ticks + 1;
       transitive_backtrack (solver, saved);
 
       if (transitive)
diff --git a/testLight/cal_solver.py b/testLight/cal_solver.py
index 4307326..50d337c 100644
--- a/testLight/cal_solver.py
+++ b/testLight/cal_solver.py
@@ -228,10 +228,10 @@ class calculater(object):
                     have_diff_res = True
 
                 # if(True):
-                # if(False):
+                if(False):
                 # if(no_answer):
                 # if(all_can_solve):
-                if(have_diff_res):
+                # if(have_diff_res):
                 # if(have_diff_res and answer_this == "sat"):
                 # if(self.solvers[-2].datas[ins_name].res != self.solvers[-1].datas[ins_name].res):
                     print_line_ct += 1
@@ -271,21 +271,48 @@ if __name__ == "__main__":
     # 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/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"))
+
+    # 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-dps-r","4-2-dps"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-2-dps2-r","4-2-dps2"))
+
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps","4-3-sharing-nps"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-rp-tc2","4-3-sharing-nps-rp2"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-p","4-3-sharing-nps-p"))
+
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-tc2","4-3-sharing-nps2"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-rp","4-3-sharing-nps-rp"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-p-tc2","4-3-sharing-nps-p2"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nopre-sharing-r","4-3-nopre"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nosharing-r","4-3-nosharing"))
+
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-2","thread2"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-4","thread4"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-8","thread8"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-16","thread16"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-tc2","thread32"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-64","thread64"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-4-nps-64-2","thread64-2"))
+
+
+    
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-tc3","4-3-sharing-nps3"))
+    # solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-3-nps-tc4","4-3-sharing-nps4"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-5-dps-20","5-5-dps-20"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-6-dps-2","5-6-dps-2"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-7-dps-20-1k","5-7-dps-20-1k"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-7-dps-20-2k","5-7-dps-20-2k"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v5-7-dps-20-4k","5-7-dps-20-4k"))
 
     # 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/sat2020/vbs.txt", "vbs"])
+    # samples.append(["/pub/data/chenzh/data/sat2021/vbs.txt", "vbs"])
+    samples.append(["/pub/data/chenzh/data/sat2022/vbs.txt", "vbs"])
     # samples.append(["/pub/data/chenzh/data/sat2022/all.txt", "all"])
+    # samples.append(["/pub/data/chenzh/data/sat2022/unknown.txt", "unknown"])
     clt = calculater(solvers, samples)
     clt.cal_and_show()
 
diff --git a/testLight/dps.log b/testLight/dps.log
new file mode 100644
index 0000000..2e3f48d
--- /dev/null
+++ b/testLight/dps.log
@@ -0,0 +1,347 @@
+nohup: ignoring input
+10pipe_k.cnf
+13pipe_k.cnf
+14pipe_q0_k.cnf
+20-100-frag12-0_sat.cnf
+20-100-frag12-14_sat.cnf
+20-100-frag12-32_sat.cnf
+20-100-frag12-53_sat.cnf
+20-100-lambda100-14_sat.cnf
+20-100-lambda100-14_unsat.cnf
+20-100-lambda100-47_unsat.cnf
+20-100-lambda100-49_sat.cnf
+20-100-lambda100-65_sat.cnf
+20-100-lambda100-89_sat.cnf
+20-100-lambda100-89_unsat.cnf
+20-100-p100-55_sat.cnf
+20-100-p100-55_unsat.cnf
+2bitcomp_5.hg_20.cnf
+51.smt2.cnf
+73.smt2.cnf
+9dlx_vliw_at_b_iq5.cnf
+9dlx_vliw_at_b_iq8.cnf
+ACG-15-10p1.cnf
+ak016modbtsimpbisc.cnf
+ak032modbtmodbtisc.cnf
+ak128paralparalisc.cnf
+assoc_mult_err_3.c.cnf
+at-least-two-aaai10-planning-ipc5-pathways-17-step20.cnf
+at-least-two-aaai10-planning-ipc5-pipesworld-12-step15.cnf
+at-least-two-hwmcc10-timeframe-expansion-k50-pdtviseisenberg2-tseitin.cnf
+at-least-two-ibm-2004-23-k100.cnf
+at-least-two-maris-s03-gripper11.cnf
+at-least-two-smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf
+at-least-two-sokoban-sequential-p145-microban-sequential.030-NOTKNOWN.cnf
+at-least-two-traffic_b_unsat.cnf
+at-least-two-traffic_f_unknown.cnf
+at-least-two-traffic_kkb_unknown.cnf
+at-least-two-traffic_pcb_unknown.cnf
+vmpc_26.cnf
+at-least-two-vmpc_28.cnf
+b04_s_unknown_pre.cnf
+b2005-p3-12x12c10h7-Ser7-0.cnf
+barman-pfile10-039.sas.ex.15.cnf
+barman-pfile10-040.sas.ex.15.cnf
+battleship-12-12-unsat.cnf
+battleship-14-26-sat.cnf
+blocks-blocks-36-0.180-SAT.cnf
+blocks-blocks-37-1.120-NOTKNOWN.cnf
+blocks-blocks-37-1.130-NOTKNOWN.cnf
+bvsdiv_19.smt2.cnf
+bvsmod_18.smt2.cnf
+bvsmod_19.smt2.cnf
+bvsub_08985.smt2.cnf
+bvsub_12973.smt2.cnf
+bvsub_19952.smt2.cnf
+bv-term-small-rw_1492.smt2.cnf
+bvurem_20.smt2.cnf
+Circuit_multiplier18.cnf
+Circuit_multiplier22.cnf
+Circuit_multiplier24.cnf
+Circuit_multiplier25.cnf
+Circuit_multiplier26.cnf
+Circuit_multiplier29.cnf
+Circuit_multiplier33.cnf
+Circuit_multiplier34.cnf
+Circuit_multiplier35.cnf
+Circuit_multiplier36.cnf
+Circuit_multiplier37.cnf
+Circuit_multiplier45.cnf
+Circuit_multiplier53.cnf
+crafted_n10_d6_c4_num15.cnf
+crafted_n10_d6_c4_num21.cnf
+crafted_n11_d6_c4_num14.cnf
+crafted_n12_d6_c3_num18.cnf
+crafted_n12_d6_c3_num28.cnf
+crafted_n12_d6_c4_num17.cnf
+ctl_4201_555_unsat.cnf
+ctl_4291_567_1_unsat.cnf
+ctl_4291_567_11_unsat.cnf
+ctl_4291_567_6_unsat_pre.cnf
+ctl_4291_567_9_unsat.cnf
+dist10.c.cnf
+dist4.c.cnf
+E00X23.cnf
+E02F17.cnf
+ecarev-110-1031-23-40-8.cnf
+ecarev-110-4099-22-30-4.cnf
+edit_distance007_85.cnf
+edit_distance019_312.cnf
+edit_distance023_281.cnf
+edit_distance023_282.cnf
+edit_distance023_283.cnf
+edit_distance025_448.cnf
+edit_distance025_449.cnf
+edit_distance025_450.cnf
+edit_distance031_283.cnf
+edit_distance031_284.cnf
+edit_distance035_393.cnf
+edit_distance041_182.cnf
+edit_distance041_183.cnf
+ER_500_40_2.apx_0.cnf
+erin2_0x0_n207-379.cnf
+erin2_0x0-379.cnf
+erin2_0x1e3-216.cnf
+ex045_7.cnf
+ex065_25.cnf
+ex095_8.cnf
+ex175_20.cnf
+HCP-424-60.cnf
+HCP-446-105.cnf
+HCP-446-420.cnf
+HCP-446-60.cnf
+HCP-470-105.cnf
+HCP-470-420.cnf
+HCP-470-60.cnf
+HCP-506-60.cnf
+HCP-522-105.cnf
+HCP-526-105.cnf
+HCP-526-420.cnf
+HCP-529-420.cnf
+HCP-529-60.cnf
+huck.col.11.cnf
+IBM_FV_2004_rule_batch_30_SAT_dat.k75.cnf
+k2fix_gr_rcs_w8.shuffled.cnf
+Kakuro-easy-045-ext.xml.hg_4.cnf
+Kakuro-easy-051-ext.xml.hg_4.cnf
+Kakuro-easy-089-ext.xml.hg_4.cnf
+Kakuro-easy-104-ext.xml.hg_6.cnf
+Kakuro-easy-112-ext.xml.hg_7.cnf
+Kakuro-easy-115-ext.xml.hg_5.cnf
+Kakuro-easy-118-ext.xml.hg_4.cnf
+Kakuro-easy-127-ext.xml.hg_7.cnf
+Kakuro-easy-132-ext.xml.hg_8.cnf
+Kakuro-easy-142-ext.xml.hg_8.cnf
+Kakuro-easy-150-ext.xml.hg_9.cnf
+Kakuro-easy-156-ext.xml.hg_7.cnf
+ktf_TF-1.tf_4_0.06_101.cnf
+ktf_TF-3.tf_2_0.02_24.cnf
+ktf_TF-3.tf_3_0.02_24.cnf
+ktf_TF-4.tf_2_0.02_18.cnf
+ktf_TF-4.tf_4_0.04_35.cnf
+ktf_TF-4.tf_4_0.06_52.cnf
+ktf_TF-6.tf_4_0.06_77.cnf
+ktf_TF-7.tf_3_0.06_113.cnf
+ktf_TF-8.tf_4_0.06_109.cnf
+LABS_n041_goal003.cnf
+LABS_n068_goal001.cnf
+LABS_n069_goal001.cnf
+LABS_n072_goal006.cnf
+LABS_n089_goal008.cnf
+maximum_constrained_partition_14_bits_n200.cnf
+maximum_constrained_partition_18_bits_n200.cnf
+maxor128.cnf
+mp1-blockpuzzle_5x10_s5_free3.cnf
+mp1-blockpuzzle_5x12_s6_free3.cnf
+mp1-blockpuzzle_9x9_s1_free8.cnf
+mp1-blockpuzzle_9x9_s5_free3.cnf
+mp1-bsat201-707.cnf
+mp1-bsat210-739.cnf
+mp1-klieber2017s-0300-034-t12.cnf
+mp1-klieber2017s-0490-024-t12.cnf
+mp1-klieber2017s-1000-023-eq.cnf
+mp1-klieber2017s-1000-024-eq.cnf
+mp1-klieber2017s-1200-022-eq.cnf
+mp1-klieber2017s-2000-022-eq.cnf
+mp1-Nb6T06.cnf
+mp1-Nb6T07.cnf
+mp1-Nb7T44.cnf
+mp1-Nb7T46.cnf
+mp1-squ_ali_s10x10_c39_abio_SAT.cnf
+mp1-squ_any_s09x07_c27_abix_UNS.cnf
+mp1-tri_ali_s11_c35_abix_UNS.cnf
+mp1-tri_ali_s11_c35_bail_UNS.cnf
+MVD_ADS_S1_5_5.cnf
+MVD_ADS_S10_5_6.cnf
+MVD_ADS_S10_6_6.cnf
+MVD_ADS_S11_6_7.cnf
+MVD_ADS_S11_7_7.cnf
+MVD_ADS_S11_8_7.cnf
+MVD_ADS_S3_5_5.cnf
+MVD_ADS_S4_5_5.cnf
+MVD_ADS_S5_6_6.cnf
+MVD_ADS_S6_6_5.cnf
+MVD_ADS_S6_6_6.cnf
+MVD_ADS_S7_6_6.cnf
+MVD_ADS_S9_6_6.cnf
+Mycielski-10-hints-10.cnf
+Mycielski-10-hints-7.cnf
+Mycielski-10-hints-8.cnf
+Mycielski-10-hints-9.cnf
+Mycielski-11-hints-1.cnf
+Mycielski-11-hints-2.cnf
+Mycielski-11-hints-3.cnf
+Mycielski-11-hints-4.cnf
+n320p5q2_n.apx_16.cnf
+n320p5q2_n.apx_17.cnf
+Nb51T6.cnf
+ndhf_xits_09_UNSAT.cnf
+p01_lb_05.cnf
+pb_300_05_lb_16.cnf
+pb_300_05_lb_17.cnf
+pb_300_06_lb_02.cnf
+pb_300_10_lb_06.cnf
+php12e12.cnf
+prime_a20_b20.cnf
+prime_a22_b22.cnf
+prime_a24_b24.cnf
+puzzle30_sat.cnf
+puzzle34_sat.cnf
+puzzle34_unsat.cnf
+puzzle35_sat.cnf
+puzzle35_unsat.cnf
+puzzle36_sat.cnf
+puzzle37_unsat.cnf
+puzzle39_sat.cnf
+puzzle42_sat.cnf
+puzzle44_unsat.cnf
+quad_res_r21_m22.cnf
+quad_res_r26_m27.cnf
+quad_res_r28_m29.cnf
+quad_res_r29_m32.cnf
+randomG-B-Mix-n15-d05.cnf
+randomG-B-Mix-n16-d05.cnf
+randomG-B-Mix-n18-d05.cnf
+randomG-Mix-n17-d05.cnf
+randomG-Mix-n18-d05.cnf
+randomG-n16-d05.cnf
+randomG-n17-d05.cnf
+randomG-n18-d05.cnf
+randomG-n19-d05.cnf
+randomG-n20-d05.cnf
+rphp4_065_shuffled.cnf
+rphp4_080_shuffled.cnf
+rphp4_090_shuffled.cnf
+rpoc_xits_10_UNKNOWN.cnf
+satch2ways12u.cnf
+satch2ways12wu.cnf
+satch2ways13wu.cnf
+satch2ways14u.cnf
+satch2ways15.cnf
+satch2ways15u.cnf
+satch2ways15wu.cnf
+satch2ways16.cnf
+satch2ways16w.cnf
+SC21_Timetable_C_466_E_62_Cl_31_S_30.cnf
+SC21_Timetable_C_527_E_71_Cl_35_S_35.cnf
+SC21_Timetable_C_542_E_71_Cl_36_S_35.cnf
+SC21_Timetable_C_557_E_73_Cl_37_S_35.cnf
+scc_1213_40_10_3.apx_0.cnf
+stb_531_83.apx_1.cnf
+stb_588_138.apx_1.cnf
+SE_PR_WS_500_16_70_10.apx_0.cnf
+shift1add.26949.cnf
+size_5_5_5_i003_r12.cnf
+size_5_5_5_i223_r12.cnf
+size_5_5_5_i251_r12.cnf
+snw_13_8_pre.cnf
+snw_13_8_pre-sc2016.cnf
+snw_13_9_pre.cnf
+snw_16_9_Encpre.cnf
+sokoban-p16.sas.ex.19-sc2016.cnf
+sokoban-p20.sas.cr.21.cnf
+sokoban-p20.sas.cr.27.cnf
+sokoban-p20.sas.ex.13.cnf
+sokoban-sequential-p145-microban-sequential.070-NOTKNOWN.cnf
+sp4-33-bin-stri-flat-noid.cnf
+sp4-33-one-nons-flat-noid.cnf
+sp4-33-one-stri-tree-noid.cnf
+sp4-33-una-stri-flat-noid.cnf
+sp5-21-15-bin-stri-flat-noid.cnf
+sp5-21-15-bin-stri-tree-noid.cnf
+sp5-21-15-one-nons-tree-noid.cnf
+sp5-21-15-one-stri-tree-noid.cnf
+sp5-21-15-una-nons-tree-noid.cnf
+sp5-21-15-una-stri-flat-noid.cnf
+sp5-26-19-bin-nons-tree-noid.cnf
+sp5-26-19-bin-stri-flat-noid.cnf
+sp5-26-19-una-nons-tree-noid.cnf
+spg_200_300.cnf
+spg_200_301.cnf
+spg_200_307.cnf
+spg_200_316.cnf
+spg_200_317.cnf
+spg_200_321.cnf
+spg_300_300.cnf
+spg_300_301.cnf
+spg_300_312.cnf
+spg_330_400.cnf
+spg_400_281.cnf
+spg_420_280.cnf
+spg_420_350.cnf
+stb_531_83.apx_0.cnf
+stb_792_333.apx_0.cnf
+sted1_0x0-637.cnf
+sted1_0x1e3-393.cnf
+sted12a_0x1e1-67.cnf
+sted2_0x0-343.cnf
+sted2_0x1e3-216.cnf
+sted3_0x0_n201-239.cnf
+sted4_0x0_n159-185.cnf
+sted5_0x0_n90-157.cnf
+sted5_0x1e3-120.cnf
+sted5_0x1e3-20.cnf
+sted6_0x1e3-97.cnf
+string_compare_safety_cbmc_unwinding_600.cnf
+string_compare_safety_cbmc_unwinding_630.cnf
+string_compare_safety_cbmc_unwinding_670.cnf
+string_compare_safety_cbmc_unwinding_680.cnf
+string_compare_safety_cbmc_unwinding_690.cnf
+string_compare_safety_cbmc_unwinding_700.cnf
+string_compare_safety_cbmc_unwinding_730.cnf
+string_compare_safety_cbmc_unwinding_780.cnf
+string_compare_safety_cbmc_unwinding_800.cnf
+string_compare_safety_cbmc_unwinding_870.cnf
+string_compare_safety_cbmc_unwinding_900.cnf
+string_compare_safety_cbmc_unwinding_930.cnf
+string_compare_safety_cbmc_unwinding_940.cnf
+sum_of_3_cubes_37_bits_87.cnf
+sum_of_3_cubes_42_bits_96.cnf
+sum_of_3_cubes_50_bits_91.cnf
+sum_of_3_cubes_51_bits_80.cnf
+sum_of_3_cubes_52_bits_39.cnf
+Sz1024_34824.smt2.cnf
+Sz512_15128_1.smt2.cnf
+test_v7_r12_vr1_c1_s10576.smt2.cnf
+toughsat_factoring_426s.cnf
+toughsat_factoring_895s.cnf
+UCG-20-10p1-sc2009.cnf
+UR-15-10p0.cnf
+g2-UR-20-5p1.cnf
+vlsat2_11_26.cnf
+vlsat2_11_42.cnf
+vlsat2_111_1186.cnf
+vlsat2_112_4223.cnf
+vlsat2_113_1150.cnf
+vlsat2_142_6781.cnf
+vlsat2_144_7585.cnf
+vlsat2_297_3780.cnf
+vlsat2_377_5364.cnf
+vlsat2_44_545.cnf
+vlsat2_51_824.cnf
+vlsat2_56_1042.cnf
+vlsat2_702_14170.cnf
+WS_300_24_90_10.apx_0.cnf
+WS_400_16_90_70.apx_0.cnf
+WS_500_16_70_10.apx_0.cnf
+WS_500_32_30_10.apx_0.cnf
diff --git a/testLight/nohup.out b/testLight/nohup.out
index abbf051..362edc6 100644
Binary files a/testLight/nohup.out and b/testLight/nohup.out differ
diff --git a/testLight/run10-1.sh b/testLight/run10-1.sh
new file mode 100755
index 0000000..48bc878
--- /dev/null
+++ b/testLight/run10-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-3-rp"
+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-3 $instance/$file --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
+	# 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
diff --git a/testLight/run10-2.sh b/testLight/run10-2.sh
new file mode 100755
index 0000000..521ff6c
--- /dev/null
+++ b/testLight/run10-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-3-rp"
+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-3 $instance/$file --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
+	# 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
diff --git a/testLight/run11-1.sh b/testLight/run11-1.sh
new file mode 100755
index 0000000..8040c5c
--- /dev/null
+++ b/testLight/run11-1.sh
@@ -0,0 +1,152 @@
+#!/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/v5-6-dps-20"
+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/vbs.txt`
+	do
+		file=$dir_file
+		echo $file
+		touch $res_solver_ins/$file
+		read -u 6
+		{
+			cd /home/chenzh/solvers/Light
+			time ./light-v5-6 $instance/$file --share=1 --DPS=2 --margin=20
+			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
diff --git a/testLight/run11-2.sh b/testLight/run11-2.sh
new file mode 100755
index 0000000..2e8f2cf
--- /dev/null
+++ b/testLight/run11-2.sh
@@ -0,0 +1,152 @@
+#!/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/v5-6-dps-2"
+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-v5-6 $instance/$file --share=1 --DPS=2 --margin=2
+			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
diff --git a/testLight/run12-1.sh b/testLight/run12-1.sh
new file mode 100755
index 0000000..33b7e5c
--- /dev/null
+++ b/testLight/run12-1.sh
@@ -0,0 +1,152 @@
+#!/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/v5-1-dps-8"
+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-v5-1 $instance/$file --share=1 --DPS=2 --margin=8
+			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
diff --git a/testLight/run12-2.sh b/testLight/run12-2.sh
new file mode 100755
index 0000000..6befa4f
--- /dev/null
+++ b/testLight/run12-2.sh
@@ -0,0 +1,152 @@
+#!/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/v5-dps-8"
+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-v5-0 $instance/$file --share=1 --DPS=2 --margin=8
+			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
diff --git a/testLight/run13-1.sh b/testLight/run13-1.sh
new file mode 100755
index 0000000..e9d2a09
--- /dev/null
+++ b/testLight/run13-1.sh
@@ -0,0 +1,152 @@
+#!/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/v5-2-nofree"
+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-v5-nofree $instance/$file --share=1 --DPS=2 --margin=8
+			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
diff --git a/testLight/run14-1.sh b/testLight/run14-1.sh
new file mode 100755
index 0000000..ffea4a2
--- /dev/null
+++ b/testLight/run14-1.sh
@@ -0,0 +1,152 @@
+#!/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/v5-2-dps-8"
+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-v5-2 $instance/$file --share=1 --DPS=2 --margin=8
+			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
diff --git a/testLight/run15-1.sh b/testLight/run15-1.sh
new file mode 100755
index 0000000..9f3825d
--- /dev/null
+++ b/testLight/run15-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-3-nosharing-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-3 $instance/$file --share=0
+			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
diff --git a/testLight/run15-2.sh b/testLight/run15-2.sh
new file mode 100755
index 0000000..826e458
--- /dev/null
+++ b/testLight/run15-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-3-nosharing-r"
+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/vbs.txt`
+	do
+		file=$dir_file
+		echo $file
+		touch $res_solver_ins/$file
+		read -u 6
+		{
+			cd /home/chenzh/solvers/Light
+			time ./light-v4-3 $instance/$file --share==0
+			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
diff --git a/testLight/run16-1-2.sh b/testLight/run16-1-2.sh
new file mode 100755
index 0000000..c03df9e
--- /dev/null
+++ b/testLight/run16-1-2.sh
@@ -0,0 +1,152 @@
+#!/bin/bash
+
+SEND_THREAD_NUM=2
+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-4-nps-64"
+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/unknown.txt`
+	do
+		file=$dir_file
+		echo $file
+		touch $res_solver_ins/$file
+		read -u 6
+		{
+			cd /home/chenzh/solvers/Light
+			time ./light-v4-4 $instance/$file --share=1 --threads=64
+			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<2;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
diff --git a/testLight/run16-1.sh b/testLight/run16-1.sh
new file mode 100755
index 0000000..cb85c13
--- /dev/null
+++ b/testLight/run16-1.sh
@@ -0,0 +1,152 @@
+#!/bin/bash
+
+SEND_THREAD_NUM=2
+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-4-nps-64"
+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/vbs.txt`
+	do
+		file=$dir_file
+		echo $file
+		touch $res_solver_ins/$file
+		read -u 6
+		{
+			cd /home/chenzh/solvers/Light
+			time ./light-v4-4 $instance/$file --share=1 --threads=64
+			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<2;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
diff --git a/testLight/run16-2.sh b/testLight/run16-2.sh
new file mode 100755
index 0000000..ee0eb87
--- /dev/null
+++ b/testLight/run16-2.sh
@@ -0,0 +1,152 @@
+#!/bin/bash
+
+SEND_THREAD_NUM=8
+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-4-nps-16"
+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-4 $instance/$file --share=1 --threads=16
+			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
diff --git a/testLight/run16-3.sh b/testLight/run16-3.sh
new file mode 100755
index 0000000..68f9e57
--- /dev/null
+++ b/testLight/run16-3.sh
@@ -0,0 +1,152 @@
+#!/bin/bash
+
+SEND_THREAD_NUM=16
+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-4-nps-8"
+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-4 $instance/$file --share=1 --threads=8
+			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
diff --git a/testLight/run16-4.sh b/testLight/run16-4.sh
new file mode 100755
index 0000000..4967a04
--- /dev/null
+++ b/testLight/run16-4.sh
@@ -0,0 +1,152 @@
+#!/bin/bash
+
+SEND_THREAD_NUM=32
+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-4-nps-4"
+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-4 $instance/$file --share=1 --threads=4
+			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<32;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
diff --git a/testLight/run16-5.sh b/testLight/run16-5.sh
new file mode 100755
index 0000000..3e51064
--- /dev/null
+++ b/testLight/run16-5.sh
@@ -0,0 +1,152 @@
+#!/bin/bash
+
+SEND_THREAD_NUM=64
+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-4-nps-2"
+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-4 $instance/$file --share=1 --threads=2
+			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<64;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
diff --git a/testLight/run17-1.sh b/testLight/run17-1.sh
new file mode 100755
index 0000000..e72b22d
--- /dev/null
+++ b/testLight/run17-1.sh
@@ -0,0 +1,169 @@
+#!/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/v5-7-dps-20-1k"
+res7="/pub/data/chenzh/res/light/v5-7-dps-10-1k"
+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=$res7
+	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-v5-7 $instance/$file --share=1 --DPS=2 --margin=10 --DPS_period=10000000
+			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-v5-7 $instance/$file --share=1 --DPS=2 --margin=20 --DPS_period=10000000
+	# 		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
diff --git a/testLight/run17-2.sh b/testLight/run17-2.sh
new file mode 100755
index 0000000..93b8644
--- /dev/null
+++ b/testLight/run17-2.sh
@@ -0,0 +1,169 @@
+#!/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/v5-7-dps-20-2k"
+res7="/pub/data/chenzh/res/light/v5-7-dps-10-2k"
+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=$res7
+	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-v5-7 $instance/$file --share=1 --DPS=2 --margin=10 --DPS_period=20000000
+			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-v5-7 $instance/$file --share=1 --DPS=2 --margin=20 --DPS_period=20000000
+	# 		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
diff --git a/testLight/run17-3.sh b/testLight/run17-3.sh
new file mode 100755
index 0000000..bdc136e
--- /dev/null
+++ b/testLight/run17-3.sh
@@ -0,0 +1,153 @@
+#!/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/v5-7-dps-20-4k"
+res7="/pub/data/chenzh/res/light/v5-7-dps-6-1k"
+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=$res7
+	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-v5-7 $instance/$file --share=1 --DPS=2 --margin=6 --DPS_period=10000000
+			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
diff --git a/testLight/run17-4.sh b/testLight/run17-4.sh
new file mode 100755
index 0000000..1b2ed53
--- /dev/null
+++ b/testLight/run17-4.sh
@@ -0,0 +1,153 @@
+#!/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/v5-7-dps-20-4k"
+res7="/pub/data/chenzh/res/light/v5-7-dps-6-2k"
+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=$res7
+	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-v5-7 $instance/$file --share=1 --DPS=2 --margin=6 --DPS_period=20000000
+			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
diff --git a/testLight/run4-1.sh b/testLight/run4-1.sh
index a7ae40e..8540703 100755
--- a/testLight/run4-1.sh
+++ b/testLight/run4-1.sh
@@ -21,7 +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"
+res6="/pub/data/chenzh/res/light/v4-3-nps-rp"
 res_no="/pub/data/chenzh/res/unused"
 #####################################################
 
@@ -42,7 +42,7 @@ do
 		read -u 6
 		{
 			cd /home/chenzh/solvers/Light
-			time ./light-v4-2 $instance/$file --share=1 --pakis=1
+			time ./light-v4-3 $instance/$file --share=1 --pakis=1
 			echo >&6
 		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
 	done
diff --git a/testLight/run4-2.sh b/testLight/run4-2.sh
index 4a35f3d..8258e37 100755
--- a/testLight/run4-2.sh
+++ b/testLight/run4-2.sh
@@ -21,11 +21,11 @@ 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"
+res6="/pub/data/chenzh/res/light/v4-3-nps-rp"
 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]}
@@ -34,7 +34,7 @@ do
 	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,7 +42,7 @@ do
 		read -u 6
 		{
 			cd /home/chenzh/solvers/Light
-			time ./light-v4-2 $instance/$file --share=1 --pakis=1
+			time ./light-v4-3 $instance/$file --share=1 --pakis=1
 			echo >&6
 		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
 	done
diff --git a/testLight/run5-1.sh b/testLight/run5-1.sh
index f64b490..cc09e23 100755
--- a/testLight/run5-1.sh
+++ b/testLight/run5-1.sh
@@ -22,7 +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"
+res7="/pub/data/chenzh/res/light/v4-3-nps-p"
 res_no="/pub/data/chenzh/res/unused"
 #####################################################
 
@@ -43,7 +43,7 @@ do
 		read -u 6
 		{
 			cd /home/chenzh/solvers/Light
-			time ./light-v4-2 $instance/$file --share=1 --shuffle=0 --pakis=1
+			time ./light-v4-3 $instance/$file --share=1 --shuffle=0 --pakis=1
 			echo >&6
 		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
 	done
diff --git a/testLight/run5-2.sh b/testLight/run5-2.sh
index 6c18088..35bb5dc 100755
--- a/testLight/run5-2.sh
+++ b/testLight/run5-2.sh
@@ -22,7 +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"
+res7="/pub/data/chenzh/res/light/v4-3-nps-p"
 res_no="/pub/data/chenzh/res/unused"
 #####################################################
 
@@ -43,7 +43,7 @@ do
 		read -u 6
 		{
 			cd /home/chenzh/solvers/Light
-			time ./light-v4-2 $instance/$file --share=1 --shuffle=0 --pakis=1
+			time ./light-v4-3 $instance/$file --share=1 --shuffle=0 --pakis=1
 			echo >&6
 		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
 	done
diff --git a/testLight/run8-1.sh b/testLight/run8-1.sh
index 10d5229..05fee6c 100755
--- a/testLight/run8-1.sh
+++ b/testLight/run8-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-1-nps2"
+res6="/pub/data/chenzh/res/light/v4-3-nps-tc3"
 res_no="/pub/data/chenzh/res/unused"
 #####################################################
 
-all_datas=($instance_21 $instance_20)
+all_datas=($instance_21)
 for((i=0;i<${#all_datas[*]};i++))
 do
 	instance=${all_datas[$i]}
@@ -43,7 +43,7 @@ do
 		read -u 6
 		{
 			cd /home/chenzh/solvers/Light
-			time ./light-v4-2 $instance/$file --share=1
+			time ./light-v4-3 $instance/$file --share=1
 			echo >&6
 		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
 	done
diff --git a/testLight/run8-2.sh b/testLight/run8-2.sh
index 8dccbd5..75e14c7 100755
--- a/testLight/run8-2.sh
+++ b/testLight/run8-2.sh
@@ -21,7 +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-1-nps2"
+res6="/pub/data/chenzh/res/light/v4-3-nps-tc3"
 res_no="/pub/data/chenzh/res/unused"
 #####################################################
 
@@ -43,7 +43,7 @@ do
 		read -u 6
 		{
 			cd /home/chenzh/solvers/Light
-			time ./light-v4-2 $instance/$file --share=1
+			time ./light-v4-3 $instance/$file --share=1
 			echo >&6
 		} >$res_solver_ins/$file  2>>$res_solver_ins/$file &
 	done
diff --git a/testLight/run9-1.sh b/testLight/run9-1.sh
new file mode 100755
index 0000000..1ce5301
--- /dev/null
+++ b/testLight/run9-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-3-nopre-sharing-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-3 $instance/$file --share=1 --simplify=0
+			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
diff --git a/testLight/run9-2.sh b/testLight/run9-2.sh
new file mode 100755
index 0000000..8f6d08b
--- /dev/null
+++ b/testLight/run9-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-3-nopre-sharing-r"
+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/vbs.txt`
+	do
+		file=$dir_file
+		echo $file
+		touch $res_solver_ins/$file
+		read -u 6
+		{
+			cd /home/chenzh/solvers/Light
+			time ./light-v4-3 $instance/$file --share=1 --simplify=0
+			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
diff --git a/testLight/test.log b/testLight/test.log
new file mode 100644
index 0000000..b88a77a
--- /dev/null
+++ b/testLight/test.log
@@ -0,0 +1,92 @@
+nohup: ignoring input
+10pipe_k.cnf
+13pipe_k.cnf
+14pipe_q0_k.cnf
+20-100-frag12-0_sat.cnf
+20-100-frag12-14_sat.cnf
+20-100-frag12-32_sat.cnf
+20-100-frag12-53_sat.cnf
+20-100-lambda100-14_sat.cnf
+20-100-lambda100-14_unsat.cnf
+20-100-lambda100-47_unsat.cnf
+20-100-lambda100-49_sat.cnf
+20-100-lambda100-65_sat.cnf
+20-100-lambda100-89_sat.cnf
+20-100-lambda100-89_unsat.cnf
+20-100-p100-55_sat.cnf
+20-100-p100-55_unsat.cnf
+2bitcomp_5.hg_20.cnf
+51.smt2.cnf
+73.smt2.cnf
+9dlx_vliw_at_b_iq5.cnf
+9dlx_vliw_at_b_iq8.cnf
+ACG-15-10p1.cnf
+ak016modbtsimpbisc.cnf
+ak032modbtmodbtisc.cnf
+ak128paralparalisc.cnf
+assoc_mult_err_3.c.cnf
+at-least-two-aaai10-planning-ipc5-pathways-17-step20.cnf
+at-least-two-aaai10-planning-ipc5-pipesworld-12-step15.cnf
+at-least-two-hwmcc10-timeframe-expansion-k50-pdtviseisenberg2-tseitin.cnf
+at-least-two-ibm-2004-23-k100.cnf
+at-least-two-maris-s03-gripper11.cnf
+at-least-two-smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf
+at-least-two-sokoban-sequential-p145-microban-sequential.030-NOTKNOWN.cnf
+at-least-two-traffic_b_unsat.cnf
+at-least-two-traffic_f_unknown.cnf
+at-least-two-traffic_kkb_unknown.cnf
+at-least-two-traffic_pcb_unknown.cnf
+vmpc_26.cnf
+at-least-two-vmpc_28.cnf
+b04_s_unknown_pre.cnf
+b2005-p3-12x12c10h7-Ser7-0.cnf
+barman-pfile10-039.sas.ex.15.cnf
+barman-pfile10-040.sas.ex.15.cnf
+battleship-12-12-unsat.cnf
+battleship-14-26-sat.cnf
+blocks-blocks-36-0.180-SAT.cnf
+blocks-blocks-37-1.120-NOTKNOWN.cnf
+blocks-blocks-37-1.130-NOTKNOWN.cnf
+bvsdiv_19.smt2.cnf
+bvsmod_18.smt2.cnf
+bvsmod_19.smt2.cnf
+bvsub_08985.smt2.cnf
+bvsub_12973.smt2.cnf
+bvsub_19952.smt2.cnf
+bv-term-small-rw_1492.smt2.cnf
+bvurem_20.smt2.cnf
+Circuit_multiplier18.cnf
+Circuit_multiplier22.cnf
+Circuit_multiplier24.cnf
+Circuit_multiplier25.cnf
+Circuit_multiplier26.cnf
+Circuit_multiplier29.cnf
+Circuit_multiplier33.cnf
+Circuit_multiplier34.cnf
+Circuit_multiplier35.cnf
+Circuit_multiplier36.cnf
+Circuit_multiplier37.cnf
+Circuit_multiplier45.cnf
+Circuit_multiplier53.cnf
+crafted_n10_d6_c4_num15.cnf
+crafted_n10_d6_c4_num21.cnf
+crafted_n11_d6_c4_num14.cnf
+crafted_n12_d6_c3_num18.cnf
+crafted_n12_d6_c3_num28.cnf
+crafted_n12_d6_c4_num17.cnf
+ctl_4201_555_unsat.cnf
+ctl_4291_567_1_unsat.cnf
+ctl_4291_567_11_unsat.cnf
+ctl_4291_567_6_unsat_pre.cnf
+ctl_4291_567_9_unsat.cnf
+dist10.c.cnf
+dist4.c.cnf
+E00X23.cnf
+E02F17.cnf
+ecarev-110-1031-23-40-8.cnf
+ecarev-110-4099-22-30-4.cnf
+edit_distance007_85.cnf
+edit_distance019_312.cnf
+edit_distance023_281.cnf
+edit_distance023_282.cnf
+edit_distance023_283.cnf
diff --git a/utils/paras.hpp b/utils/paras.hpp
index a7604fd..ecfc33d 100644
--- a/utils/paras.hpp
+++ b/utils/paras.hpp
@@ -6,9 +6,9 @@
 
 //        name,      type,   default, low, high, comments
 #define PARAS \
-    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( DPS        , int    , 0     , 0  , 2   , "DPS/NPS") \
+    PARA( DPS_period , int    , 10000 , 1  , 1e8 , "DPS sharing period") \
+    PARA( margin     , int    , 0     , 0  , 1e3 , "DPS margin") \
     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)") \
@@ -17,8 +17,8 @@
     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") \
+    PARA( times      , double , 5000  , 0  , 1e8 , "Cutoff time") \
     
 
 struct paras 
diff --git a/workers/basekissat.cpp b/workers/basekissat.cpp
index 0b99d81..c3fc0cd 100644
--- a/workers/basekissat.cpp
+++ b/workers/basekissat.cpp
@@ -64,6 +64,7 @@ bool basekissat::imp_clause(clause_store *cls, void *cl) {
     for (int i = 0; i < cls->size; i++) {
         // S->outimport << cls->data[i] << std::endl;
         int eidx = abs(cls->data[i]);
+        if (eidx >= SIZE_STACK(solver->import)) printf("c wrong %d\n", eidx);
         import *import = &PEEK_STACK (solver->import, eidx);
         if (import->eliminated) return false;
         else {
@@ -81,42 +82,117 @@ int call_back_in(void *solver, int *lbd, cvec *c) {
     if (S->import_clause.pop(cls) == false) return -1;
     *lbd = cls->lbd;
     bool res = S->imp_clause(cls, c); 
-    cls->free_clause();
+    if (S->solver->share_dps != 2) {
+        cls->free_clause();
+    }
     if (!res) return -10;
     return 1;
 } 
 
-void kissat_wait_sharing(void *solver) {
+int kissat_wait_sharing(void *solver) {
     auto clk_st = std::chrono::high_resolution_clock::now();
     basekissat* S = (basekissat *) solver;
-    // printf("c %d into Light wait\n", S->id);
-    S->x1 = S->x2 = 0;
-    sharer *s = S->in_sharer;
-    {
-        boost::mutex::scoped_lock lock(s->mtx);
-        if (s->terminated) return;
-        s->waitings += 1;
-        lock.unlock();
-        // 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);
+    sharer *share = S->in_sharer;
+    int should_free = 1;
+    if (S->solver->share_dps == 1) {
+        // printf("c %d into Light wait\n", S->id);
+        S->x1 = S->x2 = 0;
+        {
+            boost::mutex::scoped_lock lock(share->mtx);
+            if (share->terminated) return true;
+            share->waitings += 1;
+            lock.unlock();
+            // printf("c %d start wait with number %d\n", S->id, s->waitings);
+        }
+        if (share->should_sharing()) share->cond.notify_one(); 
+        boost::mutex::scoped_lock lock(share->mtx);
+        while (share->waitings > 0) {
+            share->cond.wait(lock);
+        }
     }
+    else if (S->solver->share_dps == 2) { //share_dps = 2
+        if (S->period >= S->controller->get_winner_period()) {
+            S->set_winner_period();
+            return -1;
+        }
+        // printf("c thread %d into select %d\n", S->id, S->period);
+        S->select_clauses();
+        // printf("c %d now finish period %d\n", S->id, S->get_period());
+        S->inc_period();
+        // printf("c thread %d start import at %d\n", S->id, S->period);
+        should_free = share->import_clauses(S->id);
+        // printf("c thread %d finish import at %d\n", S->id, S->period);
+    }   
     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;
+    return should_free;
     // 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;
+void call_back_free(void *solver) {
+    basekissat* S = (basekissat *) solver;
+    sharer *share = S->in_sharer;
+    int current_period = S->get_period() - 1, import_period = current_period - share->margin;
+    if (import_period < 0) return;
+    for (int i = 0; i < share->producers.size(); i++) {
+        if (i == S->id) continue;
+        basesolver *s = share->producers[i];
+        period_clauses *pc = s->pq.find(import_period);
+        if (pc->period != import_period)
+            puts("*******************************************************");
+        if (pc->free_clause()) {
+            s->pq.pop(import_period);
+            // printf("thread %d enter, %d is free\n", S->id, i);
+        }
+    }
+    // printf("end finish\n");
 }
 
+void basekissat::select_clauses() {
+    sharer *share = in_sharer;
+    cls.clear();
+    export_clauses_to(cls);
+
+    for (int i = 0; i < cls.size(); i++) {
+        int sz = cls[i]->size;
+        while (sz > bucket.size()) bucket.push();
+        if (sz * (bucket[sz - 1].size() + 1) <= share->share_lits) 
+            bucket[sz - 1].push(cls[i]);
+    }
+    period_clauses *pcls = new period_clauses(period);
+    int space = share->share_lits;
+    for (int i = 0; i < bucket.size(); i++) {
+        int clause_num = space / (i + 1);
+        if (!clause_num) break;
+        if (clause_num >= bucket[i].size()) {
+            space -= bucket[i].size() * (i + 1);
+            for (int j = 0; j < bucket[i].size(); j++)
+                pcls->push(bucket[i][j]);
+            bucket[i].clear();
+        }
+        else {
+            space -= clause_num * (i + 1);
+            for (int j = 0; j < clause_num; j++) {
+                pcls->push(bucket[i].last());
+                bucket[i].pop();
+            }
+        }
+    }
+    int percent = (share->share_lits - space) * 100 / share->share_lits;
+    if (percent < 75) broaden_export_limit();
+    if (percent > 98) restrict_export_limit();
+    //sort finish
+    pcls->increase_refs(share->producers.size() - 1);
+    pq.push(pcls);
+}
+
+
 basekissat::basekissat(int id, light* light) : basesolver(id, light) {
     good_clause_lbd = 2;
+    period = 0;
+    margin = 0;
     // outexport.open("export.txt");
     // outimport.open("import.txt");
     // outfree.open("free.txt");
@@ -129,6 +205,7 @@ basekissat::basekissat(int id, light* light) : basesolver(id, light) {
         solver -> cbkImportClause = call_back_in;
         solver -> cbkExportClause = call_back_out;
         solver -> cbkWaitSharing  = kissat_wait_sharing;
+        solver -> cbkFreeClause   = call_back_free;
         solver -> share_dps       = light->opt->DPS;
         solver -> share_dps_period= light->opt->DPS_period;
     }
@@ -180,10 +257,12 @@ void basekissat::import_clauses_from(vec<clause_store *> &clauses) {
 }
 
 void basekissat::get_model(vec<int> &model) {
+    printf("111\n");
     model.clear();
     for (int i = 1; i <= solver->max_var; i++) {
         model.push(val(i));
    }
+    printf("222\n");
 }
 
 void basekissat::broaden_export_limit() {
@@ -195,14 +274,10 @@ void basekissat::restrict_export_limit() {
         --good_clause_lbd;
 }
 
-
 int basekissat::get_conflicts() {
     return solver->nconflict;
 }
-// int basekissat::get_reset_data() {
-//     return solver->best_assigned;
-// }
 
-// void basekissat::reset() {
-//     solver->reseting = 1;
-// }
+double basekissat::get_waiting_time() {
+    return waiting_time;
+}
diff --git a/workers/basekissat.hpp b/workers/basekissat.hpp
index b7bfb13..e0c759b 100644
--- a/workers/basekissat.hpp
+++ b/workers/basekissat.hpp
@@ -1,4 +1,5 @@
 #include "basesolver.hpp"
+#include <deque>
 
 struct kissat;
 struct cvec;
@@ -10,8 +11,7 @@ public:
     int  solve();
     int  val(int l);
     void configure(const char* name, int id);
-    // int  get_reset_data();
-    // void reset();
+
     int  get_conflicts();
     void parse_from_CNF(char* filename);
     void parse_from_PAR(preprocess *pre);
@@ -31,9 +31,38 @@ public:
     kissat* solver;
     int good_clause_lbd = 0;
     
+    void select_clauses();
+    int get_period() {
+        boost::mutex::scoped_lock lock(mtx);
+        return period;
+    };
+    void inc_period() {
+        boost::mutex::scoped_lock lock(mtx);
+        period++;
+        if (period % 100 == 0) printf("c %d reach period %d\n", id, period);
+        cond.notify_all();
+    };
+
+    void set_winner_period() {
+        boost::mutex::scoped_lock lock(mtx);
+        winner_period = period;
+        cond.notify_all();
+    }
+
+    void dps_terminate() {
+        {
+            boost::mutex::scoped_lock lock(mtx);
+            terminated = 1;
+            cond.notify_all();
+            // printf("c thread %d terminated\n", id);
+        }
+        terminate();
+    }
+
     friend int cbkImportClause(void *, int *, cvec *);
     friend int cbkExportClause(void *, int *, cvec *);
-    friend void cbkWaitSharing(void *);
+    friend int cbkWaitSharing(void *);
+    friend void cbkFreeClause(void *);
     std::ofstream outimport;
     std::ofstream outexport;
     std::ofstream outfree;
diff --git a/workers/basesolver.hpp b/workers/basesolver.hpp
index 9b3f287..1e6c13a 100644
--- a/workers/basesolver.hpp
+++ b/workers/basesolver.hpp
@@ -6,6 +6,7 @@
 #include "clause.hpp"
 #include <fstream>
 #include <iostream>
+#include <boost/thread.hpp>
 #include <boost/thread/thread.hpp>
 #include <boost/lockfree/spsc_queue.hpp>
 class sharer;
@@ -18,6 +19,7 @@ public:
     virtual void configure(const char* name, int id) = 0;
     virtual int  get_conflicts() = 0;
 
+    virtual void dps_terminate() = 0;
     virtual void parse_from_CNF(char* filename) = 0;
     virtual void parse_from_PAR(preprocess* pre) = 0;
     virtual void get_model(vec<int> &model) = 0;
@@ -28,9 +30,22 @@ public:
     virtual void broaden_export_limit() = 0;
     virtual void restrict_export_limit() = 0;
     virtual double get_waiting_time() = 0;
+    virtual void select_clauses() = 0;
+    virtual int  get_period() = 0;
+    virtual void inc_period() = 0;
+    virtual void set_winner_period() = 0;
     light * controller;
     int id;
     sharer* in_sharer;
+    vec<int> model;
+
+    int winner_period = 1e9;
+    int period, margin, terminated = 0;
+    mutable boost::mutex mtx;
+    boost::condition_variable cond;
+    period_queue pq;
+    vec<clause_store *> cls;
+    vec<vec<clause_store *>> bucket;
 
     boost::lockfree::spsc_queue<clause_store*, boost::lockfree::capacity<1024000>> import_clause;
     boost::lockfree::spsc_queue<clause_store*, boost::lockfree::capacity<1024000>> export_clause;
diff --git a/workers/clause.hpp b/workers/clause.hpp
index 7624509..010accd 100644
--- a/workers/clause.hpp
+++ b/workers/clause.hpp
@@ -1,5 +1,7 @@
 #ifndef _clause_hpp_INCLUDED
 #define _clause_hpp_INCLUDED
+#include <boost/thread.hpp>
+#include <boost/thread/thread.hpp>
 
 struct clause_store {
     int size, lbd;
@@ -30,4 +32,56 @@ struct clause_store {
     }
 };
 
+
+struct period_clauses {
+    int period;
+    std::atomic<int> refs;
+    vec<clause_store *> cls;
+    period_clauses(int p = 0) {
+        refs = 0;
+        period = p;
+    }
+
+    void increase_refs(int inc) {
+        refs += inc;
+    }
+
+    bool free_clause() {
+        int ref = refs.fetch_sub(1);
+        if (ref <= 1) {
+            if (ref <= 0) puts("**************************========================");
+            return true;
+        }
+        return false;
+    }
+    void release_clause() {
+        for (int i = 0; i < cls.size(); i++)
+            cls[i]->free_clause();
+    }
+    void push(clause_store * c) {
+        cls.push(c);
+    }
+};
+
+struct period_queue {
+    std::deque<period_clauses *> q;
+    mutable boost::mutex mtx;
+    void push(period_clauses * c) {
+        boost::mutex::scoped_lock lock(mtx);
+        q.push_back(c);
+    }
+    void pop(int assert_period = -1) {
+        boost::mutex::scoped_lock lock(mtx);
+        if (assert_period != -1 && q.front()->period != assert_period) printf("c ............false free pos\n");
+        q.front()->release_clause();
+        q.pop_front();
+    }
+    period_clauses* find(int period) {
+        boost::mutex::scoped_lock lock(mtx);
+        int sp = q.front()->period;
+        if (period - sp >= q.size()) puts("may occur wrong");
+        return q[period - sp];
+    }
+};
+
 #endif
\ No newline at end of file
diff --git a/workers/sharer.cpp b/workers/sharer.cpp
index 0581889..e0faf01 100644
--- a/workers/sharer.cpp
+++ b/workers/sharer.cpp
@@ -68,6 +68,40 @@ void * share_worker(void *arg) {
     return NULL;
 }
  
+// void sharer::select_clauses(int id) {
+    
+// }
+
+bool sharer::import_clauses(int id) {
+    int current_period = producers[id]->get_period() - 1, import_period = current_period - margin;
+    if (import_period < 0) return false;
+    basesolver *t = producers[id];
+    for (int i = 0; i < producers.size(); i++) {
+        if (i == id) continue;
+        basesolver *s = producers[i];
+        //wait for s reach period $import_period
+        // printf("c %d start waiting, since import_p is %d, current_p is %d\n", id, import_period, s->get_period());
+        // if (id == 3 && current_period == 84) printf("\tc thread 3 wait for %d\n", i);
+        boost::mutex::scoped_lock lock(s->mtx);
+        while (s->period <= import_period && s->winner_period > import_period && !s->terminated) {
+            s->cond.wait(lock);
+        }
+        // if (id == 3 && current_period == 84) printf("\tc thread 3 finish wait for %d\n", i);
+        
+        if (s->terminated || s->winner_period <= import_period) return false; 
+        // if (s->terminated) return; 
+
+        period_clauses *pc = s->pq.find(import_period);
+        if (pc->period != import_period) {
+            printf("thread %d, now period = %d, import period = %d, import thread %d\n", id, current_period, import_period, i);
+            puts("*******************************************************");
+        }
+        // printf("c %d finish waiting %d %d\n", id, import_period, s->period_queue[pos]->period);
+        t->import_clauses_from(pc->cls);
+    }
+    return true;
+    // printf("c thread %d, period %d, import finish\n", id, current_period);
+}
 
 int sharer::sort_clauses(int x) {
     for (int i = 0; i < cls.size(); i++) {
@@ -110,23 +144,30 @@ int sharer::sort_clauses(int x) {
 
 void light::share() {
     printf("c sharing start\n");
-    int sharers_number = 1;
-    for (int i = 0; i < sharers_number; i++) {
-        sharer* s = new sharer(i, OPT(share_intv), OPT(share_lits), OPT(DPS));
+    if (OPT(DPS) == 2) {
+        sharer* s = new sharer(0, OPT(share_intv), OPT(share_lits), OPT(DPS));
+        s->margin = OPT(margin);
         for (int j = 0; j < OPT(threads); j++) {
             s->producers.push(workers[j]);
-            s->consumers.push(workers[j]);
             workers[j]->in_sharer = s;
         }
         sharers.push(s);
     }
-    
-    pthread_t *ptr = new pthread_t[sharers_number];
-    for (int i = 0; i < sharers_number; i++) {
-        pthread_create(&ptr[i], NULL, share_worker, sharers[i]);
-    }
-    
-    // for (int i = 0; i < sharers_number; i++) {
-    //     pthread_join(ptr[i], NULL);
-    // }   
+    else {
+        int sharers_number = 1;
+        for (int i = 0; i < sharers_number; i++) {
+            sharer* s = new sharer(i, OPT(share_intv), OPT(share_lits), OPT(DPS));
+            for (int j = 0; j < OPT(threads); j++) {
+                s->producers.push(workers[j]);
+                s->consumers.push(workers[j]);
+                workers[j]->in_sharer = s;
+            }
+            sharers.push(s);
+        }
+        
+        pthread_t *ptr = new pthread_t[sharers_number];
+        for (int i = 0; i < sharers_number; i++) {
+            pthread_create(&ptr[i], NULL, share_worker, sharers[i]);
+        }
+    }   
 }
\ No newline at end of file
diff --git a/workers/sharer.hpp b/workers/sharer.hpp
index ebc7b50..6432551 100644
--- a/workers/sharer.hpp
+++ b/workers/sharer.hpp
@@ -8,11 +8,12 @@ class sharer {
 public:
     int id;
     int share_intv, share_lits, dps;
+    int margin;
     mutable boost::mutex mtx;
     boost::condition_variable cond;
     int terminated;
     int waitings;
-    vec<vec<clause_store *>> bucket[32]; //need to update
+    vec<vec<clause_store *>> bucket[64]; //need to update
     
     vec<basesolver *> producers, consumers;
     vec<clause_store *> cls;
@@ -45,6 +46,8 @@ public:
         cond.notify_all();
     }
     int sort_clauses(int x);
+    // void select_clauses(int id);
+    bool import_clauses(int id);
 };
 
 #endif
\ No newline at end of file