satSolver2.c 66.4 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
/**************************************************************************************************
MiniSat -- Copyright (c) 2005, Niklas Sorensson
http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko

#include <stdio.h>
#include <assert.h>
#include <string.h>
#include <math.h>
26

27 28 29 30
#include "satSolver2.h"

ABC_NAMESPACE_IMPL_START

31
#define SAT_USE_PROOF_LOGGING
32 33 34

//=================================================================================================
// Debug:
35
 
36 37 38 39
//#define VERBOSEDEBUG

// For derivation output (verbosity level 2)
#define L_IND    "%-*d"
40
#define L_ind    solver2_dlevel(s)*2+2,solver2_dlevel(s)
41 42 43 44 45 46
#define L_LIT    "%sx%d"
#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
static void printlits(lit* begin, lit* end)
{
    int i;
    for (i = 0; i < end - begin; i++)
47
        Abc_Print(1,L_LIT" ",L_lit(begin[i]));
48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
}

//=================================================================================================
// Random numbers:


// Returns a random float 0 <= x < 1. Seed must never be 0.
static inline double drand(double* seed) {
    int q;
    *seed *= 1389796;
    q = (int)(*seed / 2147483647);
    *seed -= (double)q * 2147483647;
    return *seed / 2147483647; }


// Returns a random integer 0 <= x < size. Seed must never be 0.
static inline int irand(double* seed, int size) {
    return (int)(drand(seed) * size); }

//=================================================================================================
68 69
// Variable datatype + minor functions:

Alan Mishchenko committed
70
//static const int var0  = 1;
71 72 73
static const int var1  = 0;
static const int varX  = 3;

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
};

Alan Mishchenko committed
83 84 85
int    var_is_assigned(sat_solver2* s, int v)            { return s->assigns[v] != varX; }
int    var_is_partA (sat_solver2* s, int v)              { return s->vi[v].partA;        }
void   var_set_partA(sat_solver2* s, int v, int partA)   { s->vi[v].partA = partA;       }
86

87 88 89 90
//static inline int     var_level     (sat_solver2* s, int v)            { return s->vi[v].lev; }
static inline int     var_level     (sat_solver2* s, int v)            { return s->levels[v];  }
//static inline int     var_value     (sat_solver2* s, int v)            { return s->vi[v].val; }
static inline int     var_value     (sat_solver2* s, int v)            { return s->assigns[v]; }
91
static inline int     var_polar     (sat_solver2* s, int v)            { return s->vi[v].pol; }
92

93 94 95 96
//static inline void    var_set_level (sat_solver2* s, int v, int lev)   { s->vi[v].lev = lev;  }
static inline void    var_set_level (sat_solver2* s, int v, int lev)   { s->levels[v] = lev;  }
//static inline void    var_set_value (sat_solver2* s, int v, int val)   { s->vi[v].val = val;  }
static inline void    var_set_value (sat_solver2* s, int v, int val)   { s->assigns[v] = val; }
97
static inline void    var_set_polar (sat_solver2* s, int v, int pol)   { s->vi[v].pol = pol;  }
98

Alan Mishchenko committed
99 100 101 102 103
// check if the literal is false under current assumptions
static inline int     solver2_lit_is_false( sat_solver2* s, int Lit )  { return var_value(s, lit_var(Lit)) == !lit_sign(Lit); }



104
// variable tags
105
static inline int     var_tag       (sat_solver2* s, int v)            { return s->vi[v].tag; }
106
static inline void    var_set_tag   (sat_solver2* s, int v, int tag)   {
107
    assert( tag > 0 && tag < 16 );
108 109
    if ( s->vi[v].tag == 0 )
        veci_push( &s->tagged, v );
110
    s->vi[v].tag = tag;
111
}
112
static inline void    var_add_tag   (sat_solver2* s, int v, int tag)   {
113
    assert( tag > 0 && tag < 16 );
114 115
    if ( s->vi[v].tag == 0 )
        veci_push( &s->tagged, v );
116
    s->vi[v].tag |= tag;
117
}
118
static inline void    solver2_clear_tags(sat_solver2* s, int start)    {
119 120 121 122 123
    int i, * tagged = veci_begin(&s->tagged);
    for (i = start; i < veci_size(&s->tagged); i++)
        s->vi[tagged[i]].tag = 0;
    veci_resize(&s->tagged,start);
}
124

125
// level marks
126 127
static inline int     var_lev_mark (sat_solver2* s, int v)             {
    return (veci_begin(&s->trail_lim)[var_level(s,v)] & 0x80000000) > 0;
128
}
129
static inline void    var_lev_set_mark (sat_solver2* s, int v)         {
130 131 132 133 134
    int level = var_level(s,v);
    assert( level < veci_size(&s->trail_lim) );
    veci_begin(&s->trail_lim)[level] |= 0x80000000;
    veci_push(&s->mark_levels, level);
}
135
static inline void    solver2_clear_marks(sat_solver2* s)              {
136 137 138 139 140 141
    int i, * mark_levels = veci_begin(&s->mark_levels);
    for (i = 0; i < veci_size(&s->mark_levels); i++)
        veci_begin(&s->trail_lim)[mark_levels[i]] &= 0x7FFFFFFF;
    veci_resize(&s->mark_levels,0);
}

142
//=================================================================================================
143 144
// Clause datatype + minor functions:

145 146
//static inline int     var_reason    (sat_solver2* s, int v)      { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1;                   }
//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 149 150
//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;             }
static inline int     var_reason    (sat_solver2* s, int v)            { return s->reasons[v];           }
static inline int     lit_reason    (sat_solver2* s, int l)            { return s->reasons[lit_var(l)];  }
151
static inline clause* var_unit_clause(sat_solver2* s, int v)           { return clause2_read(s, s->units[v]);                                          }
152 153
static inline void    var_set_unit_clause(sat_solver2* s, int v, cla i){ 
    assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; 
154
}
155

156 157
#define clause_foreach_var( p, var, i, start )        \
    for ( i = start; (i < (int)(p)->size) && ((var) = lit_var((p)->lits[i])); i++ )
158

159 160 161 162 163
//=================================================================================================
// Simple helpers:

static inline int     solver2_dlevel(sat_solver2* s)       { return veci_size(&s->trail_lim); }
static inline veci*   solver2_wlist(sat_solver2* s, lit l) { return &s->wlists[l];            }
164 165

//=================================================================================================
166 167
// Proof logging:

168
static inline void proof_chain_start( sat_solver2* s, clause* c )
169
{
170 171
    if ( !s->fProofLogging )
        return;
172 173
    if ( s->pInt2 )
        s->tempInter = Int2_ManChainStart( s->pInt2, c );
174 175 176
    if ( s->pPrf2 )
        Prf_ManChainStart( s->pPrf2, c );
    if ( s->pPrf1 )
177
    {
178
        int ProofId = clause2_proofid(s, c, 0);
179
        assert( (ProofId >> 2) > 0 );
180 181 182 183
        veci_resize( &s->temp_proof, 0 );
        veci_push( &s->temp_proof, 0 );
        veci_push( &s->temp_proof, 0 );
        veci_push( &s->temp_proof, ProofId );
184 185 186
    }
}

187
static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var )
188
{
189 190
    if ( !s->fProofLogging )
        return;
191 192 193 194 195
    if ( s->pInt2 )
    {
        clause* c = cls ? cls : var_unit_clause( s, Var );
        s->tempInter = Int2_ManChainResolve( s->pInt2, c, s->tempInter, var_is_partA(s,Var) );
    }
196 197 198 199 200 201
    if ( s->pPrf2 )
    {
        clause* c = cls ? cls : var_unit_clause( s, Var );
        Prf_ManChainResolve( s->pPrf2, c );
    }
    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
    }
}

210
static inline int proof_chain_stop( sat_solver2* s )
211
{
212 213
    if ( !s->fProofLogging )
        return 0;
214 215 216 217 218 219
    if ( s->pInt2 )
    {
        int h = s->tempInter; 
        s->tempInter = -1; 
        return h;
    }
220 221 222
    if ( s->pPrf2 )
        Prf_ManChainStop( s->pPrf2 );
    if ( s->pPrf1 )
223
    {
224
        extern void Proof_ClauseSetEnts( Vec_Set_t* p, int h, int nEnts );
225 226
        int h = Vec_SetAppend( s->pPrf1, veci_begin(&s->temp_proof), veci_size(&s->temp_proof) );
        Proof_ClauseSetEnts( s->pPrf1, h, veci_size(&s->temp_proof) - 2 );
227
        return h;
228
    }
229
    return 0;
230 231 232
}

//=================================================================================================
233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251
// Variable order functions:

static inline void order_update(sat_solver2* s, int v) // updateorder
{
    int*      orderpos = s->orderpos;
    int*      heap     = veci_begin(&s->order);
    int       i        = orderpos[v];
    int       x        = heap[i];
    int       parent   = (i - 1) / 2;
    assert(s->orderpos[v] != -1);
    while (i != 0 && s->activity[x] > s->activity[heap[parent]]){
        heap[i]           = heap[parent];
        orderpos[heap[i]] = i;
        i                 = parent;
        parent            = (i - 1) / 2;
    }
    heap[i]     = x;
    orderpos[x] = i;
}
252
static inline void order_assigned(sat_solver2* s, int v)
253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271
{
}
static inline void order_unassigned(sat_solver2* s, int v) // undoorder
{
    int* orderpos = s->orderpos;
    if (orderpos[v] == -1){
        orderpos[v] = veci_size(&s->order);
        veci_push(&s->order,v);
        order_update(s,v);
    }
}
static inline int  order_select(sat_solver2* s, float random_var_freq) // selectvar
{
    int*      heap     = veci_begin(&s->order);
    int*      orderpos = s->orderpos;
    // Random decision:
    if (drand(&s->random_seed) < random_var_freq){
        int next = irand(&s->random_seed,s->size);
        assert(next >= 0 && next < s->size);
272
        if (var_value(s, next) == varX)
273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299
            return next;
    }
    // Activity based decision:
    while (veci_size(&s->order) > 0){
        int    next  = heap[0];
        int    size  = veci_size(&s->order)-1;
        int    x     = heap[size];
        veci_resize(&s->order,size);
        orderpos[next] = -1;
        if (size > 0){
            unsigned act   = s->activity[x];
            int      i     = 0;
            int      child = 1;
            while (child < size){
                if (child+1 < size && s->activity[heap[child]] < s->activity[heap[child+1]])
                    child++;
                assert(child < size);
                if (act >= s->activity[heap[child]])
                    break;
                heap[i]           = heap[child];
                orderpos[heap[i]] = i;
                i                 = child;
                child             = 2 * child + 1;
            }
            heap[i]           = x;
            orderpos[heap[i]] = i;
        }
300
        if (var_value(s, next) == varX)
301 302 303 304 305
            return next;
    }
    return var_Undef;
}

306

307 308 309
//=================================================================================================
// Activity functions:

310
#ifdef USE_FLOAT_ACTIVITY2
311 312 313 314

static inline void act_var_rescale(sat_solver2* s)  {
    double* activity = s->activity;
    int i;
315
    for (i = 0; i < s->size; i++)
316 317
        activity[i] *= 1e-100;
    s->var_inc *= 1e-100;
318
}
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 325
    for (i = 0; i < veci_size(&s->act_clas); i++)
        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
}
332 333
static inline void act_var_bump(sat_solver2* s, int v) {
    s->activity[v] += s->var_inc;
334
    if (s->activity[v] > 1e100)
335 336 337 338
        act_var_rescale(s);
    if (s->orderpos[v] != -1)
        order_update(s,v);
}
339 340 341 342 343
static inline void act_clause2_bump(sat_solver2* s, clause*c) {
    float * act_clas = (float *)veci_begin(&s->act_clas);
    assert( c->Id < veci_size(&s->act_clas) );
    act_clas[c->Id] += s->cla_inc;
    if (act_clas[c->Id] > (float)1e20)
344
        act_clause2_rescale(s);
345 346
}
static inline void act_var_decay(sat_solver2* s)    { s->var_inc *= s->var_decay; }
347
static inline void act_clause2_decay(sat_solver2* s) { s->cla_inc *= s->cla_decay; }
348

349
#else
350

351 352 353 354 355 356 357 358
static inline void act_var_rescale(sat_solver2* s) {
    unsigned* activity = s->activity;
    int i;
    for (i = 0; i < s->size; i++)
        activity[i] >>= 19;
    s->var_inc >>= 19;
    s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
}
359
static inline void act_clause2_rescale(sat_solver2* s) {
360 361
//    static abctime Total = 0;
//    abctime clk = Abc_Clock();
362 363 364 365
    int i;
    unsigned * act_clas = (unsigned *)veci_begin(&s->act_clas);
    for (i = 0; i < veci_size(&s->act_clas); i++)
        act_clas[i] >>= 14;
366 367
    s->cla_inc >>= 14;
    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
}
372 373 374 375 376 377 378
static inline void act_var_bump(sat_solver2* s, int v) {
    s->activity[v] += s->var_inc;
    if (s->activity[v] & 0x80000000)
        act_var_rescale(s);
    if (s->orderpos[v] != -1)
        order_update(s,v);
}
379 380 381 382 383 384
static inline void act_clause2_bump(sat_solver2* s, clause*c) {
    unsigned * act_clas = (unsigned *)veci_begin(&s->act_clas);
    int Id = clause_id(c);
    assert( Id >= 0 && Id < veci_size(&s->act_clas) );
    act_clas[Id] += s->cla_inc;
    if (act_clas[Id] & 0x80000000)
385
        act_clause2_rescale(s);
386
}
387
static inline void act_var_decay(sat_solver2* s)    { s->var_inc += (s->var_inc >>  4); }
388
static inline void act_clause2_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc >> 10); }
389

390
#endif
391 392

//=================================================================================================
393 394
// Clause functions:

395 396 397 398 399 400 401 402 403 404 405 406 407
static inline int sat_clause_compute_lbd( sat_solver2* s, clause* c )
{
    int i, lev, minl = 0, lbd = 0;
    for (i = 0; i < (int)c->size; i++) {
        lev = var_level(s, lit_var(c->lits[i]));
        if ( !(minl & (1 << (lev & 31))) ) {
            minl |= 1 << (lev & 31);
            lbd++;
        }
    }
    return lbd;
}

408
static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id )
409
{
410 411 412 413 414 415 416 417 418 419 420
    clause* c;
    int h, size = end - begin;
    assert(size < 1 || begin[0] >= 0);
    assert(size < 2 || begin[1] >= 0);
    assert(size < 1 || lit_var(begin[0]) < s->size);
    assert(size < 2 || lit_var(begin[1]) < s->size);
    // create new clause
    h = Sat_MemAppend( &s->Mem, begin, size, learnt, 1 );
    assert( !(h & 1) );
    c = clause2_read( s, h );
    if (learnt)
421
    {
422
        if ( s->pPrf1 )
423 424 425
            assert( proof_id );
        c->lbd = sat_clause_compute_lbd( s, c );
        assert( clause_id(c) == veci_size(&s->act_clas) );
426
        if ( s->pPrf1 || s->pInt2 )
427
            veci_push(&s->claProofs, proof_id);
428 429 430
//        veci_push(&s->act_clas, (1<<10));
        veci_push(&s->act_clas, 0);
        if ( size > 2 )
431
            act_clause2_bump( s,c );
432 433
        s->stats.learnts++;
        s->stats.learnts_literals += size;
434
        // remember the last one
435
        s->hLearntLast = h;
436 437 438
    }
    else
    {
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 445 446 447
    if ( size > 1 )
    {
        veci_push(solver2_wlist(s,lit_neg(begin[0])),h);
        veci_push(solver2_wlist(s,lit_neg(begin[1])),h);
448
    }
449
    return h;
450 451 452
}

//=================================================================================================
453 454
// Minor (solver) functions:

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 462 463 464
    if (var_value(s, v) != varX)
        return var_value(s, v) == lit_sign(l);
    else
    {  // 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 472 473 474 475 476
        s->trail[s->qtail++] = l;
        order_assigned(s, v);
        return true;
    }
}

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 483
    Abc_Print(1,L_IND"assume("L_LIT")  ", L_ind, L_lit(l));
    Abc_Print(1, "act = %.20f\n", s->activity[lit_var(l)] );
484 485
#endif
    veci_push(&s->trail_lim,s->qtail);
486
    return solver2_enqueue(s,l,0);
487 488
}

489
static void solver2_canceluntil(sat_solver2* s, int level) {
490 491
    int      bound;
    int      lastLev;
492
    int      c, x;
493

494
    if (solver2_dlevel(s) <= level)
495
        return;
496
    assert( solver2_dlevel(s) > 0 );
497 498 499 500

    bound   = (veci_begin(&s->trail_lim))[level];
    lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1];

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 515 516 517

    s->qhead = s->qtail = bound;
    veci_resize(&s->trail_lim,level);
}

518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538
static void solver2_canceluntil_rollback(sat_solver2* s, int NewBound) {
    int      c, x;
   
    assert( solver2_dlevel(s) == 0 );
    assert( s->qtail == s->qhead );
    assert( s->qtail >= NewBound );

    for (c = s->qtail-1; c >= NewBound; c--) 
    {
        x = lit_var(s->trail[c]);
        var_set_value(s, x, varX);
        s->reasons[x] = 0;
        s->units[x] = 0; // temporary?
    }

    for (c = s->qhead-1; c >= NewBound; c--)
        order_unassigned(s,lit_var(s->trail[c]));

    s->qhead = s->qtail = NewBound;
}

539

540
static void solver2_record(sat_solver2* s, veci* cls, int proof_id)
541
{
542 543
    lit* begin = veci_begin(cls);
    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 547
    if ( veci_size(cls) == 1 )
    {
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
}


556
static double solver2_progress(sat_solver2* s)
557
{
558 559
    int i;
    double progress = 0.0, F = 1.0 / s->size;
560
    for (i = 0; i < s->size; i++)
561 562
        if (var_value(s, i) != varX)
            progress += pow(F, var_level(s, i));
563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578
    return progress / s->size;
}

//=================================================================================================
// Major methods:

/*_________________________________________________________________________________________________
|
|  analyzeFinal : (p : Lit)  ->  [void]
|  
|  Description:
|    Specialized analysis procedure to express the final conflict in terms of assumptions.
|    Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
|    stores the result in 'out_conflict'.
|________________________________________________________________________________________________@*/
/*
579
void Solver::analyzeFinal(clause* confl, bool skip_first)
580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596
{
    // -- NOTE! This code is relatively untested. Please report bugs!
    conflict.clear();
    if (root_level == 0) return;

    vec<char>& seen  = analyze_seen;
    for (int i = skip_first ? 1 : 0; i < confl->size(); i++){
        Var x = var((*confl)[i]);
        if (level[x] > 0)
            seen[x] = 1;
    }

    int start = (root_level >= trail_lim.size()) ? trail.size()-1 : trail_lim[root_level];
    for (int i = start; i >= trail_lim[0]; i--){
        Var     x = var(trail[i]);
        if (seen[x]){
            GClause r = reason[x];
597
            if (r == Gclause2_NULL){
598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617
                assert(level[x] > 0);
                conflict.push(~trail[i]);
            }else{
                if (r.isLit()){
                    Lit p = r.lit();
                    if (level[var(p)] > 0)
                        seen[var(p)] = 1;
                }else{
                    Clause& c = *r.clause();
                    for (int j = 1; j < c.size(); j++)
                        if (level[var(c[j])] > 0)
                            seen[var(c[j])] = 1;
                }
            }
            seen[x] = 0;
        }
    }
}
*/

618
static int solver2_analyze_final(sat_solver2* s, clause* conf, int skip_first)
619
{
620
    int i, j, x;//, start;
621 622
    veci_resize(&s->conf_final,0);
    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 628
        if ( var_level(s,x) )
            var_set_tag(s, x, 1);
629 630
        else
            proof_chain_resolve( s, NULL, x );
631
    }
632 633 634
    assert( s->root_level >= veci_size(&s->trail_lim) );
//    start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level];
    for (i = s->qtail-1; i >= (veci_begin(&s->trail_lim))[0]; i--){
635 636
        x = lit_var(s->trail[i]);
        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 642 643 644
                    if ( var_level(s,x) )
                        var_set_tag(s, x, 1);
                    else
                        proof_chain_resolve( s, NULL, x );
645
                }
646 647 648
            }else {
                assert( var_level(s,x) );
                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
}

656
static int solver2_lit_removable_rec(sat_solver2* s, int v)
657
{
658 659 660 661
    // tag[0]: True if original conflict clause literal.
    // tag[1]: Processed by this procedure
    // tag[2]: 0=non-removable, 1=removable

662
    clause* c;
663 664 665 666 667 668 669
    int i, x;

    // skip visited
    if (var_tag(s,v) & 2)
        return (var_tag(s,v) & 4) > 0;

    // skip decisions on a wrong level
670
    c = clause2_read(s, var_reason(s,v));
671 672 673 674 675
    if ( c == NULL ){
        var_add_tag(s,v,2);
        return 0;
    }

676
    clause_foreach_var( c, x, i, 1 ){
677
        if (var_tag(s,x) & 1)
678
            solver2_lit_removable_rec(s, x);
679 680
        else{
            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 684
                var_add_tag(s,v,2);
                return 0;
685 686 687
            }
        }
    }
688 689
    if ( s->fProofLogging && (var_tag(s,v) & 1) )
        veci_push(&s->min_lit_order, v );
690 691 692 693
    var_add_tag(s,v,6);
    return 1;
}

694
static int solver2_lit_removable(sat_solver2* s, int x)
695
{
696
    clause* c;
697 698 699 700 701 702 703 704 705
    int i, top;
    if ( !var_reason(s,x) )
        return 0;
    if ( var_tag(s,x) & 2 )
    {
        assert( var_tag(s,x) & 1 );
        return 1;
    }
    top = veci_size(&s->tagged);
706
    veci_resize(&s->stack,0);
707 708
    veci_push(&s->stack, x << 1);
    while (veci_size(&s->stack))
709
    {
710
        x = veci_pop(&s->stack);
711 712
        if ( s->fProofLogging )
        {
713 714 715 716
            if ( x & 1 ){
                if ( var_tag(s,x >> 1) & 1 )
                    veci_push(&s->min_lit_order, x >> 1 );
                continue;
717
            }
718 719 720
            veci_push(&s->stack, x ^ 1 );
        }
        x >>= 1;
721
        c = clause2_read(s, var_reason(s,x));
722
        clause_foreach_var( c, x, i, 1 ){
723 724 725 726 727 728 729 730
            if (var_tag(s,x) || !var_level(s,x))
                continue;
            if (!var_reason(s,x) || !var_lev_mark(s,x)){
                solver2_clear_tags(s, top);
                return 0;
            }
            veci_push(&s->stack, x << 1);
            var_set_tag(s, x, 2);
731 732
        }
    }
733
    return 1;
734 735
}

736
static void solver2_logging_order(sat_solver2* s, int x)
737
{
738
    clause* c;
739 740 741 742 743 744 745 746 747 748 749 750 751 752 753
    int i;
    if ( (var_tag(s,x) & 4) )
        return;
    var_add_tag(s, x, 4);
    veci_resize(&s->stack,0);
    veci_push(&s->stack,x << 1);
    while (veci_size(&s->stack))
    {
        x = veci_pop(&s->stack);
        if ( x & 1 ){
            veci_push(&s->min_step_order, x >> 1 );
            continue;
        }
        veci_push(&s->stack, x ^ 1 );
        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 759 760 761 762 763 764
            if ( !var_level(s,x) || (var_tag(s,x) & 1) )
                continue;
            veci_push(&s->stack, x << 1);
            var_add_tag(s, x, 4);
        }
    }
}
765

766 767
static void solver2_logging_order_rec(sat_solver2* s, int x)
{
768
    clause* c;
769 770 771
    int i, y;
    if ( (var_tag(s,x) & 8) )
        return;
772
    c = clause2_read(s, var_reason(s,x));
773
    clause_foreach_var( c, y, i, 1 )
774 775 776 777 778 779
        if ( var_level(s,y) && (var_tag(s,y) & 1) == 0 )
            solver2_logging_order_rec(s, y);
    var_add_tag(s, x, 8);
    veci_push(&s->min_step_order, x);
}

780
static int solver2_analyze(sat_solver2* s, clause* c, veci* learnt)
781
{
782
    int cnt      = 0;
783
    lit p        = 0;
784 785
    int x, ind   = s->qtail-1;
    int proof_id = 0;
786 787 788
    lit* lits,* vars, i, j, k;
    assert( veci_size(&s->tagged) == 0 );
    // tag[0] - visited by conflict analysis (afterwards: literals of the learned clause)
789 790
    // tag[1] - visited by solver2_lit_removable() with success
    // tag[2] - visited by solver2_logging_order()
791

792 793 794 795
    proof_chain_start( s, c );
    veci_push(learnt,lit_Undef);
    while ( 1 ){
        assert(c != 0);
796
        if (c->lrn)
797
            act_clause2_bump(s,c);
798
        clause_foreach_var( c, x, j, (int)(p > 0) ){
799 800 801 802 803
            assert(x >= 0 && x < s->size);
            if ( var_tag(s, x) )
                continue;
            if ( var_level(s,x) == 0 )
            {
804
                proof_chain_resolve( s, NULL, x );
805 806 807 808 809 810 811
                continue;
            }
            var_set_tag(s, x, 1);
            act_var_bump(s,x);
            if (var_level(s,x) == solver2_dlevel(s))
                cnt++;
            else
812
                veci_push(learnt,c->lits[j]);
813 814 815 816 817
        }

        while (!var_tag(s, lit_var(s->trail[ind--])));

        p = s->trail[ind+1];
818
        c = clause2_read(s, lit_reason(s,p));
819 820 821 822 823
        cnt--;
        if ( cnt == 0 )
            break;
        proof_chain_resolve( s, c, lit_var(p) );
    }
824 825
    *veci_begin(learnt) = lit_neg(p);

826 827
    // mark levels
    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 841 842 843 844 845 846

    // record the proof
    if ( s->fProofLogging )
    {
        // collect additional clauses to resolve
        veci_resize(&s->min_step_order, 0);
        vars = veci_begin(&s->min_lit_order);
        for (i = 0; i < veci_size(&s->min_lit_order); i++)
847 848
//            solver2_logging_order(s, vars[i]);
            solver2_logging_order_rec(s, vars[i]);
849 850 851 852

        // add them in the reverse order
        vars = veci_begin(&s->min_step_order);
        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 863 864
    // unmark levels
    solver2_clear_marks( s );

865 866 867 868 869
    // update size of learnt + statistics
    veci_resize(learnt,j);
    s->stats.tot_literals += j;

    // clear tags
870
    solver2_clear_tags(s,0);
871 872 873

#ifdef DEBUG
    for (i = 0; i < s->size; i++)
874
        assert(!var_tag(s, i));
875 876 877
#endif

#ifdef VERBOSEDEBUG
878 879
    Abc_Print(1,L_IND"Learnt {", L_ind);
    for (i = 0; i < veci_size(learnt); i++) Abc_Print(1," "L_LIT, L_lit(lits[i]));
880 881 882
#endif
    if (veci_size(learnt) > 1){
        lit tmp;
883 884
        int max_i = 1;
        int max   = var_level(s, lit_var(lits[1]));
885
        for (i = 2; i < veci_size(learnt); i++)
886 887
            if (max < var_level(s, lit_var(lits[i]))) {
                max = var_level(s, lit_var(lits[i]));
888 889 890 891 892 893 894 895 896
                max_i = i;
            }

        tmp         = lits[1];
        lits[1]     = lits[max_i];
        lits[max_i] = tmp;
    }
#ifdef VERBOSEDEBUG
    {
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
}

904
clause* solver2_propagate(sat_solver2* s)
905
{
906
    clause* c, * confl  = NULL;
907 908 909
    veci* ws;
    lit* lits, false_lit, p, * stop, * k;
    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 917
        begin = (cla*)veci_begin(ws);
        end   = begin + veci_size(ws);
918 919 920

        s->stats.propagations++;
        for (i = j = begin; i < end; ){
921
            c = clause2_read(s,*i);
922
            lits = c->lits;
923 924 925 926 927 928 929 930 931 932 933 934 935 936

            // Make sure the false literal is data[1]:
            false_lit = lit_neg(p);
            if (lits[0] == false_lit){
                lits[0] = lits[1];
                lits[1] = false_lit;
            }
            assert(lits[1] == false_lit);

            // If 0th watch is true, then clause is already satisfied.
            if (var_value(s, lit_var(lits[0])) == lit_sign(lits[0]))
                *j++ = *i;
            else{
                // Look for new watch:
937
                stop = lits + c->size;
938 939 940 941 942 943
                for (k = lits + 2; k < stop; k++){
                    if (var_value(s, lit_var(*k)) != !lit_sign(*k)){
                        lits[1] = *k;
                        *k = false_lit;
                        veci_push(solver2_wlist(s,lit_neg(lits[1])),*i);
                        goto WatchFound; }
944
                }
945

946
                // Did not find watch -- clause is unit under assignment:
947
                Lit = lits[0];
948 949
                if ( s->fProofLogging && solver2_dlevel(s) == 0 )
                {
950
                    int k, x, proof_id, Cid, Var = lit_var(Lit);
951
                    int fLitIsFalse = (var_value(s, Var) == !lit_sign(Lit));
952 953
                    // Log production of top-level unit clause:
                    proof_chain_start( s, c );
954
                    clause_foreach_var( c, x, k, 1 ){
955 956 957 958 959
                        assert( var_level(s, x) == 0 );
                        proof_chain_resolve( s, NULL, x );
                    }
                    proof_id = proof_chain_stop( s );
                    // 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 963 964 965 966 967
                    // if variable already has unit clause, it must be with the other polarity 
                    // in this case, we should derive the empty clause here
                    if ( var_unit_clause(s, Var) == NULL )
                        var_set_unit_clause(s, Var, Cid);
                    else{
                        // Empty clause derived:
968
                        proof_chain_start( s, clause2_read(s,Cid) );
969 970
                        proof_chain_resolve( s, NULL, Var );
                        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 977

                *j++ = *i;
                // Clause is unit under assignment:
978 979
                if ( c->lrn )
                    c->lbd = sat_clause_compute_lbd(s, c);
980
                if (!solver2_enqueue(s,Lit, *i)){
981
                    confl = clause2_read(s,*i++);
982 983 984 985
                    // Copy the remaining watches:
                    while (i < end)
                        *j++ = *i++;
                }
986
            }
987
WatchFound: i++;
988
        }
989 990
        s->stats.inspects += j - (int*)veci_begin(ws);
        veci_resize(ws,j - (int*)veci_begin(ws));
991 992 993 994 995
    }

    return confl;
}

996 997
int sat_solver2_simplify(sat_solver2* s)
{
998
    assert(solver2_dlevel(s) == 0);
999
    return (solver2_propagate(s) == NULL);
1000
}
1001 1002

static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
1003 1004 1005 1006 1007
{
    double  random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;

    ABC_INT64_T  conflictC       = 0;
    veci    learnt_clause;
1008
    int     proof_id;
1009

1010
    assert(s->root_level == solver2_dlevel(s));
1011 1012

    s->stats.starts++;
1013 1014
//    s->var_decay = (float)(1 / 0.95   );
//    s->cla_decay = (float)(1 / 0.999);
1015 1016 1017
    veci_new(&learnt_clause);

    for (;;){
1018
        clause* confl = solver2_propagate(s);
1019 1020 1021 1022 1023
        if (confl != 0){
            // CONFLICT
            int blevel;

#ifdef VERBOSEDEBUG
1024
            Abc_Print(1,L_IND"**CONFLICT**\n", L_ind);
1025 1026
#endif
            s->stats.conflicts++; conflictC++;
1027 1028
            if (solver2_dlevel(s) <= s->root_level){
                proof_id = solver2_analyze_final(s, confl, 0);
1029 1030
                if ( s->pPrf1 )
                    assert( proof_id > 0 );
1031
                s->hProofLast = proof_id;
1032 1033 1034 1035 1036
                veci_delete(&learnt_clause);
                return l_False;
            }

            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 1043
            // if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0;    
            // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions)
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 1050 1051 1052

        }else{
            // NO CONFLICT
            int next;

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 1056
                s->progress_estimate = solver2_progress(s);
                solver2_canceluntil(s,s->root_level);
1057 1058 1059 1060 1061 1062 1063 1064
                veci_delete(&learnt_clause);
                return l_Undef; }

            if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
//                 (s->nInsLimit  && s->stats.inspects  > s->nInsLimit) )
                 (s->nInsLimit  && s->stats.propagations > s->nInsLimit) )
            {
                // Reached bound on number of conflicts:
1065 1066
                s->progress_estimate = solver2_progress(s);
                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 1076 1077 1078
            // Reduce the set of learnt clauses:
//            if (s->nLearntMax > 0 && s->stats.learnts >= (unsigned)s->nLearntMax)
//                sat_solver2_reducedb(s);

1079 1080 1081 1082 1083 1084 1085
            // New variable decision:
            s->stats.decisions++;
            next = order_select(s,(float)random_var_freq);

            if (next == var_Undef){
                // Model found:
                int i;
1086 1087 1088
                for (i = 0; i < s->size; i++)
                {
                    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 1093 1094 1095
                veci_delete(&learnt_clause);
                return l_True;
            }

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 1104 1105 1106 1107 1108 1109 1110
        }
    }

    return l_Undef; // cannot happen
}

//=================================================================================================
// External solver functions:

sat_solver2* sat_solver2_new(void)
{
1111
    sat_solver2* s = (sat_solver2 *)ABC_CALLOC( char, sizeof(sat_solver2) );
1112

1113
#ifdef USE_FLOAT_ACTIVITY2
1114 1115 1116 1117 1118 1119
    s->var_inc        = 1;
    s->cla_inc        = 1;
    s->var_decay      = (float)(1 / 0.95  );
    s->cla_decay      = (float)(1 / 0.999 );
//    s->cla_decay      = 1;
//    s->var_decay      = 1;
1120
#else
1121 1122
    s->var_inc        = (1 <<  5);
    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 1132
    s->fSkipSimplify  =  1;
    s->fNotUseRandom  =  0;
1133
    s->fVerbose       =  0;
1134

1135 1136 1137 1138 1139
    s->nLearntStart   = LEARNT_MAX_START_DEFAULT;  // starting learned clause limit
    s->nLearntDelta   = LEARNT_MAX_INCRE_DEFAULT;  // delta of learned clause limit
    s->nLearntRatio   = LEARNT_MAX_RATIO_DEFAULT;  // ratio of learned clause limit
    s->nLearntMax     = s->nLearntStart;

1140 1141 1142 1143 1144 1145 1146 1147 1148
    // initialize vectors
    veci_new(&s->order);
    veci_new(&s->trail_lim);
    veci_new(&s->tagged);
    veci_new(&s->stack);
    veci_new(&s->temp_clause);
    veci_new(&s->temp_proof);
    veci_new(&s->conf_final);
    veci_new(&s->mark_levels);
1149
    veci_new(&s->min_lit_order);
1150
    veci_new(&s->min_step_order);
1151 1152 1153
//    veci_new(&s->learnt_live);
    Sat_MemAlloc_( &s->Mem, 14 );
    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 1161 1162 1163 1164 1165
    s->hLearntLast            = -1; // the last learnt clause 
    s->hProofLast             = -1; // the last proof ID
    // initialize rollback
    s->iVarPivot              =  0; // the pivot for variables
    s->iTrailPivot            =  0; // the pivot for trail
    s->hProofPivot            =  1; // the pivot for proof records
1166 1167 1168
    return s;
}

1169

1170 1171 1172 1173 1174
void sat_solver2_setnvars(sat_solver2* s,int n)
{
    int var;

    if (s->cap < n){
1175
        int old_cap = s->cap;
1176 1177 1178
        while (s->cap < n) s->cap = s->cap*2+1;

        s->wlists    = ABC_REALLOC(veci,     s->wlists,   s->cap*2);
1179
        s->vi        = ABC_REALLOC(varinfo2, s->vi,       s->cap);
1180 1181
        s->levels    = ABC_REALLOC(int,      s->levels,   s->cap);
        s->assigns   = ABC_REALLOC(char,     s->assigns,  s->cap);
1182
        s->trail     = ABC_REALLOC(lit,      s->trail,    s->cap);
1183 1184
        s->orderpos  = ABC_REALLOC(int,      s->orderpos, s->cap);
        s->reasons   = ABC_REALLOC(cla,      s->reasons,  s->cap);
1185 1186
        if ( s->fProofLogging )
        s->units     = ABC_REALLOC(cla,      s->units,    s->cap);
1187
#ifdef USE_FLOAT_ACTIVITY2
1188 1189 1190
        s->activity  = ABC_REALLOC(double,   s->activity, s->cap);
#else
        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 1199 1200 1201 1202 1203
        assert(!s->wlists[2*var].size);
        assert(!s->wlists[2*var+1].size);
        if ( s->wlists[2*var].ptr == NULL )
            veci_new(&s->wlists[2*var]);
        if ( s->wlists[2*var+1].ptr == NULL )
            veci_new(&s->wlists[2*var+1]);
1204 1205 1206
        *((int*)s->vi + var) = 0; //s->vi[var].val = varX;
        s->levels  [var] = 0;
        s->assigns [var] = varX;
1207
        s->reasons [var] = 0;
1208
        if ( s->fProofLogging )
1209
        s->units   [var] = 0;
1210 1211 1212
#ifdef USE_FLOAT_ACTIVITY2
        s->activity[var] = 0;
#else
1213
        s->activity[var] = (1<<10);
1214
#endif
1215
        s->model   [var] = 0;
1216 1217
        // does not hold because variables enqueued at top level will not be reinserted in the heap
        // assert(veci_size(&s->order) == var); 
1218
        s->orderpos[var] = veci_size(&s->order);
1219 1220 1221 1222 1223
        veci_push(&s->order,var);
        order_update(s, var);
    }
    s->size = n > s->size ? n : s->size;
}
1224 1225 1226

void sat_solver2_delete(sat_solver2* s)
{
1227 1228 1229
    int fVerify = 0;
    if ( fVerify )
    {
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 1235
//        if ( s->fProofLogging )
//            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 1242 1243 1244 1245 1246
    // delete vectors
    veci_delete(&s->order);
    veci_delete(&s->trail_lim);
    veci_delete(&s->tagged);
    veci_delete(&s->stack);
    veci_delete(&s->temp_clause);
1247
    veci_delete(&s->temp_proof);
1248
    veci_delete(&s->conf_final);
1249 1250 1251
    veci_delete(&s->mark_levels);
    veci_delete(&s->min_lit_order);
    veci_delete(&s->min_step_order);
1252 1253
//    veci_delete(&s->learnt_live);
    veci_delete(&s->act_clas);
1254
    veci_delete(&s->claProofs);
1255 1256 1257
//    veci_delete(&s->clauses);
//    veci_delete(&s->lrns);
    Sat_MemFree_( &s->Mem );
1258
//    veci_delete(&s->proofs);
1259 1260
    Vec_SetFree( s->pPrf1 );
    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 1272
        ABC_FREE(s->levels   );
        ABC_FREE(s->assigns  );
1273
        ABC_FREE(s->trail    );
1274 1275
        ABC_FREE(s->orderpos );
        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
}


1287
int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end, int Id)
1288
{
1289 1290 1291 1292 1293
    cla Cid;
    lit *i,*j,*iFree = NULL;
    int maxvar, count, temp;
    assert( solver2_dlevel(s) == 0 );
    assert( begin < end );
1294
    assert( Id != 0 );
1295 1296

    // copy clause into storage
1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313
    veci_resize( &s->temp_clause, 0 );
    for ( i = begin; i < end; i++ )
        veci_push( &s->temp_clause, *i );
    begin = veci_begin( &s->temp_clause );
    end = begin + veci_size( &s->temp_clause );

    // insertion sort
    maxvar = lit_var(*begin);
    for (i = begin + 1; i < end; i++){
        lit l = *i;
        maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
        for (j = i; j > begin && *(j-1) > l; j--)
            *j = *(j-1);
        *j = l;
    }
    sat_solver2_setnvars(s,maxvar+1);

1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325

    // delete duplicates
    for (i = j = begin + 1; i < end; i++)
    {
        if ( *(i-1) == lit_neg(*i) ) // tautology
            return clause2_create_new( s, begin, end, 0, 0 ); // add it anyway, to preserve proper clause count       
        if ( *(i-1) != *i )
            *j++ = *i;
    }
    end = j;
    assert( begin < end );

1326 1327 1328
    // coount the number of 0-literals
    count = 0;
    for ( i = begin; i < end; i++ )
1329
    {
1330 1331 1332 1333
        // make sure all literals are unique
        assert( i == begin || lit_var(*(i-1)) != lit_var(*i) );
        // consider the value of this literal
        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 1336 1337 1338
        if ( var_value(s, lit_var(*i)) == varX ) // unassigned literal
            iFree = i;
        else
            count++; // literal is 0
1339
    }
1340
    assert( count < end-begin ); // the clause cannot be UNSAT
1341

1342 1343 1344 1345
    // swap variables to make sure the clause is watched using unassigned variable
    temp   = *iFree;
    *iFree = *begin;
    *begin = temp;
1346 1347

    // create a new clause
1348
    Cid = clause2_create_new( s, begin, end, 0, 0 );
1349 1350
    if ( Id )
        clause2_set_id( s, Cid, Id );
1351

1352
    // handle unit clause
1353
    if ( count+1 == end-begin )
1354 1355
    {
        if ( s->fProofLogging )
1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366
        {
            if ( count == 0 ) // original learned clause
            {
                var_set_unit_clause( s, lit_var(begin[0]), Cid );
                if ( !solver2_enqueue(s,begin[0],0) )
                    assert( 0 );
            }
            else
            {
                // Log production of top-level unit clause:
                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 1371 1372
                    proof_chain_resolve( s, NULL, x );
                proof_id = proof_chain_stop( s );
                // generate a new clause
1373
                CidNew = clause2_create_new( s, begin, begin+1, 1, proof_id );
1374 1375 1376 1377 1378
                var_set_unit_clause( s, lit_var(begin[0]), CidNew );
                if ( !solver2_enqueue(s,begin[0],Cid) )
                    assert( 0 );
            }
        }
1379
    }
1380
    return Cid;
1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 1393
}


double luby2(double y, int x)
{
    int size, seq;
    for (size = 1, seq = 0; size < x+1; seq++, size = 2*size + 1);
    while (size-1 != x){
        size = (size-1) >> 1;
        seq--;
        x = x % size;
    }
    return pow(y, (double)seq);
1394
}
1395 1396 1397 1398 1399

void luby2_test()
{
    int i;
    for ( i = 0; i < 20; i++ )
1400 1401 1402
        Abc_Print(1, "%d ", (int)luby2(2,i) );
    Abc_Print(1, "\n" );
}
1403

1404 1405

// updates clauses, watches, units, and proof
1406
void sat_solver2_reducedb(sat_solver2* s)
1407
{
1408
    static abctime TimeTotal = 0;
1409
    Sat_Mem_t * pMem = &s->Mem;
Alan Mishchenko committed
1410
    clause * c = NULL;
1411 1412 1413
    int nLearnedOld = veci_size(&s->act_clas);
    int * act_clas = veci_begin(&s->act_clas);
    int * pPerm, * pSortValues, nCutoffValue, * pClaProofs;
Alan Mishchenko committed
1414
    int i, j, k, Id, nSelected;//, LastSize = 0;
1415
    int Counter, CounterStart;
1416
    abctime clk = Abc_Clock();
1417 1418 1419 1420 1421
    static int Count = 0;
    Count++;
    assert( s->nLearntMax );
    s->nDBreduces++;
//    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 1427 1428
    // preserve 1/10 of last clauses
    CounterStart  = s->stats.learnts - (s->nLearntMax / 10);
    // preserve 1/10 of most active clauses
1429 1430 1431 1432 1433 1434 1435 1436 1437 1438 1439 1440 1441 1442 1443 1444 1445 1446 1447 1448 1449 1450 1451 1452 1453 1454 1455 1456
    pSortValues = veci_begin(&s->act_clas);
    pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld );
    assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] );
    nCutoffValue = pSortValues[pPerm[nLearnedOld*9/10]];
    ABC_FREE( pPerm );
//    nCutoffValue = ABC_INFINITY;
*/


    // find the new limit
    s->nLearntMax = s->nLearntStart + s->nLearntDelta * s->nDBreduces;
    // preserve 1/20 of last clauses
    CounterStart  = nLearnedOld - (s->nLearntMax / 20);
    // preserve 3/4 of most active clauses
    nSelected = nLearnedOld*s->nLearntRatio/100;
    // create sorting values
    pSortValues = ABC_ALLOC( int, nLearnedOld );
    Sat_MemForEachLearned( pMem, c, i, k )
    {
        Id = clause_id(c);
        pSortValues[Id] = (((7 - Abc_MinInt(c->lbd, 7)) << 28) | (act_clas[Id] >> 4));
//        pSortValues[Id] = act_clas[Id];
        assert( pSortValues[Id] >= 0 );
    }
    // find non-decreasing permutation
    pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld );
    assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] );
    nCutoffValue = pSortValues[pPerm[nLearnedOld-nSelected]];
1457
    ABC_FREE( pPerm );
1458
//    nCutoffValue = ABC_INFINITY;
1459

1460 1461 1462
    // count how many clauses satisfy the condition
    Counter = j = 0;
    Sat_MemForEachLearned( pMem, c, i, k )
1463
    {
1464 1465 1466 1467
        assert( c->mark == 0 );
        if ( Counter++ > CounterStart || clause_size(c) < 2 || pSortValues[clause_id(c)] >= nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) )
        {
        }
1468
        else
1469 1470 1471
            j++;
        if ( j >= nLearnedOld / 6 )
            break;
1472
    }
1473
    if ( j < nLearnedOld / 6 )
1474 1475
    {
        ABC_FREE( pSortValues );
1476
        return;
1477
    }
1478 1479 1480

    // mark learned clauses to remove
    Counter = j = 0;
1481
    pClaProofs = veci_size(&s->claProofs) ? veci_begin(&s->claProofs) : NULL;
1482
    Sat_MemForEachLearned( pMem, c, i, k )
1483
    {
1484 1485 1486 1487 1488
        assert( c->mark == 0 );
        if ( Counter++ > CounterStart || clause_size(c) < 2 || pSortValues[clause_id(c)] >= nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) )
        {
            pSortValues[j] = pSortValues[clause_id(c)];
            if ( pClaProofs ) 
1489 1490 1491
                pClaProofs[j] = pClaProofs[clause_id(c)];
            if ( s->pPrf2 )
                Prf_ManAddSaved( s->pPrf2, clause_id(c), j );
1492 1493 1494 1495 1496 1497 1498 1499
            j++;
        }
        else // delete
        {
            c->mark = 1;
            s->stats.learnts_literals -= clause_size(c);
            s->stats.learnts--;
        }
1500
    }
1501
    ABC_FREE( pSortValues );
1502 1503
    if ( s->pPrf2 )
        Prf_ManCompact( s->pPrf2, j );
1504 1505 1506 1507 1508 1509
//    if ( j == nLearnedOld )
//        return;

    assert( s->stats.learnts == (unsigned)j );
    assert( Counter == nLearnedOld );
    veci_resize(&s->act_clas,j);
1510
    if ( veci_size(&s->claProofs) )
1511 1512 1513 1514 1515
        veci_resize(&s->claProofs,j);

    // update ID of each clause to be its new handle
    Counter = Sat_MemCompactLearned( pMem, 0 );
    assert( Counter == (int)s->stats.learnts );
1516

1517
    // update reasons
1518
    for ( i = 0; i < s->size; i++ )
1519 1520 1521 1522 1523 1524 1525
    {
        if ( !s->reasons[i] ) // no reason
            continue;
        if ( clause_is_lit(s->reasons[i]) ) // 2-lit clause
            continue;
        if ( !clause_learnt_h(pMem, s->reasons[i]) ) // problem clause
            continue;
1526
        assert( c->lrn );
1527 1528 1529 1530
        c = clause2_read( s, s->reasons[i] );
        assert( c->mark == 0 );
        s->reasons[i] = clause_id(c); // updating handle here!!!
    }
1531

1532
    // update watches
1533 1534
    for ( i = 0; i < s->size*2; i++ )
    {
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 1541 1542 1543
            else if ( !clause_learnt_h(pMem, pArray[k]) ) // problem clause
                pArray[j++] = pArray[k];
            else 
            {
1544
                assert( c->lrn );
1545 1546 1547 1548 1549
                c = clause2_read(s, pArray[k]);
                if ( !c->mark ) // useful learned clause
                   pArray[j++] = clause_id(c); // updating handle here!!!
            }
        }
1550 1551
        veci_resize(&s->wlists[i],j);
    }
1552

1553
    // compact units
1554
    if ( s->fProofLogging )
1555 1556 1557
        for ( i = 0; i < s->size; i++ )
            if ( s->units[i] && clause_learnt_h(pMem, s->units[i]) )
            {
1558
                assert( c->lrn );
1559 1560 1561 1562 1563 1564 1565 1566
                c = clause2_read( s, s->units[i] );
                assert( c->mark == 0 );
                s->units[i] = clause_id(c);
            }

    // perform final move of the clauses
    Counter = Sat_MemCompactLearned( pMem, 1 );
    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 1580 1581 1582
    {
        Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%)  ",
            s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld );
        Abc_PrintTime( 1, "Time", TimeTotal );
    }
1583 1584
}

1585 1586 1587
// reverses to the previously bookmarked point
void sat_solver2_rollback( sat_solver2* s )
{
1588
    Sat_Mem_t * pMem = &s->Mem;
1589
    int i, k, j;
1590 1591
    static int Count = 0;
    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 1598
    // update order 
    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 1607 1608 1609 1610 1611 1612 1613
        for ( i = 0; i < s->iVarPivot; i++ )
        {
            if ( var_value(s, i) != varX )
                continue;
            s->orderpos[i] = veci_size(&s->order);
            veci_push(&s->order,i);
            order_update(s, i);
        }
1614 1615
    }
    // compact watches
1616
    for ( i = 0; i < s->iVarPivot*2; i++ )
1617
    {
1618 1619 1620 1621 1622
        cla* pArray = veci_begin(&s->wlists[i]);
        for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
            if ( Sat_MemClauseUsed(pMem, pArray[k]) )
                pArray[j++] = pArray[k];
        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 1629 1630 1631 1632 1633 1634 1635
    // reset clause counts
    s->stats.clauses = pMem->BookMarkE[0];
    s->stats.learnts = pMem->BookMarkE[1];
    // rollback clauses
    Sat_MemRollBack( pMem );

    // resize learned arrays
    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 1641
        // some weird bug here, which shows only on 64-bits!
        // temporarily, perform more general proof reduction
1642
//        Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot );
1643
    }
1644 1645 1646
    assert( s->pPrf2 == NULL );
//    if ( s->pPrf2 )
//        Prf_ManShrink( s->pPrf2, s->stats.learnts );
1647

1648
    // initialize other vars
1649
    s->size = s->iVarPivot;
1650 1651 1652 1653 1654 1655
    if ( s->size == 0 )
    {
    //    s->size                   = 0;
    //    s->cap                    = 0;
        s->qhead                  = 0;
        s->qtail                  = 0;
1656
#ifdef USE_FLOAT_ACTIVITY2
1657 1658 1659 1660 1661 1662 1663 1664 1665 1666 1667 1668 1669 1670 1671 1672 1673 1674 1675 1676 1677 1678 1679
        s->var_inc                = 1;
        s->cla_inc                = 1;
        s->var_decay              = (float)(1 / 0.95  );
        s->cla_decay              = (float)(1 / 0.999 );
#else
        s->var_inc                = (1 <<  5);
        s->cla_inc                = (1 << 11);
#endif
        s->root_level             = 0;
        s->random_seed            = 91648253;
        s->progress_estimate      = 0;
        s->verbosity              = 0;

        s->stats.starts           = 0;
        s->stats.decisions        = 0;
        s->stats.propagations     = 0;
        s->stats.inspects         = 0;
        s->stats.conflicts        = 0;
        s->stats.clauses          = 0;
        s->stats.clauses_literals = 0;
        s->stats.learnts          = 0;
        s->stats.learnts_literals = 0;
        s->stats.tot_literals     = 0;
1680
        // initialize clause pointers
1681 1682 1683 1684 1685 1686 1687
        s->hLearntLast            = -1; // the last learnt clause 
        s->hProofLast             = -1; // the last proof ID

        // initialize rollback
        s->iVarPivot              =  0; // the pivot for variables
        s->iTrailPivot            =  0; // the pivot for trail
        s->hProofPivot            =  1; // the pivot for proof records
1688 1689 1690
    }
}

1691
// returns memory in bytes used by the SAT solver
1692
double sat_solver2_memory( sat_solver2* s, int fAll )
1693 1694 1695
{
    int i;
    double Mem = sizeof(sat_solver2);
1696 1697 1698
    if ( fAll )
        for (i = 0; i < s->cap*2; i++)
            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 1702 1703 1704 1705 1706
    Mem += s->claProofs.cap * sizeof(int);
//    Mem += s->cap * sizeof(char);     // ABC_FREE(s->polarity );
//    Mem += s->cap * sizeof(char);     // ABC_FREE(s->tags     );
    Mem += s->cap * sizeof(varinfo2); // ABC_FREE(s->vi       );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->levels   );
    Mem += s->cap * sizeof(char);     // ABC_FREE(s->assigns  );
1707
#ifdef USE_FLOAT_ACTIVITY2
1708 1709 1710
    Mem += s->cap * sizeof(double);   // ABC_FREE(s->activity );
#else
    Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity );
1711 1712
    if ( s->activity2 )
    Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity2);
1713 1714 1715 1716 1717 1718 1719 1720 1721 1722 1723 1724 1725 1726 1727 1728
#endif
    Mem += s->cap * sizeof(lit);      // ABC_FREE(s->trail    );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->orderpos );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->reasons  );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->units    );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->model    );
    Mem += s->tagged.cap * sizeof(int);
    Mem += s->stack.cap * sizeof(int);
    Mem += s->order.cap * sizeof(int);
    Mem += s->trail_lim.cap * sizeof(int);
    Mem += s->temp_clause.cap * sizeof(int);
    Mem += s->conf_final.cap * sizeof(int);
    Mem += s->mark_levels.cap * sizeof(int);
    Mem += s->min_lit_order.cap * sizeof(int);
    Mem += s->min_step_order.cap * sizeof(int);
    Mem += s->temp_proof.cap * sizeof(int);
1729
    Mem += Sat_MemMemoryAll( &s->Mem );
1730
//    Mem += Vec_ReportMemory( s->pPrf1 );
1731 1732 1733 1734
    return Mem;
}
double sat_solver2_memory_proof( sat_solver2* s )
{
1735 1736 1737 1738
    double Mem = s->dPrfMemory;
    if ( s->pPrf1 )
        Mem += Vec_ReportMemory( s->pPrf1 );
    return Mem;
1739 1740 1741
}


1742
// find the clause in the watcher lists
1743
/*
1744 1745 1746 1747 1748 1749 1750 1751 1752 1753 1754 1755
int sat_solver2_find_clause( sat_solver2* s, int Hand, int fVerbose )
{
    int i, k, Found = 0;
    if ( Hand >= s->clauses.size )
        return 1;
    for ( i = 0; i < s->size*2; i++ )
    {
        cla* pArray = veci_begin(&s->wlists[i]);
        for ( k = 0; k < veci_size(&s->wlists[i]); k++ )
            if ( (pArray[k] >> 1) == Hand )
            {
                if ( fVerbose )
1756
                Abc_Print(1, "Clause found in list %d at position %d.\n", i, k );
1757 1758 1759 1760 1761 1762 1763
                Found = 1;
                break;
            }
    }
    if ( Found == 0 )
    {
        if ( fVerbose )
1764
        Abc_Print(1, "Clause with handle %d is not found.\n", Hand );
1765 1766 1767
    }
    return Found;
}
1768 1769
*/
/*
1770
// verify that all problem clauses are satisfied
1771 1772
void sat_solver2_verify( sat_solver2* s )
{
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 1780
            v = lit_var(c->lits[k]);
            if ( sat_solver2_var_value(s, v) ^ lit_sign(c->lits[k]) )
1781 1782
                break;
        }
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 1789 1790
            Counter++;
        }
    }
1791
    if ( Counter != 0 )
1792
        Abc_Print(1, "Verification failed!\n" );
1793
//    else
1794
//        Abc_Print(1, "Verification passed.\n" );
1795
}
1796
*/
1797

1798 1799 1800 1801 1802 1803 1804 1805 1806 1807 1808 1809 1810 1811 1812 1813 1814 1815 1816 1817 1818 1819 1820 1821 1822 1823 1824 1825 1826 1827 1828 1829 1830 1831 1832 1833 1834
// checks how many watched clauses are satisfied by 0-level assignments
// (this procedure may be called before setting up a new bookmark for rollback)
int sat_solver2_check_watched( sat_solver2* s )
{
    clause * c;
    int i, k, j, m;
    int claSat[2] = {0};
    // update watches
    for ( i = 0; i < s->size*2; i++ )
    {
        int * pArray = veci_begin(&s->wlists[i]);
        for ( m = k = 0; k < veci_size(&s->wlists[i]); k++ )
        {
            c = clause2_read(s, pArray[k]);
            for ( j = 0; j < (int)c->size; j++ )
                if ( var_value(s, lit_var(c->lits[j])) == lit_sign(c->lits[j]) ) // true lit
                    break;
            if ( j == (int)c->size )
            {
                pArray[m++] = pArray[k];
                continue;
            }
            claSat[c->lrn]++;
        }
        veci_resize(&s->wlists[i],m);
        if ( m == 0 )
        {
//            s->wlists[i].cap = 0;
//            s->wlists[i].size = 0;
//            ABC_FREE( s->wlists[i].ptr );
        }
    }
//    printf( "\nClauses = %d  (Sat = %d).  Learned = %d  (Sat = %d).\n",
//        s->stats.clauses, claSat[0], s->stats.learnts, claSat[1] );
    return 0;
}

1835 1836 1837 1838
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)
{
    int restart_iter = 0;
    ABC_INT64_T  nof_conflicts;
1839 1840 1841
    lbool status = l_Undef;
    int proof_id;
    lit * i;
1842

1843
    s->hLearntLast = -1;
1844
    s->hProofLast = -1;
1845

1846 1847 1848 1849 1850 1851 1852 1853 1854 1855 1856 1857 1858 1859 1860 1861 1862 1863 1864 1865 1866
    // set the external limits
//    s->nCalls++;
//    s->nRestarts  = 0;
    s->nConfLimit = 0;
    s->nInsLimit  = 0;
    if ( nConfLimit )
        s->nConfLimit = s->stats.conflicts + nConfLimit;
    if ( nInsLimit )
//        s->nInsLimit = s->stats.inspects + nInsLimit;
        s->nInsLimit = s->stats.propagations + nInsLimit;
    if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) )
        s->nConfLimit = nConfLimitGlobal;
    if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
        s->nInsLimit = nInsLimitGlobal;

/*
    // Perform assumptions:
    root_level = assumps.size();
    for (int i = 0; i < assumps.size(); i++){
        Lit p = assumps[i];
        assert(var(p) < nVars());
1867
        if (!solver2_assume(p)){
1868
            GClause r = reason[var(p)];
1869
            if (r != Gclause2_NULL){
1870
                clause* confl;
1871 1872 1873 1874 1875 1876 1877 1878 1879 1880 1881 1882 1883
                if (r.isLit()){
                    confl = propagate_tmpbin;
                    (*confl)[1] = ~p;
                    (*confl)[0] = r.lit();
                }else
                    confl = r.clause();
                analyzeFinal(confl, true);
                conflict.push(~p);
            }else
                conflict.clear(),
                conflict.push(~p);
            cancelUntil(0);
            return false; }
1884
        clause* confl = propagate();
1885 1886 1887 1888 1889 1890 1891 1892 1893 1894 1895 1896 1897 1898 1899
        if (confl != NULL){
            analyzeFinal(confl), assert(conflict.size() > 0);
            cancelUntil(0);
            return false; }
    }
    assert(root_level == decisionLevel());
*/

    // Perform assumptions:
    s->root_level = end - begin;
    for ( i = begin; i < end; i++ )
    {
        lit p = *i;
        assert(lit_var(p) < s->size);
        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 1904
            if (r != NULL)
            {
1905
                clause* confl = r;
1906
                proof_id = solver2_analyze_final(s, confl, 1);
1907 1908 1909 1910
                veci_push(&s->conf_final, lit_neg(p));
            }
            else
            {
Alan Mishchenko committed
1911 1912 1913 1914
//                assert( 0 );
//                r = var_unit_clause( s, lit_var(p) );
//                assert( r != NULL );
//                proof_id = clause2_proofid(s, r, 0);
1915
                proof_id = -1; // the only case when ProofId is not assigned (conflicting assumptions)
1916 1917
                veci_resize(&s->conf_final,0);
                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 1927
        }
        else
        {
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 1942 1943 1944
        Abc_Print(1,"==================================[MINISAT]===================================\n");
        Abc_Print(1,"| Conflicts |     ORIGINAL     |              LEARNT              | Progress |\n");
        Abc_Print(1,"|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |\n");
        Abc_Print(1,"==============================================================================\n");
1945 1946 1947 1948 1949
    }

    while (status == l_Undef){
        if (s->verbosity >= 1)
        {
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 1955
                (double)s->nLearntMax,
                (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 1959 1960
                s->progress_estimate*100);
            fflush(stdout);
        }
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 1970 1971 1972 1973 1974 1975
        // quit the loop if reached an external limit
        if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
            break;
        if ( s->nInsLimit  && s->stats.propagations > s->nInsLimit )
            break;
    }
    if (s->verbosity >= 1)
1976
        Abc_Print(1,"==============================================================================\n");
1977

1978
    solver2_canceluntil(s,0);
1979
//    assert( s->qhead == s->qtail );
1980 1981
//    if ( status == l_True )
//        sat_solver2_verify( s );
1982 1983 1984
    return status;
}

1985 1986 1987
void * Sat_ProofCore( sat_solver2 * s )
{
    extern void * Proof_DeriveCore( Vec_Set_t * vProof, int hRoot );
1988 1989 1990 1991 1992 1993 1994 1995
    if ( s->pPrf1 )
        return Proof_DeriveCore( s->pPrf1, s->hProofLast );
    if ( s->pPrf2 )
    {
        s->dPrfMemory = Abc_MaxDouble( s->dPrfMemory, Prf_ManMemory(s->pPrf2) );
        return Prf_ManUnsatCore( s->pPrf2 );
    }
    return NULL;
1996
}
1997 1998

ABC_NAMESPACE_IMPL_END