satSolver3.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "satVec.h"
#include "satClause.h"
#include "misc/util/utilDouble.h"

Include dependency graph for satSolver3.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	sat_solver3_t

Typedefs
typedef struct sat_solver3_t	sat_solver3

Functions
sat_solver3 *	sat_solver3_new (void)
sat_solver3 *	zsat_solver3_new_seed (double seed)
void	sat_solver3_delete (sat_solver3 *s)
int	sat_solver3_addclause (sat_solver3 *s, lit *begin, lit *end)
int	sat_solver3_clause_new (sat_solver3 *s, lit *begin, lit *end, int learnt)
int	sat_solver3_simplify (sat_solver3 *s)
int	sat_solver3_solve (sat_solver3 *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
int	sat_solver3_solve_internal (sat_solver3 *s)
int	sat_solver3_solve_lexsat (sat_solver3 *s, int *pLits, int nLits)
int	sat_solver3_minimize_assumptions (sat_solver3 *s, int *pLits, int nLits, int nConfLimit)
int	sat_solver3_minimize_assumptions2 (sat_solver3 *s, int *pLits, int nLits, int nConfLimit)
int	sat_solver3_push (sat_solver3 *s, int p)
void	sat_solver3_pop (sat_solver3 *s)
void	sat_solver3_set_resource_limits (sat_solver3 *s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
void	sat_solver3_restart (sat_solver3 *s)
void	zsat_solver3_restart_seed (sat_solver3 *s, double seed)
void	sat_solver3_rollback (sat_solver3 *s)
int	sat_solver3_nvars (sat_solver3 *s)
int	sat_solver3_nclauses (sat_solver3 *s)
int	sat_solver3_nconflicts (sat_solver3 *s)
double	sat_solver3_memory (sat_solver3 *s)
int	sat_solver3_count_assigned (sat_solver3 *s)
void	sat_solver3_setnvars (sat_solver3 *s, int n)
int	sat_solver3_get_var_value (sat_solver3 *s, int v)
void	sat_solver3_set_var_activity (sat_solver3 *s, int *pVars, int nVars)
void	sat_solver3WriteDimacs (sat_solver3 *p, char *pFileName, lit *assumptionsBegin, lit *assumptionsEnd, int incrementVars)
void	sat_solver3PrintStats (FILE *pFile, sat_solver3 *p)
int *	sat_solver3GetModel (sat_solver3 *p, int *pVars, int nVars)
void	sat_solver3DoubleClauses (sat_solver3 *p, int iVar)
void	sat_solver3TraceStart (sat_solver3 *pSat, char *pName)
void	sat_solver3TraceStop (sat_solver3 *pSat)
void	sat_solver3TraceWrite (sat_solver3 *pSat, int *pBeg, int *pEnd, int fRoot)
void	sat_solver3_store_alloc (sat_solver3 *s)
void	sat_solver3_store_write (sat_solver3 *s, char *pFileName)
void	sat_solver3_store_free (sat_solver3 *s)
void	sat_solver3_store_mark_roots (sat_solver3 *s)
void	sat_solver3_store_mark_clauses_a (sat_solver3 *s)
void *	sat_solver3_store_release (sat_solver3 *s)

Typedef Documentation

sat_solver3

typedef struct sat_solver3_t sat_solver3

Definition at line 41 of file satSolver3.h.

Function Documentation

sat_solver3_addclause()

int sat_solver3_addclause ( sat_solver3 * s, lit * begin, lit * end )

extern

Definition at line 1698 of file satSolver3.c.

{
    int fVerbose = 0;
    lit *i,*j;
    int maxvar;
    lit last;
    assert( begin < end );
    if ( fVerbose )
    {
        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_solver3_setnvars(s,maxvar+1);
 
    // 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_solver3_enqueue(s,*begin,0);
 
    // create new clause
    sat_solver3_clause_new(s,begin,j,0);
    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver3_clause_new()

int sat_solver3_clause_new ( sat_solver3 * s, lit * begin, lit * end, int learnt )

extern

Definition at line 514 of file satSolver3.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_solver3_read_wlist(s,lit_neg(begin[0])),(clause_from_lit(begin[1])));
        veci_push(sat_solver3_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_solver3_read_wlist(s,lit_neg(begin[0])),c);
    //veci_push(sat_solver3_read_wlist(s,lit_neg(begin[1])),c);
    veci_push(sat_solver3_read_wlist(s,lit_neg(begin[0])),(size > 2 ? h : clause_from_lit(begin[1])));
    veci_push(sat_solver3_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_solver3_count_assigned()

int sat_solver3_count_assigned ( sat_solver3 * s )

extern

Definition at line 716 of file satSolver3.c.

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

sat_solver3_delete()

void sat_solver3_delete ( sat_solver3 * s )

extern

Definition at line 1308 of file satSolver3.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);
 
    // 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    );
    }
 
    ABC_FREE(s);
}

Here is the caller graph for this function:

sat_solver3_get_var_value()

int sat_solver3_get_var_value ( sat_solver3 * s, int v )

extern

Definition at line 116 of file satSolver3.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;
}

sat_solver3_memory()

double sat_solver3_memory ( sat_solver3 * s )

extern

Definition at line 1442 of file satSolver3.c.

{
    int i;
    double Mem = sizeof(sat_solver3);
    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;
}

sat_solver3_minimize_assumptions()

int sat_solver3_minimize_assumptions ( sat_solver3 * s, int * pLits, int nLits, int nConfLimit )

extern

Definition at line 2135 of file satSolver3.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 status = l_False;
        int Temp = s->nConfLimit; 
        s->nConfLimit = nConfLimit;
        status = sat_solver3_solve_internal( s );
        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_solver3_push(s, pLits[i]) )
        {
            for ( k = i; k >= 0; k-- )
                sat_solver3_pop(s);
            return sat_solver3_minimize_assumptions( s, pLits, i+1, nConfLimit );
        }
    // solve for the right lits
    nResL = sat_solver3_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit );
    for ( i = 0; i < nLitsL; i++ )
        sat_solver3_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_solver3_push(s, pLits[i]) )
        {
            for ( k = i; k >= 0; k-- )
                sat_solver3_pop(s);
            return sat_solver3_minimize_assumptions( s, pLits, i+1, nConfLimit );
        }
    // solve for the left lits
    nResR = sat_solver3_minimize_assumptions( s, pLits + nResL, nLitsL, nConfLimit );
    for ( i = 0; i < nResL; i++ )
        sat_solver3_pop(s);
    return nResL + nResR;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver3_minimize_assumptions2()

int sat_solver3_minimize_assumptions2 ( sat_solver3 * s, int * pLits, int nLits, int nConfLimit )

extern

Definition at line 2194 of file satSolver3.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_solver3_push( s, LitNot ); assert( RetValue );
        status = sat_solver3_solve_internal( s );
        sat_solver3_pop( s );
 
        // if the problem is UNSAT, add clause
        if ( status == l_False )
        {
            RetValue = sat_solver3_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_solver3_push(s, pLits[i]) )
        {
            for ( k = i; k >= 0; k-- )
                sat_solver3_pop(s);
 
            // add clauses for these literal
            for ( k = i+1; k > nLitsL; k++ )
            {
                int LitNot = Abc_LitNot(pLits[i]);
                int RetValue = sat_solver3_addclause( s, &LitNot, &LitNot+1 );
                assert( RetValue );
            }
 
            return sat_solver3_minimize_assumptions2( s, pLits, i+1, nConfLimit );
        }
    // solve for the right lits
    nResL = sat_solver3_minimize_assumptions2( s, pLits + nLitsL, nLitsR, nConfLimit );
    for ( i = 0; i < nLitsL; i++ )
        sat_solver3_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_solver3_push(s, pLits[i]) )
        {
            for ( k = i; k >= 0; k-- )
                sat_solver3_pop(s);
 
            // add clauses for these literal
            for ( k = i+1; k > nResL; k++ )
            {
                int LitNot = Abc_LitNot(pLits[i]);
                int RetValue = sat_solver3_addclause( s, &LitNot, &LitNot+1 );
                assert( RetValue );
            }
 
            return sat_solver3_minimize_assumptions2( s, pLits, i+1, nConfLimit );
        }
    // solve for the left lits
    nResR = sat_solver3_minimize_assumptions2( s, pLits + nResL, nLitsL, nConfLimit );
    for ( i = 0; i < nResL; i++ )
        sat_solver3_pop(s);
    return nResL + nResR;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver3_nclauses()

int sat_solver3_nclauses ( sat_solver3 * s )

extern

Definition at line 2285 of file satSolver3.c.

{
    return s->stats.clauses;
}

sat_solver3_nconflicts()

int sat_solver3_nconflicts ( sat_solver3 * s )

extern

Definition at line 2291 of file satSolver3.c.

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

sat_solver3_new()

sat_solver3 * sat_solver3_new ( void )

extern

Definition at line 1109 of file satSolver3.c.

{
    sat_solver3* s = (sat_solver3*)ABC_CALLOC( char, sizeof(sat_solver3));
 
//    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;
}

Here is the caller graph for this function:

sat_solver3_nvars()

int sat_solver3_nvars ( sat_solver3 * s )

extern

Definition at line 2279 of file satSolver3.c.

{
    return s->size;
}

sat_solver3_pop()

void sat_solver3_pop ( sat_solver3 * s )

extern

Definition at line 1990 of file satSolver3.c.

{
    assert( sat_solver3_dl(s) > 0 );
    sat_solver3_canceluntil(s, --s->root_level);
}

Here is the caller graph for this function:

sat_solver3_push()

int sat_solver3_push ( sat_solver3 * s, int p )

extern

Definition at line 1947 of file satSolver3.c.

{
    assert(lit_var(p) < s->size);
    veci_push(&s->trail_lim,s->qtail);
    s->root_level++;
    if (!sat_solver3_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_solver3_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_solver3_canceluntil(s, 0);
        return false; 
    }
    else
    {
        int fConfl = sat_solver3_propagate(s);
        if (fConfl){
            sat_solver3_analyze_final(s, fConfl, 0);
            //assert(s->conf_final.size > 0);
            //sat_solver3_canceluntil(s, 0);
            return false; }
    }
    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver3_restart()

void sat_solver3_restart ( sat_solver3 * s )

extern

Definition at line 1352 of file satSolver3.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;
}

sat_solver3_rollback()

void sat_solver3_rollback ( sat_solver3 * s )

extern

Definition at line 1606 of file satSolver3.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_solver3_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:

sat_solver3_set_resource_limits()

void sat_solver3_set_resource_limits ( sat_solver3 * s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal )

extern

Definition at line 1996 of file satSolver3.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_solver3_set_var_activity()

void sat_solver3_set_var_activity ( sat_solver3 * s, int * pVars, int nVars )

extern

Definition at line 216 of file satSolver3.c.

{
    int i;
    assert( s->VarActType == 1 );
    for (i = 0; i < s->size; i++)
        s->activity[i] = 0;
    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);
        order_update( s, iVar );
    }
}

sat_solver3_setnvars()

void sat_solver3_setnvars ( sat_solver3 * s, int n )

extern

Definition at line 1239 of file satSolver3.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:

Here is the caller graph for this function:

sat_solver3_simplify()

int sat_solver3_simplify ( sat_solver3 * s )

extern

Definition at line 1478 of file satSolver3.c.

{
    assert(sat_solver3_dl(s) == 0);
    if (sat_solver3_propagate(s) != 0)
        return false;
    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver3_solve()

int sat_solver3_solve ( sat_solver3 * s, lit * begin, lit * end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal )

extern

Definition at line 2013 of file satSolver3.c.

{
    lbool status;
    lit * i;
    if ( s->fSolved )
        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_solver3_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_solver3_push(s, *i) )
        {
            sat_solver3_canceluntil(s,0);
            s->root_level = 0;
            return l_False;
        }
    assert(s->root_level == sat_solver3_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_solver3_decision(s, *i);
            if (sat_solver3_propagate(s) == 0)
                break;
            // fallthrough
        case var0: // l_False 
            sat_solver3_canceluntil(s, 0);
            return l_False;
        }
    }
    s->root_level = sat_solver3_dl(s);
#endif
 
    status = sat_solver3_solve_internal(s);
 
    sat_solver3_canceluntil(s,0);
    s->root_level = 0;
    return status;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver3_solve_internal()

int sat_solver3_solve_internal ( sat_solver3 * s )

extern

Definition at line 1896 of file satSolver3.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;
        double Ratio = (s->stats.learnts == 0)? 0.0 :
            s->stats.learnts_literals / (double)s->stats.learnts;
        if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
            break;
        if (s->verbosity >= 1)
        {
            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_solver3_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->verbosity >= 1)
        printf("==============================================================================\n");
 
    sat_solver3_canceluntil(s,s->root_level);
    return status;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver3_solve_lexsat()

int sat_solver3_solve_lexsat ( sat_solver3 * s, int * pLits, int nLits )

extern

Definition at line 2069 of file satSolver3.c.

{
    int i, iLitFail = -1;
    lbool status;
    assert( nLits > 0 );
    // help the SAT solver by setting desirable polarity
    sat_solver3_set_literal_polarity( s, pLits, nLits );
    // check if there exists a satisfying assignment
    status = sat_solver3_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_solver3_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_solver3_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_solver3_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_solver3_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_solver3_pop( s );
        pLits[iLitFail] = Abc_LitNot(pLits[iLitFail]);
        if ( !sat_solver3_push(s, pLits[iLitFail]) )
            printf( "sat_solver3_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_solver3_solve_lexsat( s, pLits + iLitFail + 1, nLits - iLitFail - 1 );
        else
            status = l_True;
    }
    // undo the assumptions
    for ( i = iLitFail; i >= 0; i-- )
        sat_solver3_pop( s );
    return status;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver3_store_alloc()

void sat_solver3_store_alloc ( sat_solver3 * s )

extern

sat_solver3_store_free()

void sat_solver3_store_free ( sat_solver3 * s )

extern

sat_solver3_store_mark_clauses_a()

void sat_solver3_store_mark_clauses_a ( sat_solver3 * s )

extern

sat_solver3_store_mark_roots()

void sat_solver3_store_mark_roots ( sat_solver3 * s )

extern

sat_solver3_store_release()

void * sat_solver3_store_release ( sat_solver3 * s )

extern

sat_solver3_store_write()

void sat_solver3_store_write ( sat_solver3 * s, char * pFileName )

extern

sat_solver3DoubleClauses()

void sat_solver3DoubleClauses ( sat_solver3 * p, int iVar )

extern

sat_solver3GetModel()

int * sat_solver3GetModel ( sat_solver3 * p, int * pVars, int nVars )

extern

sat_solver3PrintStats()

void sat_solver3PrintStats ( FILE * pFile, sat_solver3 * p )

extern

sat_solver3TraceStart()

void sat_solver3TraceStart ( sat_solver3 * pSat, char * pName )

extern

sat_solver3TraceStop()

void sat_solver3TraceStop ( sat_solver3 * pSat )

extern

sat_solver3TraceWrite()

void sat_solver3TraceWrite ( sat_solver3 * pSat, int * pBeg, int * pEnd, int fRoot )

extern

sat_solver3WriteDimacs()

void sat_solver3WriteDimacs ( sat_solver3 * p, char * pFileName, lit * assumptionsBegin, lit * assumptionsEnd, int incrementVars )

extern

zsat_solver3_new_seed()

sat_solver3 * zsat_solver3_new_seed ( double seed )

extern

Definition at line 1174 of file satSolver3.c.

{
    sat_solver3* s = (sat_solver3*)ABC_CALLOC( char, sizeof(sat_solver3));
 
//    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;
}

zsat_solver3_restart_seed()

void zsat_solver3_restart_seed ( sat_solver3 * s, double seed )

extern

Definition at line 1398 of file satSolver3.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;
}