luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
abc/src/sat/xsat/xsatSolverAPI.c

347 lines
10 KiB
C
Raw Blame History

/**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 =
{
1, //.fVerbose = 1,
0, //.nConfLimit = 0,
0, //.nInsLimit = 0,
0, //.nRuntimeLimit = 0,
0.8, //.K = 0.8,
1.4, //.R = 1.4,
10000, //.nFirstBlockRestart = 10000,
50, //.nSizeLBDQueue = 50,
5000, //.nSizeTrailQueue = 5000,
2000, //.nConfFirstReduce = 2000,
300, //.nIncReduce = 300,
1000, //.nSpecialIncReduce = 1000,
30 //.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 );
Vec_IntFree( s->vStamp );
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;
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;
}
/**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
Reference in New Issue View Git Blame Copy Permalink