version 3.-1

light.hpp

@@ -5,12 +5,14 @@
 #include "preprocess.hpp"
 #include <atomic>
 #include <iostream>
+#include <mutex>
 typedef long long ll;
 
 class basesolver;
 class sharer;
 
 extern std::atomic<int> terminated;
+extern std::mutex mtx;
 
 struct thread_inf{
     int id, inf;

makefile

@@ -5,7 +5,7 @@ OBJS = $(addsuffix .o, $(basename $(SRCS)))
 EXEC = light
 
 LIBS = -lkissat -Lsolvers/kissat-inc/build/ \
-       -lpthread -lz -lm -static
+       -lpthread -pthread -lz -lm -lboost_thread -lboost_date_time -lboost_system -static
 
 CXXFLAGS = -Isolvers/kissat-inc -std=c++11 -O3
 

res.txt

@@ -1,374 +0,0 @@
-c ------------------- Paras list -------------------
-c Name                	 Type      	 Now       	 Default   	 Comment
-c mode                	 int       	 0         	 0         	 SAT=1, UNSAT=2
-c reset               	 int       	 0         	 0         	 Dynamically reseting
-c reset_time          	 int       	 10        	 10        	 Reseting base interval (seconds)
-c share               	 int       	 1         	 0         	 Sharing learnt clauses
-c share_intv          	 int       	 500000    	 500000    	 Sharing interval (microseconds)
-c share_lits          	 int       	 1500      	 1500      	 Sharing lits (per every #share_intv seconds)
-c simplify            	 int       	 1         	 1         	 Use Simplify (only preprocess)
-c times               	 double    	 5000.000000	 5000      	 Cutoff time
-c threads             	 int       	 2         	 32        	 Thread number
-c --------------------------------------------------
-c filename: /pub/data/chenzh/data/sat2021/WS_500_16_70_10.apx_0.cnf
-c After preprocess: vars: 1500 -> 998 , clauses: 11501 -> 9964 ,
-c After preprocess: vars: 998 -> 498 , clauses: 9964 -> 8962 ,
-c -----------------solve start----------------------
-start sharing 500000
-get 101 exported clauses
-get 100 exported clauses
--106 67 
--240 213 
--480 67 
--312 4 
--148 16 -261 
--488 83 130 
--163 472 56 
--103 -93 94 
--240 352 213 
--182 284 81 
--265 431 443 
--453 314 228 
--396 168 343 
--336 -261 177 
--429 314 228 
--299 148 91 
--265 176 16 
--299 148 91 
--240 15 213 
--41 83 253 
--229 228 372 
--381 359 130 
--100 148 91 
-376 182 -5 
--316 201 377 
--293 385 86 
--6 472 56 
--182 284 81 
-261 56 4 
--148 16 -261 
--100 91 -261 
--34 94 95 
--182 81 284 
--266 16 177 
--67 270 15 
-9 -148 56 
--41 83 253 
--79 216 42 
--40 143 56 
--111 408 182 
--182 284 81 
--256 372 314 
--391 65 310 249 
-101 96 -93 94 
--103 96 -93 94 
--34 95 96 94 
--227 128 77 71 
-76 96 -93 94 
--231 35 153 199 
--377 382 34 47 
--220 331 -11 467 
--192 431 443 299 
--154 -230 153 5 
--293 385 86 118 
--303 386 47 341 
--378 168 345 343 
--243 -409 319 397 
--280 312 103 -241 
--91 95 96 79 
--432 339 178 402 
--438 40 207 119 
--304 158 34 394 
--212 7 346 166 
--480 79 96 95 
--272 341 182 -302 
--237 239 319 182 
-376 -302 182 341 
--303 386 47 341 
--239 386 47 341 
--61 -401 120 65 
--406 318 65 238 57 
--360 423 -9 58 319 
--79 216 137 -93 42 
--167 372 482 174 479 
--19 -93 58 319 423 
--127 216 137 -93 42 
--312 -93 58 319 423 
--360 -261 16 412 388 
--148 312 -261 49 320 
--154 413 257 77 409 
--5 237 281 400 178 
--42 127 344 235 317 
--163 465 39 325 56 
--209 304 158 395 -166 
--83 33 34 290 -236 
-241 395 435 98 343 
--322 66 58 -93 319 423 
--191 301 -425 171 365 159 
--67 37 181 124 472 56 
--322 352 213 5 -156 487 
--255 169 5 409 -59 192 
--489 78 278 110 327 48 
--73 158 395 304 342 377 
--243 435 319 136 22 397 
--32 237 394 314 19 439 305 
--111 69 240 46 220 237 238 
--18 56 58 55 4 54 57 42 
-395 243 90 98 435 392 48 -376 231 
--131 391 5 421 6 25 -9 388 221 
--316 339 314 160 197 343 133 369 57 377 415 
--480 67 
--240 213 
--106 67 
--488 83 130 
--488 83 130 
--44 177 176 
--67 15 270 
--103 -93 94 
--42 352 270 
--163 472 56 
--91 76 96 
--316 201 377 
--6 472 56 
--148 -261 16 
-302 143 56 
-261 4 56 
--299 91 148 
--434 433 423 
--100 91 148 
--148 -261 16 
--34 95 94 
--396 168 343 
--182 284 81 
--61 284 81 
--111 408 182 
--488 130 83 
--293 86 385 
--148 4 16 
--202 241 385 
--40 56 143 
--62 315 303 
--231 -338 153 
--41 253 83 
-261 4 56 
--100 -261 91 
--336 -261 177 
--96 42 138 
--229 228 372 
--67 15 270 
--111 182 408 
--266 16 177 
--42 270 352 
--44 176 177 
--256 314 372 
--267 179 151 
--138 96 94 95 
--280 103 312 -241 
--488 178 339 402 
--328 372 310 208 
--238 433 77 423 
--237 56 207 406 
--351 385 118 86 
--237 182 319 239 
--293 86 385 118 
--446 213 183 115 
-241 385 123 118 
-230 386 -315 277 
--244 215 64 334 
--467 413 389 78 
--127 -302 386 182 
--338 -230 5 153 
--377 382 34 47 
--432 339 402 178 
--141 129 303 389 
-425 182 341 47 
--190 312 -241 103 
--148 339 160 209 
--356 124 208 372 
--294 128 127 71 
--73 158 -386 304 
--402 77 413 409 157 
--100 419 111 436 303 
-302 449 484 45 409 
--441 463 330 90 19 
-53 423 -93 319 92 
--112 303 419 111 436 
--237 301 77 313 359 
--401 238 120 65 318 
-4 -241 103 49 67 
--111 -148 47 341 386 
--343 327 16 -261 387 
--402 413 77 157 409 
--80 360 471 267 31 
--57 160 197 339 314 
--164 -182 160 209 178 
--498 409 449 32 307 
--37 354 113 99 80 135 
--29 -261 75 37 472 124 
--244 454 5 277 386 204 
--343 327 16 387 209 -261 
--57 51 331 316 8 354 
--386 379 378 111 75 23 
--83 33 34 290 8 -236 
--138 113 102 96 91 131 
-156 321 463 331 135 146 -53 
--70 91 89 88 86 92 90 
--204 107 127 249 314 311 -236 
--446 178 202 327 313 69 294 
--489 -241 294 326 131 188 351 
--490 -193 237 400 64 38 71 121 
--369 293 244 -226 326 231 325 318 472 56 67 
-start sharing 500000
-get 135 exported clauses
-get 157 exported clauses
--381 -41 
--103 -299 
--265 16 176 
-376 -303 341 
--103 217 148 
--265 431 443 
--41 83 253 
--129 314 228 
-302 56 143 
--148 4 16 
--122 99 166 7 
--102 95 -93 94 
--401 -230 -212 449 
--265 431 299 443 
--41 151 325 253 
--43 -127 148 150 
--44 433 18 -233 
--148 -280 312 -261 
--131 42 216 302 
--204 153 5 35 
--382 95 -93 79 
--282 47 386 182 
--488 83 228 281 
--29 207 333 42 
--237 313 359 301 
--48 -41 377 201 
--112 127 121 -66 
--83 185 90 -92 
--388 423 415 449 
--83 -166 11 80 
--69 202 74 382 
--293 494 485 466 
--212 67 385 75 
--433 160 178 339 
--211 263 56 4 
--237 406 207 56 
-1 67 377 51 
--141 303 389 129 
--91 96 95 79 
--409 143 -235 395 
--400 389 20 182 
--227 338 -428 200 
--111 176 177 408 
-302 231 -397 277 
--397 -160 -237 -127 
--477 123 118 180 
-1 67 377 51 
--119 406 439 108 
--359 476 147 433 
--313 147 423 476 
--106 96 -93 79 
--294 71 128 127 
--386 63 274 398 142 
--11 445 267 360 471 
--428 338 200 161 187 
--77 102 111 121 64 
--69 76 229 -93 202 
--220 42 355 454 437 
--269 -111 240 237 238 
--290 325 112 297 39 
--243 22 136 397 319 
--255 395 343 98 90 
--224 -93 96 94 42 
--312 -431 157 470 441 
--120 237 -193 178 400 
--471 427 395 392 -376 
-302 201 34 144 382 
--83 34 33 290 -236 
--144 483 -412 163 -101 
--194 -83 -92 103 320 
--185 415 2 125 474 
--142 332 240 58 38 
--190 136 16 111 303 
--5 237 281 400 178 
--91 138 34 216 42 
--112 127 274 121 106 
--117 363 122 24 461 
--92 -305 -407 424 313 
--488 494 163 244 83 
-376 -186 111 163 323 
--392 338 200 372 161 
--136 257 157 24 413 
--250 233 234 235 232 
--229 359 65 228 77 
--195 400 237 281 178 
--122 54 323 265 305 
--130 313 65 77 228 
--350 387 17 458 400 
--83 -236 34 290 33 
--356 343 351 152 456 
--92 471 164 31 445 
--264 -230 58 451 50 47 
--43 150 95 96 -93 148 
--90 65 120 318 314 281 
--69 34 290 331 8 467 
--19 190 467 -61 395 197 
--320 420 -271 350 426 233 
--47 246 115 24 381 301 
--343 123 -399 49 408 116 
--311 346 379 395 316 373 
--247 454 277 386 199 153 
--280 215 374 38 240 58 
--361 34 290 -236 467 33 
--171 6 369 352 166 213 
-399 152 61 248 274 322 
--387 301 171 365 -425 368 
--305 -407 330 375 424 313 
--475 188 15 195 39 169 
--243 331 8 451 316 354 
--48 230 277 454 201 8 
--96 111 71 121 64 138 
--269 -97 100 55 99 98 
--111 238 69 220 240 237 
--320 304 115 246 301 24 
-76 476 253 130 147 433 
--95 472 -261 144 37 181 
-193 147 339 221 -359 448 
-412 -177 387 449 423 327 
--269 30 484 320 47 130 83 
--373 27 495 54 223 161 122 
--5 214 221 24 329 127 470 
--130 281 228 343 435 243 395 
--176 165 162 205 443 303 197 
--345 290 227 388 18 122 433 
--496 227 47 138 -76 127 266 
--67 275 39 377 327 215 496 
--35 402 160 209 78 48 -489 
-207 356 40 340 439 108 406 
--384 -221 67 -93 128 303 423 
--297 99 100 -88 55 340 40 
--24 189 -1 -226 227 229 228 
--325 -341 131 64 221 69 312 
--220 340 119 356 415 326 125 
--132 -53 68 38 312 18 484 
--237 359 301 228 147 423 476 
--103 67 100 -341 163 -85 -487 
--103 -93 -341 163 -85 -487 100 
-302 138 127 227 -185 415 125 -76 
--163 465 -177 490 290 197 34 -83 
--352 258 237 100 177 58 489 164 
--22 487 -156 391 65 431 465 299 
--319 303 206 136 158 16 -497 130 
--31 377 483 -123 -101 275 -412 163 
--293 -140 180 166 123 7 163 99 
--103 443 144 335 205 60 433 -359 
--486 451 90 19 330 267 406 359 253 
--233 -1 207 208 7 -24 127 346 11 
--90 -202 16 -261 209 322 323 -302 324 
--281 462 439 490 37 418 356 421 391 -156 
-405 280 269 -308 161 235 -108 294 167 478 
-301 115 304 24 246 385 17 75 -241 103 49 

solve.cpp

@@ -1,10 +1,13 @@
 #include "light.hpp"
 #include "workers/basekissat.hpp"
+#include "workers/sharer.hpp"
 #include <unistd.h>
 #include <chrono>
 #include <algorithm>
+#include <mutex>
 auto clk_st = std::chrono::high_resolution_clock::now();
 char* worker_sign = "";
+std::mutex mtx;
 std::atomic<int> terminated;
 int result = 0;
 int winner;
@@ -28,13 +31,15 @@ void * solve_worker(void *arg) {
             sq->get_model(seq_model);
         }
         if (res && !terminated) {
-            sq->controller->terminate_workers();
+            printf("c result: %d, winner is %d\n", res, sq->id);
             terminated = 1;
+            sq->controller->terminate_workers();
             result = res;
             winner = sq->id;
             if (res == 10) seq_model.copyTo(model);
         }
         seq_model.clear();
+        // printf("get result %d with res %d\n", sq->id, res);
    }
    return NULL;
 }
@@ -57,6 +62,9 @@ void light::terminate_workers() {
     for (int i = 0; i < OPT(threads); i++) {
         workers[i]->terminate();
     }
+    for (int i = 0; i < sharers.size(); i++) {
+        sharers[i]->set_terminated();
+    }
 }
 
 void light::parse_input() {
@@ -105,7 +113,7 @@ int light::solve() {
             puts("\n");
         }
     }
-    printf("ending solve\n");
+    // printf("ending solve\n");
     terminate_workers();
 
     for (int i = 0; i < OPT(threads); i++) {
@@ -125,7 +133,7 @@ int light::run() {
     }
     else worker_sign = filename;
     parse_input();
-    share();
+    if (OPT(share)) share();
     int res = solve();
     if (res == 10 && OPT(simplify)) {
         for (int i = 1; i <= pre->orivars; i++)

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 Sep 15 10:12:48 CST 2022 Linux seed1 5.4.0-120-generic x86_64"
+#define BUILD "Sun Dec 4 22:20:13 CST 2022 Linux seed1 5.4.0-120-generic x86_64"
 #define DIR "/home/chenzh/solvers/Light/solvers/kissat-inc/build"

solvers/kissat-inc/src/analyze.c

@@ -11,12 +11,12 @@
 #define INVALID_LEVEL UINT_MAX
 
 static bool
-one_literal_on_conflict_level (kissat * solver,
-			       clause * conflict,
-			       unsigned *conflict_level_ptr)
+one_literal_on_conflict_level(kissat *solver,
+                              clause *conflict,
+                              unsigned *conflict_level_ptr)
 {
-  assert (conflict);
-  assert (conflict->size > 1);
+  assert(conflict);
+  assert(conflict->size > 1);
 
   unsigned conflict_level = INVALID_LEVEL;
   unsigned literals_on_conflict_level = 0;
@@ -29,246 +29,244 @@ one_literal_on_conflict_level (kissat * solver,
   const unsigned *end_of_lits = lits + conflict_size;
 
   for (const unsigned *p = lits; p != end_of_lits; p++)
+  {
+    const unsigned lit = *p;
+    assert(VALUE(lit) < 0);
+    const unsigned idx = IDX(lit);
+    const unsigned level = all_assigned[idx].level;
+    if (conflict_level == level)
     {
-      const unsigned lit = *p;
-      assert (VALUE (lit) < 0);
-      const unsigned idx = IDX (lit);
-      const unsigned level = all_assigned[idx].level;
-      if (conflict_level == level)
-	{
-	  if (++literals_on_conflict_level > 1 && level == solver->level)
-	    break;
-	}
-      else if (conflict_level == INVALID_LEVEL || conflict_level < level)
-	{
-	  forced_lit = lit;
-	  conflict_level = level;
-	  literals_on_conflict_level = 1;
-	}
+      if (++literals_on_conflict_level > 1 && level == solver->level)
+        break;
     }
-  assert (conflict_level != INVALID_LEVEL);
-  assert (literals_on_conflict_level);
+    else if (conflict_level == INVALID_LEVEL || conflict_level < level)
+    {
+      forced_lit = lit;
+      conflict_level = level;
+      literals_on_conflict_level = 1;
+    }
+  }
+  assert(conflict_level != INVALID_LEVEL);
+  assert(literals_on_conflict_level);
 
-  LOG ("found %u literals on conflict level %u",
-       literals_on_conflict_level, conflict_level);
+  LOG("found %u literals on conflict level %u",
+      literals_on_conflict_level, conflict_level);
   *conflict_level_ptr = conflict_level;
 
   if (!conflict_level)
-    {
-      solver->inconsistent = true;
-      LOG ("learned empty clause from conflict at conflict level zero");
-      CHECK_AND_ADD_EMPTY ();
-      ADD_EMPTY_TO_PROOF ();
-      return false;
-    }
+  {
+    solver->inconsistent = true;
+    LOG("learned empty clause from conflict at conflict level zero");
+    CHECK_AND_ADD_EMPTY();
+    ADD_EMPTY_TO_PROOF();
+    return false;
+  }
 
   if (conflict_level < solver->level)
-    {
-      LOG ("forced backtracking due to conflict level %u < level %u",
-	   conflict_level, solver->level);
-      kissat_backtrack (solver, conflict_level);
-    }
+  {
+    LOG("forced backtracking due to conflict level %u < level %u",
+        conflict_level, solver->level);
+    kissat_backtrack(solver, conflict_level);
+  }
 
   if (conflict_size > 2)
+  {
+    for (unsigned i = 0; i < 2; i++)
     {
-      for (unsigned i = 0; i < 2; i++)
-	{
-	  const unsigned lit = lits[i];
-	  const unsigned lit_idx = IDX (lit);
-	  unsigned highest_position = i;
-	  unsigned highest_literal = lit;
-	  unsigned highest_level = all_assigned[lit_idx].level;
-	  for (unsigned j = i + 1; j < conflict_size; j++)
-	    {
-	      const unsigned other = lits[j];
-	      const unsigned other_idx = IDX (other);
-	      const unsigned level = all_assigned[other_idx].level;
-	      if (highest_level >= level)
-		continue;
-	      highest_literal = other;
-	      highest_position = j;
-	      highest_level = level;
-	      if (highest_level == conflict_level)
-		break;
-	    }
-	  if (highest_position == i)
-	    continue;
-	  reference ref = INVALID_REF;
-	  if (highest_position > 1)
-	    {
-	      ref = kissat_reference_clause (solver, conflict);
-	      kissat_unwatch_blocking (solver, lit, ref);
-	    }
-	  lits[highest_position] = lit;
-	  lits[i] = highest_literal;
-	  if (highest_position > 1)
-	    kissat_watch_blocking (solver, lits[i], lits[!i], ref);
-	}
+      const unsigned lit = lits[i];
+      const unsigned lit_idx = IDX(lit);
+      unsigned highest_position = i;
+      unsigned highest_literal = lit;
+      unsigned highest_level = all_assigned[lit_idx].level;
+      for (unsigned j = i + 1; j < conflict_size; j++)
+      {
+        const unsigned other = lits[j];
+        const unsigned other_idx = IDX(other);
+        const unsigned level = all_assigned[other_idx].level;
+        if (highest_level >= level)
+          continue;
+        highest_literal = other;
+        highest_position = j;
+        highest_level = level;
+        if (highest_level == conflict_level)
+          break;
+      }
+      if (highest_position == i)
+        continue;
+      reference ref = INVALID_REF;
+      if (highest_position > 1)
+      {
+        ref = kissat_reference_clause(solver, conflict);
+        kissat_unwatch_blocking(solver, lit, ref);
+      }
+      lits[highest_position] = lit;
+      lits[i] = highest_literal;
+      if (highest_position > 1)
+        kissat_watch_blocking(solver, lits[i], lits[!i], ref);
     }
+  }
 
   if (literals_on_conflict_level > 1)
     return false;
 
-  assert (literals_on_conflict_level == 1);
-  assert (forced_lit != INVALID_LIT);
+  assert(literals_on_conflict_level == 1);
+  assert(forced_lit != INVALID_LIT);
 
-  LOG ("reusing conflict as driving clause of %s", LOGLIT (forced_lit));
-  kissat_backtrack (solver, solver->level - 1);
+  LOG("reusing conflict as driving clause of %s", LOGLIT(forced_lit));
+  kissat_backtrack(solver, solver->level - 1);
   if (conflict_size == 2)
-    {
-      assert (conflict == &solver->conflict);
-      const unsigned other = lits[0] ^ lits[1] ^ forced_lit;
-      kissat_assign_binary (solver, conflict->redundant, forced_lit, other);
-    }
+  {
+    assert(conflict == &solver->conflict);
+    const unsigned other = lits[0] ^ lits[1] ^ forced_lit;
+    kissat_assign_binary(solver, conflict->redundant, forced_lit, other);
+  }
   else
-    {
-      const reference ref = kissat_reference_clause (solver, conflict);
-      kissat_assign_reference (solver, forced_lit, ref, conflict);
-    }
+  {
+    const reference ref = kissat_reference_clause(solver, conflict);
+    kissat_assign_reference(solver, forced_lit, ref, conflict);
+  }
 
   return true;
 }
 
 static void
-mark_literal_as_analyzed (kissat * solver, assigned * all_assigned,
-			  unsigned lit, const char *type)
+mark_literal_as_analyzed(kissat *solver, assigned *all_assigned,
+                         unsigned lit, const char *type)
 {
-  const unsigned idx = IDX (lit);
+  const unsigned idx = IDX(lit);
   assigned *a = all_assigned + idx;
   if (a->analyzed == ANALYZED)
     return;
   a->analyzed = ANALYZED;
-  LOG ("marking %s literal %s as analyzed", type, LOGLIT (lit));
-  PUSH_STACK (solver->analyzed, idx);
-  (void) type;
+  LOG("marking %s literal %s as analyzed", type, LOGLIT(lit));
+  PUSH_STACK(solver->analyzed, idx);
+  (void)type;
 }
 
 static inline void
-analyze_reason_side_literals (kissat * solver)
+analyze_reason_side_literals(kissat *solver)
 {
-  assert (!solver->probing);
-  if (!GET_OPTION (bumpreasons))
+  assert(!solver->probing);
+  if (!GET_OPTION(bumpreasons))
     return;
   assigned *all_assigned = solver->assigned;
-  for (all_stack (unsigned, lit, solver->clause.lits))
-      all_assigned[IDX (lit)].analyzed = ANALYZED;
-  word *arena = BEGIN_STACK (solver->arena);
-  for (all_stack (unsigned, lit, solver->clause.lits))
+  for (all_stack(unsigned, lit, solver->clause.lits))
+    all_assigned[IDX(lit)].analyzed = ANALYZED;
+  word *arena = BEGIN_STACK(solver->arena);
+  for (all_stack(unsigned, lit, solver->clause.lits))
+  {
+    const unsigned idx = IDX(lit);
+    assigned *a = all_assigned + idx;
+    assert(a->level > 0);
+    assert(a->reason != UNIT);
+    if (a->reason == DECISION)
+      continue;
+    if (a->binary)
+      mark_literal_as_analyzed(solver, all_assigned, a->reason,
+                               "reason side");
+    else
     {
-      const unsigned idx = IDX (lit);
-      assigned *a = all_assigned + idx;
-      assert (a->level > 0);
-      assert (a->reason != UNIT);
-      if (a->reason == DECISION)
-	continue;
-      if (a->binary)
-	mark_literal_as_analyzed (solver, all_assigned, a->reason,
-				  "reason side");
-      else
-	{
-	  assert (a->reason < SIZE_STACK (solver->arena));
-	  clause *c = (clause *) (arena + a->reason);
-	  for (all_literals_in_clause (lit, c))
-	    if (IDX (lit) != idx)
-	      mark_literal_as_analyzed (solver, all_assigned, lit,
-					"reason side");
-	}
+      assert(a->reason < SIZE_STACK(solver->arena));
+      clause *c = (clause *)(arena + a->reason);
+      for (all_literals_in_clause(lit, c))
+        if (IDX(lit) != idx)
+          mark_literal_as_analyzed(solver, all_assigned, lit,
+                                   "reason side");
     }
+  }
 }
 
 static void
-reset_levels (kissat * solver)
+reset_levels(kissat *solver)
 {
-  LOG ("reset %zu marked levels", SIZE_STACK (solver->levels));
-  frame *frames = BEGIN_STACK (solver->frames);
-  for (all_stack (unsigned, level, solver->levels))
-    {
-      assert (level < SIZE_STACK (solver->frames));
-      frame *f = frames + level;
-      assert (f->used > 0);
-      f->used = 0;
-    }
-  CLEAR_STACK (solver->levels);
+  LOG("reset %zu marked levels", SIZE_STACK(solver->levels));
+  frame *frames = BEGIN_STACK(solver->frames);
+  for (all_stack(unsigned, level, solver->levels))
+  {
+    assert(level < SIZE_STACK(solver->frames));
+    frame *f = frames + level;
+    assert(f->used > 0);
+    f->used = 0;
+  }
+  CLEAR_STACK(solver->levels);
 }
 
 static void
-reset_markings (kissat * solver)
+reset_markings(kissat *solver)
 {
-  LOG ("unmarking %zu analyzed variables", SIZE_STACK (solver->analyzed));
+  LOG("unmarking %zu analyzed variables", SIZE_STACK(solver->analyzed));
   assigned *all_assigned = solver->assigned;
-  for (all_stack (unsigned, idx, solver->analyzed))
-      all_assigned[idx].analyzed = 0;
+  for (all_stack(unsigned, idx, solver->analyzed))
+    all_assigned[idx].analyzed = 0;
 }
 
 static void
-reset_analyze (kissat * solver)
+reset_analyze(kissat *solver)
 {
-  LOG ("reset %zu analyzed variables", SIZE_STACK (solver->analyzed));
-  CLEAR_STACK (solver->analyzed);
+  LOG("reset %zu analyzed variables", SIZE_STACK(solver->analyzed));
+  CLEAR_STACK(solver->analyzed);
 
-  LOG ("reset %zu learned literals", SIZE_STACK (solver->clause.lits));
-  CLEAR_STACK (solver->clause.lits);
+  LOG("reset %zu learned literals", SIZE_STACK(solver->clause.lits));
+  CLEAR_STACK(solver->clause.lits);
 }
 
 static void
-update_trail_average (kissat * solver)
+update_trail_average(kissat *solver)
 {
-  assert (!solver->probing);
-  const unsigned size = SIZE_STACK (solver->trail);
+  assert(!solver->probing);
+  const unsigned size = SIZE_STACK(solver->trail);
   const unsigned assigned = size - solver->unflushed;
   const unsigned active = solver->active;
-  const double filled = kissat_percent (assigned, active);
-  LOG ("trail filled %.0f%% (size %u, unflushed %u, active %u)",
-       filled, size, solver->unflushed, active);
-  UPDATE (trail, filled);
+  const double filled = kissat_percent(assigned, active);
+  LOG("trail filled %.0f%% (size %u, unflushed %u, active %u)",
+      filled, size, solver->unflushed, active);
+  UPDATE(trail, filled);
 }
 
-int
-kissat_analyze (kissat * solver, clause * conflict)
+int kissat_analyze(kissat *solver, clause *conflict)
 {
-  assert (!solver->inconsistent);
-  START (analyze);
+  assert(!solver->inconsistent);
+  START(analyze);
   if (!solver->probing)
-    {
-      update_trail_average (solver);
-      UPDATE (level, solver->level);
-    }
+  {
+    update_trail_average(solver);
+    UPDATE(level, solver->level);
+  }
   int res;
   do
+  {
+    LOGCLS(conflict, "analyzing conflict %" PRIu64, CONFLICTS);
+    unsigned conflict_level;
+    if (one_literal_on_conflict_level(solver, conflict, &conflict_level))
+      res = 1;
+    else if (!conflict_level)
+      res = -1;
+    else if ((conflict = kissat_deduce_first_uip_clause(solver, conflict)))
     {
-      LOGCLS (conflict, "analyzing conflict %" PRIu64, CONFLICTS);
-      unsigned conflict_level;
-      if (one_literal_on_conflict_level (solver, conflict, &conflict_level))
-	res = 1;
-      else if (!conflict_level)
-	res = -1;
-      else if ((conflict = kissat_deduce_first_uip_clause (solver, conflict)))
-	{
-	  reset_markings (solver);
-	  reset_analyze (solver);
-	  reset_levels (solver);
-	  res = 0;
-	}
-      else
-	{
-	  kissat_minimize_clause (solver);
-	  if (!solver->probing)
-	    analyze_reason_side_literals (solver);
-	  reset_markings (solver);
-	  kissat_learn_clause (solver);
-
-	  // MAB
-	  if (!solver->probing && (!solver->stable || solver->heuristic==0))
-	    kissat_bump_variables (solver);
-	  if(!solver->probing && solver->stable && (solver->heuristic==1))
-	    kissat_update_conflicted_chb (solver);
-          
-	  reset_analyze (solver);
-	  reset_levels (solver);
-	  res = 1;
-	}
+      reset_markings(solver);
+      reset_analyze(solver);
+      reset_levels(solver);
+      res = 0;
     }
-  while (!res);
-  STOP (analyze);
+    else
+    {
+      kissat_minimize_clause(solver);
+      if (!solver->probing)
+        analyze_reason_side_literals(solver);
+      reset_markings(solver);
+      kissat_learn_clause(solver);
+      solver->nconflict++;
+      // MAB
+      if (!solver->probing && (!solver->stable || solver->heuristic == 0))
+        kissat_bump_variables(solver);
+      if (!solver->probing && solver->stable && (solver->heuristic == 1))
+        kissat_update_conflicted_chb(solver);
+
+      reset_analyze(solver);
+      reset_levels(solver);
+      res = 1;
+    }
+  } while (!res);
+  STOP(analyze);
   return res > 0 ? 0 : 20;
 }

solvers/kissat-inc/src/internal.c

@@ -33,6 +33,7 @@ kissat_init (void)
   solver->exportedClause = cvec_init();
   kissat_init_queue (&solver->queue);
   kissat_push_frame (solver, INVALID_LIT);
+  solver->nconflict = 0;
   solver->watching = true;
   solver->conflict.size = 2;
   solver->conflict.keep = true;
@@ -183,18 +184,19 @@ kissat_reserve (kissat * solver, int max_var)
     
   if (solver->order_reset != -1)
   {
-    srand(solver->order_reset);
+    // srand(solver->order_reset);
     int *id;
     id = (int *)malloc(sizeof(int) * (max_var + 1));
     for (int i = 1; i <= max_var; i++)
       id[i] = i;
     for (int i = 1; i <= max_var; i++)
     {
-      int j = (rand() % max_var) + 1;
+      int j = (rand_r(&solver->order_reset) % max_var) + 1;
       int x = id[i];
       id[i] = id[j];
       id[j] = x;
     }
+    // printf("c mxavar is %d, first is %d, tenth is %d\n", max_var, id[1], id[10]);
     for (int i = 1; i <= max_var; i++)
       kissat_activate_literal(solver, kissat_import_literal(solver, id[i]));
     free(id);

solvers/kissat-inc/src/internal.h

@@ -75,11 +75,13 @@ struct kissat
 {
   int  (* cbkImportUnit)  (void *);
   int  (* cbkImportClause)(void *, int *, cvec *);
-  void (* cbkExportClause)(void *, int, cvec *);	        // callback for clause learning
+  void (* cbkExportClause)(void *, int, cvec *);	        
+  void (* cbkWaitSharing) (void *);           // callback for clause learning
 
   cvec *importedClause;
   cvec *exportedClause;
   void *issuer;
+  int nconflict;
   int reseting;
   int order_reset;
   int max_var;

solvers/kissat-inc/src/search.c

@@ -170,7 +170,10 @@ int kissat_search(kissat *solver)
       kissat_shuffle_score(solver);
       solver->reseting = 0;
     }
-    if (!solver->level) {
+    if (!solver->level && solver->nconflict >= 10000) {
+      solver->nconflict = 0;
+      if (solver->cbkWaitSharing != NULL) 
+        solver->cbkWaitSharing(solver->issuer);
       if (!kissat_importUnitClauses(solver)) return 20;
       if (!kissat_importClauses(solver)) return 20;
     }

version.md

@@ -3,3 +3,12 @@ base Framework
 RS
 #### 1.1
 Dynamically reseting
+#### 2.0
+Sharing (NPS)
+#### 3.-1
+Sharing (DPS) 
+
+## TODO
+- need merge (add option: NPS/DPS)
+- light_print ()
+- GE FME

workers/basekissat.cpp

@@ -1,4 +1,7 @@
 #include "basekissat.hpp"
+#include "sharer.hpp"
+#include <thread>
+#include <condition_variable>
 
 extern "C" {
    #include "src/application.h"
@@ -10,16 +13,16 @@ extern "C" {
 
 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;
-    // if (S->id == 0) printf("export: ");
     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;
-        // if (S->id == 0) printf("%d ", cls->data[i]);
-        // S->outexport << cls->data[i] << std::endl;
     }
+    ++S->x2;
     // if (S->id == 0) puts("");
     cls->lbd = lbd;
     S->export_clause.push(cls);
@@ -50,6 +53,26 @@ int kissat_import_clause(void *solver, int *lbd, cvec* c) {
     return 1;
 } 
 
+void kissat_wait_sharing(void *solver) {
+    basekissat* S = (basekissat *) solver;
+    // printf("c into Light wait %d %d\n", S->x1, S->x2);
+    S->x1 = S->x2 = 0;
+    sharer *s = S->in_sharer;
+    {
+        boost::mutex::scoped_lock lock(s->mtx);
+        s->waitings += 1;
+        lock.unlock();
+        // printf("c %d start wait with number %d\n", S->id, s->waitings);
+    }
+    if (s->should_sharing()) s->cond.notify_one(); 
+    
+    boost::mutex::scoped_lock lock(s->mtx);
+    while (s->waitings > 0) {
+        s->cond.wait(lock);
+    }
+    // printf("c %d finish sharing\n", S->id);
+}
+
 basekissat::basekissat(int id, light* light) : basesolver(id, light) {
     good_clause_lbd = 2;
     // outexport.open("export.txt");
@@ -57,8 +80,14 @@ basekissat::basekissat(int id, light* light) : basesolver(id, light) {
     // outfree.open("free.txt");
     solver = kissat_init();
     solver -> issuer = this;
-    solver -> cbkImportClause = kissat_import_clause;
-    solver -> cbkExportClause = kissat_export_clause;
+    solver -> cbkImportClause = NULL;
+    solver -> cbkExportClause = NULL;
+    solver -> cbkWaitSharing  = NULL;
+    if (light->opt->share) {
+        solver -> cbkImportClause = kissat_import_clause;
+        solver -> cbkExportClause = kissat_export_clause;
+        solver -> cbkWaitSharing  = kissat_wait_sharing;
+    }
 }
 
 basekissat::~basekissat(){

workers/basekissat.hpp

@@ -23,12 +23,15 @@ public:
 
     basekissat(int id, light *light);
     ~basekissat();
+    int x1 = 0, x2 = 0;
     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 *);
     std::ofstream outimport;
     std::ofstream outexport;
     std::ofstream outfree;

workers/basesolver.hpp

@@ -6,6 +6,7 @@
 #include "clause.hpp"
 #include <fstream>
 #include <iostream>
+class sharer;
 class basesolver {
 public:
     virtual void parse_dimacs(char* filename) = 0;
@@ -22,6 +23,7 @@ public:
     virtual void restrict_export_limit() = 0;
     light * controller;
     int id;
+    sharer* in_sharer;
 
     basesolver(int sid, light* light) : id(sid), controller(light) {}
     ~basesolver() {

workers/sharer.cpp

@@ -3,16 +3,26 @@
 #include "sharer.hpp"
 #include "clause.hpp"
 #include <unistd.h>
+#include <boost/thread/thread.hpp>
 
 void * share_worker(void *arg) {
+    int nums = 0;
     sharer * sq = (sharer *)arg;
     while (true) {
-        usleep(sq->share_intv);        
-        if (terminated) break;
+        ++nums;
+        // usleep(sq->share_intv);
+        // printf("c sharing thread start wait\n");
+        sq->waiting_for_all_ready();
+        // printf("c sharing thread start sharing with number %d\n", sq->waitings);
+        if (terminated) {
+            sq->sharing_finish();
+            break;
+        }
         // printf("start sharing %d\n", sq->share_intv);
         for (int i = 0; i < sq->producers.size(); i++) {
             sq->cls.clear();
             sq->producers[i]->export_clauses_to(sq->cls);
+            // printf("c size %d\n", sq->cls.size());
             int number = sq->cls.size();
             // printf("get %d exported clauses\n", number);
             int percent = sq->sort_clauses(i);
@@ -37,12 +47,13 @@ void * share_worker(void *arg) {
                 sq->cls[k]->free_clause();
             }
         }
-        // printf("end sharing\n");
-        // terminated = 1;
+        sq->sharing_finish();
     }
-    if (terminated) puts("terminated set to 1");
+    printf("c sharing nums: %d\n", nums);
+    // if (terminated) puts("terminated set to 1");
     return NULL;
 }
+ 
 
 int sharer::sort_clauses(int x) {
     for (int i = 0; i < cls.size(); i++) {
@@ -84,12 +95,14 @@ int sharer::sort_clauses(int x) {
 }
 
 void light::share() {
+    printf("c sharing start\n");
     int sharers_number = 1;
     for (int i = 0; i < sharers_number; i++) {
         sharer* s = new sharer(i, OPT(share_intv), OPT(share_lits));
         for (int j = 0; j < OPT(threads); j++) {
             s->producers.push(workers[j]);
             s->consumers.push(workers[j]);
+            workers[j]->in_sharer = s;
         }
         sharers.push(s);
     }