xsatSolver.c File Reference

#include <stdio.h>
#include <assert.h>
#include <string.h>
#include <math.h>
#include "xsatHeap.h"
#include "xsatSolver.h"
#include "xsatUtils.h"

Include dependency graph for xsatSolver.c:

Go to the source code of this file.

Functions
void	xSAT_SolverRebuildOrderHeap (xSAT_Solver_t *s)
unsigned	xSAT_SolverClaNew (xSAT_Solver_t *s, Vec_Int_t *vLits, int fLearnt)
	FUNCTION DECLARATIONS ///.
int	xSAT_SolverEnqueue (xSAT_Solver_t *s, int Lit, unsigned Reason)
void	xSAT_SolverCancelUntil (xSAT_Solver_t *s, int Level)
unsigned	xSAT_SolverPropagate (xSAT_Solver_t *s)
void	xSAT_SolverReduceDB (xSAT_Solver_t *s)
char	xSAT_SolverSearch (xSAT_Solver_t *s)
void	xSAT_SolverClaRealloc (xSAT_Mem_t *pDest, xSAT_Mem_t *pSrc, unsigned *pCRef)
void	xSAT_SolverGarbageCollect (xSAT_Solver_t *s)

Function Documentation

xSAT_SolverCancelUntil()

void xSAT_SolverCancelUntil	(	xSAT_Solver_t *	s,
		int	Level )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 375 of file xsatSolver.c.

{
    int c;
 
    if ( xSAT_SolverDecisionLevel( s ) <= Level )
        return;
 
    for ( c = Vec_IntSize( s->vTrail ) - 1; c >= Vec_IntEntry( s->vTrailLim, Level ); c-- )
    {
        int Var = xSAT_Lit2Var( Vec_IntEntry( s->vTrail, c ) );
 
        Vec_StrWriteEntry( s->vAssigns, Var, VarX );
        Vec_IntWriteEntry( s->vReasons, Var, ( int ) CRefUndef );
        Vec_StrWriteEntry( s->vPolarity, Var, ( char )xSAT_LitSign( Vec_IntEntry( s->vTrail, c ) ) );
 
        if ( !xSAT_HeapInHeap( s->hOrder, Var ) )
            xSAT_HeapInsert( s->hOrder, Var );
    }
 
    s->iQhead = Vec_IntEntry( s->vTrailLim, Level );
    Vec_IntShrink( s->vTrail, Vec_IntEntry( s->vTrailLim, Level ) );
    Vec_IntShrink( s->vTrailLim, Level );
}

Here is the caller graph for this function:

xSAT_SolverClaNew()

unsigned xSAT_SolverClaNew	(	xSAT_Solver_t *	s,
		Vec_Int_t *	vLits,
		int	fLearnt )

FUNCTION DECLARATIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 269 of file xsatSolver.c.

{
    unsigned CRef;
    xSAT_Clause_t * pCla;
    xSAT_Watcher_t w1;
    xSAT_Watcher_t w2;
    unsigned nWords;
 
    assert( Vec_IntSize( vLits ) > 1);
    assert( fLearnt == 0 || fLearnt == 1 );
 
    nWords = 3 + fLearnt + Vec_IntSize( vLits );
    CRef = xSAT_MemAppend( s->pMemory, nWords );
    pCla = xSAT_SolverReadClause( s, CRef );
    pCla->fLearnt = fLearnt;
    pCla->fMark = 0;
    pCla->fReallocd = 0;
    pCla->fCanBeDel = fLearnt;
    pCla->nSize = Vec_IntSize( vLits );
    memcpy( &( pCla->pData[0].Lit ), Vec_IntArray( vLits ), sizeof( int ) * Vec_IntSize( vLits ) );
 
    if ( fLearnt )
    {
        Vec_IntPush( s->vLearnts, CRef );
        pCla->nLBD = xSAT_SolverClaCalcLBD2( s, vLits );
        pCla->pData[pCla->nSize].Act = 0;
        s->Stats.nLearntLits += Vec_IntSize( vLits );
        xSAT_SolverClaActBump(s, pCla);
    }
    else
    {
        Vec_IntPush( s->vClauses, CRef );
        s->Stats.nClauseLits += Vec_IntSize( vLits );
    }
 
    w1.CRef = CRef;
    w2.CRef = CRef;
    w1.Blocker = pCla->pData[1].Lit;
    w2.Blocker = pCla->pData[0].Lit;
 
    if ( Vec_IntSize( vLits ) == 2 )
    {
        xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vBinWatches, xSAT_NegLit( pCla->pData[0].Lit ) ), w1 );
        xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vBinWatches, xSAT_NegLit( pCla->pData[1].Lit ) ), w2 );
    }
    else
    {
        xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( pCla->pData[0].Lit ) ), w1 );
        xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( pCla->pData[1].Lit ) ), w2 );
    }
    return CRef;
}

Here is the call graph for this function:

Here is the caller graph for this function:

xSAT_SolverClaRealloc()

void xSAT_SolverClaRealloc	(	xSAT_Mem_t *	pDest,
		xSAT_Mem_t *	pSrc,
		unsigned *	pCRef )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 934 of file xsatSolver.c.

{
    unsigned nNewCRef;
    xSAT_Clause_t * pNewCla;
    xSAT_Clause_t * pOldCla = xSAT_MemClauseHand( pSrc, *pCRef );
 
    if ( pOldCla->fReallocd )
    {
        *pCRef = ( unsigned ) pOldCla->nSize;
        return;
    }
    nNewCRef = xSAT_MemAppend( pDest, 3 + pOldCla->fLearnt + pOldCla->nSize );
    pNewCla = xSAT_MemClauseHand( pDest, nNewCRef );
    memcpy( pNewCla, pOldCla, (size_t)(( 3 + pOldCla->fLearnt + pOldCla->nSize ) * 4) );
    pOldCla->fReallocd = 1;
    pOldCla->nSize = ( unsigned ) nNewCRef;
    *pCRef = nNewCRef;
}

Here is the call graph for this function:

Here is the caller graph for this function:

xSAT_SolverEnqueue()

int xSAT_SolverEnqueue	(	xSAT_Solver_t *	s,
		int	Lit,
		unsigned	Reason )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 333 of file xsatSolver.c.

{
    int Var = xSAT_Lit2Var( Lit );
 
    Vec_StrWriteEntry( s->vAssigns, Var, (char)xSAT_LitSign( Lit ) );
    Vec_IntWriteEntry( s->vLevels, Var, xSAT_SolverDecisionLevel( s ) );
    Vec_IntWriteEntry( s->vReasons, Var, ( int ) Reason );
    Vec_IntPush( s->vTrail, Lit );
 
    return true;
}

Here is the caller graph for this function:

xSAT_SolverGarbageCollect()

void xSAT_SolverGarbageCollect

(

xSAT_Solver_t *

s

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 964 of file xsatSolver.c.

{
    int i;
    unsigned * pArray;
    xSAT_Mem_t * pNewMemMngr = xSAT_MemAlloc(  xSAT_MemCap( s->pMemory ) - xSAT_MemWastedCap( s->pMemory ) );
 
    for ( i = 0; i < 2 * Vec_StrSize( s->vAssigns ); i++ )
    {
        xSAT_WatchList_t* ws = xSAT_VecWatchListEntry( s->vWatches, i);
        xSAT_Watcher_t* begin = xSAT_WatchListArray(ws);
        xSAT_Watcher_t* end   = begin + xSAT_WatchListSize(ws);
        xSAT_Watcher_t *w;
 
        for ( w = begin; w != end; w++ )
            xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(w->CRef) );
 
        ws = xSAT_VecWatchListEntry( s->vBinWatches, i);
        begin = xSAT_WatchListArray(ws);
        end   = begin + xSAT_WatchListSize(ws);
        for ( w = begin; w != end; w++ )
            xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(w->CRef) );
    }
 
    for ( i = 0; i < Vec_IntSize( s->vTrail ); i++ )
        if ( ( unsigned ) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) ) ) != CRefUndef )
            xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, ( unsigned * ) &( Vec_IntArray( s->vReasons )[xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) )] ) );
 
    pArray = ( unsigned * ) Vec_IntArray( s->vLearnts );
    for ( i = 0; i < Vec_IntSize( s->vLearnts ); i++ )
        xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(pArray[i]) );
 
    pArray = ( unsigned * ) Vec_IntArray( s->vClauses );
    for ( i = 0; i < Vec_IntSize( s->vClauses ); i++ )
        xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(pArray[i]) );
 
    xSAT_MemFree( s->pMemory );
    s->pMemory = pNewMemMngr;
}

Here is the call graph for this function:

Here is the caller graph for this function:

xSAT_SolverPropagate()

unsigned xSAT_SolverPropagate

(

xSAT_Solver_t *

s

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 665 of file xsatSolver.c.

{
    unsigned hConfl = CRefUndef;
    int * Lits;
    int NegLit;
    int nProp = 0;
 
    while ( s->iQhead < Vec_IntSize( s->vTrail ) )
    {
        int p = Vec_IntEntry( s->vTrail, s->iQhead++ );
        xSAT_WatchList_t* ws = xSAT_VecWatchListEntry( s->vBinWatches, p );
        xSAT_Watcher_t* begin = xSAT_WatchListArray( ws );
        xSAT_Watcher_t* end   = begin + xSAT_WatchListSize( ws );
        xSAT_Watcher_t *i, *j;
 
        nProp++;
        for ( i = begin; i < end; i++ )
        {
            if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == VarX )
                xSAT_SolverEnqueue( s, i->Blocker, i->CRef );
            else if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == xSAT_LitSign( xSAT_NegLit( i->Blocker ) ) )
                return i->CRef;
        }
 
        ws    = xSAT_VecWatchListEntry( s->vWatches, p );
        begin = xSAT_WatchListArray( ws );
        end   = begin + xSAT_WatchListSize( ws );
 
        for ( i = j = begin; i < end; )
        {
            xSAT_Clause_t * pCla;
            xSAT_Watcher_t w;
            if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == xSAT_LitSign( i->Blocker ) )
            {
                *j++ = *i++;
                continue;
            }
 
            pCla = xSAT_SolverReadClause( s, i->CRef );
            Lits = &( pCla->pData[0].Lit );
 
            // Make sure the false literal is data[1]:
            NegLit = xSAT_NegLit( p );
            if ( Lits[0] == NegLit )
            {
                Lits[0] = Lits[1];
                Lits[1] = NegLit;
            }
            assert( Lits[1] == NegLit );
 
            w.CRef = i->CRef;
            w.Blocker = Lits[0];
 
            // If 0th watch is true, then clause is already satisfied.
            if ( Lits[0] != i->Blocker && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( Lits[0] ) )
                *j++ = w;
            else
            {
                // Look for new watch:
                int * stop = Lits + pCla->nSize;
                int * k;
                for ( k = Lits + 2; k < stop; k++ )
                {
                    if (Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( *k ) ) != !xSAT_LitSign( *k ) )
                    {
                        Lits[1] = *k;
                        *k = NegLit;
                        xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( Lits[1] ) ), w );
                        goto next;
                    }
                }
 
                *j++ = w;
 
                // Clause is unit under assignment:
                if (Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) )
                {
                    hConfl = i->CRef;
                    i++;
                    s->iQhead = Vec_IntSize( s->vTrail );
                    // Copy the remaining watches:
                    while (i < end)
                        *j++ = *i++;
                }
                else
                    xSAT_SolverEnqueue( s, Lits[0], i->CRef );
            }
        next:
            i++;
        }
 
        s->Stats.nInspects += j - xSAT_WatchListArray( ws );
        xSAT_WatchListShrink( ws, j - xSAT_WatchListArray( ws ) );
    }
 
    s->Stats.nPropagations += nProp;
    s->nPropSimplify -= nProp;
 
    return hConfl;
}

Here is the call graph for this function:

Here is the caller graph for this function:

xSAT_SolverRebuildOrderHeap()

void xSAT_SolverRebuildOrderHeap

(

xSAT_Solver_t *

s

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file xsatSolver.c.

{
    Vec_Int_t * vTemp = Vec_IntAlloc( Vec_StrSize( s->vAssigns ) );
    int Var;
 
    for ( Var = 0; Var < Vec_StrSize( s->vAssigns ); Var++ )
        if ( Vec_StrEntry( s->vAssigns, Var ) == VarX )
            Vec_IntPush( vTemp, Var );
 
    xSAT_HeapBuild( s->hOrder, vTemp );
    Vec_IntFree( vTemp );
}

Here is the caller graph for this function:

xSAT_SolverReduceDB()

void xSAT_SolverReduceDB

(

xSAT_Solver_t *

s

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 777 of file xsatSolver.c.

{
    static abctime TimeTotal = 0;
    abctime clk = Abc_Clock();
    int nLearnedOld = Vec_IntSize( s->vLearnts );
    int i, limit;
    unsigned CRef;
    xSAT_Clause_t * pCla;
    xSAT_Clause_t ** learnts_cls;
 
    learnts_cls = ABC_ALLOC( xSAT_Clause_t *, nLearnedOld );
    Vec_IntForEachEntry( s->vLearnts, CRef, i )
        learnts_cls[i] = xSAT_SolverReadClause(s, CRef);
 
    limit = nLearnedOld / 2;
 
    xSAT_UtilSort((void **) learnts_cls, nLearnedOld,
                  (int (*)( const void *, const void * )) xSAT_ClauseCompare);
 
    if ( learnts_cls[nLearnedOld / 2]->nLBD <= 3 )
        s->nRC2 += s->Config.nSpecialIncReduce;
    if ( learnts_cls[nLearnedOld - 1]->nLBD <= 5 )
        s->nRC2 += s->Config.nSpecialIncReduce;
 
    Vec_IntClear( s->vLearnts );
    for ( i = 0; i < nLearnedOld; i++ )
    {
        unsigned CRef;
 
        pCla = learnts_cls[i];
        CRef = xSAT_MemCRef( s->pMemory, ( unsigned * ) pCla );
        assert( pCla->fMark == 0 );
        if ( pCla->fCanBeDel && pCla->nLBD > 2 && pCla->nSize > 2 && (unsigned) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( pCla->pData[0].Lit ) ) != CRef && ( i < limit ) )
        {
            pCla->fMark = 1;
            s->Stats.nLearntLits -= pCla->nSize;
            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
        {
            if ( !pCla->fCanBeDel )
                limit++;
            pCla->fCanBeDel = 1;
            Vec_IntPush( s->vLearnts, CRef );
        }
    }
    ABC_FREE( learnts_cls );
 
    TimeTotal += Abc_Clock() - clk;
    if ( s->Config.fVerbose )
    {
        Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%)  ",
            Vec_IntSize( s->vLearnts ), nLearnedOld, 100.0 * Vec_IntSize( s->vLearnts ) / nLearnedOld );
        Abc_PrintTime( 1, "Time", TimeTotal );
    }
    xSAT_SolverGarbageCollect(s);
}

Here is the call graph for this function:

Here is the caller graph for this function:

xSAT_SolverSearch()

char xSAT_SolverSearch

(

xSAT_Solver_t *

s

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 847 of file xsatSolver.c.

{
    iword conflictC  = 0;
 
    s->Stats.nStarts++;
    for (;;)
    {
        unsigned hConfl = xSAT_SolverPropagate( s );
 
        if ( hConfl != CRefUndef )
        {
            /* Conflict */
            int BacktrackLevel;
            unsigned nLBD;
            unsigned CRef;
 
            s->Stats.nConflicts++;
            conflictC++;
 
            if ( xSAT_SolverDecisionLevel( s ) == 0 )
                return LBoolFalse;
 
            xSAT_BQueuePush( s->bqTrail, Vec_IntSize( s->vTrail ) );
            if ( s->Stats.nConflicts > s->Config.nFirstBlockRestart && xSAT_BQueueIsValid( s->bqLBD ) && ( Vec_IntSize( s->vTrail ) > ( s->Config.R * ( iword ) xSAT_BQueueAvg( s->bqTrail ) ) ) )
                xSAT_BQueueClean(s->bqLBD);
 
            Vec_IntClear( s->vLearntClause );
            xSAT_SolverAnalyze( s, hConfl, s->vLearntClause, &BacktrackLevel, &nLBD );
 
            s->nSumLBD += nLBD;
            xSAT_BQueuePush( s->bqLBD, nLBD );
            xSAT_SolverCancelUntil( s, BacktrackLevel );
 
            CRef = Vec_IntSize( s->vLearntClause ) == 1 ? CRefUndef : xSAT_SolverClaNew( s, s->vLearntClause , 1 );
            xSAT_SolverEnqueue( s, Vec_IntEntry( s->vLearntClause , 0 ), CRef );
 
            xSAT_SolverVarActDecay( s );
            xSAT_SolverClaActDecay( s );
        }
        else
        {
            /* No conflict */
            int NextVar;
            if ( xSAT_BQueueIsValid( s->bqLBD ) && ( ( ( iword )xSAT_BQueueAvg( s->bqLBD ) * s->Config.K ) > ( s->nSumLBD / s->Stats.nConflicts ) ) )
            {
                xSAT_BQueueClean( s->bqLBD );
                xSAT_SolverCancelUntil( s, 0 );
                return LBoolUndef;
            }
 
            // Simplify the set of problem clauses:
            if ( xSAT_SolverDecisionLevel( s ) == 0 )
                xSAT_SolverSimplify( s );
 
            // Reduce the set of learnt clauses:
            if ( s->Stats.nConflicts >= s->nConfBeforeReduce )
            {
                s->nRC1 = ( s->Stats.nConflicts / s->nRC2 ) + 1;
                xSAT_SolverReduceDB(s);
                s->nRC2 += s->Config.nIncReduce;
                s->nConfBeforeReduce = s->nRC1 * s->nRC2;
            }
 
            // New variable decision:
            NextVar = xSAT_SolverDecide( s );
 
            if ( NextVar == VarUndef )
                return LBoolTrue;
 
            xSAT_SolverNewDecision( s, xSAT_Var2Lit( NextVar, ( int ) Vec_StrEntry( s->vPolarity, NextVar ) ) );
        }
    }
 
    return LBoolUndef; // cannot happen
}

Here is the call graph for this function:

Here is the caller graph for this function: