v2: sharing

.vscode/settings.json

@@ -55,6 +55,11 @@
         "streambuf": "cpp",
         "cinttypes": "cpp",
         "assert.h": "c",
-        "bitset": "cpp"
+        "bitset": "cpp",
+        "complex": "cpp",
+        "set": "cpp",
+        "iomanip": "cpp",
+        "typeindex": "cpp",
+        "variant": "cpp"
     }
 }

light.cpp

@@ -2,8 +2,6 @@
 #include "light.hpp"
 #include <unistd.h>
 #include <thread>
-using namespace std; 
-
 
 light::light():
   finalResult           (0),

light.hpp

@@ -5,13 +5,12 @@
 #include "preprocess.hpp"
 #include <atomic>
 #include <iostream>
-using namespace std;
 typedef long long ll;
 
 class basesolver;
 class sharer;
 
-extern atomic<int> terminated;
+extern std::atomic<int> terminated;
 
 struct thread_inf{
     int id, inf;
@@ -36,7 +35,7 @@ public:
     int finalResult;
     int winner;
     int maxtime;
-    atomic<bool> globalEnding;
+    std::atomic<bool> globalEnding;
 
     void arg_parse(int argc, char **argv);
     void init_workers();

main.cpp

@@ -1,7 +1,6 @@
 #include "solve.hpp"
 #include <chrono>
 #include <thread> 
-using namespace std;
 
 int main(int argc, char **argv) {
     solve(argc, argv);

res.txt

@@ -0,0 +1,374 @@
+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

@@ -5,7 +5,7 @@
 #include <algorithm>
 auto clk_st = std::chrono::high_resolution_clock::now();
 char* worker_sign = "";
-atomic<int> terminated;
+std::atomic<int> terminated;
 int result = 0;
 int winner;
 vec<int> model;
@@ -40,6 +40,7 @@ void * solve_worker(void *arg) {
 }
 
 void light::init_workers() {
+    terminated = 0;
     for (int i = 0; i < OPT(threads); i++) {
         basekissat* kissat = new basekissat(i, this);
         workers.push(kissat);
@@ -71,7 +72,6 @@ void light::parse_input() {
 
 int light::solve() {
     printf("c -----------------solve start----------------------\n");
-    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, workers[i]);
@@ -105,6 +105,8 @@ int light::solve() {
             puts("\n");
         }
     }
+    printf("ending solve\n");
+    terminate_workers();
 
     for (int i = 0; i < OPT(threads); i++) {
         pthread_join(ptr[i], NULL);

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 "Wed Aug 31 12:28:43 CST 2022 Linux seed1 5.4.0-120-generic x86_64"
+#define BUILD "Thu Sep 15 10:12:48 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/learn.c

@@ -180,7 +180,10 @@ kissat_importClauses(kissat *solver)
     return true;
   int lbd, k, l, res;
   assert(solver->importedClause->sz == 0);
-  while ((res = solver->cbkImportClause(solver->issuer, &lbd, solver->importedClause)) != -1) {
+  // while ((res = solver->cbkImportClause(solver->issuer, &lbd, solver->importedClause)) != -1) {
+  while (true) {
+    int res = solver->cbkImportClause(solver->issuer, &lbd, solver->importedClause);
+    if (res == -1) break;
     if (res == -10) {
       cvec_clear(solver->importedClause);
       continue;

workers/basekissat.cpp

@@ -8,23 +8,19 @@ extern "C" {
    #include "src/import.h"
 }
 
-basekissat::basekissat(int id, light* light) : basesolver(id, light) {
-    solver = kissat_init();
-}
-
-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;
+    // 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;
     }
+    // if (S->id == 0) puts("");
     cls->lbd = lbd;
     S->export_clause.push(cls);
 }
@@ -32,10 +28,11 @@ void kissat_export_clause(void *solver, int lbd, cvec* c) {
 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;
+    if (S->import_clause.pop(cls) == false) return -1;
 
     bool eliminated = false;
     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) {
@@ -53,6 +50,21 @@ int kissat_import_clause(void *solver, int *lbd, cvec* c) {
     return 1;
 } 
 
+basekissat::basekissat(int id, light* light) : basesolver(id, light) {
+    good_clause_lbd = 2;
+    // outexport.open("export.txt");
+    // outimport.open("import.txt");
+    // outfree.open("free.txt");
+    solver = kissat_init();
+    solver -> issuer = this;
+    solver -> cbkImportClause = kissat_import_clause;
+    solver -> cbkExportClause = kissat_export_clause;
+}
+
+basekissat::~basekissat(){
+    delete solver;
+}
+
 void basekissat::parse_dimacs(char* filename) {
     kissat_mab_parse(solver);
     strictness strict = NORMAL_PARSING;
@@ -105,9 +117,31 @@ void basekissat::reset() {
 }
 
 void basekissat::export_clauses_to(vec<clause_store *> &clauses) {
-
+    clause_store *cls;
+    while (export_clause.pop(cls)) {
+        clauses.push(cls);
+        // outexport << id << ": ";
+        // for (int i = 0; i < cls->size; i++)
+        //     outexport << cls->data[i] << " ";
+        // outexport << std::endl;
+    }
 }
 
 void basekissat::import_clauses_from(vec<clause_store *> &clauses) {
-    
+    for (int i = 0; i < clauses.size(); i++) {
+        import_clause.push(clauses[i]);
+        // outimport << id << ": ";
+        // for (int j = 0; j < clauses[i]->size; j++) 
+        //     outimport << clauses[i]->data[j] << " ";
+        // outimport << std::endl;
+    }
+}
+
+void basekissat::broaden_export_limit() {
+    // ++good_clause_lbd;
+}
+
+void basekissat::restrict_export_limit() {
+    if (good_clause_lbd > 2)
+        --good_clause_lbd;
 }

workers/basekissat.hpp

@@ -4,6 +4,7 @@
 #include <boost/lockfree/spsc_queue.hpp>
 
 struct kissat;
+struct cvec;
 
 class basekissat : public basesolver {
 public:
@@ -17,6 +18,8 @@ public:
     void reset();
     void export_clauses_to(vec<clause_store *> &clauses);
     void import_clauses_from(vec<clause_store *> &clauses);
+    void broaden_export_limit();
+    void restrict_export_limit();
 
     basekissat(int id, light *light);
     ~basekissat();
@@ -24,4 +27,9 @@ public:
     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 *);
+    std::ofstream outimport;
+    std::ofstream outexport;
+    std::ofstream outfree;
 };

workers/basesolver.hpp

@@ -3,6 +3,9 @@
 
 #include "../light.hpp"
 #include "../utils/vec.hpp"
+#include "clause.hpp"
+#include <fstream>
+#include <iostream>
 class basesolver {
 public:
     virtual void parse_dimacs(char* filename) = 0;
@@ -15,6 +18,8 @@ public:
     virtual void reset() = 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;
+    virtual void restrict_export_limit() = 0;
     light * controller;
     int id;
 

workers/clause.hpp

@@ -4,17 +4,29 @@
 struct clause_store {
     int size, lbd;
     int *data;
-    atomic<int> refs;
+    std::atomic<int> refs;
     clause_store(int sz) {
         size = sz;
         data = (int*) malloc(sizeof(int) * sz);
         lbd = 0;
         refs = 1;
     }
-    void free_clause() {
+    void increase_refs(int inc) {
+        refs += inc;
+    }
+    bool free_clause() {
         int ref = refs.fetch_sub(1);
-        if (ref <= 1)
+        if (ref <= 1) {
+            // for (int i = 0; i < size; i++)
+            //     printf("%d ", data[i]);
+            // puts("");
             free(data);
+            return true;
+        }
+        return false;
+    }
+    ~clause_store() {
+        puts("free");
     }
 };
 

workers/sharer.cpp

@@ -9,59 +9,77 @@ void * share_worker(void *arg) {
     while (true) {
         usleep(sq->share_intv);        
         if (terminated) 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);
+            int number = sq->cls.size();
+            // printf("get %d exported clauses\n", number);
+            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 k = 0; k < sq->cls.size(); k++) {
+            //     int x = sq->cls[k]->refs;
+            //     printf("%d ", x);
+            // }                
+            // puts("");
+            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();
+            }
+        }
+        // printf("end sharing\n");
+        // terminated = 1;
     }
-    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();
-            
-    }
+    if (terminated) puts("terminated set to 1");
     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();
+        // for (int j = 0; j < sz; j++) printf("%d ", cls[i]->data[j]);
+        // puts("");
+        while (sz > bucket[x].size()) bucket[x].push();
+        if (sz * (bucket[x][sz - 1].size() + 1) <= share_lits) 
+            bucket[x][sz - 1].push(cls[i]);
+        // else
+        //     cls[i]->free_clause();
     }
     cls.clear();
     int space = share_lits;
-    for (int i = 0; i < buck->size(); i++) {
+    for (int i = 0; i < bucket[x].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();
+        // printf("%d %d\n", clause_num, bucket[x][i].size());
+        if (!clause_num) break;
+        if (clause_num >= bucket[x][i].size()) {
+            space -= bucket[x][i].size() * (i + 1);
+            for (int j = 0; j < bucket[x][i].size(); j++)
+                cls.push(bucket[x][i][j]);
+            bucket[x][i].clear();
         }
         else {
             space -= clause_num * (i + 1);
             for (int j = 0; j < clause_num; j++) {
-                cls.push(buck[i].last());
-                buck[i].pop();
+                cls.push(bucket[x][i].last());
+                bucket[x][i].pop();
             }
         }
     }
+    // for (int i = 0; i < cls.size(); i++) {
+    //     int sz = cls[i]->size;
+    //     for (int j = 0; j < sz; j++) printf("%d ", cls[i]->data[j]);
+    //     puts("");
+    // }
     return (share_lits - space) * 100 / share_lits;
 }
 
@@ -69,14 +87,19 @@ 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]);
+        for (int j = 0; j < OPT(threads); j++) {
+            s->producers.push(workers[j]);
+            s->consumers.push(workers[j]);
+        }
         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]);
+        pthread_create(&ptr[i], NULL, share_worker, sharers[i]);
     }
-
+    
+    // for (int i = 0; i < sharers_number; i++) {
+    //     pthread_join(ptr[i], NULL);
+    // }   
 }