version 1.1 (add dynamically reseting)

build.sh

@@ -0,0 +1,5 @@
+cd /home/chenzh/solvers/Light/solvers/kissat-inc;
+./configure && make;
+cd ..;
+cd ..;
+make clean; make;

light.cpp

@@ -16,8 +16,8 @@ light::light():
 }
 
 light::~light() {
-    for (int i = 0; i < solvers.size(); i++) delete(solvers[i]);
+    for (int i = 0; i < workers.size(); i++) delete(workers[i]);
-    solvers.clear(true);
+    workers.clear(true);
 }
 
 void light::arg_parse(int argc, char **argv) {

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 init_workers();
-    void diversity_solvers();
+    void diversity_workers();
     void parse_input();
     int  run();
     int  solve();
-    void terminate_solvers();
+    void terminate_workers();
     void print_model();
 };
 

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,16 +298,18 @@ 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;
         int l = clause[i].size();
@@ -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];

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,17 +74,38 @@ 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);
     }    
@@ -92,8 +114,8 @@ int light::solve() {
 }
 
 int light::run() {
-    init_solvers();
+    init_workers();
-    diversity_solvers();
+    diversity_workers();
     if (OPT(simplify)) {
         pre = new preprocess();
         int res = pre->do_preprocess(filename);

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 BUILD "Wed Aug 31 12:28:43 CST 2022 Linux seed1 5.4.0-120-generic x86_64"
-#define DIR "/home/chenzh/solvers/Light/kissat-inc/build"
+#define DIR "/home/chenzh/solvers/Light/solvers/kissat-inc/build"

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
+	rm -f "/home/chenzh/solvers/Light/solvers/kissat-inc"/makefile
-	-$(MAKE) -C "/home/chenzh/solvers/Light/kissat-inc/build" clean
+	-$(MAKE) -C "/home/chenzh/solvers/Light/solvers/kissat-inc/build" clean
-	rm -rf "/home/chenzh/solvers/Light/kissat-inc/build"
+	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

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

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

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

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

solvers/kissat-inc/src/search.c

@@ -113,7 +113,8 @@ stop_search (kissat * solver, int res)
     REPORT(0, '}');
     STOP(focused);
   }
-  char type = (res == 10 ? '1' : res == 20 ? '0' : '?');
+  char type = (res == 10 ? '1' : res == 20 ? '0'
+                                           : '?');
   REPORT(0, type);
 #else
   (void)res;
@@ -137,8 +138,7 @@ conflict_limit_hit (kissat * solver)
     return false;
   if (solver->limits.conflicts > solver->statistics.conflicts)
     return false;
-  kissat_very_verbose (solver, "conflict limit %" PRIu64
+  kissat_very_verbose(solver, "conflict limit %" PRIu64 " hit after %" PRIu64 " conflicts",
-		       " hit after %" PRIu64 " conflicts",
                       solver->limits.conflicts,
                       solver->statistics.conflicts);
   return true;
@@ -151,15 +151,13 @@ decision_limit_hit (kissat * solver)
     return false;
   if (solver->limits.decisions > solver->statistics.decisions)
     return false;
-  kissat_very_verbose (solver, "decision limit %" PRIu64
+  kissat_very_verbose(solver, "decision limit %" PRIu64 " hit after %" PRIu64 " decisions",
-		       " hit after %" PRIu64 " decisions",
                       solver->limits.decisions,
                       solver->statistics.decisions);
   return true;
 }
 
-int
+int kissat_search(kissat *solver)
-kissat_search (kissat * solver)
 {
   start_search(solver);
 
@@ -167,6 +165,11 @@ kissat_search (kissat * solver)
 
   while (!res)
   {
+    if (!solver->level && solver->reseting)
+    {
+      kissat_shuffle_score(solver);
+      solver->reseting = 0;
+    }
     clause *conflict = kissat_search_propagate(solver);
     if (conflict)
       res = kissat_analyze(solver, conflict);

utils/paras.hpp

@@ -7,6 +7,8 @@
 //        name,      type,   default, low, high, comments
 #define PARAS \
     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") \

version.md

@@ -0,0 +1,5 @@
+### 1.0
+base Framework
+RS
+#### 1.1
+Dynamically reseting

workers/basekissat.cpp

@@ -58,3 +58,12 @@ void basekissat::get_model(vec<int> &model) {
       model.push(tmp);
    }
 }
+
+int basekissat::get_reset_data() {
+    return solver->best_assigned;
+}
+
+
+void basekissat::reset() {
+    solver->reseting = 1;
+}

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

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;