xsat.h File Reference

#include "misc/util/abc_global.h"
#include "misc/vec/vecInt.h"

Include dependency graph for xsat.h:

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

Go to the source code of this file.

Typedefs
typedef struct xSAT_Solver_t_	xSAT_Solver_t

Functions
int	xSAT_SolverParseDimacs (FILE *, xSAT_Solver_t **)
	FUNCTION DECLARATIONS ///.
xSAT_Solver_t *	xSAT_SolverCreate ()
void	xSAT_SolverDestroy (xSAT_Solver_t *)
int	xSAT_SolverAddClause (xSAT_Solver_t *, Vec_Int_t *)
int	xSAT_SolverSimplify (xSAT_Solver_t *)
int	xSAT_SolverSolve (xSAT_Solver_t *)
void	xSAT_SolverPrintStats (xSAT_Solver_t *)

Typedef Documentation

xSAT_Solver_t

typedef struct xSAT_Solver_t_ xSAT_Solver_t

Definition at line 36 of file xsat.h.

Function Documentation

xSAT_SolverAddClause()

int xSAT_SolverAddClause ( xSAT_Solver_t * s, Vec_Int_t * vLits )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 251 of file xsatSolverAPI.c.

{
    int i, j;
    int Lit, PrevLit;
    int MaxVar;
 
    Vec_IntSort( vLits, 0 );
    MaxVar = xSAT_Lit2Var( Vec_IntEntryLast( vLits ) );
    while ( MaxVar >= Vec_IntSize( s->vActivity ) )
        xSAT_SolverAddVariable( s, 1 );
 
    j = 0;
    PrevLit = LitUndef;
    Vec_IntForEachEntry( vLits, Lit, i )
    {
        if ( Lit == xSAT_NegLit( PrevLit ) || Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lit ) ) == xSAT_LitSign( Lit ) )
            return true;
        else if ( Lit != PrevLit && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lit ) ) == VarX )
        {
            PrevLit = Lit;
            Vec_IntWriteEntry( vLits, j++, Lit );
        }
    }
    Vec_IntShrink( vLits, j );
 
    if ( Vec_IntSize( vLits ) == 0 )
        return false;
    if ( Vec_IntSize( vLits ) == 1 )
    {
        xSAT_SolverEnqueue( s, Vec_IntEntry( vLits, 0 ), CRefUndef );
        return ( xSAT_SolverPropagate( s ) == CRefUndef );
    }
 
    xSAT_SolverClaNew( s, vLits, 0 );
    return true;
}

Here is the call graph for this function:

xSAT_SolverCreate()

xSAT_Solver_t * xSAT_SolverCreate ( )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 66 of file xsatSolverAPI.c.

{
    xSAT_Solver_t * s = (xSAT_Solver_t *) ABC_CALLOC( char, sizeof( xSAT_Solver_t ) );
    s->Config = DefaultConfig;
 
    s->pMemory = xSAT_MemAlloc(0);
    s->vClauses = Vec_IntAlloc(0);
    s->vLearnts = Vec_IntAlloc(0);
    s->vWatches = xSAT_VecWatchListAlloc( 0 );
    s->vBinWatches = xSAT_VecWatchListAlloc( 0 );
 
    s->vTrailLim = Vec_IntAlloc(0);
    s->vTrail = Vec_IntAlloc( 0 );
 
    s->vActivity = Vec_IntAlloc( 0 );
    s->hOrder = xSAT_HeapAlloc( s->vActivity );
 
    s->vPolarity = Vec_StrAlloc( 0 );
    s->vTags = Vec_StrAlloc( 0 );
    s->vAssigns = Vec_StrAlloc( 0 );
    s->vLevels = Vec_IntAlloc( 0 );
    s->vReasons = Vec_IntAlloc( 0 );
    s->vStamp = Vec_IntAlloc( 0 );
 
    s->vTagged = Vec_IntAlloc(0);
    s->vStack  = Vec_IntAlloc(0);
 
    s->vSeen = Vec_StrAlloc( 0 );
    s->vLearntClause = Vec_IntAlloc(0);
    s->vLastDLevel = Vec_IntAlloc(0);
 
 
    s->bqTrail = xSAT_BQueueNew( s->Config.nSizeTrailQueue );
    s->bqLBD = xSAT_BQueueNew( s->Config.nSizeLBDQueue );
 
    s->nVarActInc = (1 <<  5);
    s->nClaActInc = (1 << 11);
 
    s->nConfBeforeReduce = s->Config.nConfFirstReduce;
    s->nRC1 = 1;
    s->nRC2 = s->Config.nConfFirstReduce;
    return s;
}

xSAT_SolverDestroy()

void xSAT_SolverDestroy ( xSAT_Solver_t * s )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 121 of file xsatSolverAPI.c.

{
    xSAT_MemFree( s->pMemory );
    Vec_IntFree( s->vClauses );
    Vec_IntFree( s->vLearnts );
    xSAT_VecWatchListFree( s->vWatches );
    xSAT_VecWatchListFree( s->vBinWatches );
 
    xSAT_HeapFree(s->hOrder);
    Vec_IntFree( s->vTrailLim );
    Vec_IntFree( s->vTrail );
    Vec_IntFree( s->vTagged );
    Vec_IntFree( s->vStack );
 
    Vec_StrFree( s->vSeen );
    Vec_IntFree( s->vLearntClause );
    Vec_IntFree( s->vLastDLevel );
 
    Vec_IntFree( s->vActivity );
    Vec_StrFree( s->vPolarity );
    Vec_StrFree( s->vTags );
    Vec_StrFree( s->vAssigns );
    Vec_IntFree( s->vLevels );
    Vec_IntFree( s->vReasons );
    Vec_IntFree( s->vStamp );
 
    xSAT_BQueueFree(s->bqLBD);
    xSAT_BQueueFree(s->bqTrail);
 
    ABC_FREE(s);
}

xSAT_SolverParseDimacs()

int xSAT_SolverParseDimacs ( FILE * pFile, xSAT_Solver_t ** p )

extern

FUNCTION DECLARATIONS ///.

Function*************************************************************

Synopsis [Starts the solver and reads the DIMAC file.]

Description [Returns FALSE upon immediate conflict.]

SideEffects []

SeeAlso []

Definition at line 222 of file xsatCnfReader.c.

{
    char * pText;
    int  Value;
    pText = xSAT_FileRead( pFile );
    Value = xSAT_ParseDimacs( pText, p );
    ABC_FREE( pText );
    return Value;
}

Here is the call graph for this function:

xSAT_SolverPrintStats()

void xSAT_SolverPrintStats ( xSAT_Solver_t * s )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 338 of file xsatSolverAPI.c.

{
    printf( "starts        : %10d\n", s->Stats.nStarts );
    printf( "conflicts     : %10ld\n", s->Stats.nConflicts );
    printf( "decisions     : %10ld\n", s->Stats.nDecisions );
    printf( "propagations  : %10ld\n", s->Stats.nPropagations );
}

xSAT_SolverSimplify()

int xSAT_SolverSimplify ( xSAT_Solver_t * s )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 164 of file xsatSolverAPI.c.

{
    int i, j;
    unsigned CRef;
    assert( xSAT_SolverDecisionLevel(s) == 0 );
 
    if ( xSAT_SolverPropagate(s) != CRefUndef )
        return false;
 
    if ( s->nAssignSimplify == Vec_IntSize( s->vTrail ) || s->nPropSimplify > 0 )
        return true;
 
    j = 0;
    Vec_IntForEachEntry( s->vClauses, CRef, i )
    {
        xSAT_Clause_t * pCla = xSAT_SolverReadClause( s, CRef );
        if ( xSAT_SolverIsClauseSatisfied( s, pCla ) )
        {
            pCla->fMark = 1;
            s->Stats.nClauseLits -= pCla->nSize;
 
            if ( pCla->nSize == 2 )
            {
                xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vBinWatches, xSAT_NegLit(pCla->pData[0].Lit) ), CRef );
                xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vBinWatches, xSAT_NegLit(pCla->pData[1].Lit) ), CRef );
            }
            else
            {
                xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit(pCla->pData[0].Lit) ), CRef );
                xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit(pCla->pData[1].Lit) ), CRef );
            }
        }
        else
            Vec_IntWriteEntry( s->vClauses, j++, CRef );
    }
    Vec_IntShrink( s->vClauses, j );
    xSAT_SolverRebuildOrderHeap( s );
 
    s->nAssignSimplify = Vec_IntSize( s->vTrail );
    s->nPropSimplify = s->Stats.nClauseLits + s->Stats.nLearntLits;
 
    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

xSAT_SolverSolve()

int xSAT_SolverSolve ( xSAT_Solver_t * s )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 299 of file xsatSolverAPI.c.

{
    char status = LBoolUndef;
 
    assert(s);
    if ( s->Config.fVerbose )
    {
        printf( "==========================================[ BLACK MAGIC ]================================================\n" );
        printf( "|                                |                                |                                     |\n" );
        printf( "| - Restarts:                    | - Reduce Clause DB:            | - Minimize Asserting:               |\n" );
        printf( "|   * LBD Queue    : %6d      |   * First     : %6d         |    * size < %3d                     |\n",       s->Config.nSizeLBDQueue, s->Config.nConfFirstReduce, 0 );
        printf( "|   * Trail Queue  : %6d      |   * Inc       : %6d         |    * lbd  < %3d                     |\n",       s->Config.nSizeTrailQueue, s->Config.nIncReduce, 0 );
        printf( "|   * K            : %6.2f      |   * Special   : %6d         |                                     |\n",     s->Config.K, s->Config.nSpecialIncReduce );
        printf( "|   * R            : %6.2f      |   * Protected :  (lbd)< %2d     |                                     |\n", s->Config.R, s->Config.nLBDFrozenClause );
        printf( "|                                |                                |                                     |\n" );
        printf( "=========================================================================================================\n" );
    }
 
    while ( status == LBoolUndef )
        status = xSAT_SolverSearch( s );
 
    if ( s->Config.fVerbose )
        printf( "=========================================================================================================\n" );
 
    xSAT_SolverCancelUntil( s, 0 );
    return status;
}

Here is the call graph for this function: