diff options
Diffstat (limited to 'src/sat/xsat/xsatSolverAPI.c')
| -rw-r--r-- | src/sat/xsat/xsatSolverAPI.c | 345 |
1 files changed, 345 insertions, 0 deletions
diff --git a/src/sat/xsat/xsatSolverAPI.c b/src/sat/xsat/xsatSolverAPI.c new file mode 100644 index 00000000..7ee817ee --- /dev/null +++ b/src/sat/xsat/xsatSolverAPI.c @@ -0,0 +1,345 @@ +/**CFile**************************************************************** + + FileName [xsatSolverAPI.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [xSAT - A SAT solver written in C. + Read the license file for more info.] + + Synopsis [Solver external API functions implementation.] + + Author [Bruno Schmitt <boschmitt@inf.ufrgs.br>] + + Affiliation [UC Berkeley / UFRGS] + + Date [Ver. 1.0. Started - November 10, 2016.] + + Revision [] + +***********************************************************************/ +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// +#include <stdio.h> +#include <assert.h> +#include <string.h> +#include <math.h> + +#include "xsatSolver.h" + +ABC_NAMESPACE_IMPL_START + +xSAT_SolverOptions_t DefaultConfig = +{ + .fVerbose = 1, + + .nConfLimit = 0, + .nInsLimit = 0, + .nRuntimeLimit = 0, + + .K = 0.8, + .R = 1.4, + .nFirstBlockRestart = 10000, + .nSizeLBDQueue = 50, + .nSizeTrailQueue = 5000, + + .nConfFirstReduce = 2000, + .nIncReduce = 300, + .nSpecialIncReduce = 1000, + + .nLBDFrozenClause = 30 +}; + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +xSAT_Solver_t* xSAT_SolverCreate() +{ + 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; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void xSAT_SolverDestroy( xSAT_Solver_t * s ) +{ + xSAT_MemFree( s->pMemory ); + Vec_IntFree( s->vClauses ); + Vec_IntFree( s->vLearnts ); + xSAT_VecWatchListFree( s->vWatches ); + xSAT_VecWatchListFree( s->vBinWatches ); + + // delete vectors + 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 ); + + xSAT_BQueueFree(s->bqLBD); + xSAT_BQueueFree(s->bqTrail); + + ABC_FREE(s); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int xSAT_SolverSimplify( xSAT_Solver_t * s ) +{ + int i, j; + uint32_t 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; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void xSAT_SolverAddVariable( xSAT_Solver_t* s, int Sign ) +{ + int Var = Vec_IntSize( s->vActivity ); + + xSAT_VecWatchListPush( s->vWatches ); + xSAT_VecWatchListPush( s->vWatches ); + xSAT_VecWatchListPush( s->vBinWatches ); + xSAT_VecWatchListPush( s->vBinWatches ); + + Vec_IntPush( s->vActivity, 0 ); + Vec_IntPush( s->vLevels, 0 ); + Vec_StrPush( s->vAssigns, VarX ); + Vec_StrPush( s->vPolarity, 1 ); + Vec_StrPush( s->vTags, 0 ); + Vec_IntPush( s->vReasons, ( int ) CRefUndef ); + Vec_IntPush( s->vStamp, 0 ); + Vec_StrPush( s->vSeen, 0 ); + + xSAT_HeapInsert( s->hOrder, Var ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int xSAT_SolverAddClause( xSAT_Solver_t * s, Vec_Int_t * vLits ) +{ + 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; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int xSAT_SolverSolve( xSAT_Solver_t* s ) +{ + 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; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void xSAT_SolverPrintStats( xSAT_Solver_t * s ) +{ + 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 ); +} + +ABC_NAMESPACE_IMPL_END |