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 "satSolver2.h"
28
29 ABC_NAMESPACE_IMPL_START
30
31 #define SAT_USE_PROOF_LOGGING
32
33 //=================================================================================================
34 // Debug:
35
36 //#define VERBOSEDEBUG
37
38 // For derivation output (verbosity level 2)
39 #define L_IND "%-*d"
40 #define L_ind solver2_dlevel(s)*2+2,solver2_dlevel(s)
41 #define L_LIT "%sx%d"
42 #define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
printlits(lit * begin,lit * end)43 static void printlits(lit* begin, lit* end)
44 {
45 int i;
46 for (i = 0; i < end - begin; i++)
47 Abc_Print(1,L_LIT" ",L_lit(begin[i]));
48 }
49
50 //=================================================================================================
51 // Random numbers:
52
53
54 // Returns a random float 0 <= x < 1. Seed must never be 0.
drand(double * seed)55 static inline double drand(double* seed) {
56 int q;
57 *seed *= 1389796;
58 q = (int)(*seed / 2147483647);
59 *seed -= (double)q * 2147483647;
60 return *seed / 2147483647; }
61
62
63 // Returns a random integer 0 <= x < size. Seed must never be 0.
irand(double * seed,int size)64 static inline int irand(double* seed, int size) {
65 return (int)(drand(seed) * size); }
66
67 //=================================================================================================
68 // Variable datatype + minor functions:
69
70 //static const int var0 = 1;
71 static const int var1 = 0;
72 static const int varX = 3;
73
74 struct varinfo2_t
75 {
76 // unsigned val : 2; // variable value
77 unsigned pol : 1; // last polarity
78 unsigned partA : 1; // partA variable
79 unsigned tag : 4; // conflict analysis tags
80 // unsigned lev : 24; // variable level
81 };
82
var_is_assigned(sat_solver2 * s,int v)83 int var_is_assigned(sat_solver2* s, int v) { return s->assigns[v] != varX; }
var_is_partA(sat_solver2 * s,int v)84 int var_is_partA (sat_solver2* s, int v) { return s->vi[v].partA; }
var_set_partA(sat_solver2 * s,int v,int partA)85 void var_set_partA(sat_solver2* s, int v, int partA) { s->vi[v].partA = partA; }
86
87 //static inline int var_level (sat_solver2* s, int v) { return s->vi[v].lev; }
var_level(sat_solver2 * s,int v)88 static inline int var_level (sat_solver2* s, int v) { return s->levels[v]; }
89 //static inline int var_value (sat_solver2* s, int v) { return s->vi[v].val; }
var_value(sat_solver2 * s,int v)90 static inline int var_value (sat_solver2* s, int v) { return s->assigns[v]; }
var_polar(sat_solver2 * s,int v)91 static inline int var_polar (sat_solver2* s, int v) { return s->vi[v].pol; }
92
93 //static inline void var_set_level (sat_solver2* s, int v, int lev) { s->vi[v].lev = lev; }
var_set_level(sat_solver2 * s,int v,int lev)94 static inline void var_set_level (sat_solver2* s, int v, int lev) { s->levels[v] = lev; }
95 //static inline void var_set_value (sat_solver2* s, int v, int val) { s->vi[v].val = val; }
var_set_value(sat_solver2 * s,int v,int val)96 static inline void var_set_value (sat_solver2* s, int v, int val) { s->assigns[v] = val; }
var_set_polar(sat_solver2 * s,int v,int pol)97 static inline void var_set_polar (sat_solver2* s, int v, int pol) { s->vi[v].pol = pol; }
98
99 // check if the literal is false under current assumptions
solver2_lit_is_false(sat_solver2 * s,int Lit)100 static inline int solver2_lit_is_false( sat_solver2* s, int Lit ) { return var_value(s, lit_var(Lit)) == !lit_sign(Lit); }
101
102
103
104 // variable tags
var_tag(sat_solver2 * s,int v)105 static inline int var_tag (sat_solver2* s, int v) { return s->vi[v].tag; }
var_set_tag(sat_solver2 * s,int v,int tag)106 static inline void var_set_tag (sat_solver2* s, int v, int tag) {
107 assert( tag > 0 && tag < 16 );
108 if ( s->vi[v].tag == 0 )
109 veci_push( &s->tagged, v );
110 s->vi[v].tag = tag;
111 }
var_add_tag(sat_solver2 * s,int v,int tag)112 static inline void var_add_tag (sat_solver2* s, int v, int tag) {
113 assert( tag > 0 && tag < 16 );
114 if ( s->vi[v].tag == 0 )
115 veci_push( &s->tagged, v );
116 s->vi[v].tag |= tag;
117 }
solver2_clear_tags(sat_solver2 * s,int start)118 static inline void solver2_clear_tags(sat_solver2* s, int start) {
119 int i, * tagged = veci_begin(&s->tagged);
120 for (i = start; i < veci_size(&s->tagged); i++)
121 s->vi[tagged[i]].tag = 0;
122 veci_resize(&s->tagged,start);
123 }
124
125 // level marks
var_lev_mark(sat_solver2 * s,int v)126 static inline int var_lev_mark (sat_solver2* s, int v) {
127 return (veci_begin(&s->trail_lim)[var_level(s,v)] & 0x80000000) > 0;
128 }
var_lev_set_mark(sat_solver2 * s,int v)129 static inline void var_lev_set_mark (sat_solver2* s, int v) {
130 int level = var_level(s,v);
131 assert( level < veci_size(&s->trail_lim) );
132 veci_begin(&s->trail_lim)[level] |= 0x80000000;
133 veci_push(&s->mark_levels, level);
134 }
solver2_clear_marks(sat_solver2 * s)135 static inline void solver2_clear_marks(sat_solver2* s) {
136 int i, * mark_levels = veci_begin(&s->mark_levels);
137 for (i = 0; i < veci_size(&s->mark_levels); i++)
138 veci_begin(&s->trail_lim)[mark_levels[i]] &= 0x7FFFFFFF;
139 veci_resize(&s->mark_levels,0);
140 }
141
142 //=================================================================================================
143 // Clause datatype + minor functions:
144
145 //static inline int var_reason (sat_solver2* s, int v) { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1; }
146 //static inline int lit_reason (sat_solver2* s, int l) { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; }
147 //static inline clause* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? clause2_read(s, s->reasons[v] >> 1) : NULL; }
148 //static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(i && !s->reasons[v]); s->reasons[v] = (i << 1) | 1; }
var_reason(sat_solver2 * s,int v)149 static inline int var_reason (sat_solver2* s, int v) { return s->reasons[v]; }
lit_reason(sat_solver2 * s,int l)150 static inline int lit_reason (sat_solver2* s, int l) { return s->reasons[lit_var(l)]; }
var_unit_clause(sat_solver2 * s,int v)151 static inline clause* var_unit_clause(sat_solver2* s, int v) { return clause2_read(s, s->units[v]); }
var_set_unit_clause(sat_solver2 * s,int v,cla i)152 static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){
153 assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++;
154 }
155
156 #define clause_foreach_var( p, var, i, start ) \
157 for ( i = start; (i < (int)(p)->size) && ((var) = lit_var((p)->lits[i])); i++ )
158
159 //=================================================================================================
160 // Simple helpers:
161
solver2_dlevel(sat_solver2 * s)162 static inline int solver2_dlevel(sat_solver2* s) { return veci_size(&s->trail_lim); }
solver2_wlist(sat_solver2 * s,lit l)163 static inline veci* solver2_wlist(sat_solver2* s, lit l) { return &s->wlists[l]; }
164
165 //=================================================================================================
166 // Proof logging:
167
proof_chain_start(sat_solver2 * s,clause * c)168 static inline void proof_chain_start( sat_solver2* s, clause* c )
169 {
170 if ( !s->fProofLogging )
171 return;
172 if ( s->pInt2 )
173 s->tempInter = Int2_ManChainStart( s->pInt2, c );
174 if ( s->pPrf2 )
175 Prf_ManChainStart( s->pPrf2, c );
176 if ( s->pPrf1 )
177 {
178 int ProofId = clause2_proofid(s, c, 0);
179 assert( (ProofId >> 2) > 0 );
180 veci_resize( &s->temp_proof, 0 );
181 veci_push( &s->temp_proof, 0 );
182 veci_push( &s->temp_proof, 0 );
183 veci_push( &s->temp_proof, ProofId );
184 }
185 }
186
proof_chain_resolve(sat_solver2 * s,clause * cls,int Var)187 static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var )
188 {
189 if ( !s->fProofLogging )
190 return;
191 if ( s->pInt2 )
192 {
193 clause* c = cls ? cls : var_unit_clause( s, Var );
194 s->tempInter = Int2_ManChainResolve( s->pInt2, c, s->tempInter, var_is_partA(s,Var) );
195 }
196 if ( s->pPrf2 )
197 {
198 clause* c = cls ? cls : var_unit_clause( s, Var );
199 Prf_ManChainResolve( s->pPrf2, c );
200 }
201 if ( s->pPrf1 )
202 {
203 clause* c = cls ? cls : var_unit_clause( s, Var );
204 int ProofId = clause2_proofid(s, c, var_is_partA(s,Var));
205 assert( (ProofId >> 2) > 0 );
206 veci_push( &s->temp_proof, ProofId );
207 }
208 }
209
proof_chain_stop(sat_solver2 * s)210 static inline int proof_chain_stop( sat_solver2* s )
211 {
212 if ( !s->fProofLogging )
213 return 0;
214 if ( s->pInt2 )
215 {
216 int h = s->tempInter;
217 s->tempInter = -1;
218 return h;
219 }
220 if ( s->pPrf2 )
221 Prf_ManChainStop( s->pPrf2 );
222 if ( s->pPrf1 )
223 {
224 extern void Proof_ClauseSetEnts( Vec_Set_t* p, int h, int nEnts );
225 int h = Vec_SetAppend( s->pPrf1, veci_begin(&s->temp_proof), veci_size(&s->temp_proof) );
226 Proof_ClauseSetEnts( s->pPrf1, h, veci_size(&s->temp_proof) - 2 );
227 return h;
228 }
229 return 0;
230 }
231
232 //=================================================================================================
233 // Variable order functions:
234
order_update(sat_solver2 * s,int v)235 static inline void order_update(sat_solver2* s, int v) // updateorder
236 {
237 int* orderpos = s->orderpos;
238 int* heap = veci_begin(&s->order);
239 int i = orderpos[v];
240 int x = heap[i];
241 int parent = (i - 1) / 2;
242 assert(s->orderpos[v] != -1);
243 while (i != 0 && s->activity[x] > s->activity[heap[parent]]){
244 heap[i] = heap[parent];
245 orderpos[heap[i]] = i;
246 i = parent;
247 parent = (i - 1) / 2;
248 }
249 heap[i] = x;
250 orderpos[x] = i;
251 }
order_assigned(sat_solver2 * s,int v)252 static inline void order_assigned(sat_solver2* s, int v)
253 {
254 }
order_unassigned(sat_solver2 * s,int v)255 static inline void order_unassigned(sat_solver2* s, int v) // undoorder
256 {
257 int* orderpos = s->orderpos;
258 if (orderpos[v] == -1){
259 orderpos[v] = veci_size(&s->order);
260 veci_push(&s->order,v);
261 order_update(s,v);
262 }
263 }
order_select(sat_solver2 * s,float random_var_freq)264 static inline int order_select(sat_solver2* s, float random_var_freq) // selectvar
265 {
266 int* heap = veci_begin(&s->order);
267 int* orderpos = s->orderpos;
268 // Random decision:
269 if (drand(&s->random_seed) < random_var_freq){
270 int next = irand(&s->random_seed,s->size);
271 assert(next >= 0 && next < s->size);
272 if (var_value(s, next) == varX)
273 return next;
274 }
275 // Activity based decision:
276 while (veci_size(&s->order) > 0){
277 int next = heap[0];
278 int size = veci_size(&s->order)-1;
279 int x = heap[size];
280 veci_resize(&s->order,size);
281 orderpos[next] = -1;
282 if (size > 0){
283 unsigned act = s->activity[x];
284 int i = 0;
285 int child = 1;
286 while (child < size){
287 if (child+1 < size && s->activity[heap[child]] < s->activity[heap[child+1]])
288 child++;
289 assert(child < size);
290 if (act >= s->activity[heap[child]])
291 break;
292 heap[i] = heap[child];
293 orderpos[heap[i]] = i;
294 i = child;
295 child = 2 * child + 1;
296 }
297 heap[i] = x;
298 orderpos[heap[i]] = i;
299 }
300 if (var_value(s, next) == varX)
301 return next;
302 }
303 return var_Undef;
304 }
305
306
307 //=================================================================================================
308 // Activity functions:
309
310 #ifdef USE_FLOAT_ACTIVITY2
311
act_var_rescale(sat_solver2 * s)312 static inline void act_var_rescale(sat_solver2* s) {
313 double* activity = s->activity;
314 int i;
315 for (i = 0; i < s->size; i++)
316 activity[i] *= 1e-100;
317 s->var_inc *= 1e-100;
318 }
act_clause2_rescale(sat_solver2 * s)319 static inline void act_clause2_rescale(sat_solver2* s) {
320 static abctime Total = 0;
321 float * act_clas = (float *)veci_begin(&s->act_clas);
322 int i;
323 abctime clk = Abc_Clock();
324 for (i = 0; i < veci_size(&s->act_clas); i++)
325 act_clas[i] *= (float)1e-20;
326 s->cla_inc *= (float)1e-20;
327
328 Total += Abc_Clock() - clk;
329 Abc_Print(1, "Rescaling... Cla inc = %10.3f Conf = %10d ", s->cla_inc, s->stats.conflicts );
330 Abc_PrintTime( 1, "Time", Total );
331 }
act_var_bump(sat_solver2 * s,int v)332 static inline void act_var_bump(sat_solver2* s, int v) {
333 s->activity[v] += s->var_inc;
334 if (s->activity[v] > 1e100)
335 act_var_rescale(s);
336 if (s->orderpos[v] != -1)
337 order_update(s,v);
338 }
act_clause2_bump(sat_solver2 * s,clause * c)339 static inline void act_clause2_bump(sat_solver2* s, clause*c) {
340 float * act_clas = (float *)veci_begin(&s->act_clas);
341 assert( c->Id < veci_size(&s->act_clas) );
342 act_clas[c->Id] += s->cla_inc;
343 if (act_clas[c->Id] > (float)1e20)
344 act_clause2_rescale(s);
345 }
act_var_decay(sat_solver2 * s)346 static inline void act_var_decay(sat_solver2* s) { s->var_inc *= s->var_decay; }
act_clause2_decay(sat_solver2 * s)347 static inline void act_clause2_decay(sat_solver2* s) { s->cla_inc *= s->cla_decay; }
348
349 #else
350
act_var_rescale(sat_solver2 * s)351 static inline void act_var_rescale(sat_solver2* s) {
352 unsigned* activity = s->activity;
353 int i;
354 for (i = 0; i < s->size; i++)
355 activity[i] >>= 19;
356 s->var_inc >>= 19;
357 s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
358 }
act_clause2_rescale(sat_solver2 * s)359 static inline void act_clause2_rescale(sat_solver2* s) {
360 // static abctime Total = 0;
361 // abctime clk = Abc_Clock();
362 int i;
363 unsigned * act_clas = (unsigned *)veci_begin(&s->act_clas);
364 for (i = 0; i < veci_size(&s->act_clas); i++)
365 act_clas[i] >>= 14;
366 s->cla_inc >>= 14;
367 s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
368 // Total += Abc_Clock() - clk;
369 // Abc_Print(1, "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts );
370 // Abc_PrintTime( 1, "Time", Total );
371 }
act_var_bump(sat_solver2 * s,int v)372 static inline void act_var_bump(sat_solver2* s, int v) {
373 s->activity[v] += s->var_inc;
374 if (s->activity[v] & 0x80000000)
375 act_var_rescale(s);
376 if (s->orderpos[v] != -1)
377 order_update(s,v);
378 }
act_clause2_bump(sat_solver2 * s,clause * c)379 static inline void act_clause2_bump(sat_solver2* s, clause*c) {
380 unsigned * act_clas = (unsigned *)veci_begin(&s->act_clas);
381 int Id = clause_id(c);
382 assert( Id >= 0 && Id < veci_size(&s->act_clas) );
383 act_clas[Id] += s->cla_inc;
384 if (act_clas[Id] & 0x80000000)
385 act_clause2_rescale(s);
386 }
act_var_decay(sat_solver2 * s)387 static inline void act_var_decay(sat_solver2* s) { s->var_inc += (s->var_inc >> 4); }
act_clause2_decay(sat_solver2 * s)388 static inline void act_clause2_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc >> 10); }
389
390 #endif
391
392 //=================================================================================================
393 // Clause functions:
394
sat_clause_compute_lbd(sat_solver2 * s,clause * c)395 static inline int sat_clause_compute_lbd( sat_solver2* s, clause* c )
396 {
397 int i, lev, minl = 0, lbd = 0;
398 for (i = 0; i < (int)c->size; i++) {
399 lev = var_level(s, lit_var(c->lits[i]));
400 if ( !(minl & (1 << (lev & 31))) ) {
401 minl |= 1 << (lev & 31);
402 lbd++;
403 }
404 }
405 return lbd;
406 }
407
clause2_create_new(sat_solver2 * s,lit * begin,lit * end,int learnt,int proof_id)408 static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id )
409 {
410 clause* c;
411 int h, size = end - begin;
412 assert(size < 1 || begin[0] >= 0);
413 assert(size < 2 || begin[1] >= 0);
414 assert(size < 1 || lit_var(begin[0]) < s->size);
415 assert(size < 2 || lit_var(begin[1]) < s->size);
416 // create new clause
417 h = Sat_MemAppend( &s->Mem, begin, size, learnt, 1 );
418 assert( !(h & 1) );
419 c = clause2_read( s, h );
420 if (learnt)
421 {
422 if ( s->pPrf1 )
423 assert( proof_id );
424 c->lbd = sat_clause_compute_lbd( s, c );
425 assert( clause_id(c) == veci_size(&s->act_clas) );
426 if ( s->pPrf1 || s->pInt2 )
427 veci_push(&s->claProofs, proof_id);
428 // veci_push(&s->act_clas, (1<<10));
429 veci_push(&s->act_clas, 0);
430 if ( size > 2 )
431 act_clause2_bump( s,c );
432 s->stats.learnts++;
433 s->stats.learnts_literals += size;
434 // remember the last one
435 s->hLearntLast = h;
436 }
437 else
438 {
439 assert( clause_id(c) == (int)s->stats.clauses );
440 s->stats.clauses++;
441 s->stats.clauses_literals += size;
442 }
443 // watch the clause
444 if ( size > 1 )
445 {
446 veci_push(solver2_wlist(s,lit_neg(begin[0])),h);
447 veci_push(solver2_wlist(s,lit_neg(begin[1])),h);
448 }
449 return h;
450 }
451
452 //=================================================================================================
453 // Minor (solver) functions:
454
solver2_enqueue(sat_solver2 * s,lit l,cla from)455 static inline int solver2_enqueue(sat_solver2* s, lit l, cla from)
456 {
457 int v = lit_var(l);
458 #ifdef VERBOSEDEBUG
459 Abc_Print(1,L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
460 #endif
461 if (var_value(s, v) != varX)
462 return var_value(s, v) == lit_sign(l);
463 else
464 { // New fact -- store it.
465 #ifdef VERBOSEDEBUG
466 Abc_Print(1,L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
467 #endif
468 var_set_value( s, v, lit_sign(l) );
469 var_set_level( s, v, solver2_dlevel(s) );
470 s->reasons[v] = from; // = from << 1;
471 s->trail[s->qtail++] = l;
472 order_assigned(s, v);
473 return true;
474 }
475 }
476
solver2_assume(sat_solver2 * s,lit l)477 static inline int solver2_assume(sat_solver2* s, lit l)
478 {
479 assert(s->qtail == s->qhead);
480 assert(var_value(s, lit_var(l)) == varX);
481 #ifdef VERBOSEDEBUG
482 Abc_Print(1,L_IND"assume("L_LIT") ", L_ind, L_lit(l));
483 Abc_Print(1, "act = %.20f\n", s->activity[lit_var(l)] );
484 #endif
485 veci_push(&s->trail_lim,s->qtail);
486 return solver2_enqueue(s,l,0);
487 }
488
solver2_canceluntil(sat_solver2 * s,int level)489 static void solver2_canceluntil(sat_solver2* s, int level) {
490 int bound;
491 int lastLev;
492 int c, x;
493
494 if (solver2_dlevel(s) <= level)
495 return;
496 assert( solver2_dlevel(s) > 0 );
497
498 bound = (veci_begin(&s->trail_lim))[level];
499 lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1];
500
501 for (c = s->qtail-1; c >= bound; c--)
502 {
503 x = lit_var(s->trail[c]);
504 var_set_value(s, x, varX);
505 s->reasons[x] = 0;
506 s->units[x] = 0; // temporary?
507 if ( c < lastLev )
508 var_set_polar(s, x, !lit_sign(s->trail[c]));
509 }
510
511 for (c = s->qhead-1; c >= bound; c--)
512 order_unassigned(s,lit_var(s->trail[c]));
513
514 s->qhead = s->qtail = bound;
515 veci_resize(&s->trail_lim,level);
516 }
517
solver2_canceluntil_rollback(sat_solver2 * s,int NewBound)518 static void solver2_canceluntil_rollback(sat_solver2* s, int NewBound) {
519 int c, x;
520
521 assert( solver2_dlevel(s) == 0 );
522 assert( s->qtail == s->qhead );
523 assert( s->qtail >= NewBound );
524
525 for (c = s->qtail-1; c >= NewBound; c--)
526 {
527 x = lit_var(s->trail[c]);
528 var_set_value(s, x, varX);
529 s->reasons[x] = 0;
530 s->units[x] = 0; // temporary?
531 }
532
533 for (c = s->qhead-1; c >= NewBound; c--)
534 order_unassigned(s,lit_var(s->trail[c]));
535
536 s->qhead = s->qtail = NewBound;
537 }
538
539
solver2_record(sat_solver2 * s,veci * cls,int proof_id)540 static void solver2_record(sat_solver2* s, veci* cls, int proof_id)
541 {
542 lit* begin = veci_begin(cls);
543 lit* end = begin + veci_size(cls);
544 cla Cid = clause2_create_new(s,begin,end,1, proof_id);
545 assert(veci_size(cls) > 0);
546 if ( veci_size(cls) == 1 )
547 {
548 if ( s->fProofLogging )
549 var_set_unit_clause(s, lit_var(begin[0]), Cid);
550 Cid = 0;
551 }
552 solver2_enqueue(s, begin[0], Cid);
553 }
554
555
solver2_progress(sat_solver2 * s)556 static double solver2_progress(sat_solver2* s)
557 {
558 int i;
559 double progress = 0.0, F = 1.0 / s->size;
560 for (i = 0; i < s->size; i++)
561 if (var_value(s, i) != varX)
562 progress += pow(F, var_level(s, i));
563 return progress / s->size;
564 }
565
566 //=================================================================================================
567 // Major methods:
568
569 /*_________________________________________________________________________________________________
570 |
571 | analyzeFinal : (p : Lit) -> [void]
572 |
573 | Description:
574 | Specialized analysis procedure to express the final conflict in terms of assumptions.
575 | Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
576 | stores the result in 'out_conflict'.
577 |________________________________________________________________________________________________@*/
578 /*
579 void Solver::analyzeFinal(clause* confl, bool skip_first)
580 {
581 // -- NOTE! This code is relatively untested. Please report bugs!
582 conflict.clear();
583 if (root_level == 0) return;
584
585 vec<char>& seen = analyze_seen;
586 for (int i = skip_first ? 1 : 0; i < confl->size(); i++){
587 Var x = var((*confl)[i]);
588 if (level[x] > 0)
589 seen[x] = 1;
590 }
591
592 int start = (root_level >= trail_lim.size()) ? trail.size()-1 : trail_lim[root_level];
593 for (int i = start; i >= trail_lim[0]; i--){
594 Var x = var(trail[i]);
595 if (seen[x]){
596 GClause r = reason[x];
597 if (r == Gclause2_NULL){
598 assert(level[x] > 0);
599 conflict.push(~trail[i]);
600 }else{
601 if (r.isLit()){
602 Lit p = r.lit();
603 if (level[var(p)] > 0)
604 seen[var(p)] = 1;
605 }else{
606 Clause& c = *r.clause();
607 for (int j = 1; j < c.size(); j++)
608 if (level[var(c[j])] > 0)
609 seen[var(c[j])] = 1;
610 }
611 }
612 seen[x] = 0;
613 }
614 }
615 }
616 */
617
solver2_analyze_final(sat_solver2 * s,clause * conf,int skip_first)618 static int solver2_analyze_final(sat_solver2* s, clause* conf, int skip_first)
619 {
620 int i, j, x;//, start;
621 veci_resize(&s->conf_final,0);
622 if ( s->root_level == 0 )
623 return s->hProofLast;
624 proof_chain_start( s, conf );
625 assert( veci_size(&s->tagged) == 0 );
626 clause_foreach_var( conf, x, i, skip_first ){
627 if ( var_level(s,x) )
628 var_set_tag(s, x, 1);
629 else
630 proof_chain_resolve( s, NULL, x );
631 }
632 assert( s->root_level >= veci_size(&s->trail_lim) );
633 // start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level];
634 for (i = s->qtail-1; i >= (veci_begin(&s->trail_lim))[0]; i--){
635 x = lit_var(s->trail[i]);
636 if (var_tag(s,x)){
637 clause* c = clause2_read(s, var_reason(s,x));
638 if (c){
639 proof_chain_resolve( s, c, x );
640 clause_foreach_var( c, x, j, 1 ){
641 if ( var_level(s,x) )
642 var_set_tag(s, x, 1);
643 else
644 proof_chain_resolve( s, NULL, x );
645 }
646 }else {
647 assert( var_level(s,x) );
648 veci_push(&s->conf_final,lit_neg(s->trail[i]));
649 }
650 }
651 }
652 solver2_clear_tags(s,0);
653 return proof_chain_stop( s );
654 }
655
solver2_lit_removable_rec(sat_solver2 * s,int v)656 static int solver2_lit_removable_rec(sat_solver2* s, int v)
657 {
658 // tag[0]: True if original conflict clause literal.
659 // tag[1]: Processed by this procedure
660 // tag[2]: 0=non-removable, 1=removable
661
662 clause* c;
663 int i, x;
664
665 // skip visited
666 if (var_tag(s,v) & 2)
667 return (var_tag(s,v) & 4) > 0;
668
669 // skip decisions on a wrong level
670 c = clause2_read(s, var_reason(s,v));
671 if ( c == NULL ){
672 var_add_tag(s,v,2);
673 return 0;
674 }
675
676 clause_foreach_var( c, x, i, 1 ){
677 if (var_tag(s,x) & 1)
678 solver2_lit_removable_rec(s, x);
679 else{
680 if (var_level(s,x) == 0 || var_tag(s,x) == 6) continue; // -- 'x' checked before, found to be removable (or belongs to the toplevel)
681 if (var_tag(s,x) == 2 || !var_lev_mark(s,x) || !solver2_lit_removable_rec(s, x))
682 { // -- 'x' checked before, found NOT to be removable, or it belongs to a wrong level, or cannot be removed
683 var_add_tag(s,v,2);
684 return 0;
685 }
686 }
687 }
688 if ( s->fProofLogging && (var_tag(s,v) & 1) )
689 veci_push(&s->min_lit_order, v );
690 var_add_tag(s,v,6);
691 return 1;
692 }
693
solver2_lit_removable(sat_solver2 * s,int x)694 static int solver2_lit_removable(sat_solver2* s, int x)
695 {
696 clause* c;
697 int i, top;
698 if ( !var_reason(s,x) )
699 return 0;
700 if ( var_tag(s,x) & 2 )
701 {
702 assert( var_tag(s,x) & 1 );
703 return 1;
704 }
705 top = veci_size(&s->tagged);
706 veci_resize(&s->stack,0);
707 veci_push(&s->stack, x << 1);
708 while (veci_size(&s->stack))
709 {
710 x = veci_pop(&s->stack);
711 if ( s->fProofLogging )
712 {
713 if ( x & 1 ){
714 if ( var_tag(s,x >> 1) & 1 )
715 veci_push(&s->min_lit_order, x >> 1 );
716 continue;
717 }
718 veci_push(&s->stack, x ^ 1 );
719 }
720 x >>= 1;
721 c = clause2_read(s, var_reason(s,x));
722 clause_foreach_var( c, x, i, 1 ){
723 if (var_tag(s,x) || !var_level(s,x))
724 continue;
725 if (!var_reason(s,x) || !var_lev_mark(s,x)){
726 solver2_clear_tags(s, top);
727 return 0;
728 }
729 veci_push(&s->stack, x << 1);
730 var_set_tag(s, x, 2);
731 }
732 }
733 return 1;
734 }
735
solver2_logging_order(sat_solver2 * s,int x)736 static void solver2_logging_order(sat_solver2* s, int x)
737 {
738 clause* c;
739 int i;
740 if ( (var_tag(s,x) & 4) )
741 return;
742 var_add_tag(s, x, 4);
743 veci_resize(&s->stack,0);
744 veci_push(&s->stack,x << 1);
745 while (veci_size(&s->stack))
746 {
747 x = veci_pop(&s->stack);
748 if ( x & 1 ){
749 veci_push(&s->min_step_order, x >> 1 );
750 continue;
751 }
752 veci_push(&s->stack, x ^ 1 );
753 x >>= 1;
754 c = clause2_read(s, var_reason(s,x));
755 // if ( !c )
756 // Abc_Print(1, "solver2_logging_order(): Error in conflict analysis!!!\n" );
757 clause_foreach_var( c, x, i, 1 ){
758 if ( !var_level(s,x) || (var_tag(s,x) & 1) )
759 continue;
760 veci_push(&s->stack, x << 1);
761 var_add_tag(s, x, 4);
762 }
763 }
764 }
765
solver2_logging_order_rec(sat_solver2 * s,int x)766 static void solver2_logging_order_rec(sat_solver2* s, int x)
767 {
768 clause* c;
769 int i, y;
770 if ( (var_tag(s,x) & 8) )
771 return;
772 c = clause2_read(s, var_reason(s,x));
773 clause_foreach_var( c, y, i, 1 )
774 if ( var_level(s,y) && (var_tag(s,y) & 1) == 0 )
775 solver2_logging_order_rec(s, y);
776 var_add_tag(s, x, 8);
777 veci_push(&s->min_step_order, x);
778 }
779
solver2_analyze(sat_solver2 * s,clause * c,veci * learnt)780 static int solver2_analyze(sat_solver2* s, clause* c, veci* learnt)
781 {
782 int cnt = 0;
783 lit p = 0;
784 int x, ind = s->qtail-1;
785 int proof_id = 0;
786 lit* lits,* vars, i, j, k;
787 assert( veci_size(&s->tagged) == 0 );
788 // tag[0] - visited by conflict analysis (afterwards: literals of the learned clause)
789 // tag[1] - visited by solver2_lit_removable() with success
790 // tag[2] - visited by solver2_logging_order()
791
792 proof_chain_start( s, c );
793 veci_push(learnt,lit_Undef);
794 while ( 1 ){
795 assert(c != 0);
796 if (c->lrn)
797 act_clause2_bump(s,c);
798 clause_foreach_var( c, x, j, (int)(p > 0) ){
799 assert(x >= 0 && x < s->size);
800 if ( var_tag(s, x) )
801 continue;
802 if ( var_level(s,x) == 0 )
803 {
804 proof_chain_resolve( s, NULL, x );
805 continue;
806 }
807 var_set_tag(s, x, 1);
808 act_var_bump(s,x);
809 if (var_level(s,x) == solver2_dlevel(s))
810 cnt++;
811 else
812 veci_push(learnt,c->lits[j]);
813 }
814
815 while (!var_tag(s, lit_var(s->trail[ind--])));
816
817 p = s->trail[ind+1];
818 c = clause2_read(s, lit_reason(s,p));
819 cnt--;
820 if ( cnt == 0 )
821 break;
822 proof_chain_resolve( s, c, lit_var(p) );
823 }
824 *veci_begin(learnt) = lit_neg(p);
825
826 // mark levels
827 assert( veci_size(&s->mark_levels) == 0 );
828 lits = veci_begin(learnt);
829 for (i = 1; i < veci_size(learnt); i++)
830 var_lev_set_mark(s, lit_var(lits[i]));
831
832 // simplify (full)
833 veci_resize(&s->min_lit_order, 0);
834 for (i = j = 1; i < veci_size(learnt); i++){
835 // if (!solver2_lit_removable( s,lit_var(lits[i])))
836 if (!solver2_lit_removable_rec(s,lit_var(lits[i]))) // changed to vars!!!
837 lits[j++] = lits[i];
838 }
839
840 // record the proof
841 if ( s->fProofLogging )
842 {
843 // collect additional clauses to resolve
844 veci_resize(&s->min_step_order, 0);
845 vars = veci_begin(&s->min_lit_order);
846 for (i = 0; i < veci_size(&s->min_lit_order); i++)
847 // solver2_logging_order(s, vars[i]);
848 solver2_logging_order_rec(s, vars[i]);
849
850 // add them in the reverse order
851 vars = veci_begin(&s->min_step_order);
852 for (i = veci_size(&s->min_step_order); i > 0; ) { i--;
853 c = clause2_read(s, var_reason(s,vars[i]));
854 proof_chain_resolve( s, c, vars[i] );
855 clause_foreach_var(c, x, k, 1)
856 if ( var_level(s,x) == 0 )
857 proof_chain_resolve( s, NULL, x );
858 }
859 proof_id = proof_chain_stop( s );
860 }
861
862 // unmark levels
863 solver2_clear_marks( s );
864
865 // update size of learnt + statistics
866 veci_resize(learnt,j);
867 s->stats.tot_literals += j;
868
869 // clear tags
870 solver2_clear_tags(s,0);
871
872 #ifdef DEBUG
873 for (i = 0; i < s->size; i++)
874 assert(!var_tag(s, i));
875 #endif
876
877 #ifdef VERBOSEDEBUG
878 Abc_Print(1,L_IND"Learnt {", L_ind);
879 for (i = 0; i < veci_size(learnt); i++) Abc_Print(1," "L_LIT, L_lit(lits[i]));
880 #endif
881 if (veci_size(learnt) > 1){
882 lit tmp;
883 int max_i = 1;
884 int max = var_level(s, lit_var(lits[1]));
885 for (i = 2; i < veci_size(learnt); i++)
886 if (max < var_level(s, lit_var(lits[i]))) {
887 max = var_level(s, lit_var(lits[i]));
888 max_i = i;
889 }
890
891 tmp = lits[1];
892 lits[1] = lits[max_i];
893 lits[max_i] = tmp;
894 }
895 #ifdef VERBOSEDEBUG
896 {
897 int lev = veci_size(learnt) > 1 ? var_level(s, lit_var(lits[1])) : 0;
898 Abc_Print(1," } at level %d\n", lev);
899 }
900 #endif
901 return proof_id;
902 }
903
solver2_propagate(sat_solver2 * s)904 clause* solver2_propagate(sat_solver2* s)
905 {
906 clause* c, * confl = NULL;
907 veci* ws;
908 lit* lits, false_lit, p, * stop, * k;
909 cla* begin,* end, *i, *j;
910 int Lit;
911
912 while (confl == 0 && s->qtail - s->qhead > 0){
913
914 p = s->trail[s->qhead++];
915 ws = solver2_wlist(s,p);
916 begin = (cla*)veci_begin(ws);
917 end = begin + veci_size(ws);
918
919 s->stats.propagations++;
920 for (i = j = begin; i < end; ){
921 c = clause2_read(s,*i);
922 lits = c->lits;
923
924 // Make sure the false literal is data[1]:
925 false_lit = lit_neg(p);
926 if (lits[0] == false_lit){
927 lits[0] = lits[1];
928 lits[1] = false_lit;
929 }
930 assert(lits[1] == false_lit);
931
932 // If 0th watch is true, then clause is already satisfied.
933 if (var_value(s, lit_var(lits[0])) == lit_sign(lits[0]))
934 *j++ = *i;
935 else{
936 // Look for new watch:
937 stop = lits + c->size;
938 for (k = lits + 2; k < stop; k++){
939 if (var_value(s, lit_var(*k)) != !lit_sign(*k)){
940 lits[1] = *k;
941 *k = false_lit;
942 veci_push(solver2_wlist(s,lit_neg(lits[1])),*i);
943 goto WatchFound; }
944 }
945
946 // Did not find watch -- clause is unit under assignment:
947 Lit = lits[0];
948 if ( s->fProofLogging && solver2_dlevel(s) == 0 )
949 {
950 int k, x, proof_id, Cid, Var = lit_var(Lit);
951 int fLitIsFalse = (var_value(s, Var) == !lit_sign(Lit));
952 // Log production of top-level unit clause:
953 proof_chain_start( s, c );
954 clause_foreach_var( c, x, k, 1 ){
955 assert( var_level(s, x) == 0 );
956 proof_chain_resolve( s, NULL, x );
957 }
958 proof_id = proof_chain_stop( s );
959 // get a new clause
960 Cid = clause2_create_new( s, &Lit, &Lit + 1, 1, proof_id );
961 assert( (var_unit_clause(s, Var) == NULL) != fLitIsFalse );
962 // if variable already has unit clause, it must be with the other polarity
963 // in this case, we should derive the empty clause here
964 if ( var_unit_clause(s, Var) == NULL )
965 var_set_unit_clause(s, Var, Cid);
966 else{
967 // Empty clause derived:
968 proof_chain_start( s, clause2_read(s,Cid) );
969 proof_chain_resolve( s, NULL, Var );
970 proof_id = proof_chain_stop( s );
971 s->hProofLast = proof_id;
972 // clause2_create_new( s, &Lit, &Lit, 1, proof_id );
973 }
974 }
975
976 *j++ = *i;
977 // Clause is unit under assignment:
978 if ( c->lrn )
979 c->lbd = sat_clause_compute_lbd(s, c);
980 if (!solver2_enqueue(s,Lit, *i)){
981 confl = clause2_read(s,*i++);
982 // Copy the remaining watches:
983 while (i < end)
984 *j++ = *i++;
985 }
986 }
987 WatchFound: i++;
988 }
989 s->stats.inspects += j - (int*)veci_begin(ws);
990 veci_resize(ws,j - (int*)veci_begin(ws));
991 }
992
993 return confl;
994 }
995
sat_solver2_simplify(sat_solver2 * s)996 int sat_solver2_simplify(sat_solver2* s)
997 {
998 assert(solver2_dlevel(s) == 0);
999 return (solver2_propagate(s) == NULL);
1000 }
1001
solver2_search(sat_solver2 * s,ABC_INT64_T nof_conflicts)1002 static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
1003 {
1004 double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
1005
1006 ABC_INT64_T conflictC = 0;
1007 veci learnt_clause;
1008 int proof_id;
1009
1010 assert(s->root_level == solver2_dlevel(s));
1011
1012 s->stats.starts++;
1013 // s->var_decay = (float)(1 / 0.95 );
1014 // s->cla_decay = (float)(1 / 0.999);
1015 veci_new(&learnt_clause);
1016
1017 for (;;){
1018 clause* confl = solver2_propagate(s);
1019 if (confl != 0){
1020 // CONFLICT
1021 int blevel;
1022
1023 #ifdef VERBOSEDEBUG
1024 Abc_Print(1,L_IND"**CONFLICT**\n", L_ind);
1025 #endif
1026 s->stats.conflicts++; conflictC++;
1027 if (solver2_dlevel(s) <= s->root_level){
1028 proof_id = solver2_analyze_final(s, confl, 0);
1029 if ( s->pPrf1 )
1030 assert( proof_id > 0 );
1031 s->hProofLast = proof_id;
1032 veci_delete(&learnt_clause);
1033 return l_False;
1034 }
1035
1036 veci_resize(&learnt_clause,0);
1037 proof_id = solver2_analyze(s, confl, &learnt_clause);
1038 blevel = veci_size(&learnt_clause) > 1 ? var_level(s, lit_var(veci_begin(&learnt_clause)[1])) : s->root_level;
1039 blevel = s->root_level > blevel ? s->root_level : blevel;
1040 solver2_canceluntil(s,blevel);
1041 solver2_record(s,&learnt_clause, proof_id);
1042 // if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0;
1043 // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions)
1044 if ( learnt_clause.size == 1 )
1045 var_set_level( s, lit_var(learnt_clause.ptr[0]), 0 );
1046 act_var_decay(s);
1047 act_clause2_decay(s);
1048
1049 }else{
1050 // NO CONFLICT
1051 int next;
1052
1053 if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){
1054 // Reached bound on number of conflicts:
1055 s->progress_estimate = solver2_progress(s);
1056 solver2_canceluntil(s,s->root_level);
1057 veci_delete(&learnt_clause);
1058 return l_Undef; }
1059
1060 if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
1061 // (s->nInsLimit && s->stats.inspects > s->nInsLimit) )
1062 (s->nInsLimit && s->stats.propagations > s->nInsLimit) )
1063 {
1064 // Reached bound on number of conflicts:
1065 s->progress_estimate = solver2_progress(s);
1066 solver2_canceluntil(s,s->root_level);
1067 veci_delete(&learnt_clause);
1068 return l_Undef;
1069 }
1070
1071 // if (solver2_dlevel(s) == 0 && !s->fSkipSimplify)
1072 // Simplify the set of problem clauses:
1073 // sat_solver2_simplify(s);
1074
1075 // Reduce the set of learnt clauses:
1076 // if (s->nLearntMax > 0 && s->stats.learnts >= (unsigned)s->nLearntMax)
1077 // sat_solver2_reducedb(s);
1078
1079 // New variable decision:
1080 s->stats.decisions++;
1081 next = order_select(s,(float)random_var_freq);
1082
1083 if (next == var_Undef){
1084 // Model found:
1085 int i;
1086 for (i = 0; i < s->size; i++)
1087 {
1088 assert( var_value(s,i) != varX );
1089 s->model[i] = (var_value(s,i)==var1 ? l_True : l_False);
1090 }
1091 solver2_canceluntil(s,s->root_level);
1092 veci_delete(&learnt_clause);
1093 return l_True;
1094 }
1095
1096 if ( var_polar(s, next) ) // positive polarity
1097 solver2_assume(s,toLit(next));
1098 else
1099 solver2_assume(s,lit_neg(toLit(next)));
1100 }
1101 }
1102
1103 return l_Undef; // cannot happen
1104 }
1105
1106 //=================================================================================================
1107 // External solver functions:
1108
sat_solver2_new(void)1109 sat_solver2* sat_solver2_new(void)
1110 {
1111 sat_solver2* s = (sat_solver2 *)ABC_CALLOC( char, sizeof(sat_solver2) );
1112
1113 #ifdef USE_FLOAT_ACTIVITY2
1114 s->var_inc = 1;
1115 s->cla_inc = 1;
1116 s->var_decay = (float)(1 / 0.95 );
1117 s->cla_decay = (float)(1 / 0.999 );
1118 // s->cla_decay = 1;
1119 // s->var_decay = 1;
1120 #else
1121 s->var_inc = (1 << 5);
1122 s->cla_inc = (1 << 11);
1123 #endif
1124 s->random_seed = 91648253;
1125
1126 #ifdef SAT_USE_PROOF_LOGGING
1127 s->fProofLogging = 1;
1128 #else
1129 s->fProofLogging = 0;
1130 #endif
1131 s->fSkipSimplify = 1;
1132 s->fNotUseRandom = 0;
1133 s->fVerbose = 0;
1134
1135 s->nLearntStart = LEARNT_MAX_START_DEFAULT; // starting learned clause limit
1136 s->nLearntDelta = LEARNT_MAX_INCRE_DEFAULT; // delta of learned clause limit
1137 s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT; // ratio of learned clause limit
1138 s->nLearntMax = s->nLearntStart;
1139
1140 // initialize vectors
1141 veci_new(&s->order);
1142 veci_new(&s->trail_lim);
1143 veci_new(&s->tagged);
1144 veci_new(&s->stack);
1145 veci_new(&s->temp_clause);
1146 veci_new(&s->temp_proof);
1147 veci_new(&s->conf_final);
1148 veci_new(&s->mark_levels);
1149 veci_new(&s->min_lit_order);
1150 veci_new(&s->min_step_order);
1151 // veci_new(&s->learnt_live);
1152 Sat_MemAlloc_( &s->Mem, 14 );
1153 veci_new(&s->act_clas);
1154 // proof-logging
1155 veci_new(&s->claProofs);
1156 // s->pPrf1 = Vec_SetAlloc( 20 );
1157 s->tempInter = -1;
1158
1159 // initialize clause pointers
1160 s->hLearntLast = -1; // the last learnt clause
1161 s->hProofLast = -1; // the last proof ID
1162 // initialize rollback
1163 s->iVarPivot = 0; // the pivot for variables
1164 s->iTrailPivot = 0; // the pivot for trail
1165 s->hProofPivot = 1; // the pivot for proof records
1166 return s;
1167 }
1168
1169
sat_solver2_setnvars(sat_solver2 * s,int n)1170 void sat_solver2_setnvars(sat_solver2* s,int n)
1171 {
1172 int var;
1173
1174 if (s->cap < n){
1175 int old_cap = s->cap;
1176 while (s->cap < n) s->cap = s->cap*2+1;
1177
1178 s->wlists = ABC_REALLOC(veci, s->wlists, s->cap*2);
1179 s->vi = ABC_REALLOC(varinfo2, s->vi, s->cap);
1180 s->levels = ABC_REALLOC(int, s->levels, s->cap);
1181 s->assigns = ABC_REALLOC(char, s->assigns, s->cap);
1182 s->trail = ABC_REALLOC(lit, s->trail, s->cap);
1183 s->orderpos = ABC_REALLOC(int, s->orderpos, s->cap);
1184 s->reasons = ABC_REALLOC(cla, s->reasons, s->cap);
1185 if ( s->fProofLogging )
1186 s->units = ABC_REALLOC(cla, s->units, s->cap);
1187 #ifdef USE_FLOAT_ACTIVITY2
1188 s->activity = ABC_REALLOC(double, s->activity, s->cap);
1189 #else
1190 s->activity = ABC_REALLOC(unsigned, s->activity, s->cap);
1191 s->activity2 = ABC_REALLOC(unsigned, s->activity2,s->cap);
1192 #endif
1193 s->model = ABC_REALLOC(int, s->model, s->cap);
1194 memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) );
1195 }
1196
1197 for (var = s->size; var < n; var++){
1198 assert(!s->wlists[2*var].size);
1199 assert(!s->wlists[2*var+1].size);
1200 if ( s->wlists[2*var].ptr == NULL )
1201 veci_new(&s->wlists[2*var]);
1202 if ( s->wlists[2*var+1].ptr == NULL )
1203 veci_new(&s->wlists[2*var+1]);
1204 *((int*)s->vi + var) = 0; //s->vi[var].val = varX;
1205 s->levels [var] = 0;
1206 s->assigns [var] = varX;
1207 s->reasons [var] = 0;
1208 if ( s->fProofLogging )
1209 s->units [var] = 0;
1210 #ifdef USE_FLOAT_ACTIVITY2
1211 s->activity[var] = 0;
1212 #else
1213 s->activity[var] = (1<<10);
1214 #endif
1215 s->model [var] = 0;
1216 // does not hold because variables enqueued at top level will not be reinserted in the heap
1217 // assert(veci_size(&s->order) == var);
1218 s->orderpos[var] = veci_size(&s->order);
1219 veci_push(&s->order,var);
1220 order_update(s, var);
1221 }
1222 s->size = n > s->size ? n : s->size;
1223 }
1224
sat_solver2_delete(sat_solver2 * s)1225 void sat_solver2_delete(sat_solver2* s)
1226 {
1227 int fVerify = 0;
1228 if ( fVerify )
1229 {
1230 veci * pCore = (veci *)Sat_ProofCore( s );
1231 // Abc_Print(1, "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) );
1232 veci_delete( pCore );
1233 ABC_FREE( pCore );
1234 // if ( s->fProofLogging )
1235 // Sat_ProofCheck( s );
1236 }
1237
1238 // report statistics
1239 // Abc_Print(1, "Used %6.2f MB for proof-logging. Unit clauses = %d.\n", 1.0 * Vec_ReportMemory(&s->Proofs) / (1<<20), s->nUnits );
1240
1241 // delete vectors
1242 veci_delete(&s->order);
1243 veci_delete(&s->trail_lim);
1244 veci_delete(&s->tagged);
1245 veci_delete(&s->stack);
1246 veci_delete(&s->temp_clause);
1247 veci_delete(&s->temp_proof);
1248 veci_delete(&s->conf_final);
1249 veci_delete(&s->mark_levels);
1250 veci_delete(&s->min_lit_order);
1251 veci_delete(&s->min_step_order);
1252 // veci_delete(&s->learnt_live);
1253 veci_delete(&s->act_clas);
1254 veci_delete(&s->claProofs);
1255 // veci_delete(&s->clauses);
1256 // veci_delete(&s->lrns);
1257 Sat_MemFree_( &s->Mem );
1258 // veci_delete(&s->proofs);
1259 Vec_SetFree( s->pPrf1 );
1260 Prf_ManStop( s->pPrf2 );
1261 Int2_ManStop( s->pInt2 );
1262
1263 // delete arrays
1264 if (s->vi != 0){
1265 int i;
1266 if ( s->wlists )
1267 for (i = 0; i < s->cap*2; i++)
1268 veci_delete(&s->wlists[i]);
1269 ABC_FREE(s->wlists );
1270 ABC_FREE(s->vi );
1271 ABC_FREE(s->levels );
1272 ABC_FREE(s->assigns );
1273 ABC_FREE(s->trail );
1274 ABC_FREE(s->orderpos );
1275 ABC_FREE(s->reasons );
1276 ABC_FREE(s->units );
1277 ABC_FREE(s->activity );
1278 ABC_FREE(s->activity2);
1279 ABC_FREE(s->model );
1280 }
1281 ABC_FREE(s);
1282
1283 // Abc_PrintTime( 1, "Time", Time );
1284 }
1285
1286
sat_solver2_addclause(sat_solver2 * s,lit * begin,lit * end,int Id)1287 int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end, int Id)
1288 {
1289 cla Cid;
1290 lit *i,*j,*iFree = NULL;
1291 int maxvar, count, temp;
1292 assert( solver2_dlevel(s) == 0 );
1293 assert( begin < end );
1294 assert( Id != 0 );
1295
1296 // copy clause into storage
1297 veci_resize( &s->temp_clause, 0 );
1298 for ( i = begin; i < end; i++ )
1299 veci_push( &s->temp_clause, *i );
1300 begin = veci_begin( &s->temp_clause );
1301 end = begin + veci_size( &s->temp_clause );
1302
1303 // insertion sort
1304 maxvar = lit_var(*begin);
1305 for (i = begin + 1; i < end; i++){
1306 lit l = *i;
1307 maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
1308 for (j = i; j > begin && *(j-1) > l; j--)
1309 *j = *(j-1);
1310 *j = l;
1311 }
1312 sat_solver2_setnvars(s,maxvar+1);
1313
1314
1315 // delete duplicates
1316 for (i = j = begin + 1; i < end; i++)
1317 {
1318 if ( *(i-1) == lit_neg(*i) ) // tautology
1319 return clause2_create_new( s, begin, end, 0, 0 ); // add it anyway, to preserve proper clause count
1320 if ( *(i-1) != *i )
1321 *j++ = *i;
1322 }
1323 end = j;
1324 assert( begin < end );
1325
1326 // coount the number of 0-literals
1327 count = 0;
1328 for ( i = begin; i < end; i++ )
1329 {
1330 // make sure all literals are unique
1331 assert( i == begin || lit_var(*(i-1)) != lit_var(*i) );
1332 // consider the value of this literal
1333 if ( var_value(s, lit_var(*i)) == lit_sign(*i) ) // this clause is always true
1334 return clause2_create_new( s, begin, end, 0, 0 ); // add it anyway, to preserve proper clause count
1335 if ( var_value(s, lit_var(*i)) == varX ) // unassigned literal
1336 iFree = i;
1337 else
1338 count++; // literal is 0
1339 }
1340 assert( count < end-begin ); // the clause cannot be UNSAT
1341
1342 // swap variables to make sure the clause is watched using unassigned variable
1343 temp = *iFree;
1344 *iFree = *begin;
1345 *begin = temp;
1346
1347 // create a new clause
1348 Cid = clause2_create_new( s, begin, end, 0, 0 );
1349 if ( Id )
1350 clause2_set_id( s, Cid, Id );
1351
1352 // handle unit clause
1353 if ( count+1 == end-begin )
1354 {
1355 if ( s->fProofLogging )
1356 {
1357 if ( count == 0 ) // original learned clause
1358 {
1359 var_set_unit_clause( s, lit_var(begin[0]), Cid );
1360 if ( !solver2_enqueue(s,begin[0],0) )
1361 assert( 0 );
1362 }
1363 else
1364 {
1365 // Log production of top-level unit clause:
1366 int x, k, proof_id, CidNew;
1367 clause* c = clause2_read(s, Cid);
1368 proof_chain_start( s, c );
1369 clause_foreach_var( c, x, k, 1 )
1370 proof_chain_resolve( s, NULL, x );
1371 proof_id = proof_chain_stop( s );
1372 // generate a new clause
1373 CidNew = clause2_create_new( s, begin, begin+1, 1, proof_id );
1374 var_set_unit_clause( s, lit_var(begin[0]), CidNew );
1375 if ( !solver2_enqueue(s,begin[0],Cid) )
1376 assert( 0 );
1377 }
1378 }
1379 }
1380 return Cid;
1381 }
1382
1383
luby2(double y,int x)1384 double luby2(double y, int x)
1385 {
1386 int size, seq;
1387 for (size = 1, seq = 0; size < x+1; seq++, size = 2*size + 1);
1388 while (size-1 != x){
1389 size = (size-1) >> 1;
1390 seq--;
1391 x = x % size;
1392 }
1393 return pow(y, (double)seq);
1394 }
1395
luby2_test()1396 void luby2_test()
1397 {
1398 int i;
1399 for ( i = 0; i < 20; i++ )
1400 Abc_Print(1, "%d ", (int)luby2(2,i) );
1401 Abc_Print(1, "\n" );
1402 }
1403
1404
1405 // updates clauses, watches, units, and proof
sat_solver2_reducedb(sat_solver2 * s)1406 void sat_solver2_reducedb(sat_solver2* s)
1407 {
1408 static abctime TimeTotal = 0;
1409 Sat_Mem_t * pMem = &s->Mem;
1410 clause * c = NULL;
1411 int nLearnedOld = veci_size(&s->act_clas);
1412 int * act_clas = veci_begin(&s->act_clas);
1413 int * pPerm, * pSortValues, nCutoffValue, * pClaProofs;
1414 int i, j, k, Id, nSelected;//, LastSize = 0;
1415 int Counter, CounterStart;
1416 abctime clk = Abc_Clock();
1417 static int Count = 0;
1418 Count++;
1419 assert( s->nLearntMax );
1420 s->nDBreduces++;
1421 // printf( "Calling reduceDB with %d clause limit and parameters (%d %d %d).\n", s->nLearntMax, s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
1422
1423 /*
1424 // find the new limit
1425 s->nLearntMax = s->nLearntMax * 11 / 10;
1426 // preserve 1/10 of last clauses
1427 CounterStart = s->stats.learnts - (s->nLearntMax / 10);
1428 // preserve 1/10 of most active clauses
1429 pSortValues = veci_begin(&s->act_clas);
1430 pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld );
1431 assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] );
1432 nCutoffValue = pSortValues[pPerm[nLearnedOld*9/10]];
1433 ABC_FREE( pPerm );
1434 // nCutoffValue = ABC_INFINITY;
1435 */
1436
1437
1438 // find the new limit
1439 s->nLearntMax = s->nLearntStart + s->nLearntDelta * s->nDBreduces;
1440 // preserve 1/20 of last clauses
1441 CounterStart = nLearnedOld - (s->nLearntMax / 20);
1442 // preserve 3/4 of most active clauses
1443 nSelected = nLearnedOld*s->nLearntRatio/100;
1444 // create sorting values
1445 pSortValues = ABC_ALLOC( int, nLearnedOld );
1446 Sat_MemForEachLearned( pMem, c, i, k )
1447 {
1448 Id = clause_id(c);
1449 pSortValues[Id] = (((7 - Abc_MinInt(c->lbd, 7)) << 28) | (act_clas[Id] >> 4));
1450 // pSortValues[Id] = act_clas[Id];
1451 assert( pSortValues[Id] >= 0 );
1452 }
1453 // find non-decreasing permutation
1454 pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld );
1455 assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] );
1456 nCutoffValue = pSortValues[pPerm[nLearnedOld-nSelected]];
1457 ABC_FREE( pPerm );
1458 // nCutoffValue = ABC_INFINITY;
1459
1460 // count how many clauses satisfy the condition
1461 Counter = j = 0;
1462 Sat_MemForEachLearned( pMem, c, i, k )
1463 {
1464 assert( c->mark == 0 );
1465 if ( Counter++ > CounterStart || clause_size(c) < 2 || pSortValues[clause_id(c)] >= nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) )
1466 {
1467 }
1468 else
1469 j++;
1470 if ( j >= nLearnedOld / 6 )
1471 break;
1472 }
1473 if ( j < nLearnedOld / 6 )
1474 {
1475 ABC_FREE( pSortValues );
1476 return;
1477 }
1478
1479 // mark learned clauses to remove
1480 Counter = j = 0;
1481 pClaProofs = veci_size(&s->claProofs) ? veci_begin(&s->claProofs) : NULL;
1482 Sat_MemForEachLearned( pMem, c, i, k )
1483 {
1484 assert( c->mark == 0 );
1485 if ( Counter++ > CounterStart || clause_size(c) < 2 || pSortValues[clause_id(c)] >= nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) )
1486 {
1487 pSortValues[j] = pSortValues[clause_id(c)];
1488 if ( pClaProofs )
1489 pClaProofs[j] = pClaProofs[clause_id(c)];
1490 if ( s->pPrf2 )
1491 Prf_ManAddSaved( s->pPrf2, clause_id(c), j );
1492 j++;
1493 }
1494 else // delete
1495 {
1496 c->mark = 1;
1497 s->stats.learnts_literals -= clause_size(c);
1498 s->stats.learnts--;
1499 }
1500 }
1501 ABC_FREE( pSortValues );
1502 if ( s->pPrf2 )
1503 Prf_ManCompact( s->pPrf2, j );
1504 // if ( j == nLearnedOld )
1505 // return;
1506
1507 assert( s->stats.learnts == (unsigned)j );
1508 assert( Counter == nLearnedOld );
1509 veci_resize(&s->act_clas,j);
1510 if ( veci_size(&s->claProofs) )
1511 veci_resize(&s->claProofs,j);
1512
1513 // update ID of each clause to be its new handle
1514 Counter = Sat_MemCompactLearned( pMem, 0 );
1515 assert( Counter == (int)s->stats.learnts );
1516
1517 // update reasons
1518 for ( i = 0; i < s->size; i++ )
1519 {
1520 if ( !s->reasons[i] ) // no reason
1521 continue;
1522 if ( clause_is_lit(s->reasons[i]) ) // 2-lit clause
1523 continue;
1524 if ( !clause_learnt_h(pMem, s->reasons[i]) ) // problem clause
1525 continue;
1526 assert( c->lrn );
1527 c = clause2_read( s, s->reasons[i] );
1528 assert( c->mark == 0 );
1529 s->reasons[i] = clause_id(c); // updating handle here!!!
1530 }
1531
1532 // update watches
1533 for ( i = 0; i < s->size*2; i++ )
1534 {
1535 int * pArray = veci_begin(&s->wlists[i]);
1536 for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
1537 {
1538 if ( clause_is_lit(pArray[k]) ) // 2-lit clause
1539 pArray[j++] = pArray[k];
1540 else if ( !clause_learnt_h(pMem, pArray[k]) ) // problem clause
1541 pArray[j++] = pArray[k];
1542 else
1543 {
1544 assert( c->lrn );
1545 c = clause2_read(s, pArray[k]);
1546 if ( !c->mark ) // useful learned clause
1547 pArray[j++] = clause_id(c); // updating handle here!!!
1548 }
1549 }
1550 veci_resize(&s->wlists[i],j);
1551 }
1552
1553 // compact units
1554 if ( s->fProofLogging )
1555 for ( i = 0; i < s->size; i++ )
1556 if ( s->units[i] && clause_learnt_h(pMem, s->units[i]) )
1557 {
1558 assert( c->lrn );
1559 c = clause2_read( s, s->units[i] );
1560 assert( c->mark == 0 );
1561 s->units[i] = clause_id(c);
1562 }
1563
1564 // perform final move of the clauses
1565 Counter = Sat_MemCompactLearned( pMem, 1 );
1566 assert( Counter == (int)s->stats.learnts );
1567
1568 // compact proof (compacts 'proofs' and update 'claProofs')
1569 if ( s->pPrf1 )
1570 {
1571 extern int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot );
1572 s->hProofPivot = Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot );
1573 }
1574
1575 // report the results
1576 TimeTotal += Abc_Clock() - clk;
1577 if ( s->fVerbose )
1578 {
1579 Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ",
1580 s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld );
1581 Abc_PrintTime( 1, "Time", TimeTotal );
1582 }
1583 }
1584
1585 // reverses to the previously bookmarked point
sat_solver2_rollback(sat_solver2 * s)1586 void sat_solver2_rollback( sat_solver2* s )
1587 {
1588 Sat_Mem_t * pMem = &s->Mem;
1589 int i, k, j;
1590 static int Count = 0;
1591 Count++;
1592 assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
1593 assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail );
1594 assert( s->pPrf1 == NULL || (s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(s->pPrf1)) );
1595 // reset implication queue
1596 solver2_canceluntil_rollback( s, s->iTrailPivot );
1597 // update order
1598 if ( s->iVarPivot < s->size )
1599 {
1600 if ( s->activity2 )
1601 {
1602 s->var_inc = s->var_inc2;
1603 memcpy( s->activity, s->activity2, sizeof(unsigned) * s->iVarPivot );
1604 }
1605 veci_resize(&s->order, 0);
1606 for ( i = 0; i < s->iVarPivot; i++ )
1607 {
1608 if ( var_value(s, i) != varX )
1609 continue;
1610 s->orderpos[i] = veci_size(&s->order);
1611 veci_push(&s->order,i);
1612 order_update(s, i);
1613 }
1614 }
1615 // compact watches
1616 for ( i = 0; i < s->iVarPivot*2; i++ )
1617 {
1618 cla* pArray = veci_begin(&s->wlists[i]);
1619 for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
1620 if ( Sat_MemClauseUsed(pMem, pArray[k]) )
1621 pArray[j++] = pArray[k];
1622 veci_resize(&s->wlists[i],j);
1623 }
1624 // reset watcher lists
1625 for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
1626 s->wlists[i].size = 0;
1627
1628 // reset clause counts
1629 s->stats.clauses = pMem->BookMarkE[0];
1630 s->stats.learnts = pMem->BookMarkE[1];
1631 // rollback clauses
1632 Sat_MemRollBack( pMem );
1633
1634 // resize learned arrays
1635 veci_resize(&s->act_clas, s->stats.learnts);
1636 if ( s->pPrf1 )
1637 {
1638 veci_resize(&s->claProofs, s->stats.learnts);
1639 Vec_SetShrink(s->pPrf1, s->hProofPivot);
1640 // some weird bug here, which shows only on 64-bits!
1641 // temporarily, perform more general proof reduction
1642 // Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot );
1643 }
1644 assert( s->pPrf2 == NULL );
1645 // if ( s->pPrf2 )
1646 // Prf_ManShrink( s->pPrf2, s->stats.learnts );
1647
1648 // initialize other vars
1649 s->size = s->iVarPivot;
1650 if ( s->size == 0 )
1651 {
1652 // s->size = 0;
1653 // s->cap = 0;
1654 s->qhead = 0;
1655 s->qtail = 0;
1656 #ifdef USE_FLOAT_ACTIVITY2
1657 s->var_inc = 1;
1658 s->cla_inc = 1;
1659 s->var_decay = (float)(1 / 0.95 );
1660 s->cla_decay = (float)(1 / 0.999 );
1661 #else
1662 s->var_inc = (1 << 5);
1663 s->cla_inc = (1 << 11);
1664 #endif
1665 s->root_level = 0;
1666 s->random_seed = 91648253;
1667 s->progress_estimate = 0;
1668 s->verbosity = 0;
1669
1670 s->stats.starts = 0;
1671 s->stats.decisions = 0;
1672 s->stats.propagations = 0;
1673 s->stats.inspects = 0;
1674 s->stats.conflicts = 0;
1675 s->stats.clauses = 0;
1676 s->stats.clauses_literals = 0;
1677 s->stats.learnts = 0;
1678 s->stats.learnts_literals = 0;
1679 s->stats.tot_literals = 0;
1680 // initialize clause pointers
1681 s->hLearntLast = -1; // the last learnt clause
1682 s->hProofLast = -1; // the last proof ID
1683
1684 // initialize rollback
1685 s->iVarPivot = 0; // the pivot for variables
1686 s->iTrailPivot = 0; // the pivot for trail
1687 s->hProofPivot = 1; // the pivot for proof records
1688 }
1689 }
1690
1691 // returns memory in bytes used by the SAT solver
sat_solver2_memory(sat_solver2 * s,int fAll)1692 double sat_solver2_memory( sat_solver2* s, int fAll )
1693 {
1694 int i;
1695 double Mem = sizeof(sat_solver2);
1696 if ( fAll )
1697 for (i = 0; i < s->cap*2; i++)
1698 Mem += s->wlists[i].cap * sizeof(int);
1699 Mem += s->cap * sizeof(veci); // ABC_FREE(s->wlists );
1700 Mem += s->act_clas.cap * sizeof(int);
1701 Mem += s->claProofs.cap * sizeof(int);
1702 // Mem += s->cap * sizeof(char); // ABC_FREE(s->polarity );
1703 // Mem += s->cap * sizeof(char); // ABC_FREE(s->tags );
1704 Mem += s->cap * sizeof(varinfo2); // ABC_FREE(s->vi );
1705 Mem += s->cap * sizeof(int); // ABC_FREE(s->levels );
1706 Mem += s->cap * sizeof(char); // ABC_FREE(s->assigns );
1707 #ifdef USE_FLOAT_ACTIVITY2
1708 Mem += s->cap * sizeof(double); // ABC_FREE(s->activity );
1709 #else
1710 Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity );
1711 if ( s->activity2 )
1712 Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity2);
1713 #endif
1714 Mem += s->cap * sizeof(lit); // ABC_FREE(s->trail );
1715 Mem += s->cap * sizeof(int); // ABC_FREE(s->orderpos );
1716 Mem += s->cap * sizeof(int); // ABC_FREE(s->reasons );
1717 Mem += s->cap * sizeof(int); // ABC_FREE(s->units );
1718 Mem += s->cap * sizeof(int); // ABC_FREE(s->model );
1719 Mem += s->tagged.cap * sizeof(int);
1720 Mem += s->stack.cap * sizeof(int);
1721 Mem += s->order.cap * sizeof(int);
1722 Mem += s->trail_lim.cap * sizeof(int);
1723 Mem += s->temp_clause.cap * sizeof(int);
1724 Mem += s->conf_final.cap * sizeof(int);
1725 Mem += s->mark_levels.cap * sizeof(int);
1726 Mem += s->min_lit_order.cap * sizeof(int);
1727 Mem += s->min_step_order.cap * sizeof(int);
1728 Mem += s->temp_proof.cap * sizeof(int);
1729 Mem += Sat_MemMemoryAll( &s->Mem );
1730 // Mem += Vec_ReportMemory( s->pPrf1 );
1731 return Mem;
1732 }
sat_solver2_memory_proof(sat_solver2 * s)1733 double sat_solver2_memory_proof( sat_solver2* s )
1734 {
1735 double Mem = s->dPrfMemory;
1736 if ( s->pPrf1 )
1737 Mem += Vec_ReportMemory( s->pPrf1 );
1738 return Mem;
1739 }
1740
1741
1742 // find the clause in the watcher lists
1743 /*
1744 int sat_solver2_find_clause( sat_solver2* s, int Hand, int fVerbose )
1745 {
1746 int i, k, Found = 0;
1747 if ( Hand >= s->clauses.size )
1748 return 1;
1749 for ( i = 0; i < s->size*2; i++ )
1750 {
1751 cla* pArray = veci_begin(&s->wlists[i]);
1752 for ( k = 0; k < veci_size(&s->wlists[i]); k++ )
1753 if ( (pArray[k] >> 1) == Hand )
1754 {
1755 if ( fVerbose )
1756 Abc_Print(1, "Clause found in list %d at position %d.\n", i, k );
1757 Found = 1;
1758 break;
1759 }
1760 }
1761 if ( Found == 0 )
1762 {
1763 if ( fVerbose )
1764 Abc_Print(1, "Clause with handle %d is not found.\n", Hand );
1765 }
1766 return Found;
1767 }
1768 */
1769 /*
1770 // verify that all problem clauses are satisfied
1771 void sat_solver2_verify( sat_solver2* s )
1772 {
1773 clause * c;
1774 int i, k, v, Counter = 0;
1775 clause_foreach_entry( &s->clauses, c, i, 1 )
1776 {
1777 for ( k = 0; k < (int)c->size; k++ )
1778 {
1779 v = lit_var(c->lits[k]);
1780 if ( sat_solver2_var_value(s, v) ^ lit_sign(c->lits[k]) )
1781 break;
1782 }
1783 if ( k == (int)c->size )
1784 {
1785 Abc_Print(1, "Clause %d is not satisfied. ", c->Id );
1786 clause_print_( c );
1787 sat_solver2_find_clause( s, clause_handle(&s->clauses, c), 1 );
1788 Counter++;
1789 }
1790 }
1791 if ( Counter != 0 )
1792 Abc_Print(1, "Verification failed!\n" );
1793 // else
1794 // Abc_Print(1, "Verification passed.\n" );
1795 }
1796 */
1797
1798 // checks how many watched clauses are satisfied by 0-level assignments
1799 // (this procedure may be called before setting up a new bookmark for rollback)
sat_solver2_check_watched(sat_solver2 * s)1800 int sat_solver2_check_watched( sat_solver2* s )
1801 {
1802 clause * c;
1803 int i, k, j, m;
1804 int claSat[2] = {0};
1805 // update watches
1806 for ( i = 0; i < s->size*2; i++ )
1807 {
1808 int * pArray = veci_begin(&s->wlists[i]);
1809 for ( m = k = 0; k < veci_size(&s->wlists[i]); k++ )
1810 {
1811 c = clause2_read(s, pArray[k]);
1812 for ( j = 0; j < (int)c->size; j++ )
1813 if ( var_value(s, lit_var(c->lits[j])) == lit_sign(c->lits[j]) ) // true lit
1814 break;
1815 if ( j == (int)c->size )
1816 {
1817 pArray[m++] = pArray[k];
1818 continue;
1819 }
1820 claSat[c->lrn]++;
1821 }
1822 veci_resize(&s->wlists[i],m);
1823 if ( m == 0 )
1824 {
1825 // s->wlists[i].cap = 0;
1826 // s->wlists[i].size = 0;
1827 // ABC_FREE( s->wlists[i].ptr );
1828 }
1829 }
1830 // printf( "\nClauses = %d (Sat = %d). Learned = %d (Sat = %d).\n",
1831 // s->stats.clauses, claSat[0], s->stats.learnts, claSat[1] );
1832 return 0;
1833 }
1834
sat_solver2_solve(sat_solver2 * s,lit * begin,lit * end,ABC_INT64_T nConfLimit,ABC_INT64_T nInsLimit,ABC_INT64_T nConfLimitGlobal,ABC_INT64_T nInsLimitGlobal)1835 int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
1836 {
1837 int restart_iter = 0;
1838 ABC_INT64_T nof_conflicts;
1839 lbool status = l_Undef;
1840 int proof_id;
1841 lit * i;
1842
1843 s->hLearntLast = -1;
1844 s->hProofLast = -1;
1845
1846 // set the external limits
1847 // s->nCalls++;
1848 // s->nRestarts = 0;
1849 s->nConfLimit = 0;
1850 s->nInsLimit = 0;
1851 if ( nConfLimit )
1852 s->nConfLimit = s->stats.conflicts + nConfLimit;
1853 if ( nInsLimit )
1854 // s->nInsLimit = s->stats.inspects + nInsLimit;
1855 s->nInsLimit = s->stats.propagations + nInsLimit;
1856 if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) )
1857 s->nConfLimit = nConfLimitGlobal;
1858 if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
1859 s->nInsLimit = nInsLimitGlobal;
1860
1861 /*
1862 // Perform assumptions:
1863 root_level = assumps.size();
1864 for (int i = 0; i < assumps.size(); i++){
1865 Lit p = assumps[i];
1866 assert(var(p) < nVars());
1867 if (!solver2_assume(p)){
1868 GClause r = reason[var(p)];
1869 if (r != Gclause2_NULL){
1870 clause* confl;
1871 if (r.isLit()){
1872 confl = propagate_tmpbin;
1873 (*confl)[1] = ~p;
1874 (*confl)[0] = r.lit();
1875 }else
1876 confl = r.clause();
1877 analyzeFinal(confl, true);
1878 conflict.push(~p);
1879 }else
1880 conflict.clear(),
1881 conflict.push(~p);
1882 cancelUntil(0);
1883 return false; }
1884 clause* confl = propagate();
1885 if (confl != NULL){
1886 analyzeFinal(confl), assert(conflict.size() > 0);
1887 cancelUntil(0);
1888 return false; }
1889 }
1890 assert(root_level == decisionLevel());
1891 */
1892
1893 // Perform assumptions:
1894 s->root_level = end - begin;
1895 for ( i = begin; i < end; i++ )
1896 {
1897 lit p = *i;
1898 assert(lit_var(p) < s->size);
1899 veci_push(&s->trail_lim,s->qtail);
1900 if (!solver2_enqueue(s,p,0))
1901 {
1902 clause* r = clause2_read(s, lit_reason(s,p));
1903 if (r != NULL)
1904 {
1905 clause* confl = r;
1906 proof_id = solver2_analyze_final(s, confl, 1);
1907 veci_push(&s->conf_final, lit_neg(p));
1908 }
1909 else
1910 {
1911 // assert( 0 );
1912 // r = var_unit_clause( s, lit_var(p) );
1913 // assert( r != NULL );
1914 // proof_id = clause2_proofid(s, r, 0);
1915 proof_id = -1; // the only case when ProofId is not assigned (conflicting assumptions)
1916 veci_resize(&s->conf_final,0);
1917 veci_push(&s->conf_final, lit_neg(p));
1918 // the two lines below are a bug fix by Siert Wieringa
1919 if (var_level(s, lit_var(p)) > 0)
1920 veci_push(&s->conf_final, p);
1921 }
1922 s->hProofLast = proof_id;
1923 solver2_canceluntil(s, 0);
1924 return l_False;
1925 }
1926 else
1927 {
1928 clause* confl = solver2_propagate(s);
1929 if (confl != NULL){
1930 proof_id = solver2_analyze_final(s, confl, 0);
1931 assert(s->conf_final.size > 0);
1932 s->hProofLast = proof_id;
1933 solver2_canceluntil(s, 0);
1934 return l_False;
1935 }
1936 }
1937 }
1938 assert(s->root_level == solver2_dlevel(s));
1939
1940 if (s->verbosity >= 1){
1941 Abc_Print(1,"==================================[MINISAT]===================================\n");
1942 Abc_Print(1,"| Conflicts | ORIGINAL | LEARNT | Progress |\n");
1943 Abc_Print(1,"| | Clauses Literals | Limit Clauses Literals Lit/Cl | |\n");
1944 Abc_Print(1,"==============================================================================\n");
1945 }
1946
1947 while (status == l_Undef){
1948 if (s->verbosity >= 1)
1949 {
1950 Abc_Print(1,"| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n",
1951 (double)s->stats.conflicts,
1952 (double)s->stats.clauses,
1953 (double)s->stats.clauses_literals,
1954 (double)s->nLearntMax,
1955 (double)s->stats.learnts,
1956 (double)s->stats.learnts_literals,
1957 (s->stats.learnts == 0)? 0.0 : (double)s->stats.learnts_literals / s->stats.learnts,
1958 s->progress_estimate*100);
1959 fflush(stdout);
1960 }
1961 if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
1962 break;
1963 // reduce the set of learnt clauses
1964 if ( s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax && s->pPrf2 == NULL )
1965 sat_solver2_reducedb(s);
1966 // perform next run
1967 nof_conflicts = (ABC_INT64_T)( 100 * luby2(2, restart_iter++) );
1968 status = solver2_search(s, nof_conflicts);
1969 // quit the loop if reached an external limit
1970 if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
1971 break;
1972 if ( s->nInsLimit && s->stats.propagations > s->nInsLimit )
1973 break;
1974 }
1975 if (s->verbosity >= 1)
1976 Abc_Print(1,"==============================================================================\n");
1977
1978 solver2_canceluntil(s,0);
1979 // assert( s->qhead == s->qtail );
1980 // if ( status == l_True )
1981 // sat_solver2_verify( s );
1982 return status;
1983 }
1984
Sat_ProofCore(sat_solver2 * s)1985 void * Sat_ProofCore( sat_solver2 * s )
1986 {
1987 extern void * Proof_DeriveCore( Vec_Set_t * vProof, int hRoot );
1988 if ( s->pPrf1 )
1989 return Proof_DeriveCore( s->pPrf1, s->hProofLast );
1990 if ( s->pPrf2 )
1991 {
1992 s->dPrfMemory = Abc_MaxDouble( s->dPrfMemory, Prf_ManMemory(s->pPrf2) );
1993 return Prf_ManUnsatCore( s->pPrf2 );
1994 }
1995 return NULL;
1996 }
1997
1998 ABC_NAMESPACE_IMPL_END
1999