satSolver.c File Reference

#include <stdio.h>
#include <assert.h>
#include <string.h>
#include <math.h>
#include "satSolver.h"
#include "satStore.h"

Include dependency graph for satSolver.c:

Go to the source code of this file.

Classes
struct	varinfo_t

Macros
#define	SAT_USE_ANALYZE_FINAL
#define	L_IND   "%-*d"
#define	L_ind   sat_solver_dl(s)*2+2,sat_solver_dl(s)
#define	L_LIT   "%sx%d"
#define	L_lit(p)

Functions
int	sat_solver_get_var_value (sat_solver *s, int v)
void	sat_solver_set_var_activity (sat_solver *s, int *pVars, int nVars)
int	sat_solver_clause_new (sat_solver *s, lit *begin, lit *end, int learnt)
int	sat_solver_count_assigned (sat_solver *s)
int	sat_solver_propagate (sat_solver *s)
sat_solver *	sat_solver_new (void)
sat_solver *	zsat_solver_new_seed (double seed)
int	sat_solver_addvar (sat_solver *s)
void	sat_solver_setnvars (sat_solver *s, int n)
void	sat_solver_delete (sat_solver *s)
void	sat_solver_restart (sat_solver *s)
void	zsat_solver_restart_seed (sat_solver *s, double seed)
double	sat_solver_memory (sat_solver *s)
int	sat_solver_simplify (sat_solver *s)
void	sat_solver_reducedb (sat_solver *s)
void	sat_solver_rollback (sat_solver *s)
int	sat_solver_addclause (sat_solver *s, lit *begin, lit *end)
double	luby (double y, int x)
void	luby_test ()
int	sat_solver_solve_internal (sat_solver *s)
int	sat_solver_push (sat_solver *s, int p)
void	sat_solver_pop (sat_solver *s)
void	sat_solver_set_resource_limits (sat_solver *s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
int	sat_solver_solve (sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
int	sat_solver_solve_lexsat (sat_solver *s, int *pLits, int nLits)
int	sat_solver_minimize_assumptions (sat_solver *s, int *pLits, int nLits, int nConfLimit)
int	sat_solver_minimize_assumptions2 (sat_solver *s, int *pLits, int nLits, int nConfLimit)
int	sat_solver_nvars (sat_solver *s)
int	sat_solver_nclauses (sat_solver *s)
int	sat_solver_nconflicts (sat_solver *s)
void	sat_solver_store_alloc (sat_solver *s)
void	sat_solver_store_write (sat_solver *s, char *pFileName)
void	sat_solver_store_free (sat_solver *s)
int	sat_solver_store_change_last (sat_solver *s)
void	sat_solver_store_mark_roots (sat_solver *s)
void	sat_solver_store_mark_clauses_a (sat_solver *s)
void *	sat_solver_store_release (sat_solver *s)

Macro Definition Documentation

L_IND

#define L_IND   "%-*d"

Definition at line 40 of file satSolver.c.

L_ind

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

Definition at line 41 of file satSolver.c.

L_LIT

#define L_LIT   "%sx%d"

Definition at line 42 of file satSolver.c.

L_lit

#define L_lit

(

p

)

Value:

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

Definition at line 43 of file satSolver.c.

SAT_USE_ANALYZE_FINAL

#define SAT_USE_ANALYZE_FINAL

Definition at line 32 of file satSolver.c.

Function Documentation

luby()

double luby	(	double	y,
		int	x )

Definition at line 1797 of file satSolver.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:

luby_test()

void luby_test

(

)

Definition at line 1809 of file satSolver.c.

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

Here is the call graph for this function:

sat_solver_addclause()

int sat_solver_addclause	(	sat_solver *	s,
		lit *	begin,
		lit *	end )

Definition at line 1735 of file satSolver.c.

{
    lit *i,*j;
    int maxvar;
    lit last;
    assert( begin < end );
    if ( s->fPrintClause )
    {
        for ( i = begin; i < end; i++ )
            printf( "%s%d ", (*i)&1 ? "!":"", (*i)>>1 );
        printf( "\n" );
    }
 
    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_solver_setnvars(s,maxvar+1);

    // add clause to internal storage
    if ( s->pStore )
    {
        int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
        assert( RetValue );
        (void) RetValue;
    }
 
    // delete duplicates
    last = lit_Undef;
    for (i = j = begin; i < end; i++){
        //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]));
        if (*i == lit_neg(last) || var_value(s, lit_var(*i)) == lit_sign(*i))
            return true;   // tautology
        else if (*i != last && var_value(s, lit_var(*i)) == varX)
            last = *j++ = *i;
    }
//    j = i;
 
    if (j == begin)          // empty clause
        return false;
 
    if (j - begin == 1) // unit clause
        return sat_solver_enqueue(s,*begin,0);
 
    // create new clause
    sat_solver_clause_new(s,begin,j,0);
    return true;
}

Here is the call graph for this function:

sat_solver_addvar()

int sat_solver_addvar

(

sat_solver *

s

)

Definition at line 1267 of file satSolver.c.

{
    sat_solver_setnvars(s, s->size+1);
    return s->size-1;
}

Here is the call graph for this function:

sat_solver_clause_new()

int sat_solver_clause_new	(	sat_solver *	s,
		lit *	begin,
		lit *	end,
		int	learnt )

Definition at line 533 of file satSolver.c.

{
    int fUseBinaryClauses = 1;
    int size;
    clause* c;
    int h;
 
    assert(end - begin > 1);
    assert(learnt >= 0 && learnt < 2);
    size           = end - begin;
 
    // do not allocate memory for the two-literal problem clause
    if ( fUseBinaryClauses && size == 2 && !learnt )
    {
        veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(clause_from_lit(begin[1])));
        veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(clause_from_lit(begin[0])));
        s->stats.clauses++;
        s->stats.clauses_literals += size;
        return 0;
    }
 
    // create new clause
//    h = Vec_SetAppend( &s->Mem, NULL, size + learnt + 1 + 1 ) << 1;
    h = Sat_MemAppend( &s->Mem, begin, size, learnt, 0 );
    assert( !(h & 1) );
    if ( s->hLearnts == -1 && learnt )
        s->hLearnts = h;
    if (learnt)
    {
        c = clause_read( s, h );
        c->lbd = sat_clause_compute_lbd( s, c );
        assert( clause_id(c) == veci_size(&s->act_clas) );
//        veci_push(&s->learned, h);
//        act_clause_bump(s,clause_read(s, h));
        if ( s->ClaActType == 0 )
            veci_push(&s->act_clas, (1<<10));
        else
            veci_push(&s->act_clas, s->cla_inc);
        s->stats.learnts++;
        s->stats.learnts_literals += size;
    }
    else
    {
        s->stats.clauses++;
        s->stats.clauses_literals += size;
    }
 
    assert(begin[0] >= 0);
    assert(begin[0] < s->size*2);
    assert(begin[1] >= 0);
    assert(begin[1] < s->size*2);
 
    assert(lit_neg(begin[0]) < s->size*2);
    assert(lit_neg(begin[1]) < s->size*2);
 
    //veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),c);
    //veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),c);
    veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(size > 2 ? h : clause_from_lit(begin[1])));
    veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(size > 2 ? h : clause_from_lit(begin[0])));
 
    return h;
}

Here is the caller graph for this function:

sat_solver_count_assigned()

int sat_solver_count_assigned

(

sat_solver *

s

)

Definition at line 744 of file satSolver.c.

{
    // count top-level assignments
    int i, Count = 0;
    assert(sat_solver_dl(s) == 0);
    for ( i = 0; i < s->size; i++ )
        if (var_value(s, i) != varX)
            Count++;
    return Count;
}

sat_solver_delete()

void sat_solver_delete

(

sat_solver *

s

)

Definition at line 1341 of file satSolver.c.

{
//    Vec_SetFree_( &s->Mem );
    Sat_MemFree_( &s->Mem );
 
    // delete vectors
    veci_delete(&s->order);
    veci_delete(&s->trail_lim);
    veci_delete(&s->tagged);
//    veci_delete(&s->learned);
    veci_delete(&s->act_clas);
    veci_delete(&s->stack);
//    veci_delete(&s->model);
    veci_delete(&s->act_vars);
    veci_delete(&s->unit_lits);
    veci_delete(&s->pivot_vars);
    veci_delete(&s->temp_clause);
    veci_delete(&s->conf_final);
 
    veci_delete(&s->user_vars);
    veci_delete(&s->user_values);
 
    // delete arrays
    if (s->reasons != 0){
        int i;
        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->polarity );
        ABC_FREE(s->tags     );
        ABC_FREE(s->loads    );
        ABC_FREE(s->activity );
        ABC_FREE(s->activity2);
        ABC_FREE(s->pFreqs   );
        ABC_FREE(s->factors  );
        ABC_FREE(s->orderpos );
        ABC_FREE(s->reasons  );
        ABC_FREE(s->trail    );
        ABC_FREE(s->model    );
    }
 
    sat_solver_store_free(s);
    ABC_FREE(s);
}

Here is the call graph for this function:

sat_solver_get_var_value()

int sat_solver_get_var_value	(	sat_solver *	s,
		int	v )

Definition at line 118 of file satSolver.c.

{
    if ( var_value(s, v) == var0 )
        return l_False;
    if ( var_value(s, v) == var1 )
        return l_True;
    if ( var_value(s, v) == varX )
        return l_Undef;
    assert( 0 );
    return 0;
}

Here is the caller graph for this function:

sat_solver_memory()

double sat_solver_memory

(

sat_solver *

s

)

Definition at line 1479 of file satSolver.c.

{
    int i;
    double Mem = sizeof(sat_solver);
    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->cap * sizeof(int);      // ABC_FREE(s->levels   );
    Mem += s->cap * sizeof(char);     // ABC_FREE(s->assigns  );
    Mem += s->cap * sizeof(char);     // ABC_FREE(s->polarity );
    Mem += s->cap * sizeof(char);     // ABC_FREE(s->tags     );
    Mem += s->cap * sizeof(char);     // ABC_FREE(s->loads    );
    Mem += s->cap * sizeof(word);     // ABC_FREE(s->activity );
    if ( s->activity2 )
    Mem += s->cap * sizeof(word);     // ABC_FREE(s->activity );
    if ( s->factors )
    Mem += s->cap * sizeof(double);   // ABC_FREE(s->factors  );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->orderpos );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->reasons  );
    Mem += s->cap * sizeof(lit);      // ABC_FREE(s->trail    );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->model    );
 
    Mem += s->order.cap * sizeof(int);
    Mem += s->trail_lim.cap * sizeof(int);
    Mem += s->tagged.cap * sizeof(int);
//    Mem += s->learned.cap * sizeof(int);
    Mem += s->stack.cap * sizeof(int);
    Mem += s->act_vars.cap * sizeof(int);
    Mem += s->unit_lits.cap * sizeof(int);
    Mem += s->act_clas.cap * sizeof(int);
    Mem += s->temp_clause.cap * sizeof(int);
    Mem += s->conf_final.cap * sizeof(int);
    Mem += Sat_MemMemoryAll( &s->Mem );
    return Mem;
}

Here is the caller graph for this function:

sat_solver_minimize_assumptions()

int sat_solver_minimize_assumptions	(	sat_solver *	s,
		int *	pLits,
		int	nLits,
		int	nConfLimit )

Definition at line 2209 of file satSolver.c.

{
    int i, k, nLitsL, nLitsR, nResL, nResR, status;
    if ( nLits == 1 )
    {
        // since the problem is UNSAT, we will try to solve it without assuming the last literal
        // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
        if ( nConfLimit ) s->nConfLimit = s->stats.conflicts + nConfLimit;
        status = sat_solver_solve_internal( s );
        //printf( "%c", status == l_False ? 'u' : 's' );
        return (int)(status != l_False); // return 1 if the problem is not UNSAT
    }
    assert( nLits >= 2 );
    nLitsL = nLits / 2;
    nLitsR = nLits - nLitsL;
    // assume the left lits
    for ( i = 0; i < nLitsL; i++ )
        if ( !sat_solver_push(s, pLits[i]) )
        {
            for ( k = i; k >= 0; k-- )
                sat_solver_pop(s);
            return sat_solver_minimize_assumptions( s, pLits, i+1, nConfLimit );
        }
    // solve with these assumptions
    if ( nConfLimit ) s->nConfLimit = s->stats.conflicts + nConfLimit;
    status = sat_solver_solve_internal( s );
    if ( status == l_False ) // these are enough
    {
        for ( i = 0; i < nLitsL; i++ )
            sat_solver_pop(s);
        return sat_solver_minimize_assumptions( s, pLits, nLitsL, nConfLimit );
    }
    // solve for the right lits
    nResL = nLitsR == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit );
    for ( i = 0; i < nLitsL; i++ )
        sat_solver_pop(s);
    // swap literals
//    assert( nResL <= nLitsL );
//    for ( i = 0; i < nResL; i++ )
//        ABC_SWAP( int, pLits[i], pLits[nLitsL+i] );
    veci_resize( &s->temp_clause, 0 );
    for ( i = 0; i < nLitsL; i++ )
        veci_push( &s->temp_clause, pLits[i] );
    for ( i = 0; i < nResL; i++ )
        pLits[i] = pLits[nLitsL+i];
    for ( i = 0; i < nLitsL; i++ )
        pLits[nResL+i] = veci_begin(&s->temp_clause)[i];
    // assume the right lits
    for ( i = 0; i < nResL; i++ )
        if ( !sat_solver_push(s, pLits[i]) )
        {
            for ( k = i; k >= 0; k-- )
                sat_solver_pop(s);
            return sat_solver_minimize_assumptions( s, pLits, i+1, nConfLimit );
        }
    // solve with these assumptions
    if ( nConfLimit ) s->nConfLimit = s->stats.conflicts + nConfLimit;
    status = sat_solver_solve_internal( s );
    if ( status == l_False ) // these are enough
    {
        for ( i = 0; i < nResL; i++ )
            sat_solver_pop(s);
        return nResL;
    }
    // solve for the left lits
    nResR = nLitsL == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nResL, nLitsL, nConfLimit );
    for ( i = 0; i < nResL; i++ )
        sat_solver_pop(s);
    return nResL + nResR;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_minimize_assumptions2()

int sat_solver_minimize_assumptions2	(	sat_solver *	s,
		int *	pLits,
		int	nLits,
		int	nConfLimit )

Definition at line 2284 of file satSolver.c.

{
    int i, k, nLitsL, nLitsR, nResL, nResR;
    if ( nLits == 1 )
    {
        // since the problem is UNSAT, we will try to solve it without assuming the last literal
        // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
        int RetValue = 1, LitNot = Abc_LitNot(pLits[0]);
        int status = l_False;
        int Temp = s->nConfLimit; 
        s->nConfLimit = nConfLimit;
 
        RetValue = sat_solver_push( s, LitNot ); assert( RetValue );
        status = sat_solver_solve_internal( s );
        sat_solver_pop( s );
 
        // if the problem is UNSAT, add clause
        if ( status == l_False )
        {
            RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
            assert( RetValue );
        }
 
        s->nConfLimit = Temp;
        return (int)(status != l_False); // return 1 if the problem is not UNSAT
    }
    assert( nLits >= 2 );
    nLitsL = nLits / 2;
    nLitsR = nLits - nLitsL;
    // assume the left lits
    for ( i = 0; i < nLitsL; i++ )
        if ( !sat_solver_push(s, pLits[i]) )
        {
            for ( k = i; k >= 0; k-- )
                sat_solver_pop(s);
 
            // add clauses for these literal
            for ( k = i+1; k > nLitsL; k++ )
            {
                int LitNot = Abc_LitNot(pLits[i]);
                int RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
                assert( RetValue );
            }
 
            return sat_solver_minimize_assumptions2( s, pLits, i+1, nConfLimit );
        }
    // solve for the right lits
    nResL = sat_solver_minimize_assumptions2( s, pLits + nLitsL, nLitsR, nConfLimit );
    for ( i = 0; i < nLitsL; i++ )
        sat_solver_pop(s);
    // swap literals
//    assert( nResL <= nLitsL );
    veci_resize( &s->temp_clause, 0 );
    for ( i = 0; i < nLitsL; i++ )
        veci_push( &s->temp_clause, pLits[i] );
    for ( i = 0; i < nResL; i++ )
        pLits[i] = pLits[nLitsL+i];
    for ( i = 0; i < nLitsL; i++ )
        pLits[nResL+i] = veci_begin(&s->temp_clause)[i];
    // assume the right lits
    for ( i = 0; i < nResL; i++ )
        if ( !sat_solver_push(s, pLits[i]) )
        {
            for ( k = i; k >= 0; k-- )
                sat_solver_pop(s);
 
            // add clauses for these literal
            for ( k = i+1; k > nResL; k++ )
            {
                int LitNot = Abc_LitNot(pLits[i]);
                int RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
                assert( RetValue );
            }
 
            return sat_solver_minimize_assumptions2( s, pLits, i+1, nConfLimit );
        }
    // solve for the left lits
    nResR = sat_solver_minimize_assumptions2( s, pLits + nResL, nLitsL, nConfLimit );
    for ( i = 0; i < nResL; i++ )
        sat_solver_pop(s);
    return nResL + nResR;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_nclauses()

int sat_solver_nclauses

(

sat_solver *

s

)

Definition at line 2375 of file satSolver.c.

{
    return s->stats.clauses;
}

Here is the caller graph for this function:

sat_solver_nconflicts()

int sat_solver_nconflicts

(

sat_solver *

s

)

Definition at line 2381 of file satSolver.c.

{
    return (int)s->stats.conflicts;
}

Here is the caller graph for this function:

sat_solver_new()

sat_solver * sat_solver_new

(

void

)

Definition at line 1137 of file satSolver.c.

{
    sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver));
 
//    Vec_SetAlloc_(&s->Mem, 15);
    Sat_MemAlloc_(&s->Mem, 17);
    s->hLearnts = -1;
    s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
    s->binary = clause_read( s, s->hBinary );
 
    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->learned);
    veci_new(&s->act_clas);
    veci_new(&s->stack);
//    veci_new(&s->model);
    veci_new(&s->unit_lits);
    veci_new(&s->temp_clause);
    veci_new(&s->conf_final);
 
    // initialize arrays
    s->wlists    = 0;
    s->activity  = 0;
    s->orderpos  = 0;
    s->reasons   = 0;
    s->trail     = 0;
 
    // initialize other vars
    s->size                   = 0;
    s->cap                    = 0;
    s->qhead                  = 0;
    s->qtail                  = 0;
 
    solver_init_activities(s);
    veci_new(&s->act_vars);
 
    s->root_level             = 0;
//    s->simpdb_assigns         = 0;
//    s->simpdb_props           = 0;
    s->random_seed            = 91648253;
    s->progress_estimate      = 0;
//    s->binary                 = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
//    s->binary->size_learnt    = (2 << 1);
    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;
    return s;
}

sat_solver_nvars()

int sat_solver_nvars

(

sat_solver *

s

)

Definition at line 2369 of file satSolver.c.

{
    return s->size;
}

sat_solver_pop()

void sat_solver_pop

(

sat_solver *

s

)

Definition at line 2045 of file satSolver.c.

{
    assert( sat_solver_dl(s) > 0 );
    sat_solver_canceluntil(s, --s->root_level);
}

Here is the caller graph for this function:

sat_solver_propagate()

int sat_solver_propagate

(

sat_solver *

s

)

Definition at line 1019 of file satSolver.c.

{
    int     hConfl = 0;
    lit*    lits;
    lit false_lit;
 
    //printf("sat_solver_propagate\n");
    while (hConfl == 0 && s->qtail - s->qhead > 0){
        lit p = s->trail[s->qhead++];
 
#ifdef TEST_CNF_LOAD
        int v = lit_var(p);
        if ( s->pCnfFunc )
        {
            if ( lit_sign(p) )
            {
                if ( (s->loads[v] & 1) == 0 )
                {
                    s->loads[v] ^= 1;
                    s->pCnfFunc( s->pCnfMan, p );
                }
            }
            else
            {
                if ( (s->loads[v] & 2) == 0 )
                {
                    s->loads[v] ^= 2;
                    s->pCnfFunc( s->pCnfMan, p );
                }
            }
        }
        {
#endif
 
        veci* ws    = sat_solver_read_wlist(s,p);
        int*  begin = veci_begin(ws);
        int*  end   = begin + veci_size(ws);
        int*i, *j;
 
        s->stats.propagations++;
//        s->simpdb_props--;
 
        //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
        for (i = j = begin; i < end; ){
            if (clause_is_lit(*i)){
 
                int Lit = clause_read_lit(*i);
                if (var_value(s, lit_var(Lit)) == lit_sign(Lit)){
                    *j++ = *i++;
                    continue;
                }
 
                *j++ = *i;
                if (!sat_solver_enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
                    hConfl = s->hBinary;
                    (clause_begin(s->binary))[1] = lit_neg(p);
                    (clause_begin(s->binary))[0] = clause_read_lit(*i++);
                    // Copy the remaining watches:
                    while (i < end)
                        *j++ = *i++;
                }
            }else{
 
                clause* c = clause_read(s,*i);
                lits = clause_begin(c);
 
                // 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:
                    lit* stop = lits + clause_size(c);
                    lit* k;
                    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(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
                            goto next; }
                    }
 
                    *j++ = *i;
                    // Clause is unit under assignment:
                    if ( c->lrn )
                        c->lbd = sat_clause_compute_lbd(s, c);
                    if (!sat_solver_enqueue(s,lits[0], *i)){
                        hConfl = *i++;
                        // Copy the remaining watches:
                        while (i < end)
                            *j++ = *i++;
                    }
                }
            }
        next:
            i++;
        }
 
        s->stats.inspects += j - veci_begin(ws);
        veci_resize(ws,j - veci_begin(ws));
#ifdef TEST_CNF_LOAD
        }
#endif
    }
 
    return hConfl;
}

Here is the caller graph for this function:

sat_solver_push()

int sat_solver_push	(	sat_solver *	s,
		int	p )

Definition at line 2002 of file satSolver.c.

{
    assert(lit_var(p) < s->size);
    veci_push(&s->trail_lim,s->qtail);
    s->root_level++;
    if (!sat_solver_enqueue(s,p,0))
    {
        int h = s->reasons[lit_var(p)];
        if (h)
        {
            if (clause_is_lit(h))
            {
                (clause_begin(s->binary))[1] = lit_neg(p);
                (clause_begin(s->binary))[0] = clause_read_lit(h);
                h = s->hBinary;
            }
            sat_solver_analyze_final(s, h, 1);
            veci_push(&s->conf_final, lit_neg(p));
        }
        else
        {
            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);
        }
        //sat_solver_canceluntil(s, 0);
        return false; 
    }
    else
    {
        int fConfl = sat_solver_propagate(s);
        if (fConfl){
            sat_solver_analyze_final(s, fConfl, 0);
            //assert(s->conf_final.size > 0);
            //sat_solver_canceluntil(s, 0);
            return false; }
    }
    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_reducedb()

void sat_solver_reducedb

(

sat_solver *

s

)

Definition at line 1523 of file satSolver.c.

{
    static abctime TimeTotal = 0;
    abctime clk = Abc_Clock();
    Sat_Mem_t * pMem = &s->Mem;
    int nLearnedOld = veci_size(&s->act_clas);
    int * act_clas = veci_begin(&s->act_clas);
    int * pPerm, * pArray, * pSortValues, nCutoffValue;
    int i, k, j, Id, Counter, CounterStart, nSelected;
    clause * c;
 
    assert( s->nLearntMax > 0 );
    assert( nLearnedOld == Sat_MemEntryNum(pMem, 1) );
    assert( nLearnedOld == (int)s->stats.learnts );
 
    s->nDBreduces++;
 
    //printf( "Calling reduceDB with %d learned clause limit.\n", s->nLearntMax );
    s->nLearntMax = s->nLearntStart + s->nLearntDelta * s->nDBreduces;
//    return;
 
    // create sorting values
    pSortValues = ABC_ALLOC( int, nLearnedOld );
    Sat_MemForEachLearned( pMem, c, i, k )
    {
        Id = clause_id(c);
//        pSortValues[Id] = act[Id];
        if ( s->ClaActType == 0 )
            pSortValues[Id] = ((7 - Abc_MinInt(c->lbd, 7)) << 28) | (act_clas[Id] >> 4);
        else
            pSortValues[Id] = ((7 - Abc_MinInt(c->lbd, 7)) << 28);// | (act_clas[Id] >> 4);
        assert( pSortValues[Id] >= 0 );
    }
 
    // preserve 1/20 of last clauses
    CounterStart  = nLearnedOld - (s->nLearntMax / 20);
 
    // preserve 3/4 of most active clauses
    nSelected = nLearnedOld*s->nLearntRatio/100;
 
    // 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 );
//    ActCutOff = ABC_INFINITY;
 
    // mark learned clauses to remove
    Counter = j = 0;
    Sat_MemForEachLearned( pMem, c, i, k )
    {
        assert( c->mark == 0 );
        if ( Counter++ > CounterStart || clause_size(c) < 3 || pSortValues[clause_id(c)] > nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) )
            act_clas[j++] = act_clas[clause_id(c)];
        else // delete
        {
            c->mark = 1;
            s->stats.learnts_literals -= clause_size(c);
            s->stats.learnts--;
        }
    }
    assert( s->stats.learnts == (unsigned)j );
    assert( Counter == nLearnedOld );
    veci_resize(&s->act_clas,j);
    ABC_FREE( pSortValues );
 
    // 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;
        c = clause_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++ )
    {
        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 
            {
                c = clause_read(s, pArray[k]);
                if ( !c->mark ) // useful learned clause
                   pArray[j++] = clause_id(c); // updating handle here!!!
            }
        }
        veci_resize(&s->wlists[i],j);
    }
 
    // perform final move of the clauses
    Counter = Sat_MemCompactLearned( pMem, 1 );
    assert( Counter == (int)s->stats.learnts );
 
    // 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:

sat_solver_restart()

void sat_solver_restart

(

sat_solver *

s

)

Definition at line 1389 of file satSolver.c.

{
    int i;
    Sat_MemRestart( &s->Mem );
    s->hLearnts = -1;
    s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
    s->binary = clause_read( s, s->hBinary );
 
    veci_resize(&s->trail_lim, 0);
    veci_resize(&s->order, 0);
    for ( i = 0; i < s->size*2; i++ )
        s->wlists[i].size = 0;
 
    s->nDBreduces = 0;
 
    // initialize other vars
    s->size                   = 0;
//    s->cap                    = 0;
    s->qhead                  = 0;
    s->qtail                  = 0;
 
 
    // variable activities
    solver_init_activities(s);
    veci_resize(&s->act_clas, 0);
 
 
    s->root_level             = 0;
//    s->simpdb_assigns         = 0;
//    s->simpdb_props           = 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;
}

Here is the caller graph for this function:

sat_solver_rollback()

void sat_solver_rollback

(

sat_solver *

s

)

Definition at line 1643 of file satSolver.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 );
    // reset implication queue
    sat_solver_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(word) * 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 ( clause_is_lit(pArray[k]) )
            {
                if ( clause_read_lit(pArray[k]) < s->iVarPivot*2 )
                    pArray[j++] = pArray[k];
            }
            else 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);
 
    // initialize other vars
    s->size = s->iVarPivot;
    if ( s->size == 0 )
    {
    //    s->size                   = 0;
    //    s->cap                    = 0;
        s->qhead                  = 0;
        s->qtail                  = 0;
 
        solver_init_activities(s);
 
        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 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_solver_set_resource_limits()

void sat_solver_set_resource_limits	(	sat_solver *	s,
		ABC_INT64_T	nConfLimit,
		ABC_INT64_T	nInsLimit,
		ABC_INT64_T	nConfLimitGlobal,
		ABC_INT64_T	nInsLimitGlobal )

Definition at line 2051 of file satSolver.c.

{
    // set the external limits
    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;
}

Here is the caller graph for this function:

sat_solver_set_var_activity()

void sat_solver_set_var_activity	(	sat_solver *	s,
		int *	pVars,
		int	nVars )

Definition at line 218 of file satSolver.c.

{
    int i;
    for (i = 0; i < s->size; i++)
        s->activity[i] = 0;
    if ( s->VarActType == 0 )
    {
        s->var_inc            = (1 <<  5);
        s->var_decay          = -1;
        for ( i = 0; i < nVars; i++ )
        {
            int iVar = pVars ? pVars[i] : i;
            s->activity[iVar] = s->var_inc*(nVars-i);
            if (s->orderpos[iVar] != -1)
                order_update( s, iVar );
        }
    }
    else if ( s->VarActType == 1 )
    {
        s->var_inc = Abc_Dbl2Word(1);
        for ( i = 0; i < nVars; i++ )
        {
            int iVar = pVars ? pVars[i] : i;
            s->activity[iVar] = Abc_Dbl2Word(nVars-i);
            if (s->orderpos[iVar] != -1)
                order_update( s, iVar );
        }
    }
    else assert( 0 );
}

sat_solver_setnvars()

void sat_solver_setnvars	(	sat_solver *	s,
		int	n )

Definition at line 1272 of file satSolver.c.

{
    int var;
 
    if (s->cap < n){
        int old_cap = s->cap;
        while (s->cap < n) s->cap = s->cap*2+1;
        if ( s->cap < 50000 )
            s->cap = 50000;
 
        s->wlists    = ABC_REALLOC(veci,   s->wlists,   s->cap*2);
//        s->vi        = ABC_REALLOC(varinfo,s->vi,       s->cap);
        s->levels    = ABC_REALLOC(int,    s->levels,   s->cap);
        s->assigns   = ABC_REALLOC(char,   s->assigns,  s->cap);
        s->polarity  = ABC_REALLOC(char,   s->polarity, s->cap);
        s->tags      = ABC_REALLOC(char,   s->tags,     s->cap);
        s->loads     = ABC_REALLOC(char,   s->loads,    s->cap);
        s->activity  = ABC_REALLOC(word,   s->activity, s->cap);
        s->activity2 = ABC_REALLOC(word,   s->activity2,s->cap);
        s->pFreqs    = ABC_REALLOC(char,   s->pFreqs,   s->cap);
 
        if ( s->factors )
        s->factors   = ABC_REALLOC(double, s->factors,  s->cap);
        s->orderpos  = ABC_REALLOC(int,    s->orderpos, s->cap);
        s->reasons   = ABC_REALLOC(int,    s->reasons,  s->cap);
        s->trail     = ABC_REALLOC(lit,    s->trail,    s->cap);
        s->model     = ABC_REALLOC(int,    s->model,    s->cap);
        memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(veci) );
    } 
 
    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]);
 
        if ( s->VarActType == 0 )
            s->activity[var] = (1<<10);
        else if ( s->VarActType == 1 )
            s->activity[var] = 0;
        else if ( s->VarActType == 2 )
            s->activity[var] = 0;
        else assert(0);
 
        s->pFreqs[var]   = 0;
        if ( s->factors )
        s->factors [var] = 0;
//        *((int*)s->vi + var) = 0; s->vi[var].val = varX;
        s->levels  [var] = 0;
        s->assigns [var] = varX;
        s->polarity[var] = 0;
        s->tags    [var] = 0;
        s->loads   [var] = 0;
        s->orderpos[var] = veci_size(&s->order);
        s->reasons [var] = 0;
        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); 
         */
        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:

sat_solver_simplify()

int sat_solver_simplify

(

sat_solver *

s

)

Definition at line 1515 of file satSolver.c.

{
    assert(sat_solver_dl(s) == 0);
    if (sat_solver_propagate(s) != 0)
        return false;
    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_solve()

int sat_solver_solve	(	sat_solver *	s,
		lit *	begin,
		lit *	end,
		ABC_INT64_T	nConfLimit,
		ABC_INT64_T	nInsLimit,
		ABC_INT64_T	nConfLimitGlobal,
		ABC_INT64_T	nInsLimitGlobal )

Definition at line 2068 of file satSolver.c.

{
    lbool status;
    lit * i;
    if ( s->fSolved )
    {
        if ( s->pStore )
        {
            int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
            assert( RetValue );
            (void) RetValue;
        }
        return l_False;
    }
 
    if ( s->fVerbose )
        printf( "Running SAT solver with parameters %d and %d and %d.\n", s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
 
    sat_solver_set_resource_limits( s, nConfLimit, nInsLimit, nConfLimitGlobal, nInsLimitGlobal );
 
#ifdef SAT_USE_ANALYZE_FINAL
    // Perform assumptions:
    s->root_level = 0;
    for ( i = begin; i < end; i++ )
        if ( !sat_solver_push(s, *i) )
        {
            sat_solver_canceluntil(s,0);
            s->root_level = 0;
            return l_False;
        }
    assert(s->root_level == sat_solver_dl(s));
#else
    //printf("solve: "); printlits(begin, end); printf("\n");
    for (i = begin; i < end; i++){
//        switch (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]){
        switch (var_value(s, *i)) {
        case var1: // l_True: 
            break;
        case varX: // l_Undef
            sat_solver_decision(s, *i);
            if (sat_solver_propagate(s) == 0)
                break;
            // fallthrough
        case var0: // l_False 
            sat_solver_canceluntil(s, 0);
            return l_False;
        }
    }
    s->root_level = sat_solver_dl(s);
#endif
 
    status = sat_solver_solve_internal(s);
 
    sat_solver_canceluntil(s,0);
    s->root_level = 0;

    if ( status == l_False && s->pStore )
    {
        int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
        assert( RetValue );
        (void) RetValue;
    }
    return status;
}

Here is the call graph for this function:

sat_solver_solve_internal()

int sat_solver_solve_internal

(

sat_solver *

s

)

Definition at line 1942 of file satSolver.c.

{
    lbool status = l_Undef;
    int restart_iter = 0;
    veci_resize(&s->unit_lits, 0);
    s->nCalls++;
 
    if (s->verbosity >= 1){
        printf("==================================[MINISAT]===================================\n");
        printf("| Conflicts |     ORIGINAL     |              LEARNT              | Progress |\n");
        printf("|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |\n");
        printf("==============================================================================\n");
    }
 
    while (status == l_Undef){
        ABC_INT64_T nof_conflicts;
        if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
            break;
        if (s->verbosity >= 1)
        {
            double Ratio = (s->stats.learnts == 0)? 0.0 :
                s->stats.learnts_literals / (double)s->stats.learnts;
            printf("| %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)0, 
                (double)s->stats.learnts, 
                (double)s->stats.learnts_literals,
                Ratio,
                s->progress_estimate*100);
            fflush(stdout);
        }
        nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) );
        status = sat_solver_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->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
            break;
        if ( s->pFuncStop && s->pFuncStop(s->RunId) )
            break;
    }
    if (s->verbosity >= 1)
        printf("==============================================================================\n");
 
    sat_solver_canceluntil(s,s->root_level);
    // save variable values
    if ( status == l_True && s->user_vars.size )
    {
        int v;
        for ( v = 0; v < s->user_vars.size; v++ )
            veci_push(&s->user_values, sat_solver_var_value(s, s->user_vars.ptr[v]));
    }
    return status;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_solve_lexsat()

int sat_solver_solve_lexsat	(	sat_solver *	s,
		int *	pLits,
		int	nLits )

Definition at line 2143 of file satSolver.c.

{
    int i, iLitFail = -1;
    lbool status;
    assert( nLits > 0 );
    // help the SAT solver by setting desirable polarity
    sat_solver_set_literal_polarity( s, pLits, nLits );
    // check if there exists a satisfying assignment
    status = sat_solver_solve_internal( s );
    if ( status != l_True ) // no assignment
        return status;
    // there is at least one satisfying assignment
    assert( status == l_True );
    // find the first mismatching literal
    for ( i = 0; i < nLits; i++ )
        if ( pLits[i] != sat_solver_var_literal(s, Abc_Lit2Var(pLits[i])) )
            break;
    if ( i == nLits ) // no mismatch - the current assignment is the minimum one!
        return l_True;
    // mismatch happens in literal i
    iLitFail = i;
    // create assumptions up to this literal (as in pLits) - including this literal!
    for ( i = 0; i <= iLitFail; i++ )
        if ( !sat_solver_push(s, pLits[i]) ) // can become UNSAT while adding the last assumption
            break;
    if ( i < iLitFail + 1 ) // the solver became UNSAT while adding assumptions
        status = l_False;
    else // solve under the assumptions
        status = sat_solver_solve_internal( s );
    if ( status == l_True )
    {
        // we proved that there is a sat assignment with literal (iLitFail) having polarity as in pLits
        // continue solving recursively
        if ( iLitFail + 1 < nLits )
            status = sat_solver_solve_lexsat( s, pLits + iLitFail + 1, nLits - iLitFail - 1 );
    }
    else if ( status == l_False )
    {
        // we proved that there is no assignment with iLitFail having polarity as in pLits
        assert( Abc_LitIsCompl(pLits[iLitFail]) ); // literal is 0 
        // (this assert may fail only if there is a sat assignment smaller than one originally given in pLits)
        // now we flip this literal (make it 1), change the last assumption
        // and contiue looking for the 000...0-assignment of other literals
        sat_solver_pop( s );
        pLits[iLitFail] = Abc_LitNot(pLits[iLitFail]);
        if ( !sat_solver_push(s, pLits[iLitFail]) )
            printf( "sat_solver_solve_lexsat(): A satisfying assignment should exist.\n" ); // because we know that the problem is satisfiable
        // update other literals to be 000...0
        for ( i = iLitFail + 1; i < nLits; i++ )
            pLits[i] = Abc_LitNot( Abc_LitRegular(pLits[i]) );
        // continue solving recursively
        if ( iLitFail + 1 < nLits )
            status = sat_solver_solve_lexsat( s, pLits + iLitFail + 1, nLits - iLitFail - 1 );
        else
            status = l_True;
    }
    // undo the assumptions
    for ( i = iLitFail; i >= 0; i-- )
        sat_solver_pop( s );
    return status;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_store_alloc()

void sat_solver_store_alloc

(

sat_solver *

s

)

Definition at line 2389 of file satSolver.c.

{
    assert( s->pStore == NULL );
    s->pStore = Sto_ManAlloc();
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_store_change_last()

int sat_solver_store_change_last

(

sat_solver *

s

)

Definition at line 2406 of file satSolver.c.

{
    if ( s->pStore ) return Sto_ManChangeLastClause( (Sto_Man_t *)s->pStore );
    return -1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_store_free()

void sat_solver_store_free

(

sat_solver *

s

)

Definition at line 2400 of file satSolver.c.

{
    if ( s->pStore ) Sto_ManFree( (Sto_Man_t *)s->pStore );
    s->pStore = NULL;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_store_mark_clauses_a()

void sat_solver_store_mark_clauses_a

(

sat_solver *

s

)

Definition at line 2417 of file satSolver.c.

{
    if ( s->pStore ) Sto_ManMarkClausesA( (Sto_Man_t *)s->pStore );
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_store_mark_roots()

void sat_solver_store_mark_roots

(

sat_solver *

s

)

Definition at line 2412 of file satSolver.c.

{
    if ( s->pStore ) Sto_ManMarkRoots( (Sto_Man_t *)s->pStore );
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_store_release()

void * sat_solver_store_release

(

sat_solver *

s

)

Definition at line 2422 of file satSolver.c.

{
    void * pTemp;
    if ( s->pStore == NULL )
        return NULL;
    pTemp = s->pStore;
    s->pStore = NULL;
    return pTemp;
}

Here is the caller graph for this function:

sat_solver_store_write()

void sat_solver_store_write	(	sat_solver *	s,
		char *	pFileName )

Definition at line 2395 of file satSolver.c.

{
    if ( s->pStore ) Sto_ManDumpClauses( (Sto_Man_t *)s->pStore, pFileName );
}

Here is the call graph for this function:

Here is the caller graph for this function:

zsat_solver_new_seed()

sat_solver * zsat_solver_new_seed

(

double

seed

)

Definition at line 1202 of file satSolver.c.

{
    sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver));
 
//    Vec_SetAlloc_(&s->Mem, 15);
    Sat_MemAlloc_(&s->Mem, 15);
    s->hLearnts = -1;
    s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
    s->binary = clause_read( s, s->hBinary );
 
    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->learned);
    veci_new(&s->act_clas);
    veci_new(&s->stack);
//    veci_new(&s->model);
    veci_new(&s->unit_lits);
    veci_new(&s->temp_clause);
    veci_new(&s->conf_final);
 
    // initialize arrays
    s->wlists    = 0;
    s->activity  = 0;
    s->orderpos  = 0;
    s->reasons   = 0;
    s->trail     = 0;
 
    // initialize other vars
    s->size                   = 0;
    s->cap                    = 0;
    s->qhead                  = 0;
    s->qtail                  = 0;
 
    solver_init_activities(s);
    veci_new(&s->act_vars);
 
    s->root_level             = 0;
//    s->simpdb_assigns         = 0;
//    s->simpdb_props           = 0;
    s->random_seed            = seed;
    s->progress_estimate      = 0;
//    s->binary                 = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
//    s->binary->size_learnt    = (2 << 1);
    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;
    return s;
}

Here is the caller graph for this function:

zsat_solver_restart_seed()

void zsat_solver_restart_seed	(	sat_solver *	s,
		double	seed )

Definition at line 1435 of file satSolver.c.

{
    int i;
    Sat_MemRestart( &s->Mem );
    s->hLearnts = -1;
    s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
    s->binary = clause_read( s, s->hBinary );
 
    veci_resize(&s->trail_lim, 0);
    veci_resize(&s->order, 0);
    for ( i = 0; i < s->size*2; i++ )
        s->wlists[i].size = 0;
 
    s->nDBreduces = 0;
 
    // initialize other vars
    s->size                   = 0;
//    s->cap                    = 0;
    s->qhead                  = 0;
    s->qtail                  = 0;
 
    solver_init_activities(s);
    veci_resize(&s->act_clas, 0);
 
    s->root_level             = 0;
//    s->simpdb_assigns         = 0;
//    s->simpdb_props           = 0;
    s->random_seed            = seed;
    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;
}

Here is the caller graph for this function: