unfinish v1.2

.vscode/settings.json

@@ -53,6 +53,8 @@
         "sstream": "cpp",
         "stdexcept": "cpp",
         "streambuf": "cpp",
-        "cinttypes": "cpp"
+        "cinttypes": "cpp",
+        "assert.h": "c",
+        "bitset": "cpp"
     }
 }

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();

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++)

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;
+}

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

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;

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;

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;
+}

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

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);

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") \
     

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) {
+    
 }

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;
 };

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;
 

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

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]);
+    }
+
+}

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