diff --git a/build.sh b/build.sh
new file mode 100755
index 0000000..3655bfc
--- /dev/null
+++ b/build.sh
@@ -0,0 +1,5 @@
+cd /home/chenzh/solvers/Light/solvers/kissat-inc;
+./configure && make;
+cd ..;
+cd ..;
+make clean; make;
\ No newline at end of file
diff --git a/light b/light
index 0247fd2..289f437 100755
Binary files a/light and b/light differ
diff --git a/light-v1 b/light-v1
new file mode 100755
index 0000000..0247fd2
Binary files /dev/null and b/light-v1 differ
diff --git a/light.cpp b/light.cpp
index 1a41b99..5179ce9 100644
--- a/light.cpp
+++ b/light.cpp
@@ -16,8 +16,8 @@ light::light():
 }
 
 light::~light() {
-    for (int i = 0; i < solvers.size(); i++) delete(solvers[i]);
-    solvers.clear(true);
+    for (int i = 0; i < workers.size(); i++) delete(workers[i]);
+    workers.clear(true);
 }
 
 void light::arg_parse(int argc, char **argv) {
diff --git a/light.hpp b/light.hpp
index b40d9ca..7448fca 100644
--- a/light.hpp
+++ b/light.hpp
@@ -10,6 +10,14 @@ typedef long long ll;
 
 class basesolver;
 
+struct thread_inf{
+    int id, inf;
+    bool operator < ( const thread_inf &other ) const
+	{
+		return inf > other.inf;
+	}
+};
+
 struct light
 {
 public:
@@ -19,7 +27,7 @@ public:
     char *filename;
     paras *opt;
     preprocess *pre;
-    vec<basesolver *> solvers;
+    vec<basesolver *> workers;
 
     int finalResult;
     int winner;
@@ -27,12 +35,12 @@ public:
     atomic<bool> globalEnding;
 
     void arg_parse(int argc, char **argv);
-    void init_solvers();
-    void diversity_solvers();
+    void init_workers();
+    void diversity_workers();
     void parse_input();
     int  run();
     int  solve();
-    void terminate_solvers();
+    void terminate_workers();
     void print_model();
 };
 
diff --git a/light.o b/light.o
index cc59b95..8d8ebb0 100644
Binary files a/light.o and b/light.o differ
diff --git a/preprocess.cpp b/preprocess.cpp
index 1c85ee3..d5bdf53 100644
--- a/preprocess.cpp
+++ b/preprocess.cpp
@@ -246,7 +246,7 @@ bool preprocess::preprocess_binary() {
         for (int j = 0; j < l; j++)
             clause[i][j] = tolit(clause[i][j]);
     }
-    nlit = vars << 1;
+    nlit = (vars << 1) + 2;
     for (int i = 1; i <= vars; i++) f[i] = i, val[i] = 1, color[i] = 0;
     for (int i = 1; i <= clauses; i++) clause_delete[i] = 0;
     int len = 0;
@@ -284,6 +284,8 @@ bool preprocess::preprocess_binary() {
         }
     }
     
+    for (int i = 1; i <= vars; i++) find(i);
+
     for (int i = 1; i <= clauses; i++) {
         if (clause_delete[i]) continue;
         int l = clause[i].size(), oril = l;
@@ -296,15 +298,17 @@ bool preprocess::preprocess_binary() {
             if (resseen[a[j]] == i) continue;
             resseen[a[j]] = i, a[t++] = a[j];
         }
-        if (t != l) l = t;
+        if (t != l) {l = t;}
         for (int j = 0; j < l; j++)
-            if (resseen[negative(a[j])] == i)
+            if (resseen[negative(a[j])] == i) {
                 clause_delete[i] = 1;
+            }
         for (int j = 0; j < l; j++) resseen[a[j]] = 0;
         clause[i].clear();
         for (int j = 0; j < l; j++)
             clause[i].push(a[j]);
     }
+    
 
     for (int i = 1; i <= clauses; i++) {
         if (clause_delete[i]) continue;
@@ -313,6 +317,7 @@ bool preprocess::preprocess_binary() {
             clause[i][j] = toeidx(clause[i][j]);
         }
     }
+
     update_var_clause_label();
     for (int i = 1; i <= orivars; i++) {
         if (mapval[i]) continue;
@@ -420,7 +425,6 @@ bool preprocess::preprocess_easy_clause() {
         }
     }
     update_var_clause_label();
-
     for (int i = 1; i <= tail; i++) {
         int v = q[i];
         mapval[v] = varval[v];
diff --git a/preprocess.o b/preprocess.o
index aff7fa4..b37f4ac 100644
Binary files a/preprocess.o and b/preprocess.o differ
diff --git a/solve.cpp b/solve.cpp
index 727b80c..65e84e9 100644
--- a/solve.cpp
+++ b/solve.cpp
@@ -2,6 +2,7 @@
 #include "workers/basekissat.hpp"
 #include <unistd.h>
 #include <chrono>
+#include <algorithm>
 char* worker_sign = "";
 atomic<int> terminated;
 auto clk_st = std::chrono::high_resolution_clock::now();
@@ -27,7 +28,7 @@ void * solve_worker(void *arg) {
             sq->get_model(seq_model);
         }
         if (res && !terminated) {
-            sq->controller->terminate_solvers();
+            sq->controller->terminate_workers();
             terminated = 1;
             result = res;
             winner = sq->id;
@@ -38,29 +39,29 @@ void * solve_worker(void *arg) {
    return NULL;
 }
 
-void light::init_solvers() {
+void light::init_workers() {
     for (int i = 0; i < OPT(threads); i++) {
         basekissat* kissat = new basekissat(i, this);
-        solvers.push(kissat);
+        workers.push(kissat);
     }
 }
 
-void light::diversity_solvers() {
+void light::diversity_workers() {
     for (int i = 0; i < OPT(threads); i++) {
-        solvers[i]->diversity(i);
+        workers[i]->diversity(i);
     }
 }
 
-void light::terminate_solvers() {
+void light::terminate_workers() {
     for (int i = 0; i < OPT(threads); i++) {
-        solvers[i]->terminate();
+        workers[i]->terminate();
     }
 }
 
 void light::parse_input() {
     pthread_t *ptr = new pthread_t[OPT(threads)];
     for (int i = 0; i < OPT(threads); i++) {
-      pthread_create(&ptr[i], NULL, read_worker, solvers[i]);
+      pthread_create(&ptr[i], NULL, read_worker, workers[i]);
    }   
    for (int i = 0; i < OPT(threads); i++) {
       pthread_join(ptr[i], NULL);
@@ -73,27 +74,48 @@ int light::solve() {
     terminated = 0;
     pthread_t *ptr = new pthread_t[OPT(threads)];
     for (int i = 0; i < OPT(threads); i++) {
-      pthread_create(&ptr[i], NULL, solve_worker, solvers[i]);
-   }
+      pthread_create(&ptr[i], NULL, solve_worker, workers[i]);
+    }
+
+    thread_inf unimprove[OPT(threads)];
+    auto clk_sol_st = std::chrono::high_resolution_clock::now();
+    int pre_time = std::chrono::duration_cast<std::chrono::seconds>(clk_sol_st - clk_st).count();
+    int sol_thd = 0, intv_time = OPT(reset_time);
     while (!terminated) {
         usleep(100000);        
         auto clk_now = std::chrono::high_resolution_clock::now();
         int solve_time = std::chrono::duration_cast<std::chrono::seconds>(clk_now - clk_st).count();
         if (solve_time >= OPT(times)) {
             terminated = 1;
-            terminate_solvers();
+            terminate_workers();
+        }
+        if (OPT(reset) && solve_time >= pre_time + intv_time) {
+            pre_time = solve_time;
+            intv_time += OPT(reset_time);
+            sol_thd = 0;
+            for (int i = 0; i < OPT(threads); i++) {
+                unimprove[sol_thd++] = (thread_inf) {i, workers[i]->get_reset_data()};
+            }
+            std::sort(unimprove, unimprove + sol_thd);
+            printf("Reset thread (%d): ", solve_time);
+            for (int i = 0; i < sol_thd / 2; i++) {
+                workers[i]->reset();
+                printf("%d(%d) ", unimprove[i].id, unimprove[i].inf);
+            }
+            puts("\n");
         }
     }
+
     for (int i = 0; i < OPT(threads); i++) {
         pthread_join(ptr[i], NULL);
     }    
-   delete []ptr;
-   return result;
+    delete []ptr;
+    return result;
 }
 
 int light::run() {
-    init_solvers();
-    diversity_solvers();
+    init_workers();
+    diversity_workers();
     if (OPT(simplify)) {
         pre = new preprocess();
         int res = pre->do_preprocess(filename);
diff --git a/solve.o b/solve.o
index 3a9cf06..4e470a7 100644
Binary files a/solve.o and b/solve.o differ
diff --git a/solvers/kissat-inc/build/analyze.o b/solvers/kissat-inc/build/analyze.o
index f978eb6..14243fc 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/assign.o b/solvers/kissat-inc/build/assign.o
index f033b03..38c7f19 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 cae3412..59798c7 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/backtrack.o b/solvers/kissat-inc/build/backtrack.o
index 331ce73..496140f 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 5ee0fee..7024dc7 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 fb20088..c2c8a8e 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 "Thu Aug 25 15:41:16 CST 2022 Linux seed1 5.4.0-120-generic x86_64"
-#define DIR "/home/chenzh/solvers/Light/kissat-inc/build"
+#define BUILD "Wed Aug 31 12:28:43 CST 2022 Linux seed1 5.4.0-120-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 9928ed7..7ba6f65 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 89bba9f..73ba9ad 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 ccc2300..a8826c6 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/collect.o b/solvers/kissat-inc/build/collect.o
index 3773666..e6dbae4 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 ce265a8..0c636de 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 fa2f05f..e3be995 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/dense.o b/solvers/kissat-inc/build/dense.o
index a3d73b8..26214a6 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/eliminate.o b/solvers/kissat-inc/build/eliminate.o
index af67cd1..b1c09af 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/extend.o b/solvers/kissat-inc/build/extend.o
index 3473491..e72d712 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 c99e07c..15da60e 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 2244f7b..8352767 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 2787f11..81096bf 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/import.o b/solvers/kissat-inc/build/import.o
index 55682e5..f6b3fa8 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 d7f36cc..6f1ed22 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 bc004cc..7c46888 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 53cf0f8..b1be301 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 11ca41d..b41b840 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 cdbaba1..c7a66f5 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/mode.o b/solvers/kissat-inc/build/mode.o
index b671eaf..01d75a7 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/phases.o b/solvers/kissat-inc/build/phases.o
index 41e8a5d..9161d8d 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 f7f0464..82c65b3 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 a994c51..36385d4 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 f839f97..103e5f6 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/propdense.o b/solvers/kissat-inc/build/propdense.o
index 206f903..be95827 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 0e025cd..f6a1b32 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 4e9e0ff..1825789 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 13297af..bd1a996 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/reduce.o b/solvers/kissat-inc/build/reduce.o
index a6cc5dd..d0c113e 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/rephase.o b/solvers/kissat-inc/build/rephase.o
index 0296a82..e5880df 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 d72d89d..cf3a1a7 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/restart.o b/solvers/kissat-inc/build/restart.o
index 33b96a6..f37712a 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 060116c..559b880 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/substitute.o b/solvers/kissat-inc/build/substitute.o
index 10f045b..05df643 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 671fba7..e79d2f2 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/transitive.o b/solvers/kissat-inc/build/transitive.o
index ec9cc26..49a5b27 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/vivify.o b/solvers/kissat-inc/build/vivify.o
index 34b588e..8320006 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 a81c44e..f06e127 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 f20d8a0..f7c1e08 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/xors.o b/solvers/kissat-inc/build/xors.o
index c139bc0..6b1e726 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/makefile b/solvers/kissat-inc/makefile
index d672564..f359a7a 100644
--- a/solvers/kissat-inc/makefile
+++ b/solvers/kissat-inc/makefile
@@ -1,17 +1,17 @@
 all:
-	$(MAKE) -C "/home/chenzh/solvers/Light/kissat-inc/build"
+	$(MAKE) -C "/home/chenzh/solvers/Light/solvers/kissat-inc/build"
 kissat:
-	$(MAKE) -C "/home/chenzh/solvers/Light/kissat-inc/build" kissat
+	$(MAKE) -C "/home/chenzh/solvers/Light/solvers/kissat-inc/build" kissat
 tissat:
-	$(MAKE) -C "/home/chenzh/solvers/Light/kissat-inc/build" tissat
+	$(MAKE) -C "/home/chenzh/solvers/Light/solvers/kissat-inc/build" tissat
 clean:
-	rm -f "/home/chenzh/solvers/Light/kissat-inc"/makefile
-	-$(MAKE) -C "/home/chenzh/solvers/Light/kissat-inc/build" clean
-	rm -rf "/home/chenzh/solvers/Light/kissat-inc/build"
+	rm -f "/home/chenzh/solvers/Light/solvers/kissat-inc"/makefile
+	-$(MAKE) -C "/home/chenzh/solvers/Light/solvers/kissat-inc/build" clean
+	rm -rf "/home/chenzh/solvers/Light/solvers/kissat-inc/build"
 coverage:
-	$(MAKE) -C "/home/chenzh/solvers/Light/kissat-inc/build" coverage
+	$(MAKE) -C "/home/chenzh/solvers/Light/solvers/kissat-inc/build" coverage
 indent:
-	$(MAKE) -C "/home/chenzh/solvers/Light/kissat-inc/build" indent
+	$(MAKE) -C "/home/chenzh/solvers/Light/solvers/kissat-inc/build" indent
 test:
-	$(MAKE) -C "/home/chenzh/solvers/Light/kissat-inc/build" test
+	$(MAKE) -C "/home/chenzh/solvers/Light/solvers/kissat-inc/build" test
 .PHONY: all clean coverage indent kissat test tissat
diff --git a/solvers/kissat-inc/src/bump.c b/solvers/kissat-inc/src/bump.c
index b042a74..f6f8fa4 100644
--- a/solvers/kissat-inc/src/bump.c
+++ b/solvers/kissat-inc/src/bump.c
@@ -53,6 +53,36 @@ rescale_scores (kissat * solver, heap * scores)
 		GET (rescaled), "rescaled by factor %g", factor);
 }
 
+void kissat_shuffle_score(kissat * solver) {
+  heap *scores = &solver->scores;
+  heap *scores_chb = &solver->scores_chb;
+  flags *flags = solver->flags;
+  int *id = (int *)malloc(sizeof(int) * (VARS));
+  for (int i = 0; i < VARS; i++) id[i] = i;
+  for (int i = 0; i < VARS; i++)
+  {
+    int j = (rand() % VARS);
+    int x = id[i];
+    id[i] = id[j];
+    id[j] = x;
+  }
+  for (int i = 0; i < VARS; i++) {
+    int idx = id[i];
+    if (flags[idx].active) {
+      double new_score = 1.0 * i / VARS;
+      kissat_update_heap (solver, scores, idx, new_score);
+      kissat_update_heap (solver, scores_chb, idx, new_score);
+    }
+  }
+  for (int i = 0; i < VARS; i++) {
+    int idx = id[i];
+    if (flags[idx].active)
+      kissat_move_to_front(solver, idx);
+  }
+  solver->scinc = 1.0;
+  free(id);
+}
+
 static void
 bump_score_increment (kissat * solver, heap * scores)
 {
diff --git a/solvers/kissat-inc/src/bump.h b/solvers/kissat-inc/src/bump.h
index b77e25b..bf69e76 100644
--- a/solvers/kissat-inc/src/bump.h
+++ b/solvers/kissat-inc/src/bump.h
@@ -6,6 +6,7 @@ struct kissat;
 void kissat_bump_variables (struct kissat *);
 void kissat_bump_chb (struct kissat *, unsigned idx, double multiplier);
 void kissat_decay_chb (struct kissat *);
+void kissat_shuffle_score(struct kissat *);
 void kissat_update_conflicted_chb (struct kissat *);
 
 #define MAX_SCORE 1e150
diff --git a/solvers/kissat-inc/src/internal.c b/solvers/kissat-inc/src/internal.c
index 8eea2bc..096ab7b 100644
--- a/solvers/kissat-inc/src/internal.c
+++ b/solvers/kissat-inc/src/internal.c
@@ -45,6 +45,7 @@ kissat_init (void)
   solver-> mab_decisions = 0;
   solver-> mab_chosen_tot = 0;
   solver-> order_reset = -1;
+  solver-> reseting = 0;
 #ifndef NDEBUG
   kissat_init_checker (solver);
 #endif
diff --git a/solvers/kissat-inc/src/internal.h b/solvers/kissat-inc/src/internal.h
index a4ce104..5985fa1 100644
--- a/solvers/kissat-inc/src/internal.h
+++ b/solvers/kissat-inc/src/internal.h
@@ -72,6 +72,7 @@ typedef STACK (watch *) patches;
 
 struct kissat
 {
+  int reseting;
   int order_reset;
   int max_var;
 #ifdef LOGGING
diff --git a/solvers/kissat-inc/src/search.c b/solvers/kissat-inc/src/search.c
index c8ad280..5b23708 100644
--- a/solvers/kissat-inc/src/search.c
+++ b/solvers/kissat-inc/src/search.c
@@ -18,185 +18,188 @@
 #include <inttypes.h>
 
 static void
-start_search (kissat * solver)
+start_search(kissat *solver)
 {
-  START (search);
-  INC (searches);
+  START(search);
+  INC(searches);
 
-  REPORT (0, '*');
+  REPORT(0, '*');
 
-  bool stable = (GET_OPTION (stable) == 2);
+  bool stable = (GET_OPTION(stable) == 2);
 
   solver->stable = stable;
-  kissat_phase (solver, "search", GET (searches),
-		"initializing %s search after %" PRIu64 " conflicts",
-		(stable ? "stable" : "focus"), CONFLICTS);
+  kissat_phase(solver, "search", GET(searches),
+               "initializing %s search after %" PRIu64 " conflicts",
+               (stable ? "stable" : "focus"), CONFLICTS);
 
-  kissat_init_averages (solver, &AVERAGES);
+  kissat_init_averages(solver, &AVERAGES);
 
   if (solver->stable)
-    kissat_init_reluctant (solver);
+    kissat_init_reluctant(solver);
 
-  kissat_init_limits (solver);
+  kissat_init_limits(solver);
 
-  unsigned seed = GET_OPTION (seed);
+  unsigned seed = GET_OPTION(seed);
   solver->random = seed;
-  LOG ("initialized random number generator with seed %u", seed);
+  LOG("initialized random number generator with seed %u", seed);
 
-  kissat_reset_rephased (solver);
+  kissat_reset_rephased(solver);
 
-  const unsigned eagersubsume = GET_OPTION (eagersubsume);
+  const unsigned eagersubsume = GET_OPTION(eagersubsume);
   if (eagersubsume && !solver->clueue.elements)
-    kissat_init_clueue (solver, &solver->clueue, eagersubsume);
+    kissat_init_clueue(solver, &solver->clueue, eagersubsume);
 #ifndef QUIET
   limits *limits = &solver->limits;
   limited *limited = &solver->limited;
   if (!limited->conflicts && !limited->decisions)
-    kissat_very_verbose (solver, "starting unlimited search");
+    kissat_very_verbose(solver, "starting unlimited search");
   else if (limited->conflicts && !limited->decisions)
-    kissat_very_verbose (solver,
-			 "starting search with conflicts limited to %" PRIu64,
-			 limits->conflicts);
+    kissat_very_verbose(solver,
+                        "starting search with conflicts limited to %" PRIu64,
+                        limits->conflicts);
   else if (!limited->conflicts && limited->decisions)
-    kissat_very_verbose (solver,
-			 "starting search with decisions limited to %" PRIu64,
-			 limits->decisions);
+    kissat_very_verbose(solver,
+                        "starting search with decisions limited to %" PRIu64,
+                        limits->decisions);
   else
-    kissat_very_verbose (solver,
-			 "starting search with decisions limited to %" PRIu64
-			 " and conflicts limited to %" PRIu64,
-			 limits->decisions, limits->conflicts);
+    kissat_very_verbose(solver,
+                        "starting search with decisions limited to %" PRIu64
+                        " and conflicts limited to %" PRIu64,
+                        limits->decisions, limits->conflicts);
   if (stable)
-    {
-      START (stable);
-      REPORT (0, '[');
-    }
+  {
+    START(stable);
+    REPORT(0, '[');
+  }
   else
-    {
-      START (focused);
-      REPORT (0, '{');
-    }
+  {
+    START(focused);
+    REPORT(0, '{');
+  }
 #endif
 }
 
 static void
-stop_search (kissat * solver, int res)
+stop_search(kissat *solver, int res)
 {
   if (solver->limited.conflicts)
-    {
-      LOG ("reset conflict limit");
-      solver->limited.conflicts = false;
-    }
+  {
+    LOG("reset conflict limit");
+    solver->limited.conflicts = false;
+  }
 
   if (solver->limited.decisions)
-    {
-      LOG ("reset decision limit");
-      solver->limited.decisions = false;
-    }
+  {
+    LOG("reset decision limit");
+    solver->limited.decisions = false;
+  }
 
   if (solver->terminate)
-    {
-      kissat_very_verbose (solver, "termination forced externally");
-      solver->terminate = 0;
-    }
+  {
+    kissat_very_verbose(solver, "termination forced externally");
+    solver->terminate = 0;
+  }
 
 #ifndef QUIET
-  LOG ("search result %d", res);
+  LOG("search result %d", res);
   if (solver->stable)
-    {
-      REPORT (0, ']');
-      STOP (stable);
-      solver->stable = false;
-    }
+  {
+    REPORT(0, ']');
+    STOP(stable);
+    solver->stable = false;
+  }
   else
-    {
-      REPORT (0, '}');
-      STOP (focused);
-    }
-  char type = (res == 10 ? '1' : res == 20 ? '0' : '?');
-  REPORT (0, type);
+  {
+    REPORT(0, '}');
+    STOP(focused);
+  }
+  char type = (res == 10 ? '1' : res == 20 ? '0'
+                                           : '?');
+  REPORT(0, type);
 #else
-  (void) res;
+  (void)res;
 #endif
 
-  STOP (search);
+  STOP(search);
 }
 
 static void
-iterate (kissat * solver)
+iterate(kissat *solver)
 {
-  assert (solver->iterating);
+  assert(solver->iterating);
   solver->iterating = false;
-  REPORT (0, 'i');
+  REPORT(0, 'i');
 }
 
 static bool
-conflict_limit_hit (kissat * solver)
+conflict_limit_hit(kissat *solver)
 {
   if (!solver->limited.conflicts)
     return false;
   if (solver->limits.conflicts > solver->statistics.conflicts)
     return false;
-  kissat_very_verbose (solver, "conflict limit %" PRIu64
-		       " hit after %" PRIu64 " conflicts",
-		       solver->limits.conflicts,
-		       solver->statistics.conflicts);
+  kissat_very_verbose(solver, "conflict limit %" PRIu64 " hit after %" PRIu64 " conflicts",
+                      solver->limits.conflicts,
+                      solver->statistics.conflicts);
   return true;
 }
 
 static bool
-decision_limit_hit (kissat * solver)
+decision_limit_hit(kissat *solver)
 {
   if (!solver->limited.decisions)
     return false;
   if (solver->limits.decisions > solver->statistics.decisions)
     return false;
-  kissat_very_verbose (solver, "decision limit %" PRIu64
-		       " hit after %" PRIu64 " decisions",
-		       solver->limits.decisions,
-		       solver->statistics.decisions);
+  kissat_very_verbose(solver, "decision limit %" PRIu64 " hit after %" PRIu64 " decisions",
+                      solver->limits.decisions,
+                      solver->statistics.decisions);
   return true;
 }
 
-int
-kissat_search (kissat * solver)
+int kissat_search(kissat *solver)
 {
-  start_search (solver);
+  start_search(solver);
 
-  int res = kissat_walk_initially (solver);
+  int res = kissat_walk_initially(solver);
 
   while (!res)
+  {
+    if (!solver->level && solver->reseting)
     {
-      clause *conflict = kissat_search_propagate (solver);
-      if (conflict)
-	res = kissat_analyze (solver, conflict);
-      else if (solver->iterating)
-	iterate (solver);
-      else if (!solver->unassigned)
-	res = 10;
-      else if (TERMINATED (11))
-	break;
-      else if (conflict_limit_hit (solver))
-	break;
-      else if (kissat_reducing (solver))
-	res = kissat_reduce (solver);
-      else if (kissat_restarting (solver))
-	kissat_restart (solver);
-      else if (kissat_rephasing (solver))
-	kissat_rephase (solver);
-      else if (kissat_eliminating (solver))
-	res = kissat_eliminate (solver);
-      else if (kissat_probing (solver))
-	res = kissat_probe (solver);
-      else if (!solver->level && solver->unflushed)
-	kissat_flush_trail (solver);
-      else if (decision_limit_hit (solver))
-	break;
-      else
-	kissat_decide (solver);
+      kissat_shuffle_score(solver);
+      solver->reseting = 0;
     }
+    clause *conflict = kissat_search_propagate(solver);
+    if (conflict)
+      res = kissat_analyze(solver, conflict);
+    else if (solver->iterating)
+      iterate(solver);
+    else if (!solver->unassigned)
+      res = 10;
+    else if (TERMINATED(11))
+      break;
+    else if (conflict_limit_hit(solver))
+      break;
+    else if (kissat_reducing(solver))
+      res = kissat_reduce(solver);
+    else if (kissat_restarting(solver))
+      kissat_restart(solver);
+    else if (kissat_rephasing(solver))
+      kissat_rephase(solver);
+    else if (kissat_eliminating(solver))
+      res = kissat_eliminate(solver);
+    else if (kissat_probing(solver))
+      res = kissat_probe(solver);
+    else if (!solver->level && solver->unflushed)
+      kissat_flush_trail(solver);
+    else if (decision_limit_hit(solver))
+      break;
+    else
+      kissat_decide(solver);
+  }
 
-  stop_search (solver, res);
+  stop_search(solver, res);
 
   return res;
 }
diff --git a/utils/paras.hpp b/utils/paras.hpp
index 87827ec..d052dad 100644
--- a/utils/paras.hpp
+++ b/utils/paras.hpp
@@ -6,10 +6,12 @@
 
 //        name,      type,   default, low, high, comments
 #define PARAS \
-    PARA( mode     , int    , 0     , 0  , 2   , "SAT=1, UNSAT=2") \
-    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( mode       , int    , 0     , 0  , 2   , "SAT=1, UNSAT=2") \
+    PARA( reset      , int    , 0     , 0  , 1   , "Dynamically reseting") \
+    PARA( reset_time , int    , 10    , 1  , 1e5 , "Reseting base interval (seconds)") \
+    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") \
     
 
 struct paras 
diff --git a/utils/paras.o b/utils/paras.o
index fc49148..b64ce2b 100644
Binary files a/utils/paras.o and b/utils/paras.o differ
diff --git a/version.md b/version.md
new file mode 100644
index 0000000..fc84339
--- /dev/null
+++ b/version.md
@@ -0,0 +1,5 @@
+### 1.0
+base Framework
+RS
+#### 1.1
+Dynamically reseting
diff --git a/workers/basekissat.cpp b/workers/basekissat.cpp
index e0219e9..73aef06 100644
--- a/workers/basekissat.cpp
+++ b/workers/basekissat.cpp
@@ -57,4 +57,13 @@ void basekissat::get_model(vec<int> &model) {
       if (!tmp) tmp = i;
       model.push(tmp);
    }
+}
+
+int basekissat::get_reset_data() {
+    return solver->best_assigned;
+}
+
+
+void basekissat::reset() {
+    solver->reseting = 1;
 }
\ No newline at end of file
diff --git a/workers/basekissat.hpp b/workers/basekissat.hpp
index c20fcc2..0390a37 100644
--- a/workers/basekissat.hpp
+++ b/workers/basekissat.hpp
@@ -10,6 +10,8 @@ public:
     void terminate();
     int  solve();
     void get_model(vec<int> &model);
+    int  get_reset_data();
+    void reset();
 
     basekissat(int id, light *light);
     ~basekissat();
diff --git a/workers/basekissat.o b/workers/basekissat.o
index a2e4c23..dc2b24b 100644
Binary files a/workers/basekissat.o and b/workers/basekissat.o differ
diff --git a/workers/basesolver.hpp b/workers/basesolver.hpp
index 38b7646..2f867f4 100644
--- a/workers/basesolver.hpp
+++ b/workers/basesolver.hpp
@@ -11,6 +11,8 @@ public:
     virtual int  solve() = 0;
     virtual void terminate() = 0;
     virtual void get_model(vec<int> &model) = 0;
+    virtual int  get_reset_data() = 0;
+    virtual void reset() = 0;
     light * controller;
     int id;