1 /**************************************************************************************************
2 MiniSat -- Copyright (c) 2005, Niklas Sorensson
3 http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
4
5 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
6 associated documentation files (the "Software"), to deal in the Software without restriction,
7 including without limitation the rights to use, copy, modify, merge, publish, distribute,
8 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
10
11 The above copyright notice and this permission notice shall be included in all copies or
12 substantial portions of the Software.
13
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
15 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
16 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
17 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
18 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
19 **************************************************************************************************/
20 // Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
21
22 #include <stdio.h>
23 #include <assert.h>
24 #include <string.h>
25 #include <math.h>
26
27 #include "satSolver.h"
28 #include "satStore.h"
29
30 ABC_NAMESPACE_IMPL_START
31
32 #define SAT_USE_ANALYZE_FINAL
33
34 //=================================================================================================
35 // Debug:
36
37 //#define VERBOSEDEBUG
38
39 // For derivation output (verbosity level 2)
40 #define L_IND "%-*d"
41 #define L_ind sat_solver_dl(s)*2+2,sat_solver_dl(s)
42 #define L_LIT "%sx%d"
43 #define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
44
45 // Just like 'assert()' but expression will be evaluated in the release version as well.
check(int expr)46 static inline void check(int expr) { assert(expr); }
47
printlits(lit * begin,lit * end)48 static void printlits(lit* begin, lit* end)
49 {
50 int i;
51 for (i = 0; i < end - begin; i++)
52 printf(L_LIT" ",L_lit(begin[i]));
53 }
54
55 //=================================================================================================
56 // Random numbers:
57
58
59 // Returns a random float 0 <= x < 1. Seed must never be 0.
drand(double * seed)60 static inline double drand(double* seed) {
61 int q;
62 *seed *= 1389796;
63 q = (int)(*seed / 2147483647);
64 *seed -= (double)q * 2147483647;
65 return *seed / 2147483647; }
66
67
68 // Returns a random integer 0 <= x < size. Seed must never be 0.
irand(double * seed,int size)69 static inline int irand(double* seed, int size) {
70 return (int)(drand(seed) * size); }
71
72
73 //=================================================================================================
74 // Variable datatype + minor functions:
75
76 static const int var0 = 1;
77 static const int var1 = 0;
78 static const int varX = 3;
79
80 struct varinfo_t
81 {
82 unsigned val : 2; // variable value
83 unsigned pol : 1; // last polarity
84 unsigned tag : 1; // conflict analysis tag
85 unsigned lev : 28; // variable level
86 };
87
var_level(sat_solver * s,int v)88 static inline int var_level (sat_solver* s, int v) { return s->levels[v]; }
var_value(sat_solver * s,int v)89 static inline int var_value (sat_solver* s, int v) { return s->assigns[v]; }
var_polar(sat_solver * s,int v)90 static inline int var_polar (sat_solver* s, int v) { return s->polarity[v]; }
91
var_set_level(sat_solver * s,int v,int lev)92 static inline void var_set_level (sat_solver* s, int v, int lev) { s->levels[v] = lev; }
var_set_value(sat_solver * s,int v,int val)93 static inline void var_set_value (sat_solver* s, int v, int val) { s->assigns[v] = val; }
var_set_polar(sat_solver * s,int v,int pol)94 static inline void var_set_polar (sat_solver* s, int v, int pol) { s->polarity[v] = pol; }
95
96 // variable tags
var_tag(sat_solver * s,int v)97 static inline int var_tag (sat_solver* s, int v) { return s->tags[v]; }
var_set_tag(sat_solver * s,int v,int tag)98 static inline void var_set_tag (sat_solver* s, int v, int tag) {
99 assert( tag > 0 && tag < 16 );
100 if ( s->tags[v] == 0 )
101 veci_push( &s->tagged, v );
102 s->tags[v] = tag;
103 }
var_add_tag(sat_solver * s,int v,int tag)104 static inline void var_add_tag (sat_solver* s, int v, int tag) {
105 assert( tag > 0 && tag < 16 );
106 if ( s->tags[v] == 0 )
107 veci_push( &s->tagged, v );
108 s->tags[v] |= tag;
109 }
solver2_clear_tags(sat_solver * s,int start)110 static inline void solver2_clear_tags(sat_solver* s, int start) {
111 int i, * tagged = veci_begin(&s->tagged);
112 for (i = start; i < veci_size(&s->tagged); i++)
113 s->tags[tagged[i]] = 0;
114 veci_resize(&s->tagged,start);
115 }
116
sat_solver_get_var_value(sat_solver * s,int v)117 int sat_solver_get_var_value(sat_solver* s, int v)
118 {
119 if ( var_value(s, v) == var0 )
120 return l_False;
121 if ( var_value(s, v) == var1 )
122 return l_True;
123 if ( var_value(s, v) == varX )
124 return l_Undef;
125 assert( 0 );
126 return 0;
127 }
128
129 //=================================================================================================
130 // Simple helpers:
131
sat_solver_dl(sat_solver * s)132 static inline int sat_solver_dl(sat_solver* s) { return veci_size(&s->trail_lim); }
sat_solver_read_wlist(sat_solver * s,lit l)133 static inline veci* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; }
134
135 //=================================================================================================
136 // Variable order functions:
137
order_update(sat_solver * s,int v)138 static inline void order_update(sat_solver* s, int v) // updateorder
139 {
140 int* orderpos = s->orderpos;
141 int* heap = veci_begin(&s->order);
142 int i = orderpos[v];
143 int x = heap[i];
144 int parent = (i - 1) / 2;
145
146 assert(s->orderpos[v] != -1);
147
148 while (i != 0 && s->activity[x] > s->activity[heap[parent]]){
149 heap[i] = heap[parent];
150 orderpos[heap[i]] = i;
151 i = parent;
152 parent = (i - 1) / 2;
153 }
154
155 heap[i] = x;
156 orderpos[x] = i;
157 }
158
order_assigned(sat_solver * s,int v)159 static inline void order_assigned(sat_solver* s, int v)
160 {
161 }
162
order_unassigned(sat_solver * s,int v)163 static inline void order_unassigned(sat_solver* s, int v) // undoorder
164 {
165 int* orderpos = s->orderpos;
166 if (orderpos[v] == -1){
167 orderpos[v] = veci_size(&s->order);
168 veci_push(&s->order,v);
169 order_update(s,v);
170 //printf( "+%d ", v );
171 }
172 }
173
order_select(sat_solver * s,float random_var_freq)174 static inline int order_select(sat_solver* s, float random_var_freq) // selectvar
175 {
176 int* heap = veci_begin(&s->order);
177 int* orderpos = s->orderpos;
178 // Random decision:
179 if (drand(&s->random_seed) < random_var_freq){
180 int next = irand(&s->random_seed,s->size);
181 assert(next >= 0 && next < s->size);
182 if (var_value(s, next) == varX)
183 return next;
184 }
185 // Activity based decision:
186 while (veci_size(&s->order) > 0){
187 int next = heap[0];
188 int size = veci_size(&s->order)-1;
189 int x = heap[size];
190 veci_resize(&s->order,size);
191 orderpos[next] = -1;
192 if (size > 0){
193 int i = 0;
194 int child = 1;
195 while (child < size){
196
197 if (child+1 < size && s->activity[heap[child]] < s->activity[heap[child+1]])
198 child++;
199 assert(child < size);
200 if (s->activity[x] >= s->activity[heap[child]])
201 break;
202
203 heap[i] = heap[child];
204 orderpos[heap[i]] = i;
205 i = child;
206 child = 2 * child + 1;
207 }
208 heap[i] = x;
209 orderpos[heap[i]] = i;
210 }
211 if (var_value(s, next) == varX)
212 return next;
213 }
214 return var_Undef;
215 }
216
sat_solver_set_var_activity(sat_solver * s,int * pVars,int nVars)217 void sat_solver_set_var_activity(sat_solver* s, int * pVars, int nVars)
218 {
219 int i;
220 for (i = 0; i < s->size; i++)
221 s->activity[i] = 0;
222 if ( s->VarActType == 0 )
223 {
224 s->var_inc = (1 << 5);
225 s->var_decay = -1;
226 for ( i = 0; i < nVars; i++ )
227 {
228 int iVar = pVars ? pVars[i] : i;
229 s->activity[iVar] = s->var_inc*(nVars-i);
230 if (s->orderpos[iVar] != -1)
231 order_update( s, iVar );
232 }
233 }
234 else if ( s->VarActType == 1 )
235 {
236 s->var_inc = Abc_Dbl2Word(1);
237 for ( i = 0; i < nVars; i++ )
238 {
239 int iVar = pVars ? pVars[i] : i;
240 s->activity[iVar] = Abc_Dbl2Word(nVars-i);
241 if (s->orderpos[iVar] != -1)
242 order_update( s, iVar );
243 }
244 }
245 else assert( 0 );
246 }
247
248 //=================================================================================================
249 // variable activities
250
solver_init_activities(sat_solver * s)251 static inline void solver_init_activities(sat_solver* s)
252 {
253 // variable activities
254 s->VarActType = 0;
255 if ( s->VarActType == 0 )
256 {
257 s->var_inc = (1 << 5);
258 s->var_decay = -1;
259 }
260 else if ( s->VarActType == 1 )
261 {
262 s->var_inc = Abc_Dbl2Word(1.0);
263 s->var_decay = Abc_Dbl2Word(1.0 / 0.95);
264 }
265 else if ( s->VarActType == 2 )
266 {
267 s->var_inc = Xdbl_FromDouble(1.0);
268 s->var_decay = Xdbl_FromDouble(1.0 / 0.950);
269 }
270 else assert(0);
271
272 // clause activities
273 s->ClaActType = 0;
274 if ( s->ClaActType == 0 )
275 {
276 s->cla_inc = (1 << 11);
277 s->cla_decay = -1;
278 }
279 else
280 {
281 s->cla_inc = 1;
282 s->cla_decay = (float)(1 / 0.999);
283 }
284 }
285
act_var_rescale(sat_solver * s)286 static inline void act_var_rescale(sat_solver* s)
287 {
288 if ( s->VarActType == 0 )
289 {
290 word* activity = s->activity;
291 int i;
292 for (i = 0; i < s->size; i++)
293 activity[i] >>= 19;
294 s->var_inc >>= 19;
295 s->var_inc = Abc_MaxInt( (unsigned)s->var_inc, (1<<4) );
296 }
297 else if ( s->VarActType == 1 )
298 {
299 double* activity = (double*)s->activity;
300 int i;
301 for (i = 0; i < s->size; i++)
302 activity[i] *= 1e-100;
303 s->var_inc = Abc_Dbl2Word( Abc_Word2Dbl(s->var_inc) * 1e-100 );
304 //printf( "Rescaling var activity...\n" );
305 }
306 else if ( s->VarActType == 2 )
307 {
308 xdbl * activity = s->activity;
309 int i;
310 for (i = 0; i < s->size; i++)
311 activity[i] = Xdbl_Div( activity[i], 200 ); // activity[i] / 2^200
312 s->var_inc = Xdbl_Div( s->var_inc, 200 );
313 }
314 else assert(0);
315 }
act_var_bump(sat_solver * s,int v)316 static inline void act_var_bump(sat_solver* s, int v)
317 {
318 if ( s->VarActType == 0 )
319 {
320 s->activity[v] += s->var_inc;
321 if ((unsigned)s->activity[v] & 0x80000000)
322 act_var_rescale(s);
323 if (s->orderpos[v] != -1)
324 order_update(s,v);
325 }
326 else if ( s->VarActType == 1 )
327 {
328 double act = Abc_Word2Dbl(s->activity[v]) + Abc_Word2Dbl(s->var_inc);
329 s->activity[v] = Abc_Dbl2Word(act);
330 if (act > 1e100)
331 act_var_rescale(s);
332 if (s->orderpos[v] != -1)
333 order_update(s,v);
334 }
335 else if ( s->VarActType == 2 )
336 {
337 s->activity[v] = Xdbl_Add( s->activity[v], s->var_inc );
338 if (s->activity[v] > ABC_CONST(0x014c924d692ca61b))
339 act_var_rescale(s);
340 if (s->orderpos[v] != -1)
341 order_update(s,v);
342 }
343 else assert(0);
344 }
act_var_bump_global(sat_solver * s,int v)345 static inline void act_var_bump_global(sat_solver* s, int v)
346 {
347 if ( !s->pGlobalVars || !s->pGlobalVars[v] )
348 return;
349 if ( s->VarActType == 0 )
350 {
351 s->activity[v] += (int)((unsigned)s->var_inc * 3);
352 if (s->activity[v] & 0x80000000)
353 act_var_rescale(s);
354 if (s->orderpos[v] != -1)
355 order_update(s,v);
356 }
357 else if ( s->VarActType == 1 )
358 {
359 double act = Abc_Word2Dbl(s->activity[v]) + Abc_Word2Dbl(s->var_inc) * 3.0;
360 s->activity[v] = Abc_Dbl2Word(act);
361 if ( act > 1e100)
362 act_var_rescale(s);
363 if (s->orderpos[v] != -1)
364 order_update(s,v);
365 }
366 else if ( s->VarActType == 2 )
367 {
368 s->activity[v] = Xdbl_Add( s->activity[v], Xdbl_Mul(s->var_inc, Xdbl_FromDouble(3.0)) );
369 if (s->activity[v] > ABC_CONST(0x014c924d692ca61b))
370 act_var_rescale(s);
371 if (s->orderpos[v] != -1)
372 order_update(s,v);
373 }
374 else assert( 0 );
375 }
act_var_bump_factor(sat_solver * s,int v)376 static inline void act_var_bump_factor(sat_solver* s, int v)
377 {
378 if ( !s->factors )
379 return;
380 if ( s->VarActType == 0 )
381 {
382 s->activity[v] += (int)((unsigned)s->var_inc * (float)s->factors[v]);
383 if (s->activity[v] & 0x80000000)
384 act_var_rescale(s);
385 if (s->orderpos[v] != -1)
386 order_update(s,v);
387 }
388 else if ( s->VarActType == 1 )
389 {
390 double act = Abc_Word2Dbl(s->activity[v]) + Abc_Word2Dbl(s->var_inc) * s->factors[v];
391 s->activity[v] = Abc_Dbl2Word(act);
392 if ( act > 1e100)
393 act_var_rescale(s);
394 if (s->orderpos[v] != -1)
395 order_update(s,v);
396 }
397 else if ( s->VarActType == 2 )
398 {
399 s->activity[v] = Xdbl_Add( s->activity[v], Xdbl_Mul(s->var_inc, Xdbl_FromDouble(s->factors[v])) );
400 if (s->activity[v] > ABC_CONST(0x014c924d692ca61b))
401 act_var_rescale(s);
402 if (s->orderpos[v] != -1)
403 order_update(s,v);
404 }
405 else assert( 0 );
406 }
407
act_var_decay(sat_solver * s)408 static inline void act_var_decay(sat_solver* s)
409 {
410 if ( s->VarActType == 0 )
411 s->var_inc += (s->var_inc >> 4);
412 else if ( s->VarActType == 1 )
413 s->var_inc = Abc_Dbl2Word( Abc_Word2Dbl(s->var_inc) * Abc_Word2Dbl(s->var_decay) );
414 else if ( s->VarActType == 2 )
415 s->var_inc = Xdbl_Mul(s->var_inc, s->var_decay);
416 else assert(0);
417 }
418
419 // clause activities
act_clause_rescale(sat_solver * s)420 static inline void act_clause_rescale(sat_solver* s)
421 {
422 if ( s->ClaActType == 0 )
423 {
424 unsigned* activity = (unsigned *)veci_begin(&s->act_clas);
425 int i;
426 for (i = 0; i < veci_size(&s->act_clas); i++)
427 activity[i] >>= 14;
428 s->cla_inc >>= 14;
429 s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
430 }
431 else
432 {
433 float* activity = (float *)veci_begin(&s->act_clas);
434 int i;
435 for (i = 0; i < veci_size(&s->act_clas); i++)
436 activity[i] *= (float)1e-20;
437 s->cla_inc *= (float)1e-20;
438 }
439 }
act_clause_bump(sat_solver * s,clause * c)440 static inline void act_clause_bump(sat_solver* s, clause *c)
441 {
442 if ( s->ClaActType == 0 )
443 {
444 unsigned* act = (unsigned *)veci_begin(&s->act_clas) + c->lits[c->size];
445 *act += s->cla_inc;
446 if ( *act & 0x80000000 )
447 act_clause_rescale(s);
448 }
449 else
450 {
451 float* act = (float *)veci_begin(&s->act_clas) + c->lits[c->size];
452 *act += s->cla_inc;
453 if (*act > 1e20)
454 act_clause_rescale(s);
455 }
456 }
act_clause_decay(sat_solver * s)457 static inline void act_clause_decay(sat_solver* s)
458 {
459 if ( s->ClaActType == 0 )
460 s->cla_inc += (s->cla_inc >> 10);
461 else
462 s->cla_inc *= s->cla_decay;
463 }
464
465
466 //=================================================================================================
467 // Sorting functions (sigh):
468
selectionsort(void ** array,int size,int (* comp)(const void *,const void *))469 static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
470 {
471 int i, j, best_i;
472 void* tmp;
473
474 for (i = 0; i < size-1; i++){
475 best_i = i;
476 for (j = i+1; j < size; j++){
477 if (comp(array[j], array[best_i]) < 0)
478 best_i = j;
479 }
480 tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
481 }
482 }
483
sortrnd(void ** array,int size,int (* comp)(const void *,const void *),double * seed)484 static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
485 {
486 if (size <= 15)
487 selectionsort(array, size, comp);
488
489 else{
490 void* pivot = array[irand(seed, size)];
491 void* tmp;
492 int i = -1;
493 int j = size;
494
495 for(;;){
496 do i++; while(comp(array[i], pivot)<0);
497 do j--; while(comp(pivot, array[j])<0);
498
499 if (i >= j) break;
500
501 tmp = array[i]; array[i] = array[j]; array[j] = tmp;
502 }
503
504 sortrnd(array , i , comp, seed);
505 sortrnd(&array[i], size-i, comp, seed);
506 }
507 }
508
509 //=================================================================================================
510 // Clause functions:
511
sat_clause_compute_lbd(sat_solver * s,clause * c)512 static inline int sat_clause_compute_lbd( sat_solver* s, clause* c )
513 {
514 int i, lev, minl = 0, lbd = 0;
515 for (i = 0; i < (int)c->size; i++)
516 {
517 lev = var_level(s, lit_var(c->lits[i]));
518 if ( !(minl & (1 << (lev & 31))) )
519 {
520 minl |= 1 << (lev & 31);
521 lbd++;
522 // printf( "%d ", lev );
523 }
524 }
525 // printf( " -> %d\n", lbd );
526 return lbd;
527 }
528
529 /* pre: size > 1 && no variable occurs twice
530 */
sat_solver_clause_new(sat_solver * s,lit * begin,lit * end,int learnt)531 int sat_solver_clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
532 {
533 int fUseBinaryClauses = 1;
534 int size;
535 clause* c;
536 int h;
537
538 assert(end - begin > 1);
539 assert(learnt >= 0 && learnt < 2);
540 size = end - begin;
541
542 // do not allocate memory for the two-literal problem clause
543 if ( fUseBinaryClauses && size == 2 && !learnt )
544 {
545 veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(clause_from_lit(begin[1])));
546 veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(clause_from_lit(begin[0])));
547 s->stats.clauses++;
548 s->stats.clauses_literals += size;
549 return 0;
550 }
551
552 // create new clause
553 // h = Vec_SetAppend( &s->Mem, NULL, size + learnt + 1 + 1 ) << 1;
554 h = Sat_MemAppend( &s->Mem, begin, size, learnt, 0 );
555 assert( !(h & 1) );
556 if ( s->hLearnts == -1 && learnt )
557 s->hLearnts = h;
558 if (learnt)
559 {
560 c = clause_read( s, h );
561 c->lbd = sat_clause_compute_lbd( s, c );
562 assert( clause_id(c) == veci_size(&s->act_clas) );
563 // veci_push(&s->learned, h);
564 // act_clause_bump(s,clause_read(s, h));
565 if ( s->ClaActType == 0 )
566 veci_push(&s->act_clas, (1<<10));
567 else
568 veci_push(&s->act_clas, s->cla_inc);
569 s->stats.learnts++;
570 s->stats.learnts_literals += size;
571 }
572 else
573 {
574 s->stats.clauses++;
575 s->stats.clauses_literals += size;
576 }
577
578 assert(begin[0] >= 0);
579 assert(begin[0] < s->size*2);
580 assert(begin[1] >= 0);
581 assert(begin[1] < s->size*2);
582
583 assert(lit_neg(begin[0]) < s->size*2);
584 assert(lit_neg(begin[1]) < s->size*2);
585
586 //veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),c);
587 //veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),c);
588 veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(size > 2 ? h : clause_from_lit(begin[1])));
589 veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(size > 2 ? h : clause_from_lit(begin[0])));
590
591 return h;
592 }
593
594
595 //=================================================================================================
596 // Minor (solver) functions:
597
sat_solver_enqueue(sat_solver * s,lit l,int from)598 static inline int sat_solver_enqueue(sat_solver* s, lit l, int from)
599 {
600 int v = lit_var(l);
601 if ( s->pFreqs[v] == 0 )
602 // {
603 s->pFreqs[v] = 1;
604 // s->nVarUsed++;
605 // }
606
607 #ifdef VERBOSEDEBUG
608 printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
609 #endif
610 if (var_value(s, v) != varX)
611 return var_value(s, v) == lit_sign(l);
612 else{
613 /*
614 if ( s->pCnfFunc )
615 {
616 if ( lit_sign(l) )
617 {
618 if ( (s->loads[v] & 1) == 0 )
619 {
620 s->loads[v] ^= 1;
621 s->pCnfFunc( s->pCnfMan, l );
622 }
623 }
624 else
625 {
626 if ( (s->loads[v] & 2) == 0 )
627 {
628 s->loads[v] ^= 2;
629 s->pCnfFunc( s->pCnfMan, l );
630 }
631 }
632 }
633 */
634 // New fact -- store it.
635 #ifdef VERBOSEDEBUG
636 printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
637 #endif
638 var_set_value(s, v, lit_sign(l));
639 var_set_level(s, v, sat_solver_dl(s));
640 s->reasons[v] = from;
641 s->trail[s->qtail++] = l;
642 order_assigned(s, v);
643 return true;
644 }
645 }
646
647
sat_solver_decision(sat_solver * s,lit l)648 static inline int sat_solver_decision(sat_solver* s, lit l){
649 assert(s->qtail == s->qhead);
650 assert(var_value(s, lit_var(l)) == varX);
651 #ifdef VERBOSEDEBUG
652 printf(L_IND"assume("L_LIT") ", L_ind, L_lit(l));
653 printf( "act = %.20f\n", s->activity[lit_var(l)] );
654 #endif
655 veci_push(&s->trail_lim,s->qtail);
656 return sat_solver_enqueue(s,l,0);
657 }
658
659
sat_solver_canceluntil(sat_solver * s,int level)660 static void sat_solver_canceluntil(sat_solver* s, int level) {
661 int bound;
662 int lastLev;
663 int c;
664
665 if (sat_solver_dl(s) <= level)
666 return;
667
668 assert( veci_size(&s->trail_lim) > 0 );
669 bound = (veci_begin(&s->trail_lim))[level];
670 lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1];
671
672 ////////////////////////////////////////
673 // added to cancel all assignments
674 // if ( level == -1 )
675 // bound = 0;
676 ////////////////////////////////////////
677
678 for (c = s->qtail-1; c >= bound; c--) {
679 int x = lit_var(s->trail[c]);
680 var_set_value(s, x, varX);
681 s->reasons[x] = 0;
682 if ( c < lastLev )
683 var_set_polar( s, x, !lit_sign(s->trail[c]) );
684 }
685 //printf( "\n" );
686
687 for (c = s->qhead-1; c >= bound; c--)
688 order_unassigned(s,lit_var(s->trail[c]));
689
690 s->qhead = s->qtail = bound;
691 veci_resize(&s->trail_lim,level);
692 }
693
sat_solver_canceluntil_rollback(sat_solver * s,int NewBound)694 static void sat_solver_canceluntil_rollback(sat_solver* s, int NewBound) {
695 int c, x;
696
697 assert( sat_solver_dl(s) == 0 );
698 assert( s->qtail == s->qhead );
699 assert( s->qtail >= NewBound );
700
701 for (c = s->qtail-1; c >= NewBound; c--)
702 {
703 x = lit_var(s->trail[c]);
704 var_set_value(s, x, varX);
705 s->reasons[x] = 0;
706 }
707
708 for (c = s->qhead-1; c >= NewBound; c--)
709 order_unassigned(s,lit_var(s->trail[c]));
710
711 s->qhead = s->qtail = NewBound;
712 }
713
sat_solver_record(sat_solver * s,veci * cls)714 static void sat_solver_record(sat_solver* s, veci* cls)
715 {
716 lit* begin = veci_begin(cls);
717 lit* end = begin + veci_size(cls);
718 int h = (veci_size(cls) > 1) ? sat_solver_clause_new(s,begin,end,1) : 0;
719 sat_solver_enqueue(s,*begin,h);
720 assert(veci_size(cls) > 0);
721 if ( h == 0 )
722 veci_push( &s->unit_lits, *begin );
723
724 ///////////////////////////////////
725 // add clause to internal storage
726 if ( s->pStore )
727 {
728 int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
729 assert( RetValue );
730 (void) RetValue;
731 }
732 ///////////////////////////////////
733 /*
734 if (h != 0) {
735 act_clause_bump(s,clause_read(s, h));
736 s->stats.learnts++;
737 s->stats.learnts_literals += veci_size(cls);
738 }
739 */
740 }
741
sat_solver_count_assigned(sat_solver * s)742 int sat_solver_count_assigned(sat_solver* s)
743 {
744 // count top-level assignments
745 int i, Count = 0;
746 assert(sat_solver_dl(s) == 0);
747 for ( i = 0; i < s->size; i++ )
748 if (var_value(s, i) != varX)
749 Count++;
750 return Count;
751 }
752
sat_solver_progress(sat_solver * s)753 static double sat_solver_progress(sat_solver* s)
754 {
755 int i;
756 double progress = 0;
757 double F = 1.0 / s->size;
758 for (i = 0; i < s->size; i++)
759 if (var_value(s, i) != varX)
760 progress += pow(F, var_level(s, i));
761 return progress / s->size;
762 }
763
764 //=================================================================================================
765 // Major methods:
766
sat_solver_lit_removable(sat_solver * s,int x,int minl)767 static int sat_solver_lit_removable(sat_solver* s, int x, int minl)
768 {
769 int top = veci_size(&s->tagged);
770
771 assert(s->reasons[x] != 0);
772 veci_resize(&s->stack,0);
773 veci_push(&s->stack,x);
774
775 while (veci_size(&s->stack)){
776 int v = veci_pop(&s->stack);
777 assert(s->reasons[v] != 0);
778 if (clause_is_lit(s->reasons[v])){
779 v = lit_var(clause_read_lit(s->reasons[v]));
780 if (!var_tag(s,v) && var_level(s, v)){
781 if (s->reasons[v] != 0 && ((1 << (var_level(s, v) & 31)) & minl)){
782 veci_push(&s->stack,v);
783 var_set_tag(s, v, 1);
784 }else{
785 solver2_clear_tags(s, top);
786 return 0;
787 }
788 }
789 }else{
790 clause* c = clause_read(s, s->reasons[v]);
791 lit* lits = clause_begin(c);
792 int i;
793 for (i = 1; i < clause_size(c); i++){
794 int v = lit_var(lits[i]);
795 if (!var_tag(s,v) && var_level(s, v)){
796 if (s->reasons[v] != 0 && ((1 << (var_level(s, v) & 31)) & minl)){
797 veci_push(&s->stack,lit_var(lits[i]));
798 var_set_tag(s, v, 1);
799 }else{
800 solver2_clear_tags(s, top);
801 return 0;
802 }
803 }
804 }
805 }
806 }
807 return 1;
808 }
809
810
811 /*_________________________________________________________________________________________________
812 |
813 | analyzeFinal : (p : Lit) -> [void]
814 |
815 | Description:
816 | Specialized analysis procedure to express the final conflict in terms of assumptions.
817 | Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
818 | stores the result in 'out_conflict'.
819 |________________________________________________________________________________________________@*/
820 /*
821 void Solver::analyzeFinal(Clause* confl, bool skip_first)
822 {
823 // -- NOTE! This code is relatively untested. Please report bugs!
824 conflict.clear();
825 if (root_level == 0) return;
826
827 vec<char>& seen = analyze_seen;
828 for (int i = skip_first ? 1 : 0; i < confl->size(); i++){
829 Var x = var((*confl)[i]);
830 if (level[x] > 0)
831 seen[x] = 1;
832 }
833
834 int start = (root_level >= trail_lim.size()) ? trail.size()-1 : trail_lim[root_level];
835 for (int i = start; i >= trail_lim[0]; i--){
836 Var x = var(trail[i]);
837 if (seen[x]){
838 GClause r = reason[x];
839 if (r == GClause_NULL){
840 assert(level[x] > 0);
841 conflict.push(~trail[i]);
842 }else{
843 if (r.isLit()){
844 Lit p = r.lit();
845 if (level[var(p)] > 0)
846 seen[var(p)] = 1;
847 }else{
848 Clause& c = *r.clause();
849 for (int j = 1; j < c.size(); j++)
850 if (level[var(c[j])] > 0)
851 seen[var(c[j])] = 1;
852 }
853 }
854 seen[x] = 0;
855 }
856 }
857 }
858 */
859
860 #ifdef SAT_USE_ANALYZE_FINAL
861
sat_solver_analyze_final(sat_solver * s,int hConf,int skip_first)862 static void sat_solver_analyze_final(sat_solver* s, int hConf, int skip_first)
863 {
864 clause* conf = clause_read(s, hConf);
865 int i, j, start;
866 veci_resize(&s->conf_final,0);
867 if ( s->root_level == 0 )
868 return;
869 assert( veci_size(&s->tagged) == 0 );
870 // assert( s->tags[lit_var(p)] == l_Undef );
871 // s->tags[lit_var(p)] = l_True;
872 for (i = skip_first ? 1 : 0; i < clause_size(conf); i++)
873 {
874 int x = lit_var(clause_begin(conf)[i]);
875 if (var_level(s, x) > 0)
876 var_set_tag(s, x, 1);
877 }
878
879 start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level];
880 for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){
881 int x = lit_var(s->trail[i]);
882 if (var_tag(s,x)){
883 if (s->reasons[x] == 0){
884 assert(var_level(s, x) > 0);
885 veci_push(&s->conf_final,lit_neg(s->trail[i]));
886 }else{
887 if (clause_is_lit(s->reasons[x])){
888 lit q = clause_read_lit(s->reasons[x]);
889 assert(lit_var(q) >= 0 && lit_var(q) < s->size);
890 if (var_level(s, lit_var(q)) > 0)
891 var_set_tag(s, lit_var(q), 1);
892 }
893 else{
894 clause* c = clause_read(s, s->reasons[x]);
895 int* lits = clause_begin(c);
896 for (j = 1; j < clause_size(c); j++)
897 if (var_level(s, lit_var(lits[j])) > 0)
898 var_set_tag(s, lit_var(lits[j]), 1);
899 }
900 }
901 }
902 }
903 solver2_clear_tags(s,0);
904 }
905
906 #endif
907
sat_solver_analyze(sat_solver * s,int h,veci * learnt)908 static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
909 {
910 lit* trail = s->trail;
911 int cnt = 0;
912 lit p = lit_Undef;
913 int ind = s->qtail-1;
914 lit* lits;
915 int i, j, minl;
916 veci_push(learnt,lit_Undef);
917 do{
918 assert(h != 0);
919 if (clause_is_lit(h)){
920 int x = lit_var(clause_read_lit(h));
921 if (var_tag(s, x) == 0 && var_level(s, x) > 0){
922 var_set_tag(s, x, 1);
923 act_var_bump(s,x);
924 if (var_level(s, x) == sat_solver_dl(s))
925 cnt++;
926 else
927 veci_push(learnt,clause_read_lit(h));
928 }
929 }else{
930 clause* c = clause_read(s, h);
931
932 if (clause_learnt(c))
933 act_clause_bump(s,c);
934 lits = clause_begin(c);
935 //printlits(lits,lits+clause_size(c)); printf("\n");
936 for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
937 int x = lit_var(lits[j]);
938 if (var_tag(s, x) == 0 && var_level(s, x) > 0){
939 var_set_tag(s, x, 1);
940 act_var_bump(s,x);
941 // bump variables propaged by the LBD=2 clause
942 // if ( s->reasons[x] && clause_read(s, s->reasons[x])->lbd <= 2 )
943 // act_var_bump(s,x);
944 if (var_level(s,x) == sat_solver_dl(s))
945 cnt++;
946 else
947 veci_push(learnt,lits[j]);
948 }
949 }
950 }
951
952 while ( !var_tag(s, lit_var(trail[ind--])) );
953
954 p = trail[ind+1];
955 h = s->reasons[lit_var(p)];
956 cnt--;
957
958 }while (cnt > 0);
959
960 *veci_begin(learnt) = lit_neg(p);
961
962 lits = veci_begin(learnt);
963 minl = 0;
964 for (i = 1; i < veci_size(learnt); i++){
965 int lev = var_level(s, lit_var(lits[i]));
966 minl |= 1 << (lev & 31);
967 }
968
969 // simplify (full)
970 for (i = j = 1; i < veci_size(learnt); i++){
971 if (s->reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lit_var(lits[i]),minl))
972 lits[j++] = lits[i];
973 }
974
975 // update size of learnt + statistics
976 veci_resize(learnt,j);
977 s->stats.tot_literals += j;
978
979
980 // clear tags
981 solver2_clear_tags(s,0);
982
983 #ifdef DEBUG
984 for (i = 0; i < s->size; i++)
985 assert(!var_tag(s, i));
986 #endif
987
988 #ifdef VERBOSEDEBUG
989 printf(L_IND"Learnt {", L_ind);
990 for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i]));
991 #endif
992 if (veci_size(learnt) > 1){
993 int max_i = 1;
994 int max = var_level(s, lit_var(lits[1]));
995 lit tmp;
996
997 for (i = 2; i < veci_size(learnt); i++)
998 if (var_level(s, lit_var(lits[i])) > max){
999 max = var_level(s, lit_var(lits[i]));
1000 max_i = i;
1001 }
1002
1003 tmp = lits[1];
1004 lits[1] = lits[max_i];
1005 lits[max_i] = tmp;
1006 }
1007 #ifdef VERBOSEDEBUG
1008 {
1009 int lev = veci_size(learnt) > 1 ? var_level(s, lit_var(lits[1])) : 0;
1010 printf(" } at level %d\n", lev);
1011 }
1012 #endif
1013 }
1014
1015 //#define TEST_CNF_LOAD
1016
sat_solver_propagate(sat_solver * s)1017 int sat_solver_propagate(sat_solver* s)
1018 {
1019 int hConfl = 0;
1020 lit* lits;
1021 lit false_lit;
1022
1023 //printf("sat_solver_propagate\n");
1024 while (hConfl == 0 && s->qtail - s->qhead > 0){
1025 lit p = s->trail[s->qhead++];
1026
1027 #ifdef TEST_CNF_LOAD
1028 int v = lit_var(p);
1029 if ( s->pCnfFunc )
1030 {
1031 if ( lit_sign(p) )
1032 {
1033 if ( (s->loads[v] & 1) == 0 )
1034 {
1035 s->loads[v] ^= 1;
1036 s->pCnfFunc( s->pCnfMan, p );
1037 }
1038 }
1039 else
1040 {
1041 if ( (s->loads[v] & 2) == 0 )
1042 {
1043 s->loads[v] ^= 2;
1044 s->pCnfFunc( s->pCnfMan, p );
1045 }
1046 }
1047 }
1048 {
1049 #endif
1050
1051 veci* ws = sat_solver_read_wlist(s,p);
1052 int* begin = veci_begin(ws);
1053 int* end = begin + veci_size(ws);
1054 int*i, *j;
1055
1056 s->stats.propagations++;
1057 // s->simpdb_props--;
1058
1059 //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
1060 for (i = j = begin; i < end; ){
1061 if (clause_is_lit(*i)){
1062
1063 int Lit = clause_read_lit(*i);
1064 if (var_value(s, lit_var(Lit)) == lit_sign(Lit)){
1065 *j++ = *i++;
1066 continue;
1067 }
1068
1069 *j++ = *i;
1070 if (!sat_solver_enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
1071 hConfl = s->hBinary;
1072 (clause_begin(s->binary))[1] = lit_neg(p);
1073 (clause_begin(s->binary))[0] = clause_read_lit(*i++);
1074 // Copy the remaining watches:
1075 while (i < end)
1076 *j++ = *i++;
1077 }
1078 }else{
1079
1080 clause* c = clause_read(s,*i);
1081 lits = clause_begin(c);
1082
1083 // Make sure the false literal is data[1]:
1084 false_lit = lit_neg(p);
1085 if (lits[0] == false_lit){
1086 lits[0] = lits[1];
1087 lits[1] = false_lit;
1088 }
1089 assert(lits[1] == false_lit);
1090
1091 // If 0th watch is true, then clause is already satisfied.
1092 if (var_value(s, lit_var(lits[0])) == lit_sign(lits[0]))
1093 *j++ = *i;
1094 else{
1095 // Look for new watch:
1096 lit* stop = lits + clause_size(c);
1097 lit* k;
1098 for (k = lits + 2; k < stop; k++){
1099 if (var_value(s, lit_var(*k)) != !lit_sign(*k)){
1100 lits[1] = *k;
1101 *k = false_lit;
1102 veci_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
1103 goto next; }
1104 }
1105
1106 *j++ = *i;
1107 // Clause is unit under assignment:
1108 if ( c->lrn )
1109 c->lbd = sat_clause_compute_lbd(s, c);
1110 if (!sat_solver_enqueue(s,lits[0], *i)){
1111 hConfl = *i++;
1112 // Copy the remaining watches:
1113 while (i < end)
1114 *j++ = *i++;
1115 }
1116 }
1117 }
1118 next:
1119 i++;
1120 }
1121
1122 s->stats.inspects += j - veci_begin(ws);
1123 veci_resize(ws,j - veci_begin(ws));
1124 #ifdef TEST_CNF_LOAD
1125 }
1126 #endif
1127 }
1128
1129 return hConfl;
1130 }
1131
1132 //=================================================================================================
1133 // External solver functions:
1134
sat_solver_new(void)1135 sat_solver* sat_solver_new(void)
1136 {
1137 sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver));
1138
1139 // Vec_SetAlloc_(&s->Mem, 15);
1140 Sat_MemAlloc_(&s->Mem, 17);
1141 s->hLearnts = -1;
1142 s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
1143 s->binary = clause_read( s, s->hBinary );
1144
1145 s->nLearntStart = LEARNT_MAX_START_DEFAULT; // starting learned clause limit
1146 s->nLearntDelta = LEARNT_MAX_INCRE_DEFAULT; // delta of learned clause limit
1147 s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT; // ratio of learned clause limit
1148 s->nLearntMax = s->nLearntStart;
1149
1150 // initialize vectors
1151 veci_new(&s->order);
1152 veci_new(&s->trail_lim);
1153 veci_new(&s->tagged);
1154 // veci_new(&s->learned);
1155 veci_new(&s->act_clas);
1156 veci_new(&s->stack);
1157 // veci_new(&s->model);
1158 veci_new(&s->unit_lits);
1159 veci_new(&s->temp_clause);
1160 veci_new(&s->conf_final);
1161
1162 // initialize arrays
1163 s->wlists = 0;
1164 s->activity = 0;
1165 s->orderpos = 0;
1166 s->reasons = 0;
1167 s->trail = 0;
1168
1169 // initialize other vars
1170 s->size = 0;
1171 s->cap = 0;
1172 s->qhead = 0;
1173 s->qtail = 0;
1174
1175 solver_init_activities(s);
1176 veci_new(&s->act_vars);
1177
1178 s->root_level = 0;
1179 // s->simpdb_assigns = 0;
1180 // s->simpdb_props = 0;
1181 s->random_seed = 91648253;
1182 s->progress_estimate = 0;
1183 // s->binary = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
1184 // s->binary->size_learnt = (2 << 1);
1185 s->verbosity = 0;
1186
1187 s->stats.starts = 0;
1188 s->stats.decisions = 0;
1189 s->stats.propagations = 0;
1190 s->stats.inspects = 0;
1191 s->stats.conflicts = 0;
1192 s->stats.clauses = 0;
1193 s->stats.clauses_literals = 0;
1194 s->stats.learnts = 0;
1195 s->stats.learnts_literals = 0;
1196 s->stats.tot_literals = 0;
1197 return s;
1198 }
1199
zsat_solver_new_seed(double seed)1200 sat_solver* zsat_solver_new_seed(double seed)
1201 {
1202 sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver));
1203
1204 // Vec_SetAlloc_(&s->Mem, 15);
1205 Sat_MemAlloc_(&s->Mem, 15);
1206 s->hLearnts = -1;
1207 s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
1208 s->binary = clause_read( s, s->hBinary );
1209
1210 s->nLearntStart = LEARNT_MAX_START_DEFAULT; // starting learned clause limit
1211 s->nLearntDelta = LEARNT_MAX_INCRE_DEFAULT; // delta of learned clause limit
1212 s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT; // ratio of learned clause limit
1213 s->nLearntMax = s->nLearntStart;
1214
1215 // initialize vectors
1216 veci_new(&s->order);
1217 veci_new(&s->trail_lim);
1218 veci_new(&s->tagged);
1219 // veci_new(&s->learned);
1220 veci_new(&s->act_clas);
1221 veci_new(&s->stack);
1222 // veci_new(&s->model);
1223 veci_new(&s->unit_lits);
1224 veci_new(&s->temp_clause);
1225 veci_new(&s->conf_final);
1226
1227 // initialize arrays
1228 s->wlists = 0;
1229 s->activity = 0;
1230 s->orderpos = 0;
1231 s->reasons = 0;
1232 s->trail = 0;
1233
1234 // initialize other vars
1235 s->size = 0;
1236 s->cap = 0;
1237 s->qhead = 0;
1238 s->qtail = 0;
1239
1240 solver_init_activities(s);
1241 veci_new(&s->act_vars);
1242
1243 s->root_level = 0;
1244 // s->simpdb_assigns = 0;
1245 // s->simpdb_props = 0;
1246 s->random_seed = seed;
1247 s->progress_estimate = 0;
1248 // s->binary = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
1249 // s->binary->size_learnt = (2 << 1);
1250 s->verbosity = 0;
1251
1252 s->stats.starts = 0;
1253 s->stats.decisions = 0;
1254 s->stats.propagations = 0;
1255 s->stats.inspects = 0;
1256 s->stats.conflicts = 0;
1257 s->stats.clauses = 0;
1258 s->stats.clauses_literals = 0;
1259 s->stats.learnts = 0;
1260 s->stats.learnts_literals = 0;
1261 s->stats.tot_literals = 0;
1262 return s;
1263 }
1264
sat_solver_addvar(sat_solver * s)1265 int sat_solver_addvar(sat_solver* s)
1266 {
1267 sat_solver_setnvars(s, s->size+1);
1268 return s->size-1;
1269 }
sat_solver_setnvars(sat_solver * s,int n)1270 void sat_solver_setnvars(sat_solver* s,int n)
1271 {
1272 int var;
1273
1274 if (s->cap < n){
1275 int old_cap = s->cap;
1276 while (s->cap < n) s->cap = s->cap*2+1;
1277 if ( s->cap < 50000 )
1278 s->cap = 50000;
1279
1280 s->wlists = ABC_REALLOC(veci, s->wlists, s->cap*2);
1281 // s->vi = ABC_REALLOC(varinfo,s->vi, s->cap);
1282 s->levels = ABC_REALLOC(int, s->levels, s->cap);
1283 s->assigns = ABC_REALLOC(char, s->assigns, s->cap);
1284 s->polarity = ABC_REALLOC(char, s->polarity, s->cap);
1285 s->tags = ABC_REALLOC(char, s->tags, s->cap);
1286 s->loads = ABC_REALLOC(char, s->loads, s->cap);
1287 s->activity = ABC_REALLOC(word, s->activity, s->cap);
1288 s->activity2 = ABC_REALLOC(word, s->activity2,s->cap);
1289 s->pFreqs = ABC_REALLOC(char, s->pFreqs, s->cap);
1290
1291 if ( s->factors )
1292 s->factors = ABC_REALLOC(double, s->factors, s->cap);
1293 s->orderpos = ABC_REALLOC(int, s->orderpos, s->cap);
1294 s->reasons = ABC_REALLOC(int, s->reasons, s->cap);
1295 s->trail = ABC_REALLOC(lit, s->trail, s->cap);
1296 s->model = ABC_REALLOC(int, s->model, s->cap);
1297 memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(veci) );
1298 }
1299
1300 for (var = s->size; var < n; var++){
1301 assert(!s->wlists[2*var].size);
1302 assert(!s->wlists[2*var+1].size);
1303 if ( s->wlists[2*var].ptr == NULL )
1304 veci_new(&s->wlists[2*var]);
1305 if ( s->wlists[2*var+1].ptr == NULL )
1306 veci_new(&s->wlists[2*var+1]);
1307
1308 if ( s->VarActType == 0 )
1309 s->activity[var] = (1<<10);
1310 else if ( s->VarActType == 1 )
1311 s->activity[var] = 0;
1312 else if ( s->VarActType == 2 )
1313 s->activity[var] = 0;
1314 else assert(0);
1315
1316 s->pFreqs[var] = 0;
1317 if ( s->factors )
1318 s->factors [var] = 0;
1319 // *((int*)s->vi + var) = 0; s->vi[var].val = varX;
1320 s->levels [var] = 0;
1321 s->assigns [var] = varX;
1322 s->polarity[var] = 0;
1323 s->tags [var] = 0;
1324 s->loads [var] = 0;
1325 s->orderpos[var] = veci_size(&s->order);
1326 s->reasons [var] = 0;
1327 s->model [var] = 0;
1328
1329 /* does not hold because variables enqueued at top level will not be reinserted in the heap
1330 assert(veci_size(&s->order) == var);
1331 */
1332 veci_push(&s->order,var);
1333 order_update(s, var);
1334 }
1335
1336 s->size = n > s->size ? n : s->size;
1337 }
1338
sat_solver_delete(sat_solver * s)1339 void sat_solver_delete(sat_solver* s)
1340 {
1341 // Vec_SetFree_( &s->Mem );
1342 Sat_MemFree_( &s->Mem );
1343
1344 // delete vectors
1345 veci_delete(&s->order);
1346 veci_delete(&s->trail_lim);
1347 veci_delete(&s->tagged);
1348 // veci_delete(&s->learned);
1349 veci_delete(&s->act_clas);
1350 veci_delete(&s->stack);
1351 // veci_delete(&s->model);
1352 veci_delete(&s->act_vars);
1353 veci_delete(&s->unit_lits);
1354 veci_delete(&s->pivot_vars);
1355 veci_delete(&s->temp_clause);
1356 veci_delete(&s->conf_final);
1357
1358 veci_delete(&s->user_vars);
1359 veci_delete(&s->user_values);
1360
1361 // delete arrays
1362 if (s->reasons != 0){
1363 int i;
1364 for (i = 0; i < s->cap*2; i++)
1365 veci_delete(&s->wlists[i]);
1366 ABC_FREE(s->wlists );
1367 // ABC_FREE(s->vi );
1368 ABC_FREE(s->levels );
1369 ABC_FREE(s->assigns );
1370 ABC_FREE(s->polarity );
1371 ABC_FREE(s->tags );
1372 ABC_FREE(s->loads );
1373 ABC_FREE(s->activity );
1374 ABC_FREE(s->activity2);
1375 ABC_FREE(s->pFreqs );
1376 ABC_FREE(s->factors );
1377 ABC_FREE(s->orderpos );
1378 ABC_FREE(s->reasons );
1379 ABC_FREE(s->trail );
1380 ABC_FREE(s->model );
1381 }
1382
1383 sat_solver_store_free(s);
1384 ABC_FREE(s);
1385 }
1386
sat_solver_restart(sat_solver * s)1387 void sat_solver_restart( sat_solver* s )
1388 {
1389 int i;
1390 Sat_MemRestart( &s->Mem );
1391 s->hLearnts = -1;
1392 s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
1393 s->binary = clause_read( s, s->hBinary );
1394
1395 veci_resize(&s->trail_lim, 0);
1396 veci_resize(&s->order, 0);
1397 for ( i = 0; i < s->size*2; i++ )
1398 s->wlists[i].size = 0;
1399
1400 s->nDBreduces = 0;
1401
1402 // initialize other vars
1403 s->size = 0;
1404 // s->cap = 0;
1405 s->qhead = 0;
1406 s->qtail = 0;
1407
1408
1409 // variable activities
1410 solver_init_activities(s);
1411 veci_resize(&s->act_clas, 0);
1412
1413
1414 s->root_level = 0;
1415 // s->simpdb_assigns = 0;
1416 // s->simpdb_props = 0;
1417 s->random_seed = 91648253;
1418 s->progress_estimate = 0;
1419 s->verbosity = 0;
1420
1421 s->stats.starts = 0;
1422 s->stats.decisions = 0;
1423 s->stats.propagations = 0;
1424 s->stats.inspects = 0;
1425 s->stats.conflicts = 0;
1426 s->stats.clauses = 0;
1427 s->stats.clauses_literals = 0;
1428 s->stats.learnts = 0;
1429 s->stats.learnts_literals = 0;
1430 s->stats.tot_literals = 0;
1431 }
1432
zsat_solver_restart_seed(sat_solver * s,double seed)1433 void zsat_solver_restart_seed( sat_solver* s, double seed )
1434 {
1435 int i;
1436 Sat_MemRestart( &s->Mem );
1437 s->hLearnts = -1;
1438 s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
1439 s->binary = clause_read( s, s->hBinary );
1440
1441 veci_resize(&s->trail_lim, 0);
1442 veci_resize(&s->order, 0);
1443 for ( i = 0; i < s->size*2; i++ )
1444 s->wlists[i].size = 0;
1445
1446 s->nDBreduces = 0;
1447
1448 // initialize other vars
1449 s->size = 0;
1450 // s->cap = 0;
1451 s->qhead = 0;
1452 s->qtail = 0;
1453
1454 solver_init_activities(s);
1455 veci_resize(&s->act_clas, 0);
1456
1457 s->root_level = 0;
1458 // s->simpdb_assigns = 0;
1459 // s->simpdb_props = 0;
1460 s->random_seed = seed;
1461 s->progress_estimate = 0;
1462 s->verbosity = 0;
1463
1464 s->stats.starts = 0;
1465 s->stats.decisions = 0;
1466 s->stats.propagations = 0;
1467 s->stats.inspects = 0;
1468 s->stats.conflicts = 0;
1469 s->stats.clauses = 0;
1470 s->stats.clauses_literals = 0;
1471 s->stats.learnts = 0;
1472 s->stats.learnts_literals = 0;
1473 s->stats.tot_literals = 0;
1474 }
1475
1476 // returns memory in bytes used by the SAT solver
sat_solver_memory(sat_solver * s)1477 double sat_solver_memory( sat_solver* s )
1478 {
1479 int i;
1480 double Mem = sizeof(sat_solver);
1481 for (i = 0; i < s->cap*2; i++)
1482 Mem += s->wlists[i].cap * sizeof(int);
1483 Mem += s->cap * sizeof(veci); // ABC_FREE(s->wlists );
1484 Mem += s->cap * sizeof(int); // ABC_FREE(s->levels );
1485 Mem += s->cap * sizeof(char); // ABC_FREE(s->assigns );
1486 Mem += s->cap * sizeof(char); // ABC_FREE(s->polarity );
1487 Mem += s->cap * sizeof(char); // ABC_FREE(s->tags );
1488 Mem += s->cap * sizeof(char); // ABC_FREE(s->loads );
1489 Mem += s->cap * sizeof(word); // ABC_FREE(s->activity );
1490 if ( s->activity2 )
1491 Mem += s->cap * sizeof(word); // ABC_FREE(s->activity );
1492 if ( s->factors )
1493 Mem += s->cap * sizeof(double); // ABC_FREE(s->factors );
1494 Mem += s->cap * sizeof(int); // ABC_FREE(s->orderpos );
1495 Mem += s->cap * sizeof(int); // ABC_FREE(s->reasons );
1496 Mem += s->cap * sizeof(lit); // ABC_FREE(s->trail );
1497 Mem += s->cap * sizeof(int); // ABC_FREE(s->model );
1498
1499 Mem += s->order.cap * sizeof(int);
1500 Mem += s->trail_lim.cap * sizeof(int);
1501 Mem += s->tagged.cap * sizeof(int);
1502 // Mem += s->learned.cap * sizeof(int);
1503 Mem += s->stack.cap * sizeof(int);
1504 Mem += s->act_vars.cap * sizeof(int);
1505 Mem += s->unit_lits.cap * sizeof(int);
1506 Mem += s->act_clas.cap * sizeof(int);
1507 Mem += s->temp_clause.cap * sizeof(int);
1508 Mem += s->conf_final.cap * sizeof(int);
1509 Mem += Sat_MemMemoryAll( &s->Mem );
1510 return Mem;
1511 }
1512
sat_solver_simplify(sat_solver * s)1513 int sat_solver_simplify(sat_solver* s)
1514 {
1515 assert(sat_solver_dl(s) == 0);
1516 if (sat_solver_propagate(s) != 0)
1517 return false;
1518 return true;
1519 }
1520
sat_solver_reducedb(sat_solver * s)1521 void sat_solver_reducedb(sat_solver* s)
1522 {
1523 static abctime TimeTotal = 0;
1524 abctime clk = Abc_Clock();
1525 Sat_Mem_t * pMem = &s->Mem;
1526 int nLearnedOld = veci_size(&s->act_clas);
1527 int * act_clas = veci_begin(&s->act_clas);
1528 int * pPerm, * pArray, * pSortValues, nCutoffValue;
1529 int i, k, j, Id, Counter, CounterStart, nSelected;
1530 clause * c;
1531
1532 assert( s->nLearntMax > 0 );
1533 assert( nLearnedOld == Sat_MemEntryNum(pMem, 1) );
1534 assert( nLearnedOld == (int)s->stats.learnts );
1535
1536 s->nDBreduces++;
1537
1538 //printf( "Calling reduceDB with %d learned clause limit.\n", s->nLearntMax );
1539 s->nLearntMax = s->nLearntStart + s->nLearntDelta * s->nDBreduces;
1540 // return;
1541
1542 // create sorting values
1543 pSortValues = ABC_ALLOC( int, nLearnedOld );
1544 Sat_MemForEachLearned( pMem, c, i, k )
1545 {
1546 Id = clause_id(c);
1547 // pSortValues[Id] = act[Id];
1548 if ( s->ClaActType == 0 )
1549 pSortValues[Id] = ((7 - Abc_MinInt(c->lbd, 7)) << 28) | (act_clas[Id] >> 4);
1550 else
1551 pSortValues[Id] = ((7 - Abc_MinInt(c->lbd, 7)) << 28);// | (act_clas[Id] >> 4);
1552 assert( pSortValues[Id] >= 0 );
1553 }
1554
1555 // preserve 1/20 of last clauses
1556 CounterStart = nLearnedOld - (s->nLearntMax / 20);
1557
1558 // preserve 3/4 of most active clauses
1559 nSelected = nLearnedOld*s->nLearntRatio/100;
1560
1561 // find non-decreasing permutation
1562 pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld );
1563 assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] );
1564 nCutoffValue = pSortValues[pPerm[nLearnedOld-nSelected]];
1565 ABC_FREE( pPerm );
1566 // ActCutOff = ABC_INFINITY;
1567
1568 // mark learned clauses to remove
1569 Counter = j = 0;
1570 Sat_MemForEachLearned( pMem, c, i, k )
1571 {
1572 assert( c->mark == 0 );
1573 if ( Counter++ > CounterStart || clause_size(c) < 3 || pSortValues[clause_id(c)] > nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) )
1574 act_clas[j++] = act_clas[clause_id(c)];
1575 else // delete
1576 {
1577 c->mark = 1;
1578 s->stats.learnts_literals -= clause_size(c);
1579 s->stats.learnts--;
1580 }
1581 }
1582 assert( s->stats.learnts == (unsigned)j );
1583 assert( Counter == nLearnedOld );
1584 veci_resize(&s->act_clas,j);
1585 ABC_FREE( pSortValues );
1586
1587 // update ID of each clause to be its new handle
1588 Counter = Sat_MemCompactLearned( pMem, 0 );
1589 assert( Counter == (int)s->stats.learnts );
1590
1591 // update reasons
1592 for ( i = 0; i < s->size; i++ )
1593 {
1594 if ( !s->reasons[i] ) // no reason
1595 continue;
1596 if ( clause_is_lit(s->reasons[i]) ) // 2-lit clause
1597 continue;
1598 if ( !clause_learnt_h(pMem, s->reasons[i]) ) // problem clause
1599 continue;
1600 c = clause_read( s, s->reasons[i] );
1601 assert( c->mark == 0 );
1602 s->reasons[i] = clause_id(c); // updating handle here!!!
1603 }
1604
1605 // update watches
1606 for ( i = 0; i < s->size*2; i++ )
1607 {
1608 pArray = veci_begin(&s->wlists[i]);
1609 for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
1610 {
1611 if ( clause_is_lit(pArray[k]) ) // 2-lit clause
1612 pArray[j++] = pArray[k];
1613 else if ( !clause_learnt_h(pMem, pArray[k]) ) // problem clause
1614 pArray[j++] = pArray[k];
1615 else
1616 {
1617 c = clause_read(s, pArray[k]);
1618 if ( !c->mark ) // useful learned clause
1619 pArray[j++] = clause_id(c); // updating handle here!!!
1620 }
1621 }
1622 veci_resize(&s->wlists[i],j);
1623 }
1624
1625 // perform final move of the clauses
1626 Counter = Sat_MemCompactLearned( pMem, 1 );
1627 assert( Counter == (int)s->stats.learnts );
1628
1629 // report the results
1630 TimeTotal += Abc_Clock() - clk;
1631 if ( s->fVerbose )
1632 {
1633 Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ",
1634 s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld );
1635 Abc_PrintTime( 1, "Time", TimeTotal );
1636 }
1637 }
1638
1639
1640 // reverses to the previously bookmarked point
sat_solver_rollback(sat_solver * s)1641 void sat_solver_rollback( sat_solver* s )
1642 {
1643 Sat_Mem_t * pMem = &s->Mem;
1644 int i, k, j;
1645 static int Count = 0;
1646 Count++;
1647 assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
1648 assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail );
1649 // reset implication queue
1650 sat_solver_canceluntil_rollback( s, s->iTrailPivot );
1651 // update order
1652 if ( s->iVarPivot < s->size )
1653 {
1654 if ( s->activity2 )
1655 {
1656 s->var_inc = s->var_inc2;
1657 memcpy( s->activity, s->activity2, sizeof(word) * s->iVarPivot );
1658 }
1659 veci_resize(&s->order, 0);
1660 for ( i = 0; i < s->iVarPivot; i++ )
1661 {
1662 if ( var_value(s, i) != varX )
1663 continue;
1664 s->orderpos[i] = veci_size(&s->order);
1665 veci_push(&s->order,i);
1666 order_update(s, i);
1667 }
1668 }
1669 // compact watches
1670 for ( i = 0; i < s->iVarPivot*2; i++ )
1671 {
1672 cla* pArray = veci_begin(&s->wlists[i]);
1673 for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
1674 {
1675 if ( clause_is_lit(pArray[k]) )
1676 {
1677 if ( clause_read_lit(pArray[k]) < s->iVarPivot*2 )
1678 pArray[j++] = pArray[k];
1679 }
1680 else if ( Sat_MemClauseUsed(pMem, pArray[k]) )
1681 pArray[j++] = pArray[k];
1682 }
1683 veci_resize(&s->wlists[i],j);
1684 }
1685 // reset watcher lists
1686 for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
1687 s->wlists[i].size = 0;
1688
1689 // reset clause counts
1690 s->stats.clauses = pMem->BookMarkE[0];
1691 s->stats.learnts = pMem->BookMarkE[1];
1692 // rollback clauses
1693 Sat_MemRollBack( pMem );
1694
1695 // resize learned arrays
1696 veci_resize(&s->act_clas, s->stats.learnts);
1697
1698 // initialize other vars
1699 s->size = s->iVarPivot;
1700 if ( s->size == 0 )
1701 {
1702 // s->size = 0;
1703 // s->cap = 0;
1704 s->qhead = 0;
1705 s->qtail = 0;
1706
1707 solver_init_activities(s);
1708
1709 s->root_level = 0;
1710 s->random_seed = 91648253;
1711 s->progress_estimate = 0;
1712 s->verbosity = 0;
1713
1714 s->stats.starts = 0;
1715 s->stats.decisions = 0;
1716 s->stats.propagations = 0;
1717 s->stats.inspects = 0;
1718 s->stats.conflicts = 0;
1719 s->stats.clauses = 0;
1720 s->stats.clauses_literals = 0;
1721 s->stats.learnts = 0;
1722 s->stats.learnts_literals = 0;
1723 s->stats.tot_literals = 0;
1724
1725 // initialize rollback
1726 s->iVarPivot = 0; // the pivot for variables
1727 s->iTrailPivot = 0; // the pivot for trail
1728 s->hProofPivot = 1; // the pivot for proof records
1729 }
1730 }
1731
1732
sat_solver_addclause(sat_solver * s,lit * begin,lit * end)1733 int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
1734 {
1735 lit *i,*j;
1736 int maxvar;
1737 lit last;
1738 assert( begin < end );
1739 if ( s->fPrintClause )
1740 {
1741 for ( i = begin; i < end; i++ )
1742 printf( "%s%d ", (*i)&1 ? "!":"", (*i)>>1 );
1743 printf( "\n" );
1744 }
1745
1746 veci_resize( &s->temp_clause, 0 );
1747 for ( i = begin; i < end; i++ )
1748 veci_push( &s->temp_clause, *i );
1749 begin = veci_begin( &s->temp_clause );
1750 end = begin + veci_size( &s->temp_clause );
1751
1752 // insertion sort
1753 maxvar = lit_var(*begin);
1754 for (i = begin + 1; i < end; i++){
1755 lit l = *i;
1756 maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
1757 for (j = i; j > begin && *(j-1) > l; j--)
1758 *j = *(j-1);
1759 *j = l;
1760 }
1761 sat_solver_setnvars(s,maxvar+1);
1762
1763 ///////////////////////////////////
1764 // add clause to internal storage
1765 if ( s->pStore )
1766 {
1767 int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
1768 assert( RetValue );
1769 (void) RetValue;
1770 }
1771 ///////////////////////////////////
1772
1773 // delete duplicates
1774 last = lit_Undef;
1775 for (i = j = begin; i < end; i++){
1776 //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]));
1777 if (*i == lit_neg(last) || var_value(s, lit_var(*i)) == lit_sign(*i))
1778 return true; // tautology
1779 else if (*i != last && var_value(s, lit_var(*i)) == varX)
1780 last = *j++ = *i;
1781 }
1782 // j = i;
1783
1784 if (j == begin) // empty clause
1785 return false;
1786
1787 if (j - begin == 1) // unit clause
1788 return sat_solver_enqueue(s,*begin,0);
1789
1790 // create new clause
1791 sat_solver_clause_new(s,begin,j,0);
1792 return true;
1793 }
1794
luby(double y,int x)1795 double luby(double y, int x)
1796 {
1797 int size, seq;
1798 for (size = 1, seq = 0; size < x+1; seq++, size = 2*size + 1);
1799 while (size-1 != x){
1800 size = (size-1) >> 1;
1801 seq--;
1802 x = x % size;
1803 }
1804 return pow(y, (double)seq);
1805 }
1806
luby_test()1807 void luby_test()
1808 {
1809 int i;
1810 for ( i = 0; i < 20; i++ )
1811 printf( "%d ", (int)luby(2,i) );
1812 printf( "\n" );
1813 }
1814
sat_solver_search(sat_solver * s,ABC_INT64_T nof_conflicts)1815 static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
1816 {
1817 // double var_decay = 0.95;
1818 // double clause_decay = 0.999;
1819 double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
1820 ABC_INT64_T conflictC = 0;
1821 veci learnt_clause;
1822 int i;
1823
1824 assert(s->root_level == sat_solver_dl(s));
1825
1826 s->nRestarts++;
1827 s->stats.starts++;
1828 // s->var_decay = (float)(1 / var_decay ); // move this to sat_solver_new()
1829 // s->cla_decay = (float)(1 / clause_decay); // move this to sat_solver_new()
1830 // veci_resize(&s->model,0);
1831 veci_new(&learnt_clause);
1832
1833 // use activity factors in every even restart
1834 if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 )
1835 // if ( veci_size(&s->act_vars) > 0 )
1836 for ( i = 0; i < s->act_vars.size; i++ )
1837 act_var_bump_factor(s, s->act_vars.ptr[i]);
1838
1839 // use activity factors in every restart
1840 if ( s->pGlobalVars && veci_size(&s->act_vars) > 0 )
1841 for ( i = 0; i < s->act_vars.size; i++ )
1842 act_var_bump_global(s, s->act_vars.ptr[i]);
1843
1844 for (;;){
1845 int hConfl = sat_solver_propagate(s);
1846 if (hConfl != 0){
1847 // CONFLICT
1848 int blevel;
1849
1850 #ifdef VERBOSEDEBUG
1851 printf(L_IND"**CONFLICT**\n", L_ind);
1852 #endif
1853 s->stats.conflicts++; conflictC++;
1854 if (sat_solver_dl(s) == s->root_level){
1855 #ifdef SAT_USE_ANALYZE_FINAL
1856 sat_solver_analyze_final(s, hConfl, 0);
1857 #endif
1858 veci_delete(&learnt_clause);
1859 return l_False;
1860 }
1861
1862 veci_resize(&learnt_clause,0);
1863 sat_solver_analyze(s, hConfl, &learnt_clause);
1864 blevel = veci_size(&learnt_clause) > 1 ? var_level(s, lit_var(veci_begin(&learnt_clause)[1])) : s->root_level;
1865 blevel = s->root_level > blevel ? s->root_level : blevel;
1866 sat_solver_canceluntil(s,blevel);
1867 sat_solver_record(s,&learnt_clause);
1868 #ifdef SAT_USE_ANALYZE_FINAL
1869 // if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0; // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions)
1870 if ( learnt_clause.size == 1 )
1871 var_set_level(s, lit_var(learnt_clause.ptr[0]), 0);
1872 #endif
1873 act_var_decay(s);
1874 act_clause_decay(s);
1875
1876 }else{
1877 // NO CONFLICT
1878 int next;
1879
1880 // Reached bound on number of conflicts:
1881 if ( (!s->fNoRestarts && nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){
1882 s->progress_estimate = sat_solver_progress(s);
1883 sat_solver_canceluntil(s,s->root_level);
1884 veci_delete(&learnt_clause);
1885 return l_Undef; }
1886
1887 // Reached bound on number of conflicts:
1888 if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
1889 (s->nInsLimit && s->stats.propagations > s->nInsLimit) )
1890 {
1891 s->progress_estimate = sat_solver_progress(s);
1892 sat_solver_canceluntil(s,s->root_level);
1893 veci_delete(&learnt_clause);
1894 return l_Undef;
1895 }
1896
1897 // Simplify the set of problem clauses:
1898 if (sat_solver_dl(s) == 0 && !s->fSkipSimplify)
1899 sat_solver_simplify(s);
1900
1901 // Reduce the set of learnt clauses:
1902 // if (s->nLearntMax && veci_size(&s->learned) - s->qtail >= s->nLearntMax)
1903 if (s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax)
1904 sat_solver_reducedb(s);
1905
1906 // New variable decision:
1907 s->stats.decisions++;
1908 next = order_select(s,(float)random_var_freq);
1909
1910 if (next == var_Undef){
1911 // Model found:
1912 int i;
1913 for (i = 0; i < s->size; i++)
1914 s->model[i] = (var_value(s,i)==var1 ? l_True : l_False);
1915 sat_solver_canceluntil(s,s->root_level);
1916 veci_delete(&learnt_clause);
1917
1918 /*
1919 veci apa; veci_new(&apa);
1920 for (i = 0; i < s->size; i++)
1921 veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i))));
1922 printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n");
1923 veci_delete(&apa);
1924 */
1925
1926 return l_True;
1927 }
1928
1929 if ( var_polar(s, next) ) // positive polarity
1930 sat_solver_decision(s,toLit(next));
1931 else
1932 sat_solver_decision(s,lit_neg(toLit(next)));
1933 }
1934 }
1935
1936 return l_Undef; // cannot happen
1937 }
1938
1939 // internal call to the SAT solver
sat_solver_solve_internal(sat_solver * s)1940 int sat_solver_solve_internal(sat_solver* s)
1941 {
1942 lbool status = l_Undef;
1943 int restart_iter = 0;
1944 veci_resize(&s->unit_lits, 0);
1945 s->nCalls++;
1946
1947 if (s->verbosity >= 1){
1948 printf("==================================[MINISAT]===================================\n");
1949 printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n");
1950 printf("| | Clauses Literals | Limit Clauses Literals Lit/Cl | |\n");
1951 printf("==============================================================================\n");
1952 }
1953
1954 while (status == l_Undef){
1955 ABC_INT64_T nof_conflicts;
1956 double Ratio = (s->stats.learnts == 0)? 0.0 :
1957 s->stats.learnts_literals / (double)s->stats.learnts;
1958 if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
1959 break;
1960 if (s->verbosity >= 1)
1961 {
1962 printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n",
1963 (double)s->stats.conflicts,
1964 (double)s->stats.clauses,
1965 (double)s->stats.clauses_literals,
1966 (double)0,
1967 (double)s->stats.learnts,
1968 (double)s->stats.learnts_literals,
1969 Ratio,
1970 s->progress_estimate*100);
1971 fflush(stdout);
1972 }
1973 nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) );
1974 status = sat_solver_search(s, nof_conflicts);
1975 // quit the loop if reached an external limit
1976 if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
1977 break;
1978 if ( s->nInsLimit && s->stats.propagations > s->nInsLimit )
1979 break;
1980 if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
1981 break;
1982 if ( s->pFuncStop && s->pFuncStop(s->RunId) )
1983 break;
1984 }
1985 if (s->verbosity >= 1)
1986 printf("==============================================================================\n");
1987
1988 sat_solver_canceluntil(s,s->root_level);
1989 // save variable values
1990 if ( status == l_True && s->user_vars.size )
1991 {
1992 int v;
1993 for ( v = 0; v < s->user_vars.size; v++ )
1994 veci_push(&s->user_values, sat_solver_var_value(s, s->user_vars.ptr[v]));
1995 }
1996 return status;
1997 }
1998
1999 // pushing one assumption to the stack of assumptions
sat_solver_push(sat_solver * s,int p)2000 int sat_solver_push(sat_solver* s, int p)
2001 {
2002 assert(lit_var(p) < s->size);
2003 veci_push(&s->trail_lim,s->qtail);
2004 s->root_level++;
2005 if (!sat_solver_enqueue(s,p,0))
2006 {
2007 int h = s->reasons[lit_var(p)];
2008 if (h)
2009 {
2010 if (clause_is_lit(h))
2011 {
2012 (clause_begin(s->binary))[1] = lit_neg(p);
2013 (clause_begin(s->binary))[0] = clause_read_lit(h);
2014 h = s->hBinary;
2015 }
2016 sat_solver_analyze_final(s, h, 1);
2017 veci_push(&s->conf_final, lit_neg(p));
2018 }
2019 else
2020 {
2021 veci_resize(&s->conf_final,0);
2022 veci_push(&s->conf_final, lit_neg(p));
2023 // the two lines below are a bug fix by Siert Wieringa
2024 if (var_level(s, lit_var(p)) > 0)
2025 veci_push(&s->conf_final, p);
2026 }
2027 //sat_solver_canceluntil(s, 0);
2028 return false;
2029 }
2030 else
2031 {
2032 int fConfl = sat_solver_propagate(s);
2033 if (fConfl){
2034 sat_solver_analyze_final(s, fConfl, 0);
2035 //assert(s->conf_final.size > 0);
2036 //sat_solver_canceluntil(s, 0);
2037 return false; }
2038 }
2039 return true;
2040 }
2041
2042 // removing one assumption from the stack of assumptions
sat_solver_pop(sat_solver * s)2043 void sat_solver_pop(sat_solver* s)
2044 {
2045 assert( sat_solver_dl(s) > 0 );
2046 sat_solver_canceluntil(s, --s->root_level);
2047 }
2048
sat_solver_set_resource_limits(sat_solver * s,ABC_INT64_T nConfLimit,ABC_INT64_T nInsLimit,ABC_INT64_T nConfLimitGlobal,ABC_INT64_T nInsLimitGlobal)2049 void sat_solver_set_resource_limits(sat_solver* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
2050 {
2051 // set the external limits
2052 s->nRestarts = 0;
2053 s->nConfLimit = 0;
2054 s->nInsLimit = 0;
2055 if ( nConfLimit )
2056 s->nConfLimit = s->stats.conflicts + nConfLimit;
2057 if ( nInsLimit )
2058 // s->nInsLimit = s->stats.inspects + nInsLimit;
2059 s->nInsLimit = s->stats.propagations + nInsLimit;
2060 if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) )
2061 s->nConfLimit = nConfLimitGlobal;
2062 if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
2063 s->nInsLimit = nInsLimitGlobal;
2064 }
2065
sat_solver_solve(sat_solver * s,lit * begin,lit * end,ABC_INT64_T nConfLimit,ABC_INT64_T nInsLimit,ABC_INT64_T nConfLimitGlobal,ABC_INT64_T nInsLimitGlobal)2066 int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
2067 {
2068 lbool status;
2069 lit * i;
2070 ////////////////////////////////////////////////
2071 if ( s->fSolved )
2072 {
2073 if ( s->pStore )
2074 {
2075 int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
2076 assert( RetValue );
2077 (void) RetValue;
2078 }
2079 return l_False;
2080 }
2081 ////////////////////////////////////////////////
2082
2083 if ( s->fVerbose )
2084 printf( "Running SAT solver with parameters %d and %d and %d.\n", s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
2085
2086 sat_solver_set_resource_limits( s, nConfLimit, nInsLimit, nConfLimitGlobal, nInsLimitGlobal );
2087
2088 #ifdef SAT_USE_ANALYZE_FINAL
2089 // Perform assumptions:
2090 s->root_level = 0;
2091 for ( i = begin; i < end; i++ )
2092 if ( !sat_solver_push(s, *i) )
2093 {
2094 sat_solver_canceluntil(s,0);
2095 s->root_level = 0;
2096 return l_False;
2097 }
2098 assert(s->root_level == sat_solver_dl(s));
2099 #else
2100 //printf("solve: "); printlits(begin, end); printf("\n");
2101 for (i = begin; i < end; i++){
2102 // switch (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]){
2103 switch (var_value(s, *i)) {
2104 case var1: // l_True:
2105 break;
2106 case varX: // l_Undef
2107 sat_solver_decision(s, *i);
2108 if (sat_solver_propagate(s) == 0)
2109 break;
2110 // fallthrough
2111 case var0: // l_False
2112 sat_solver_canceluntil(s, 0);
2113 return l_False;
2114 }
2115 }
2116 s->root_level = sat_solver_dl(s);
2117 #endif
2118
2119 status = sat_solver_solve_internal(s);
2120
2121 sat_solver_canceluntil(s,0);
2122 s->root_level = 0;
2123
2124 ////////////////////////////////////////////////
2125 if ( status == l_False && s->pStore )
2126 {
2127 int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
2128 assert( RetValue );
2129 (void) RetValue;
2130 }
2131 ////////////////////////////////////////////////
2132 return status;
2133 }
2134
2135 // This LEXSAT procedure should be called with a set of literals (pLits, nLits),
2136 // which defines both (1) variable order, and (2) assignment to begin search from.
2137 // It retuns the LEXSAT assigment that is the same or larger than the given one.
2138 // (It assumes that there is no smaller assignment than the one given!)
2139 // The resulting assignment is returned in the same set of literals (pLits, nLits).
2140 // It pushes/pops assumptions internally and will undo them before terminating.
sat_solver_solve_lexsat(sat_solver * s,int * pLits,int nLits)2141 int sat_solver_solve_lexsat( sat_solver* s, int * pLits, int nLits )
2142 {
2143 int i, iLitFail = -1;
2144 lbool status;
2145 assert( nLits > 0 );
2146 // help the SAT solver by setting desirable polarity
2147 sat_solver_set_literal_polarity( s, pLits, nLits );
2148 // check if there exists a satisfying assignment
2149 status = sat_solver_solve_internal( s );
2150 if ( status != l_True ) // no assignment
2151 return status;
2152 // there is at least one satisfying assignment
2153 assert( status == l_True );
2154 // find the first mismatching literal
2155 for ( i = 0; i < nLits; i++ )
2156 if ( pLits[i] != sat_solver_var_literal(s, Abc_Lit2Var(pLits[i])) )
2157 break;
2158 if ( i == nLits ) // no mismatch - the current assignment is the minimum one!
2159 return l_True;
2160 // mismatch happens in literal i
2161 iLitFail = i;
2162 // create assumptions up to this literal (as in pLits) - including this literal!
2163 for ( i = 0; i <= iLitFail; i++ )
2164 if ( !sat_solver_push(s, pLits[i]) ) // can become UNSAT while adding the last assumption
2165 break;
2166 if ( i < iLitFail + 1 ) // the solver became UNSAT while adding assumptions
2167 status = l_False;
2168 else // solve under the assumptions
2169 status = sat_solver_solve_internal( s );
2170 if ( status == l_True )
2171 {
2172 // we proved that there is a sat assignment with literal (iLitFail) having polarity as in pLits
2173 // continue solving recursively
2174 if ( iLitFail + 1 < nLits )
2175 status = sat_solver_solve_lexsat( s, pLits + iLitFail + 1, nLits - iLitFail - 1 );
2176 }
2177 else if ( status == l_False )
2178 {
2179 // we proved that there is no assignment with iLitFail having polarity as in pLits
2180 assert( Abc_LitIsCompl(pLits[iLitFail]) ); // literal is 0
2181 // (this assert may fail only if there is a sat assignment smaller than one originally given in pLits)
2182 // now we flip this literal (make it 1), change the last assumption
2183 // and contiue looking for the 000...0-assignment of other literals
2184 sat_solver_pop( s );
2185 pLits[iLitFail] = Abc_LitNot(pLits[iLitFail]);
2186 if ( !sat_solver_push(s, pLits[iLitFail]) )
2187 printf( "sat_solver_solve_lexsat(): A satisfying assignment should exist.\n" ); // because we know that the problem is satisfiable
2188 // update other literals to be 000...0
2189 for ( i = iLitFail + 1; i < nLits; i++ )
2190 pLits[i] = Abc_LitNot( Abc_LitRegular(pLits[i]) );
2191 // continue solving recursively
2192 if ( iLitFail + 1 < nLits )
2193 status = sat_solver_solve_lexsat( s, pLits + iLitFail + 1, nLits - iLitFail - 1 );
2194 else
2195 status = l_True;
2196 }
2197 // undo the assumptions
2198 for ( i = iLitFail; i >= 0; i-- )
2199 sat_solver_pop( s );
2200 return status;
2201 }
2202
2203 // This procedure is called on a set of assumptions to minimize their number.
2204 // The procedure relies on the fact that the current set of assumptions is UNSAT.
2205 // It receives and returns SAT solver without assumptions. It returns the number
2206 // of assumptions after minimization. The set of assumptions is returned in pLits.
sat_solver_minimize_assumptions(sat_solver * s,int * pLits,int nLits,int nConfLimit)2207 int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int nConfLimit )
2208 {
2209 int i, k, nLitsL, nLitsR, nResL, nResR, status;
2210 if ( nLits == 1 )
2211 {
2212 // since the problem is UNSAT, we will try to solve it without assuming the last literal
2213 // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
2214 if ( nConfLimit ) s->nConfLimit = s->stats.conflicts + nConfLimit;
2215 status = sat_solver_solve_internal( s );
2216 //printf( "%c", status == l_False ? 'u' : 's' );
2217 return (int)(status != l_False); // return 1 if the problem is not UNSAT
2218 }
2219 assert( nLits >= 2 );
2220 nLitsL = nLits / 2;
2221 nLitsR = nLits - nLitsL;
2222 // assume the left lits
2223 for ( i = 0; i < nLitsL; i++ )
2224 if ( !sat_solver_push(s, pLits[i]) )
2225 {
2226 for ( k = i; k >= 0; k-- )
2227 sat_solver_pop(s);
2228 return sat_solver_minimize_assumptions( s, pLits, i+1, nConfLimit );
2229 }
2230 // solve with these assumptions
2231 if ( nConfLimit ) s->nConfLimit = s->stats.conflicts + nConfLimit;
2232 status = sat_solver_solve_internal( s );
2233 if ( status == l_False ) // these are enough
2234 {
2235 for ( i = 0; i < nLitsL; i++ )
2236 sat_solver_pop(s);
2237 return sat_solver_minimize_assumptions( s, pLits, nLitsL, nConfLimit );
2238 }
2239 // solve for the right lits
2240 nResL = nLitsR == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit );
2241 for ( i = 0; i < nLitsL; i++ )
2242 sat_solver_pop(s);
2243 // swap literals
2244 // assert( nResL <= nLitsL );
2245 // for ( i = 0; i < nResL; i++ )
2246 // ABC_SWAP( int, pLits[i], pLits[nLitsL+i] );
2247 veci_resize( &s->temp_clause, 0 );
2248 for ( i = 0; i < nLitsL; i++ )
2249 veci_push( &s->temp_clause, pLits[i] );
2250 for ( i = 0; i < nResL; i++ )
2251 pLits[i] = pLits[nLitsL+i];
2252 for ( i = 0; i < nLitsL; i++ )
2253 pLits[nResL+i] = veci_begin(&s->temp_clause)[i];
2254 // assume the right lits
2255 for ( i = 0; i < nResL; i++ )
2256 if ( !sat_solver_push(s, pLits[i]) )
2257 {
2258 for ( k = i; k >= 0; k-- )
2259 sat_solver_pop(s);
2260 return sat_solver_minimize_assumptions( s, pLits, i+1, nConfLimit );
2261 }
2262 // solve with these assumptions
2263 if ( nConfLimit ) s->nConfLimit = s->stats.conflicts + nConfLimit;
2264 status = sat_solver_solve_internal( s );
2265 if ( status == l_False ) // these are enough
2266 {
2267 for ( i = 0; i < nResL; i++ )
2268 sat_solver_pop(s);
2269 return nResL;
2270 }
2271 // solve for the left lits
2272 nResR = nLitsL == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nResL, nLitsL, nConfLimit );
2273 for ( i = 0; i < nResL; i++ )
2274 sat_solver_pop(s);
2275 return nResL + nResR;
2276 }
2277
2278 // This is a specialized version of the above procedure with several custom changes:
2279 // - makes sure that at least one of the marked literals is preserved in the clause
2280 // - sets literals to zero when they do not have to be used
2281 // - sets literals to zero for disproved variables
sat_solver_minimize_assumptions2(sat_solver * s,int * pLits,int nLits,int nConfLimit)2282 int sat_solver_minimize_assumptions2( sat_solver* s, int * pLits, int nLits, int nConfLimit )
2283 {
2284 int i, k, nLitsL, nLitsR, nResL, nResR;
2285 if ( nLits == 1 )
2286 {
2287 // since the problem is UNSAT, we will try to solve it without assuming the last literal
2288 // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
2289 int RetValue = 1, LitNot = Abc_LitNot(pLits[0]);
2290 int status = l_False;
2291 int Temp = s->nConfLimit;
2292 s->nConfLimit = nConfLimit;
2293
2294 RetValue = sat_solver_push( s, LitNot ); assert( RetValue );
2295 status = sat_solver_solve_internal( s );
2296 sat_solver_pop( s );
2297
2298 // if the problem is UNSAT, add clause
2299 if ( status == l_False )
2300 {
2301 RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
2302 assert( RetValue );
2303 }
2304
2305 s->nConfLimit = Temp;
2306 return (int)(status != l_False); // return 1 if the problem is not UNSAT
2307 }
2308 assert( nLits >= 2 );
2309 nLitsL = nLits / 2;
2310 nLitsR = nLits - nLitsL;
2311 // assume the left lits
2312 for ( i = 0; i < nLitsL; i++ )
2313 if ( !sat_solver_push(s, pLits[i]) )
2314 {
2315 for ( k = i; k >= 0; k-- )
2316 sat_solver_pop(s);
2317
2318 // add clauses for these literal
2319 for ( k = i+1; k > nLitsL; k++ )
2320 {
2321 int LitNot = Abc_LitNot(pLits[i]);
2322 int RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
2323 assert( RetValue );
2324 }
2325
2326 return sat_solver_minimize_assumptions2( s, pLits, i+1, nConfLimit );
2327 }
2328 // solve for the right lits
2329 nResL = sat_solver_minimize_assumptions2( s, pLits + nLitsL, nLitsR, nConfLimit );
2330 for ( i = 0; i < nLitsL; i++ )
2331 sat_solver_pop(s);
2332 // swap literals
2333 // assert( nResL <= nLitsL );
2334 veci_resize( &s->temp_clause, 0 );
2335 for ( i = 0; i < nLitsL; i++ )
2336 veci_push( &s->temp_clause, pLits[i] );
2337 for ( i = 0; i < nResL; i++ )
2338 pLits[i] = pLits[nLitsL+i];
2339 for ( i = 0; i < nLitsL; i++ )
2340 pLits[nResL+i] = veci_begin(&s->temp_clause)[i];
2341 // assume the right lits
2342 for ( i = 0; i < nResL; i++ )
2343 if ( !sat_solver_push(s, pLits[i]) )
2344 {
2345 for ( k = i; k >= 0; k-- )
2346 sat_solver_pop(s);
2347
2348 // add clauses for these literal
2349 for ( k = i+1; k > nResL; k++ )
2350 {
2351 int LitNot = Abc_LitNot(pLits[i]);
2352 int RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
2353 assert( RetValue );
2354 }
2355
2356 return sat_solver_minimize_assumptions2( s, pLits, i+1, nConfLimit );
2357 }
2358 // solve for the left lits
2359 nResR = sat_solver_minimize_assumptions2( s, pLits + nResL, nLitsL, nConfLimit );
2360 for ( i = 0; i < nResL; i++ )
2361 sat_solver_pop(s);
2362 return nResL + nResR;
2363 }
2364
2365
2366
sat_solver_nvars(sat_solver * s)2367 int sat_solver_nvars(sat_solver* s)
2368 {
2369 return s->size;
2370 }
2371
2372
sat_solver_nclauses(sat_solver * s)2373 int sat_solver_nclauses(sat_solver* s)
2374 {
2375 return s->stats.clauses;
2376 }
2377
2378
sat_solver_nconflicts(sat_solver * s)2379 int sat_solver_nconflicts(sat_solver* s)
2380 {
2381 return (int)s->stats.conflicts;
2382 }
2383
2384 //=================================================================================================
2385 // Clause storage functions:
2386
sat_solver_store_alloc(sat_solver * s)2387 void sat_solver_store_alloc( sat_solver * s )
2388 {
2389 assert( s->pStore == NULL );
2390 s->pStore = Sto_ManAlloc();
2391 }
2392
sat_solver_store_write(sat_solver * s,char * pFileName)2393 void sat_solver_store_write( sat_solver * s, char * pFileName )
2394 {
2395 if ( s->pStore ) Sto_ManDumpClauses( (Sto_Man_t *)s->pStore, pFileName );
2396 }
2397
sat_solver_store_free(sat_solver * s)2398 void sat_solver_store_free( sat_solver * s )
2399 {
2400 if ( s->pStore ) Sto_ManFree( (Sto_Man_t *)s->pStore );
2401 s->pStore = NULL;
2402 }
2403
sat_solver_store_change_last(sat_solver * s)2404 int sat_solver_store_change_last( sat_solver * s )
2405 {
2406 if ( s->pStore ) return Sto_ManChangeLastClause( (Sto_Man_t *)s->pStore );
2407 return -1;
2408 }
2409
sat_solver_store_mark_roots(sat_solver * s)2410 void sat_solver_store_mark_roots( sat_solver * s )
2411 {
2412 if ( s->pStore ) Sto_ManMarkRoots( (Sto_Man_t *)s->pStore );
2413 }
2414
sat_solver_store_mark_clauses_a(sat_solver * s)2415 void sat_solver_store_mark_clauses_a( sat_solver * s )
2416 {
2417 if ( s->pStore ) Sto_ManMarkClausesA( (Sto_Man_t *)s->pStore );
2418 }
2419
sat_solver_store_release(sat_solver * s)2420 void * sat_solver_store_release( sat_solver * s )
2421 {
2422 void * pTemp;
2423 if ( s->pStore == NULL )
2424 return NULL;
2425 pTemp = s->pStore;
2426 s->pStore = NULL;
2427 return pTemp;
2428 }
2429
2430
2431 ABC_NAMESPACE_IMPL_END
2432
2433