xsatSolver.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/util/abc_global.h"
#include "misc/vec/vecStr.h"
#include "xsat.h"
#include "xsatBQueue.h"
#include "xsatClause.h"
#include "xsatHeap.h"
#include "xsatMemory.h"
#include "xsatWatchList.h"

Include dependency graph for xsatSolver.h:

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

Go to the source code of this file.

Classes
struct	xSAT_SolverOptions_t_
struct	xSAT_Stats_t_
struct	xSAT_Solver_t_

Macros
#define	false   0
	INCLUDES ///.
#define	true   1
#define	CRefUndef   0xFFFFFFFF

Typedefs
typedef struct xSAT_SolverOptions_t_	xSAT_SolverOptions_t
	STRUCTURE DEFINITIONS ///.
typedef struct xSAT_Stats_t_	xSAT_Stats_t

Enumerations
enum	{ Var0 = 1 , Var1 = 0 , VarX = 3 }
enum	{ LBoolUndef = 0 , LBoolTrue = 1 , LBoolFalse = -1 }
enum	{ VarUndef = -1 , LitUndef = -2 }

Functions
unsigned	xSAT_SolverClaNew (xSAT_Solver_t *s, Vec_Int_t *vLits, int fLearnt)
	FUNCTION DECLARATIONS ///.
char	xSAT_SolverSearch (xSAT_Solver_t *s)
void	xSAT_SolverGarbageCollect (xSAT_Solver_t *s)
int	xSAT_SolverEnqueue (xSAT_Solver_t *s, int Lit, unsigned From)
void	xSAT_SolverCancelUntil (xSAT_Solver_t *s, int Level)
unsigned	xSAT_SolverPropagate (xSAT_Solver_t *s)
void	xSAT_SolverRebuildOrderHeap (xSAT_Solver_t *s)

Macro Definition Documentation

CRefUndef

#define CRefUndef   0xFFFFFFFF

Definition at line 73 of file xsatSolver.h.

false

#define false   0

INCLUDES ///.

CFile****************************************************************

FileName [xsatSolver.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [xSAT - A SAT solver written in C. Read the license file for more info.]

Synopsis [Internal definitions of the solver.]

Author [Bruno Schmitt bosch.nosp@m.mitt.nosp@m.@inf..nosp@m.ufrg.nosp@m.s.br]

Affiliation [UC Berkeley / UFRGS]

Date [Ver. 1.0. Started - November 10, 2016.]

Revision []

Definition at line 46 of file xsatSolver.h.

true

#define true   1

Definition at line 49 of file xsatSolver.h.

Typedef Documentation

xSAT_SolverOptions_t

typedef struct xSAT_SolverOptions_t_ xSAT_SolverOptions_t

STRUCTURE DEFINITIONS ///.

Definition at line 78 of file xsatSolver.h.

xSAT_Stats_t

typedef struct xSAT_Stats_t_ xSAT_Stats_t

Definition at line 102 of file xsatSolver.h.

Enumeration Type Documentation

anonymous enum

anonymous enum

Enumerator
VarUndef
LitUndef

Definition at line 67 of file xsatSolver.h.

{
    VarUndef = -1,
    LitUndef = -2
};

anonymous enum

anonymous enum

Enumerator
LBoolUndef
LBoolTrue
LBoolFalse

Definition at line 60 of file xsatSolver.h.

{
    LBoolUndef =  0,
    LBoolTrue  =  1,
    LBoolFalse = -1
};

anonymous enum

anonymous enum

Enumerator
Var0
Var1
VarX

Definition at line 53 of file xsatSolver.h.

{
    Var0 = 1,
    Var1 = 0,
    VarX = 3
};

Function Documentation

xSAT_SolverCancelUntil()

void xSAT_SolverCancelUntil ( xSAT_Solver_t * s, int Level )

extern

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 )

extern

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_SolverEnqueue()

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

extern

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 )

extern

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 )

extern

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 )

extern

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_SolverSearch()

char xSAT_SolverSearch ( xSAT_Solver_t * s )

extern

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: