diff --git a/.vscode/settings.json b/.vscode/settings.json
index 0417e34..d24a403 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -53,6 +53,8 @@
         "sstream": "cpp",
         "stdexcept": "cpp",
         "streambuf": "cpp",
-        "cinttypes": "cpp"
+        "cinttypes": "cpp",
+        "assert.h": "c",
+        "bitset": "cpp"
     }
 }
\ No newline at end of file
diff --git a/light b/light
index 289f437..96cfbfb 100755
Binary files a/light and b/light differ
diff --git a/light-v1-1 b/light-v1-1
new file mode 100755
index 0000000..289f437
Binary files /dev/null and b/light-v1-1 differ
diff --git a/light.hpp b/light.hpp
index 7448fca..24c498c 100644
--- a/light.hpp
+++ b/light.hpp
@@ -9,6 +9,9 @@ using namespace std;
 typedef long long ll;
 
 class basesolver;
+class sharer;
+
+extern atomic<int> terminated;
 
 struct thread_inf{
     int id, inf;
@@ -28,6 +31,7 @@ public:
     paras *opt;
     preprocess *pre;
     vec<basesolver *> workers;
+    vec<sharer *> sharers;
 
     int finalResult;
     int winner;
@@ -39,6 +43,7 @@ public:
     void diversity_workers();
     void parse_input();
     int  run();
+    void share();
     int  solve();
     void terminate_workers();
     void print_model();
diff --git a/solve.cpp b/solve.cpp
index 65e84e9..10b1010 100644
--- a/solve.cpp
+++ b/solve.cpp
@@ -3,9 +3,9 @@
 #include <unistd.h>
 #include <chrono>
 #include <algorithm>
+auto clk_st = std::chrono::high_resolution_clock::now();
 char* worker_sign = "";
 atomic<int> terminated;
-auto clk_st = std::chrono::high_resolution_clock::now();
 int result = 0;
 int winner;
 vec<int> model;
@@ -123,6 +123,7 @@ int light::run() {
     }
     else worker_sign = filename;
     parse_input();
+    share();
     int res = solve();
     if (res == 10 && OPT(simplify)) {
         for (int i = 1; i <= pre->orivars; i++)
diff --git a/solvers/kissat-inc/src/cvec.c b/solvers/kissat-inc/src/cvec.c
new file mode 100644
index 0000000..3debeff
--- /dev/null
+++ b/solvers/kissat-inc/src/cvec.c
@@ -0,0 +1,64 @@
+#include "cvec.h"
+
+#include <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <errno.h>
+#include <stddef.h>
+
+static inline int imax(int x, int y)
+{
+    int mask = (y - x) >> (sizeof(int) * 8 - 1);
+    return (x & mask) + (y & (~mask));
+}
+
+
+
+void capInc(cvec *vec, int to_cap)
+{
+    if (vec->cap >= to_cap)
+        return;
+    int add = imax((to_cap - vec->cap + 1) & ~1, ((vec->cap >> 1) + 2) & ~1);
+    vec->data = (int*)realloc(vec->data, (vec->cap += add) * sizeof(int));
+}
+
+
+cvec *cvec_init()
+{
+    cvec *v;
+    v = (cvec *)malloc(sizeof(cvec));
+    v->sz = 0;
+    v->cap = 0;
+    v->data = NULL;
+    return v;
+}
+
+void cvec_release(cvec *vec)
+{
+    if (vec->data != NULL)
+        free(vec->data);
+    free(vec);
+}
+
+int cvec_data(cvec *vec, int id)
+{
+    assert(id < vec->sz);
+    return vec->data[id];
+}
+
+void cvec_setsize(cvec *vec, int v) 
+{ 
+    vec->sz = v; 
+}
+
+void cvec_push(cvec *vec, int v)
+{
+    if (vec->sz == vec->cap)
+        capInc(vec, vec->sz + 1);
+    vec->data[vec->sz++] = v;
+}
+
+void cvec_clear(cvec *vec) {
+    if (vec->data != NULL)
+        vec->sz = 0;
+}
\ No newline at end of file
diff --git a/solvers/kissat-inc/src/cvec.h b/solvers/kissat-inc/src/cvec.h
new file mode 100644
index 0000000..94cbec5
--- /dev/null
+++ b/solvers/kissat-inc/src/cvec.h
@@ -0,0 +1,17 @@
+#ifndef _cvec_h_INCLUDED
+#define _cvec_h_INCLUDED
+
+typedef struct cvec cvec;
+struct cvec
+{
+    int *data;
+    int sz, cap;
+};
+
+cvec *cvec_init();
+void cvec_release(cvec *vec);
+int cvec_data(cvec *vec, int id);
+void cvec_setsize(cvec *vec, int v);
+void cvec_push(cvec *vec, int v);
+void cvec_clear(cvec *vec);
+#endif
\ No newline at end of file
diff --git a/solvers/kissat-inc/src/internal.c b/solvers/kissat-inc/src/internal.c
index 096ab7b..64c721b 100644
--- a/solvers/kissat-inc/src/internal.c
+++ b/solvers/kissat-inc/src/internal.c
@@ -29,6 +29,8 @@ kissat_init (void)
   kissat_init_profiles (&solver->profiles);
 #endif
   START (total);
+  solver->importedClause = cvec_init();
+  solver->exportedClause = cvec_init();
   kissat_init_queue (&solver->queue);
   kissat_push_frame (solver, INVALID_LIT);
   solver->watching = true;
diff --git a/solvers/kissat-inc/src/internal.h b/solvers/kissat-inc/src/internal.h
index 5985fa1..4530de9 100644
--- a/solvers/kissat-inc/src/internal.h
+++ b/solvers/kissat-inc/src/internal.h
@@ -32,6 +32,7 @@
 #include "value.h"
 #include "vector.h"
 #include "watch.h"
+#include "cvec.h"
 
 typedef struct temporary temporary;
 
@@ -72,6 +73,13 @@ typedef STACK (watch *) patches;
 
 struct kissat
 {
+  int  (* cbkImportUnit)  (void *);
+  int  (* cbkImportClause)(void *, int *, cvec *);
+  void (* cbkExportClause)(void *, int, cvec *);	        // callback for clause learning
+
+  cvec *importedClause;
+  cvec *exportedClause;
+  void *issuer;
   int reseting;
   int order_reset;
   int max_var;
diff --git a/solvers/kissat-inc/src/learn.c b/solvers/kissat-inc/src/learn.c
index 99f7f7c..913e40f 100644
--- a/solvers/kissat-inc/src/learn.c
+++ b/solvers/kissat-inc/src/learn.c
@@ -140,4 +140,95 @@ kissat_learn_clause (kissat * solver)
     learn_binary (solver);
   else
     learn_reference (solver);
+
+  if (solver->cbkExportClause != NULL) {
+    cvec_clear(solver->exportedClause);
+    unsigned *lits = BEGIN_STACK (solver->clause.lits);
+    const unsigned *end = END_STACK (solver->clause.lits);
+    for (unsigned *p = lits; p != end; p++)
+    {
+      cvec_push(solver->exportedClause, *p);
+    }
+    solver->cbkExportClause(solver->issuer, glue, solver->exportedClause);
+  }
 }
+
+int 
+kissat_importUnitClauses(kissat *solver) 
+{
+  if (solver->cbkImportUnit == NULL) return true;
+  int l;
+  while ((l = solver->cbkImportUnit(solver->issuer)) != -1) {
+    if (l == -20) {
+      return false;
+    }
+    if (l == -10) continue;
+    if (solver->values[l] == -1) {
+      return false;
+    }
+    if (solver->values[l] == 0){
+      kissat_assign_unit(solver, l);
+    }
+  }
+  return true;
+}
+
+int
+kissat_importClauses(kissat *solver)
+{
+  if (solver->cbkImportClause == NULL)
+    return true;
+  int lbd, k, l, res;
+  assert(solver->importedClause->sz == 0);
+  while ((res = solver->cbkImportClause(solver->issuer, &lbd, solver->importedClause)) != -1) {
+    if (res == -10) {
+      cvec_clear(solver->importedClause);
+      continue;
+    }
+    assert(res == 1);
+    bool alreadySat = false;
+    for (k = l = 0; k < solver->importedClause->sz; k++) {
+      int v = cvec_data(solver->importedClause, k);
+      if (solver->values[v] == 1) {
+        alreadySat = true;
+        break;
+      }
+      else if (solver->values[v] == 0)
+        solver->importedClause->data[l++] = v;
+    }
+    solver->importedClause->sz = l;
+    if (alreadySat) {
+      cvec_clear(solver->importedClause);
+      continue;
+    }
+    if (solver->importedClause->sz == 0) {
+      cvec_clear(solver->importedClause);
+      return false;
+    }
+    if (solver->importedClause->sz == 1) {
+      kissat_assign_unit(solver, solver->importedClause->data[0]);
+      cvec_clear(solver->importedClause);
+    }
+    else {
+      lbd = solver->importedClause->sz;
+      assert (EMPTY_STACK(solver->clause.lits));
+      for (int i = 0; i < solver->importedClause->sz; i++)
+        PUSH_STACK(solver->clause.lits, solver->importedClause->data[i]);
+      const reference ref = kissat_new_redundant_clause (solver, lbd);
+      if (solver->importedClause->sz == 2) {
+        assert(ref == INVALID_REF);
+        kissat_eager_subsume (solver);
+      }
+      else {
+        assert (ref != INVALID_REF);
+        clause *c = kissat_dereference_clause (solver, ref);
+        c->used = 1 + (lbd <= (unsigned) GET_OPTION (tier2));
+        kissat_eager_subsume (solver);
+        kissat_push_clueue (&solver->clueue, ref);
+      }
+      CLEAR_STACK(solver->clause.lits);
+      cvec_clear(solver->importedClause);
+    }
+  }
+  return true;
+}
\ No newline at end of file
diff --git a/solvers/kissat-inc/src/learn.h b/solvers/kissat-inc/src/learn.h
index e17a00c..cb30688 100644
--- a/solvers/kissat-inc/src/learn.h
+++ b/solvers/kissat-inc/src/learn.h
@@ -5,4 +5,7 @@ struct kissat;
 
 void kissat_learn_clause (struct kissat *);
 
+int  kissat_importClauses(kissat *solver);
+int  kissat_importUnitClauses(kissat *solver);
+
 #endif
diff --git a/solvers/kissat-inc/src/search.c b/solvers/kissat-inc/src/search.c
index 5b23708..bfc64a2 100644
--- a/solvers/kissat-inc/src/search.c
+++ b/solvers/kissat-inc/src/search.c
@@ -170,6 +170,10 @@ int kissat_search(kissat *solver)
       kissat_shuffle_score(solver);
       solver->reseting = 0;
     }
+    if (!solver->level) {
+      if (!kissat_importUnitClauses(solver)) return 20;
+      if (!kissat_importClauses(solver)) return 20;
+    }
     clause *conflict = kissat_search_propagate(solver);
     if (conflict)
       res = kissat_analyze(solver, conflict);
diff --git a/utils/paras.hpp b/utils/paras.hpp
index d052dad..efec76c 100644
--- a/utils/paras.hpp
+++ b/utils/paras.hpp
@@ -9,7 +9,10 @@
     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( share      , int    , 0     , 0  , 1   , "Sharing learnt clauses") \
+    PARA( share_intv , int    , 500000, 0  , 1e9 , "Sharing interval (microseconds)") \
+    PARA( share_lits , int    , 1500  , 0  , 1e6 , "Sharing lits (per every #share_intv seconds)") \
+    PARA( 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") \
     
diff --git a/workers/basekissat.cpp b/workers/basekissat.cpp
index 73aef06..ee4c2bc 100644
--- a/workers/basekissat.cpp
+++ b/workers/basekissat.cpp
@@ -16,6 +16,43 @@ basekissat::~basekissat(){
     delete solver;
 }
 
+void kissat_export_clause(void *solver, int lbd, cvec* c) {
+    basekissat* S = (basekissat *) solver;
+    if (lbd > S->good_clause_lbd) return;
+    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));
+        cls->data[i] = v & 1 ? -eidx : eidx;
+    }
+    cls->lbd = lbd;
+    S->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;
+    for (int i = 0; i < cls->size; i++) {
+        int eidx = abs(cls->data[i]);
+        import *import = &PEEK_STACK (S->solver->import, eidx);
+        if (import->eliminated) {
+            eliminated = true;
+        }
+        else {
+            int ilit = import->lit;
+            if (cls->data[i] < 0) ilit = ilit ^ 1;
+            cvec_push(c, ilit);
+        }
+    }
+    *lbd = cls->lbd;
+    cls->free_clause();
+    if (eliminated) return -10;
+    return 1;
+} 
+
 void basekissat::parse_dimacs(char* filename) {
     kissat_mab_parse(solver);
     strictness strict = NORMAL_PARSING;
@@ -63,7 +100,14 @@ int basekissat::get_reset_data() {
     return solver->best_assigned;
 }
 
-
 void basekissat::reset() {
     solver->reseting = 1;
+}
+
+void basekissat::export_clauses_to(vec<clause_store *> &clauses) {
+
+}
+
+void basekissat::import_clauses_from(vec<clause_store *> &clauses) {
+    
 }
\ No newline at end of file
diff --git a/workers/basekissat.hpp b/workers/basekissat.hpp
index 0390a37..26e1f59 100644
--- a/workers/basekissat.hpp
+++ b/workers/basekissat.hpp
@@ -1,4 +1,7 @@
 #include "basesolver.hpp"
+#include "clause.hpp"
+#include <boost/thread/thread.hpp>
+#include <boost/lockfree/spsc_queue.hpp>
 
 struct kissat;
 
@@ -12,9 +15,13 @@ public:
     void get_model(vec<int> &model);
     int  get_reset_data();
     void reset();
+    void export_clauses_to(vec<clause_store *> &clauses);
+    void import_clauses_from(vec<clause_store *> &clauses);
 
     basekissat(int id, light *light);
     ~basekissat();
     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;
 };
\ No newline at end of file
diff --git a/workers/basekissat.o b/workers/basekissat.o
index dc2b24b..b03a801 100644
Binary files a/workers/basekissat.o and b/workers/basekissat.o differ
diff --git a/workers/basesolver.hpp b/workers/basesolver.hpp
index 2f867f4..2952854 100644
--- a/workers/basesolver.hpp
+++ b/workers/basesolver.hpp
@@ -13,6 +13,8 @@ public:
     virtual void get_model(vec<int> &model) = 0;
     virtual int  get_reset_data() = 0;
     virtual void reset() = 0;
+    virtual void export_clauses_to(vec<clause_store *> &clauses) = 0;
+    virtual void import_clauses_from(vec<clause_store *> &clauses) = 0;
     light * controller;
     int id;
 
diff --git a/workers/clause.hpp b/workers/clause.hpp
new file mode 100644
index 0000000..5f5992b
--- /dev/null
+++ b/workers/clause.hpp
@@ -0,0 +1,21 @@
+#ifndef _clause_hpp_INCLUDED
+#define _clause_hpp_INCLUDED
+
+struct clause_store {
+    int size, lbd;
+    int *data;
+    atomic<int> refs;
+    clause_store(int sz) {
+        size = sz;
+        data = (int*) malloc(sizeof(int) * sz);
+        lbd = 0;
+        refs = 1;
+    }
+    void free_clause() {
+        int ref = refs.fetch_sub(1);
+        if (ref <= 1)
+            free(data);
+    }
+};
+
+#endif
\ No newline at end of file
diff --git a/workers/sharer.cpp b/workers/sharer.cpp
new file mode 100644
index 0000000..c89915a
--- /dev/null
+++ b/workers/sharer.cpp
@@ -0,0 +1,82 @@
+#include "../light.hpp"
+#include "basesolver.hpp"
+#include "sharer.hpp"
+#include "clause.hpp"
+#include <unistd.h>
+
+void * share_worker(void *arg) {
+    sharer * sq = (sharer *)arg;
+    while (true) {
+        usleep(sq->share_intv);        
+        if (terminated) break;
+    }
+    for (int i = 0; i < sq->producers.size(); i++) {
+        sq->producers[i]->export_clause_to(sq->cls);
+        int number = sq->cls.size();
+        int percent = sq->sort_clauses(i);
+        if (percent < 75) {
+            sq->producers[i]->broaden_export_limit();
+        }
+        else if (percent > 98) {
+            sq->producers[i]->restrict_export_limit();
+        }
+        for (int j = 0; j < sq->consumers.size(); j++) {
+            if (sq->producers[i]->id == sq->consumers[j]->id) continue;
+            for (int k = 0; k < sq->cls.size(); k++)
+                sq->cls[k]->increase_refs(1);
+            sq->consumers[j]->import_clauses_from(sq->cls);
+        }
+        for (int k = 0; k < sq->cls.size(); k++)
+            sq->cls[k]->free_clause();
+            
+    }
+    return NULL;
+}
+
+int sharer::sort_clauses(int x) {
+    vec<vec<clause_store *>> *buck = &bucket[x];
+    for (int i = 0; i < cls.size(); i++) {
+        int sz = cls[i]->size;
+        while (sz > buck->size()) buck->push();
+        if (sz * (buck[sz - 1].size() + 1) <= share_lits) 
+            buck[sz - 1].push(cls[i]);
+        else
+            cls[i]->free_clause();
+    }
+    cls.clear();
+    int space = share_lits;
+    for (int i = 0; i < buck->size(); i++) {
+        int clause_num = space / (i + 1);
+        if (!clause_num) return;
+        if (clause_num >= buck[i].size()) {
+            space -= buck[i].size() * (i + 1);
+            for (int j = 0; j < buck[i].size(); j++)
+                cls.push(buck[i][j]);
+            buck[i].clear();
+        }
+        else {
+            space -= clause_num * (i + 1);
+            for (int j = 0; j < clause_num; j++) {
+                cls.push(buck[i].last());
+                buck[i].pop();
+            }
+        }
+    }
+    return (share_lits - space) * 100 / share_lits;
+}
+
+void light::share() {
+    int sharers_number = 1;
+    for (int i = 0; i < sharers_number; i++) {
+        sharer* s = new sharer(i, OPT(share_intv), OPT(share_lits));
+        s->producers.push(workers[0]);
+        s->consumers.push(workers[1]);
+        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, shares[i]);
+    }
+
+}
\ No newline at end of file
diff --git a/workers/sharer.hpp b/workers/sharer.hpp
new file mode 100644
index 0000000..b29a191
--- /dev/null
+++ b/workers/sharer.hpp
@@ -0,0 +1,22 @@
+#ifndef _sharer_hpp_INCLUDED
+#define _sharer_hpp_INCLUDED
+#include "../utils/paras.hpp"
+
+class basesolver;
+class sharer {
+public:
+    int id;
+    int share_intv, share_lits;
+    vec<vec<clause_store *>> bucket[32]; //need to update
+    vec<basesolver *> producers, consumers;
+    vec<clause_store *> cls;
+    sharer(int idx, int intv, int lits) {
+        share_intv = intv;
+        share_lits = lits;
+        id = idx;
+    }
+
+    int sort_clauses(int x);
+};
+
+#endif
\ No newline at end of file