satSolver2.c File Reference

#include <stdio.h>
#include <assert.h>
#include <string.h>
#include <math.h>
#include "satSolver2.h"

Include dependency graph for satSolver2.c:

Go to the source code of this file.

Classes
struct	varinfo2_t

Macros
#define	SAT_USE_PROOF_LOGGING
#define	L_IND   "%-*d"
#define	L_ind   solver2_dlevel(s)*2+2,solver2_dlevel(s)
#define	L_LIT   "%sx%d"
#define	L_lit(p)
#define	clause_foreach_var(p, var, i, start)

Functions
int	var_is_assigned (sat_solver2 *s, int v)
int	var_is_partA (sat_solver2 *s, int v)
void	var_set_partA (sat_solver2 *s, int v, int partA)
clause *	solver2_propagate (sat_solver2 *s)
int	sat_solver2_simplify (sat_solver2 *s)
sat_solver2 *	sat_solver2_new (void)
void	sat_solver2_setnvars (sat_solver2 *s, int n)
void	sat_solver2_delete (sat_solver2 *s)
int	sat_solver2_addclause (sat_solver2 *s, lit *begin, lit *end, int Id)
double	luby2 (double y, int x)
void	luby2_test ()
void	sat_solver2_reducedb (sat_solver2 *s)
void	sat_solver2_rollback (sat_solver2 *s)
double	sat_solver2_memory (sat_solver2 *s, int fAll)
double	sat_solver2_memory_proof (sat_solver2 *s)
int	sat_solver2_check_watched (sat_solver2 *s)
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)
void *	Sat_ProofCore (sat_solver2 *s)

Macro Definition Documentation

clause_foreach_var

#define clause_foreach_var	(		p,
			var,
			i,
			start )

Value:

    for ( i = start; (i < (int)(p)->size) && ((var) = lit_var((p)->lits[i])); i++ )

Definition at line 156 of file satSolver2.c.

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

L_IND

#define L_IND   "%-*d"

Definition at line 39 of file satSolver2.c.

L_ind

#define L_ind   solver2_dlevel(s)*2+2,solver2_dlevel(s)

Definition at line 40 of file satSolver2.c.

L_LIT

#define L_LIT   "%sx%d"

Definition at line 41 of file satSolver2.c.

L_lit

#define L_lit

(

p

)

Value:

lit_sign(p)?"~":"", (lit_var(p))

Definition at line 42 of file satSolver2.c.

SAT_USE_PROOF_LOGGING

#define SAT_USE_PROOF_LOGGING

Definition at line 31 of file satSolver2.c.

Function Documentation

luby2()

double luby2	(	double	y,
		int	x )

Definition at line 1384 of file satSolver2.c.

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

Here is the caller graph for this function:

luby2_test()

void luby2_test

(

)

Definition at line 1396 of file satSolver2.c.

{
    int i;
    for ( i = 0; i < 20; i++ )
        Abc_Print(1, "%d ", (int)luby2(2,i) );
    Abc_Print(1, "\n" );
}

Here is the call graph for this function:

Sat_ProofCore()

void * Sat_ProofCore

(

sat_solver2 *

s

)

Definition at line 1985 of file satSolver2.c.

{
    extern void * Proof_DeriveCore( Vec_Set_t * vProof, int hRoot );
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver2_addclause()

int sat_solver2_addclause	(	sat_solver2 *	s,
		lit *	begin,
		lit *	end,
		int	Id )

Definition at line 1287 of file satSolver2.c.

{
    cla Cid;
    lit *i,*j,*iFree = NULL;
    int maxvar, count, temp;
    assert( solver2_dlevel(s) == 0 );
    assert( begin < end );
    assert( Id != 0 );
 
    // copy clause into storage
    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);
 
 
    // 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 );
 
    // coount the number of 0-literals
    count = 0;
    for ( i = begin; i < end; i++ )
    {
        // 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
            return clause2_create_new( s, begin, end, 0, 0 ); // add it anyway, to preserve proper clause count       
        if ( var_value(s, lit_var(*i)) == varX ) // unassigned literal
            iFree = i;
        else
            count++; // literal is 0
    }
    assert( count < end-begin ); // the clause cannot be UNSAT
 
    // swap variables to make sure the clause is watched using unassigned variable
    temp   = *iFree;
    *iFree = *begin;
    *begin = temp;
 
    // create a new clause
    Cid = clause2_create_new( s, begin, end, 0, 0 );
    if ( Id )
        clause2_set_id( s, Cid, Id );
 
    // handle unit clause
    if ( count+1 == end-begin )
    {
        if ( s->fProofLogging )
        {
            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;
                clause* c = clause2_read(s, Cid);
                proof_chain_start( s, c );
                clause_foreach_var( c, x, k, 1 )
                    proof_chain_resolve( s, NULL, x );
                proof_id = proof_chain_stop( s );
                // generate a new clause
                CidNew = clause2_create_new( s, begin, begin+1, 1, proof_id );
                var_set_unit_clause( s, lit_var(begin[0]), CidNew );
                if ( !solver2_enqueue(s,begin[0],Cid) )
                    assert( 0 );
            }
        }
    }
    return Cid;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver2_check_watched()

int sat_solver2_check_watched

(

sat_solver2 *

s

)

Definition at line 1800 of file satSolver2.c.

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

sat_solver2_delete()

void sat_solver2_delete

(

sat_solver2 *

s

)

Definition at line 1225 of file satSolver2.c.

{
    int fVerify = 0;
    if ( fVerify )
    {
        veci * pCore = (veci *)Sat_ProofCore( s );
//        Abc_Print(1, "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) );
        veci_delete( pCore );
        ABC_FREE( pCore );
//        if ( s->fProofLogging )
//            Sat_ProofCheck( s );
    }
 
    // report statistics
//    Abc_Print(1, "Used %6.2f MB for proof-logging.   Unit clauses = %d.\n", 1.0 * Vec_ReportMemory(&s->Proofs) / (1<<20), s->nUnits );
 
    // delete vectors
    veci_delete(&s->order);
    veci_delete(&s->trail_lim);
    veci_delete(&s->tagged);
    veci_delete(&s->stack);
    veci_delete(&s->temp_clause);
    veci_delete(&s->temp_proof);
    veci_delete(&s->conf_final);
    veci_delete(&s->mark_levels);
    veci_delete(&s->min_lit_order);
    veci_delete(&s->min_step_order);
//    veci_delete(&s->learnt_live);
    veci_delete(&s->act_clas);
    veci_delete(&s->claProofs);
//    veci_delete(&s->clauses);
//    veci_delete(&s->lrns);
    Sat_MemFree_( &s->Mem );
//    veci_delete(&s->proofs);
    Vec_SetFree( s->pPrf1 );
    Prf_ManStop( s->pPrf2 );
    Int2_ManStop( s->pInt2 );
 
    // delete arrays
    if (s->vi != 0){
        int i;
        if ( s->wlists )
            for (i = 0; i < s->cap*2; i++)
                veci_delete(&s->wlists[i]);
        ABC_FREE(s->wlists   );
        ABC_FREE(s->vi       );
        ABC_FREE(s->levels   );
        ABC_FREE(s->assigns  );
        ABC_FREE(s->trail    );
        ABC_FREE(s->orderpos );
        ABC_FREE(s->reasons  );
        ABC_FREE(s->units    );
        ABC_FREE(s->activity );
        ABC_FREE(s->activity2);
        ABC_FREE(s->model    );
    }
    ABC_FREE(s);
 
//    Abc_PrintTime( 1, "Time", Time );
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver2_memory()

double sat_solver2_memory	(	sat_solver2 *	s,
		int	fAll )

Definition at line 1692 of file satSolver2.c.

{
    int i;
    double Mem = sizeof(sat_solver2);
    if ( fAll )
        for (i = 0; i < s->cap*2; i++)
            Mem += s->wlists[i].cap * sizeof(int);
    Mem += s->cap * sizeof(veci);     // ABC_FREE(s->wlists   );
    Mem += s->act_clas.cap * sizeof(int);
    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  );
#ifdef USE_FLOAT_ACTIVITY2
    Mem += s->cap * sizeof(double);   // ABC_FREE(s->activity );
#else
    Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity );
    if ( s->activity2 )
    Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity2);
#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);
    Mem += Sat_MemMemoryAll( &s->Mem );
//    Mem += Vec_ReportMemory( s->pPrf1 );
    return Mem;
}

Here is the caller graph for this function:

sat_solver2_memory_proof()

double sat_solver2_memory_proof

(

sat_solver2 *

s

)

Definition at line 1733 of file satSolver2.c.

{
    double Mem = s->dPrfMemory;
    if ( s->pPrf1 )
        Mem += Vec_ReportMemory( s->pPrf1 );
    return Mem;
}

Here is the caller graph for this function:

sat_solver2_new()

sat_solver2 * sat_solver2_new

(

void

)

Definition at line 1109 of file satSolver2.c.

{
    sat_solver2* s = (sat_solver2 *)ABC_CALLOC( char, sizeof(sat_solver2) );
 
#ifdef USE_FLOAT_ACTIVITY2
    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;
#else
    s->var_inc        = (1 <<  5);
    s->cla_inc        = (1 << 11);
#endif
    s->random_seed    = 91648253;
 
#ifdef SAT_USE_PROOF_LOGGING
    s->fProofLogging  =  1;
#else
    s->fProofLogging  =  0;
#endif
    s->fSkipSimplify  =  1;
    s->fNotUseRandom  =  0;
    s->fVerbose       =  0;
 
    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;
 
    // 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);
    veci_new(&s->min_lit_order);
    veci_new(&s->min_step_order);
//    veci_new(&s->learnt_live);
    Sat_MemAlloc_( &s->Mem, 14 );
    veci_new(&s->act_clas);  
    // proof-logging
    veci_new(&s->claProofs);
//    s->pPrf1 = Vec_SetAlloc( 20 );
    s->tempInter = -1;
 
    // initialize clause pointers
    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
    return s;
}

Here is the caller graph for this function:

sat_solver2_reducedb()

void sat_solver2_reducedb

(

sat_solver2 *

s

)

Definition at line 1406 of file satSolver2.c.

{
    static abctime TimeTotal = 0;
    Sat_Mem_t * pMem = &s->Mem;
    clause * c = NULL;
    int nLearnedOld = veci_size(&s->act_clas);
    int * act_clas = veci_begin(&s->act_clas);
    int * pPerm, * pSortValues, nCutoffValue, * pClaProofs;
    int i, j, k, Id, nSelected;//, LastSize = 0;
    int Counter, CounterStart;
    abctime clk = Abc_Clock();
    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 );
 
/*
    // find the new limit
    s->nLearntMax = s->nLearntMax * 11 / 10;
    // preserve 1/10 of last clauses
    CounterStart  = s->stats.learnts - (s->nLearntMax / 10);
    // preserve 1/10 of most active clauses
    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]];
    ABC_FREE( pPerm );
//    nCutoffValue = ABC_INFINITY;
 
    // count how many clauses satisfy the condition
    Counter = j = 0;
    Sat_MemForEachLearned( pMem, c, i, k )
    {
        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) )
        {
        }
        else
            j++;
        if ( j >= nLearnedOld / 6 )
            break;
    }
    if ( j < nLearnedOld / 6 )
    {
        ABC_FREE( pSortValues );
        return;
    }
 
    // mark learned clauses to remove
    Counter = j = 0;
    pClaProofs = veci_size(&s->claProofs) ? veci_begin(&s->claProofs) : NULL;
    Sat_MemForEachLearned( pMem, c, i, k )
    {
        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 ) 
                pClaProofs[j] = pClaProofs[clause_id(c)];
            if ( s->pPrf2 )
                Prf_ManAddSaved( s->pPrf2, clause_id(c), j );
            j++;
        }
        else // delete
        {
            c->mark = 1;
            s->stats.learnts_literals -= clause_size(c);
            s->stats.learnts--;
        }
    }
    ABC_FREE( pSortValues );
    if ( s->pPrf2 )
        Prf_ManCompact( s->pPrf2, j );
//    if ( j == nLearnedOld )
//        return;
 
    assert( s->stats.learnts == (unsigned)j );
    assert( Counter == nLearnedOld );
    veci_resize(&s->act_clas,j);
    if ( veci_size(&s->claProofs) )
        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 );
 
    // update reasons
    for ( i = 0; i < s->size; i++ )
    {
        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;
        assert( c->lrn );
        c = clause2_read( s, s->reasons[i] );
        assert( c->mark == 0 );
        s->reasons[i] = clause_id(c); // updating handle here!!!
    }
 
    // update watches
    for ( i = 0; i < s->size*2; i++ )
    {
        int * pArray = veci_begin(&s->wlists[i]);
        for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
        {
            if ( clause_is_lit(pArray[k]) ) // 2-lit clause
                pArray[j++] = pArray[k];
            else if ( !clause_learnt_h(pMem, pArray[k]) ) // problem clause
                pArray[j++] = pArray[k];
            else 
            {
                assert( c->lrn );
                c = clause2_read(s, pArray[k]);
                if ( !c->mark ) // useful learned clause
                   pArray[j++] = clause_id(c); // updating handle here!!!
            }
        }
        veci_resize(&s->wlists[i],j);
    }
 
    // compact units
    if ( s->fProofLogging )
        for ( i = 0; i < s->size; i++ )
            if ( s->units[i] && clause_learnt_h(pMem, s->units[i]) )
            {
                assert( c->lrn );
                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 );
 
    // compact proof (compacts 'proofs' and update 'claProofs')
    if ( s->pPrf1 )
    {
        extern int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot );
        s->hProofPivot = Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot );
    }
 
    // report the results
    TimeTotal += Abc_Clock() - clk;
    if ( s->fVerbose )
    {
        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 );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver2_rollback()

void sat_solver2_rollback

(

sat_solver2 *

s

)

Definition at line 1586 of file satSolver2.c.

{
    Sat_Mem_t * pMem = &s->Mem;
    int i, k, j;
    static int Count = 0;
    Count++;
    assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
    assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail );
    assert( s->pPrf1 == NULL || (s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(s->pPrf1)) );
    // reset implication queue
    solver2_canceluntil_rollback( s, s->iTrailPivot );
    // update order 
    if ( s->iVarPivot < s->size )
    { 
        if ( s->activity2 )
        {
            s->var_inc = s->var_inc2;
            memcpy( s->activity, s->activity2, sizeof(unsigned) * s->iVarPivot );
        }
        veci_resize(&s->order, 0);
        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);
        }
    }
    // compact watches
    for ( i = 0; i < s->iVarPivot*2; i++ )
    {
        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);
    }
    // reset watcher lists
    for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
        s->wlists[i].size = 0;
 
    // 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);
    if ( s->pPrf1 ) 
    {
        veci_resize(&s->claProofs, s->stats.learnts);
        Vec_SetShrink(s->pPrf1, s->hProofPivot); 
        // some weird bug here, which shows only on 64-bits!
        // temporarily, perform more general proof reduction
//        Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot );
    }
    assert( s->pPrf2 == NULL );
//    if ( s->pPrf2 )
//        Prf_ManShrink( s->pPrf2, s->stats.learnts );
 
    // initialize other vars
    s->size = s->iVarPivot;
    if ( s->size == 0 )
    {
    //    s->size                   = 0;
    //    s->cap                    = 0;
        s->qhead                  = 0;
        s->qtail                  = 0;
#ifdef USE_FLOAT_ACTIVITY2
        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;
        // initialize clause pointers
        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
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver2_setnvars()

void sat_solver2_setnvars	(	sat_solver2 *	s,
		int	n )

Definition at line 1170 of file satSolver2.c.

{
    int var;
 
    if (s->cap < n){
        int old_cap = s->cap;
        while (s->cap < n) s->cap = s->cap*2+1;
 
        s->wlists    = ABC_REALLOC(veci,     s->wlists,   s->cap*2);
        s->vi        = ABC_REALLOC(varinfo2, s->vi,       s->cap);
        s->levels    = ABC_REALLOC(int,      s->levels,   s->cap);
        s->assigns   = ABC_REALLOC(char,     s->assigns,  s->cap);
        s->trail     = ABC_REALLOC(lit,      s->trail,    s->cap);
        s->orderpos  = ABC_REALLOC(int,      s->orderpos, s->cap);
        s->reasons   = ABC_REALLOC(cla,      s->reasons,  s->cap);
        if ( s->fProofLogging )
        s->units     = ABC_REALLOC(cla,      s->units,    s->cap);
#ifdef USE_FLOAT_ACTIVITY2
        s->activity  = ABC_REALLOC(double,   s->activity, s->cap);
#else
        s->activity  = ABC_REALLOC(unsigned, s->activity, s->cap);
        s->activity2 = ABC_REALLOC(unsigned, s->activity2,s->cap);
#endif
        s->model     = ABC_REALLOC(int,      s->model,    s->cap);
        memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) );
    }
 
    for (var = s->size; var < n; var++){
        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]);
        *((int*)s->vi + var) = 0; //s->vi[var].val = varX;
        s->levels  [var] = 0;
        s->assigns [var] = varX;
        s->reasons [var] = 0;
        if ( s->fProofLogging )
        s->units   [var] = 0;
#ifdef USE_FLOAT_ACTIVITY2
        s->activity[var] = 0;
#else
        s->activity[var] = (1<<10);
#endif
        s->model   [var] = 0;
        // does not hold because variables enqueued at top level will not be reinserted in the heap
        // assert(veci_size(&s->order) == var); 
        s->orderpos[var] = veci_size(&s->order);
        veci_push(&s->order,var);
        order_update(s, var);
    }
    s->size = n > s->size ? n : s->size;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver2_simplify()

int sat_solver2_simplify

(

sat_solver2 *

s

)

Definition at line 996 of file satSolver2.c.

{
    assert(solver2_dlevel(s) == 0);
    return (solver2_propagate(s) == NULL);
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver2_solve()

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 )

Definition at line 1835 of file satSolver2.c.

{
    int restart_iter = 0;
    ABC_INT64_T  nof_conflicts;
    lbool status = l_Undef;
    int proof_id;
    lit * i;
 
    s->hLearntLast = -1;
    s->hProofLast = -1;
 
    // 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());
        if (!solver2_assume(p)){
            GClause r = reason[var(p)];
            if (r != Gclause2_NULL){
                clause* confl;
                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; }
        clause* confl = propagate();
        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);
        if (!solver2_enqueue(s,p,0))
        {
            clause* r = clause2_read(s, lit_reason(s,p));
            if (r != NULL)
            {
                clause* confl = r;
                proof_id = solver2_analyze_final(s, confl, 1);
                veci_push(&s->conf_final, lit_neg(p));
            }
            else
            {
//                assert( 0 );
//                r = var_unit_clause( s, lit_var(p) );
//                assert( r != NULL );
//                proof_id = clause2_proofid(s, r, 0);
                proof_id = -1; // the only case when ProofId is not assigned (conflicting assumptions)
                veci_resize(&s->conf_final,0);
                veci_push(&s->conf_final, lit_neg(p));
                // the two lines below are a bug fix by Siert Wieringa 
                if (var_level(s, lit_var(p)) > 0)
                    veci_push(&s->conf_final, p);
            }
            s->hProofLast = proof_id;
            solver2_canceluntil(s, 0);
            return l_False;
        }
        else
        {
            clause* confl = solver2_propagate(s);
            if (confl != NULL){
                proof_id = solver2_analyze_final(s, confl, 0);
                assert(s->conf_final.size > 0);
                s->hProofLast = proof_id;
                solver2_canceluntil(s, 0);
                return l_False;
            }
        }
    }
    assert(s->root_level == solver2_dlevel(s));
 
    if (s->verbosity >= 1){
        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");
    }
 
    while (status == l_Undef){
        if (s->verbosity >= 1)
        {
            Abc_Print(1,"| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n",
                (double)s->stats.conflicts,
                (double)s->stats.clauses,
                (double)s->stats.clauses_literals,
                (double)s->nLearntMax,
                (double)s->stats.learnts,
                (double)s->stats.learnts_literals,
                (s->stats.learnts == 0)? 0.0 : (double)s->stats.learnts_literals / s->stats.learnts,
                s->progress_estimate*100);
            fflush(stdout);
        }
        if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
            break;
        // reduce the set of learnt clauses
        if ( s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax && s->pPrf2 == NULL )
            sat_solver2_reducedb(s);
        // perform next run
        nof_conflicts = (ABC_INT64_T)( 100 * luby2(2, restart_iter++) );
        status = solver2_search(s, nof_conflicts);
        // 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)
        Abc_Print(1,"==============================================================================\n");
 
    solver2_canceluntil(s,0);
//    assert( s->qhead == s->qtail );
//    if ( status == l_True )
//        sat_solver2_verify( s );
    return status;
}

Here is the call graph for this function:

Here is the caller graph for this function:

solver2_propagate()

clause * solver2_propagate

(

sat_solver2 *

s

)

Definition at line 904 of file satSolver2.c.

{
    clause* c, * confl  = NULL;
    veci* ws;
    lit* lits, false_lit, p, * stop, * k;
    cla* begin,* end, *i, *j;
    int Lit;
 
    while (confl == 0 && s->qtail - s->qhead > 0){
 
        p  = s->trail[s->qhead++];
        ws = solver2_wlist(s,p);
        begin = (cla*)veci_begin(ws);
        end   = begin + veci_size(ws);
 
        s->stats.propagations++;
        for (i = j = begin; i < end; ){
            c = clause2_read(s,*i);
            lits = c->lits;
 
            // 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:
                stop = lits + c->size;
                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; }
                }
 
                // Did not find watch -- clause is unit under assignment:
                Lit = lits[0];
                if ( s->fProofLogging && solver2_dlevel(s) == 0 )
                {
                    int k, x, proof_id, Cid, Var = lit_var(Lit);
                    int fLitIsFalse = (var_value(s, Var) == !lit_sign(Lit));
                    // Log production of top-level unit clause:
                    proof_chain_start( s, c );
                    clause_foreach_var( c, x, k, 1 ){
                        assert( var_level(s, x) == 0 );
                        proof_chain_resolve( s, NULL, x );
                    }
                    proof_id = proof_chain_stop( s );
                    // get a new clause
                    Cid = clause2_create_new( s, &Lit, &Lit + 1, 1, proof_id );
                    assert( (var_unit_clause(s, Var) == NULL) != fLitIsFalse );
                    // 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:
                        proof_chain_start( s, clause2_read(s,Cid) );
                        proof_chain_resolve( s, NULL, Var );
                        proof_id = proof_chain_stop( s );
                        s->hProofLast = proof_id;
//                        clause2_create_new( s, &Lit, &Lit, 1, proof_id );
                    }
                }
 
                *j++ = *i;
                // Clause is unit under assignment:
                if ( c->lrn )
                    c->lbd = sat_clause_compute_lbd(s, c);
                if (!solver2_enqueue(s,Lit, *i)){
                    confl = clause2_read(s,*i++);
                    // Copy the remaining watches:
                    while (i < end)
                        *j++ = *i++;
                }
            }
WatchFound: i++;
        }
        s->stats.inspects += j - (int*)veci_begin(ws);
        veci_resize(ws,j - (int*)veci_begin(ws));
    }
 
    return confl;
}

Here is the caller graph for this function:

var_is_assigned()

int var_is_assigned	(	sat_solver2 *	s,
		int	v )

Definition at line 83 of file satSolver2.c.

{ return s->assigns[v] != varX; }

Here is the caller graph for this function:

var_is_partA()

int var_is_partA	(	sat_solver2 *	s,
		int	v )

Definition at line 84 of file satSolver2.c.

{ return s->vi[v].partA;        }

var_set_partA()

void var_set_partA	(	sat_solver2 *	s,
		int	v,
		int	partA )

Definition at line 85 of file satSolver2.c.

{ s->vi[v].partA = partA;       }

Here is the caller graph for this function: