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