diff --git a/light-v4 b/light-v4-1
similarity index 65%
rename from light-v4
rename to light-v4-1
index 5c503fa..827deb8 100755
Binary files a/light-v4 and b/light-v4-1 differ
diff --git a/preprocess/card.cpp b/preprocess/card.cpp
index a6518be..650d199 100644
--- a/preprocess/card.cpp
+++ b/preprocess/card.cpp
@@ -70,13 +70,13 @@ void preprocess::upd_occur(int v, int s) {
     if (v > 0) {
         for (int j = 0; j < occurp[x].size(); j++)
             if (occurp[x][j] != s) occurp[x][t++] = occurp[x][j]; 
-        assert(t == occurp[x].size() - 1);
+        // assert(t == occurp[x].size() - 1);
         occurp[x].setsize(t);
     }
     else {
         for (int j = 0; j < occurn[x].size(); j++)
             if (occurn[x][j] != s) occurn[x][t++] = occurn[x][j];
-        assert(t == occurn[x].size() - 1);
+        // assert(t == occurn[x].size() - 1);
         occurn[x].setsize(t);
     }
 }
@@ -310,7 +310,7 @@ int preprocess::card_elimination() {
 
 int preprocess::preprocess_card() {
     int sone = search_almost_one();
-    // printf("c [CE] almost one cons: %d\n", sone);
+    printf("c [CE] almost one cons: %d\n", sone);
     if (!sone) return 1;
     int scc = scc_almost_one();
     int sz = card_one.size();
diff --git a/preprocess/gauss.cpp b/preprocess/gauss.cpp
index 97562f2..ebb394b 100644
--- a/preprocess/gauss.cpp
+++ b/preprocess/gauss.cpp
@@ -210,7 +210,7 @@ int preprocess::gauss_elimination() {
             }
             else if (ones.size() == 2) {
                 ++gauss_eli_binary;
-                assert(clauses == clause.size() - 1);
+                // assert(clauses == clause.size() - 1);
                 int p = ones[0], q = rhs ? ones[1] : -ones[1];
                 clause.push();
                 ++clauses;
diff --git a/solve.cpp b/solve.cpp
index df11183..11c5aae 100644
--- a/solve.cpp
+++ b/solve.cpp
@@ -10,15 +10,15 @@ char* worker_sign = "";
 std::mutex mtx;
 std::atomic<int> terminated;
 int result = 0;
-int winner;
+int winner, winner_conf;
 vec<int> model;
 
 void * read_worker(void *arg) {
    basesolver * sq = (basesolver *)arg;
     if (worker_sign == "") 
-      sq->import_original_clause(sq->controller->pre);
+      sq->parse_from_PAR(sq->controller->pre);
    else 
-      sq->parse_dimacs(worker_sign);
+      sq->parse_from_CNF(worker_sign);
    return NULL;
 }
 
@@ -31,11 +31,12 @@ void * solve_worker(void *arg) {
             sq->get_model(seq_model);
         }
         if (res && !terminated) {
-            printf("c result: %d, winner is %d\n", res, sq->id);
+            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();
@@ -54,7 +55,7 @@ void light::init_workers() {
 
 void light::diversity_workers() {
     for (int i = 0; i < OPT(threads); i++) {
-        workers[i]->diversity(i);
+        if (i) workers[i]->configure("order_reset", i);
     }
 }
 
@@ -97,21 +98,21 @@ int light::solve() {
             terminated = 1;
             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");
-        }
+        // 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");
+        // }
     }
     // printf("ending solve\n");
     terminate_workers();
diff --git a/solvers/kissat-inc/build/analyze.o b/solvers/kissat-inc/build/analyze.o
index af903ec..78299ea 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 4d9d678..e4d94dd 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 d1031ec..7bfc775 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 ff7a127..526d141 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 68bfdee..e81b424 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 ec663d4..d776ada 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 f1a3c4e..596fe2d 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 574ff8b..6cd8818 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 8963d43..ee51e16 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 de9a812..ddb7273 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 "Fri Feb 24 13:59:13 CST 2023 Linux seed1 5.4.0-120-generic x86_64"
+#define BUILD "Mon Feb 27 07:44:55 UTC 2023 Linux seed4 5.4.0-125-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 8e7913c..f90b7a0 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 fca32f6..918b958 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 376592d..fe567e6 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 5abade0..bc7de95 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 f57c54f..59f1a4c 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 7f4544b..11d0f37 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 ebb604c..6b43679 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 13df167..42800c1 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 4c88d1f..2b22678 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 9eb975c..cce757d 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 d89820f..5cca1af 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 d7db26e..12e24ec 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 09f2928..837aaad 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 8c7fa0b..dbd62e0 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 1243459..7aa6dc7 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 bcde158..4069774 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 b119370..7acff15 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 e6da163..2f4ba95 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 8340bd7..71b3180 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 ef4c0ca..c22e7fb 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 48d2e49..b61d4aa 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 2567f4c..43c2d21 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 42357ce..4d8813b 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 170dda2..855eb09 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 0410613..1c435ca 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 6017952..0aca901 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 3742fbd..c297fa5 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/options.o b/solvers/kissat-inc/build/options.o
index a64c181..feedbcc 100644
Binary files a/solvers/kissat-inc/build/options.o and b/solvers/kissat-inc/build/options.o differ
diff --git a/solvers/kissat-inc/build/parse.o b/solvers/kissat-inc/build/parse.o
index 40ff329..83da2c0 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 ab693d7..f50a106 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 8e05c6b..6e145e7 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 0a35290..5915217 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 f112a57..b471860 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 4199f60..d6f4eea 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 4cab26e..df7fef3 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 4ca0459..95d84a1 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 d6ac7d3..55ec5a8 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 87d1c1f..fe3d596 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 bd63dd2..4a64bfa 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 b9551c9..fabe247 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 db19a72..d09c36a 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 8116923..164891e 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 4ab4642..1d0ffaf 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 12d966f..56f25fe 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 cab5e72..d0f5328 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 1d5b549..04265e0 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 1211332..adbac54 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 4bf0594..45c009d 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 36a4851..e516e53 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 750e1a2..687fc08 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 1de15e0..60b8718 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 262e4f3..7992d03 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 647670b..1988311 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 e439857..5f25454 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 8708300..ff6839c 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 bb5a670..bb1dc01 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 5d9106a..0c97b85 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 850353a..8a89c5b 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 27efc01..cfc4d3e 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 37d6964..44d4884 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 cae2afa..779e5c6 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/application.c b/solvers/kissat-inc/src/application.c
index 550ce90..1edaef2 100644
--- a/solvers/kissat-inc/src/application.c
+++ b/solvers/kissat-inc/src/application.c
@@ -606,20 +606,6 @@ parse_options (application * application, int argc, char **argv)
   return true;
 }
 
-void kissat_mab_parse(kissat* solver) {
-  solver->step_chb = 0.1*GET_OPTION(stepchb);
-  solver->heuristic = GET_OPTION(heuristic);
-  solver->mab = GET_OPTION(mab);
-  if(solver->mab) {
-	for (unsigned i=0;i<solver->mab_heuristics;i++) {
-		solver->mab_reward[i] = 0; 
-		solver->mab_select[i] = 0;
-	}
-	solver->mabc = GET_OPTION(mabcint)+0.1*GET_OPTION(mabcdecimal);
-	solver->mab_select[solver->heuristic]++; 
-  }
-}
-
 static bool
 parse_input (application * application)
 {
diff --git a/solvers/kissat-inc/src/application.h b/solvers/kissat-inc/src/application.h
index 30a8abb..f4a5b12 100644
--- a/solvers/kissat-inc/src/application.h
+++ b/solvers/kissat-inc/src/application.h
@@ -4,6 +4,5 @@
 struct kissat;
 
 int kissat_application (struct kissat *, int argc, char **argv);
-void kissat_mab_parse  (struct kissat *);
 
 #endif
diff --git a/solvers/kissat-inc/src/internal.c b/solvers/kissat-inc/src/internal.c
index 9f33b31..c5af8d5 100644
--- a/solvers/kissat-inc/src/internal.c
+++ b/solvers/kissat-inc/src/internal.c
@@ -49,11 +49,21 @@ kissat_init (void)
   solver->mab_heuristics = 2;
   solver-> mab_decisions = 0;
   solver-> mab_chosen_tot = 0;
-  solver-> order_reset = -1;
   solver-> reseting = 0;
 #ifndef NDEBUG
   kissat_init_checker (solver);
 #endif
+  solver->step_chb = 0.1*GET_OPTION(stepchb);
+  solver->heuristic = GET_OPTION(heuristic);
+  solver->mab = GET_OPTION(mab);
+  if(solver->mab) {
+    for (unsigned i=0;i<solver->mab_heuristics;i++) {
+      solver->mab_reward[i] = 0; 
+      solver->mab_select[i] = 0;
+    }
+    solver->mabc = GET_OPTION(mabcint)+0.1*GET_OPTION(mabcdecimal);
+    solver->mab_select[solver->heuristic]++; 
+  }
   return solver;
 }
 
@@ -184,7 +194,8 @@ kissat_reserve (kissat * solver, int max_var)
 		  "invalid maximum variable argument '%d'", max_var);
   kissat_increase_size (solver, (unsigned) max_var);
     
-  if (solver->order_reset != -1)
+  int seed = GET_OPTION(order_reset);
+  if (seed != -1)
   {
     // srand(solver->order_reset);
     int *id;
@@ -193,7 +204,7 @@ kissat_reserve (kissat * solver, int max_var)
       id[i] = i;
     for (int i = 1; i <= max_var; i++)
     {
-      int j = (rand_r(&solver->order_reset) % max_var) + 1;
+      int j = (rand_r(&seed) % max_var) + 1;
       int x = id[i];
       id[i] = id[j];
       id[j] = x;
diff --git a/solvers/kissat-inc/src/internal.h b/solvers/kissat-inc/src/internal.h
index 2c037da..a8931b7 100644
--- a/solvers/kissat-inc/src/internal.h
+++ b/solvers/kissat-inc/src/internal.h
@@ -84,7 +84,6 @@ struct kissat
   void *issuer;
   int nconflict;
   int reseting;
-  int order_reset;
   int max_var;
 #ifdef LOGGING
   bool compacting;
diff --git a/solvers/kissat-inc/src/options.h b/solvers/kissat-inc/src/options.h
index 3adf4ab..e210198 100644
--- a/solvers/kissat-inc/src/options.h
+++ b/solvers/kissat-inc/src/options.h
@@ -55,6 +55,7 @@ OPTION( mabcint, 4, 0, 10, "mab const floor") \
 OPTION( minimizedepth, 1e3, 1, 1e6, "minimization depth") \
 OPTION( modeinit, 1e3, 10, 1e8, "initial mode change interval") \
 OPTION( modeint, 1e3, 10, 1e8, "base mode change interval") \
+OPTION( order_reset, -1, -1, 1e5, "order seed") \
 OPTION( otfs, 1, 0, 1, "on-the-fly strengthening") \
 OPTION( phase, 1, 0, 1, "initial decision phase") \
 OPTION( phasesaving, 1, 0, 1, "enable phase saving") \
diff --git a/testLight/cal_solver.py b/testLight/cal_solver.py
index b2294ee..7437800 100644
--- a/testLight/cal_solver.py
+++ b/testLight/cal_solver.py
@@ -268,10 +268,9 @@ if __name__ == "__main__":
     solvers = []
 
 
-    solvers.append(solver_SAT_standard_gnomon("/home/chenzh/res/testLight/v1","v1"))
-    solvers.append(solver_SAT_standard_gnomon("/home/chenzh/res/testLight/v2","v2"))
-    solvers.append(solver_SAT_standard_gnomon("/home/chenzh/res/testLight/v3","v3"))
-
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v3--1-preprocess","preprocess"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-nps","sharing-nps"))
+    solvers.append(solver_SAT_standard_gnomon("/pub/data/chenzh/res/light/v4-dps","sharing-dps"))
 
     # append_all_solvers_in_dir(solvers, "/pub/data/chenzh/res/light/")
     samples = []
diff --git a/testLight/nohup.out b/testLight/nohup.out
index 3d80fcd..00dae28 100644
Binary files a/testLight/nohup.out and b/testLight/nohup.out differ
diff --git a/testLight/run7_1.sh b/testLight/run7_1.sh
new file mode 100755
index 0000000..184b453
--- /dev/null
+++ b/testLight/run7_1.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/v4-nps"
+res7="/pub/data/chenzh/res/light/v4-dps"
+res8="/pub/data/chenzh/res/light/v4-dps-2w"
+res_no="/pub/data/chenzh/res/unused"
+#####################################################
+
+all_datas=($instance_21 $instance_20)
+for((i=0;i<${#all_datas[*]};i++))
+do
+	instance=${all_datas[$i]}
+	
+	res_solver_ins=$res8
+	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 $instance/$file --share=1 --DPS=1 --DPS_period=20000
+			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/run7_2.sh b/testLight/run7_2.sh
new file mode 100755
index 0000000..758a7c3
--- /dev/null
+++ b/testLight/run7_2.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/v4-nps"
+res7="/pub/data/chenzh/res/light/v4-dps"
+res8="/pub/data/chenzh/res/light/v4-dps-2w"
+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=$res8
+	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 $instance/$file --share=1 --DPS=1 --DPS_period=20000
+			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/workers/basekissat.cpp b/workers/basekissat.cpp
index 0894c11..7e820d4 100644
--- a/workers/basekissat.cpp
+++ b/workers/basekissat.cpp
@@ -11,45 +11,78 @@ extern "C" {
    #include "src/import.h"
 }
 
-void kissat_export_clause(void *solver, int lbd, cvec* c) {
-    basekissat* S = (basekissat *) solver;
-    ++S->x1;
-    if (S->solver->nconflict != S->x1 - 1) printf("%d %d\n", S->solver->nconflict, S->x1);
-    if (lbd > S->good_clause_lbd) return;
+void basekissat::add(int l) {
+    kissat_add(solver, l);
+}
+
+void basekissat::configure(char* name, int id) {
+    kissat_set_option(solver, name, id);
+}
+
+int  basekissat::solve() {
+    return kissat_solve(solver);
+}
+
+void basekissat::terminate() {
+    kissat_terminate(solver);
+}
+
+int  basekissat::val(int l) {
+    int v = abs(l);
+    int tmp = kissat_value(solver, v);
+    if (!tmp) tmp = v;
+    if (l < 0) tmp = -tmp;
+    return tmp;
+}
+
+void basekissat::exp_clause(void* cl, int lbd) {
+    cvec *c = (cvec *) cl;
     clause_store* cls = new clause_store(c->sz);
     for (int i = 0; i < c->sz; i++) {
         int v = cvec_data(c, i);
-        int eidx = PEEK_STACK(S->solver->exportk, (v >> 1));
+        int eidx = PEEK_STACK(solver->exportk, (v >> 1));
         cls->data[i] = v & 1 ? -eidx : eidx;
     }
-    ++S->x2;
+    // ++S->x2;
     // if (S->id == 0) puts("");
     cls->lbd = lbd;
-    S->export_clause.push(cls);
+    export_clause.push(cls);
 }
 
-int kissat_import_clause(void *solver, int *lbd, cvec* c) {
-    basekissat* S = (basekissat *) solver;
-    clause_store* cls = NULL;
-    if (S->import_clause.pop(cls) == false) return -1;
 
-    bool eliminated = false;
+void call_back_out(void *solver, int lbd, cvec *c) {
+    basekissat* S = (basekissat *) solver;
+    // ++S->x1;
+    // if (S->solver->nconflict != S->x1 - 1) printf("%d %d\n", S->solver->nconflict, S->x1);
+    if (lbd <= S->good_clause_lbd) {
+        S->exp_clause(c, lbd);       
+    }
+}
+
+bool basekissat::imp_clause(clause_store *cls, void *cl) {
+    cvec *c = (cvec *) cl;
     for (int i = 0; i < cls->size; i++) {
         // S->outimport << cls->data[i] << std::endl;
         int eidx = abs(cls->data[i]);
-        import *import = &PEEK_STACK (S->solver->import, eidx);
-        if (import->eliminated) {
-            eliminated = true;
-        }
+        import *import = &PEEK_STACK (solver->import, eidx);
+        if (import->eliminated) return false;
         else {
             int ilit = import->lit;
             if (cls->data[i] < 0) ilit = ilit ^ 1;
             cvec_push(c, ilit);
         }
     }
+    return true;
+}
+
+int call_back_in(void *solver, int *lbd, cvec *c) {
+    basekissat* S = (basekissat *) solver;
+    clause_store* cls = NULL;
+    if (S->import_clause.pop(cls) == false) return -1;
     *lbd = cls->lbd;
+    bool res = S->imp_clause(cls, c); 
     cls->free_clause();
-    if (eliminated) return -10;
+    if (!res) return -10;
     return 1;
 } 
 
@@ -90,8 +123,8 @@ basekissat::basekissat(int id, light* light) : basesolver(id, light) {
     solver -> cbkExportClause = NULL;
     solver -> cbkWaitSharing  = NULL;
     if (light->opt->share) {
-        solver -> cbkImportClause = kissat_import_clause;
-        solver -> cbkExportClause = kissat_export_clause;
+        solver -> cbkImportClause = call_back_in;
+        solver -> cbkExportClause = call_back_out;
         solver -> cbkWaitSharing  = kissat_wait_sharing;
         solver -> share_dps       = light->opt->DPS;
         solver -> share_dps_period= light->opt->DPS_period;
@@ -102,8 +135,7 @@ basekissat::~basekissat(){
     delete solver;
 }
 
-void basekissat::parse_dimacs(char* filename) {
-    kissat_mab_parse(solver);
+void basekissat::parse_from_CNF(char* filename) {
     strictness strict = NORMAL_PARSING;
     file in;
     uint64_t lineno;
@@ -112,47 +144,17 @@ void basekissat::parse_dimacs(char* filename) {
     kissat_close_file(&in);
 }
 
-void basekissat::import_original_clause(preprocess* pre) {
+void basekissat::parse_from_PAR(preprocess* pre) {
     solver->max_var = pre->vars;
-    kissat_mab_parse(solver);
     kissat_reserve(solver, pre->vars);
     for (int i = 1; i <= pre->clauses; i++) {
         int l = pre->clause[i].size();
         for (int j = 0; j < l; j++)
-            kissat_add(solver, pre->clause[i][j]);
-        kissat_add(solver, 0);
+            add(pre->clause[i][j]);
+        add(0);
     }
 }
 
-void basekissat::diversity(int id) {
-    if (id) solver->order_reset = id;
-}
-
-int  basekissat::solve() {
-    return kissat_solve(solver);
-}
-
-void basekissat::terminate() {
-    kissat_terminate(solver);
-}
-
-void basekissat::get_model(vec<int> &model) {
-    model.clear();
-    for (int i = 1; i <= solver->max_var; i++) {
-      int tmp = kissat_value(solver, i);
-      if (!tmp) tmp = i;
-      model.push(tmp);
-   }
-}
-
-int basekissat::get_reset_data() {
-    return solver->best_assigned;
-}
-
-void basekissat::reset() {
-    solver->reseting = 1;
-}
-
 void basekissat::export_clauses_to(vec<clause_store *> &clauses) {
     clause_store *cls;
     while (export_clause.pop(cls)) {
@@ -174,11 +176,30 @@ void basekissat::import_clauses_from(vec<clause_store *> &clauses) {
     }
 }
 
+void basekissat::get_model(vec<int> &model) {
+    model.clear();
+    for (int i = 1; i <= solver->max_var; i++) {
+        model.push(val(i));
+   }
+}
+
 void basekissat::broaden_export_limit() {
-    // ++good_clause_lbd;
+    ++good_clause_lbd;
 }
 
 void basekissat::restrict_export_limit() {
     if (good_clause_lbd > 2)
         --good_clause_lbd;
-}
\ No newline at end of file
+}
+
+
+int basekissat::get_conflicts() {
+    return solver->nconflict;
+}
+// int basekissat::get_reset_data() {
+//     return solver->best_assigned;
+// }
+
+// void basekissat::reset() {
+//     solver->reseting = 1;
+// }
diff --git a/workers/basekissat.hpp b/workers/basekissat.hpp
index fc6967a..1fe78dc 100644
--- a/workers/basekissat.hpp
+++ b/workers/basekissat.hpp
@@ -1,21 +1,23 @@
 #include "basesolver.hpp"
-#include "clause.hpp"
-#include <boost/thread/thread.hpp>
-#include <boost/lockfree/spsc_queue.hpp>
 
 struct kissat;
 struct cvec;
 
 class basekissat : public basesolver {
 public:
-    void parse_dimacs(char* filename);
-    void import_original_clause(preprocess *pre);
-    void diversity(int id);
     void terminate();
+    void add(int l);
     int  solve();
+    int  val(int l);
+    void configure(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);
     void get_model(vec<int> &model);
-    int  get_reset_data();
-    void reset();
+    void exp_clause(void *cl, int lbd);
+    bool imp_clause(clause_store *cls, void *cl);
     void export_clauses_to(vec<clause_store *> &clauses);
     void import_clauses_from(vec<clause_store *> &clauses);
     void broaden_export_limit();
@@ -27,8 +29,6 @@ public:
     kissat* solver;
     int good_clause_lbd = 0;
     
-    boost::lockfree::spsc_queue<clause_store*, boost::lockfree::capacity<1024000>> import_clause;
-    boost::lockfree::spsc_queue<clause_store*, boost::lockfree::capacity<1024000>> export_clause;
     friend int cbkImportClause(void *, int *, cvec *);
     friend int cbkExportClause(void *, int *, cvec *);
     friend void cbkWaitSharing(void *);
diff --git a/workers/basesolver.hpp b/workers/basesolver.hpp
index 9008e2a..0858f91 100644
--- a/workers/basesolver.hpp
+++ b/workers/basesolver.hpp
@@ -6,17 +6,23 @@
 #include "clause.hpp"
 #include <fstream>
 #include <iostream>
+#include <boost/thread/thread.hpp>
+#include <boost/lockfree/spsc_queue.hpp>
 class sharer;
 class basesolver {
 public:
-    virtual void parse_dimacs(char* filename) = 0;
-    virtual void import_original_clause(preprocess* pre) = 0;
-    virtual void diversity(int id) = 0;
+    virtual void add(int l) = 0;
     virtual int  solve() = 0;
+    virtual int  val(int l) = 0;
     virtual void terminate() = 0;
+    virtual void configure(char* name, int id) = 0;
+    virtual int  get_conflicts() = 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;
-    virtual int  get_reset_data() = 0;
-    virtual void reset() = 0;
+    virtual void exp_clause(void *cl, int lbd) = 0;
+    virtual bool imp_clause(clause_store *cls, void *cl) = 0;
     virtual void export_clauses_to(vec<clause_store *> &clauses) = 0;
     virtual void import_clauses_from(vec<clause_store *> &clauses) = 0;
     virtual void broaden_export_limit() = 0;
@@ -25,9 +31,11 @@ public:
     int id;
     sharer* in_sharer;
 
+    boost::lockfree::spsc_queue<clause_store*, boost::lockfree::capacity<1024000>> import_clause;
+    boost::lockfree::spsc_queue<clause_store*, boost::lockfree::capacity<1024000>> export_clause;
+
     basesolver(int sid, light* light) : id(sid), controller(light) {}
     ~basesolver() {
-        printf("destru %dbase\n", id);
         if (controller) {
             controller = NULL;
         }