diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
commit | 4812c90424dfc40d26725244723887a2d16ddfd9 (patch) | |
tree | b32ace96e7e2d84d586e09ba605463b6f49c3271 /src/sat/msat/msatClause.c | |
parent | e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (diff) | |
download | abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.gz abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.bz2 abc-4812c90424dfc40d26725244723887a2d16ddfd9.zip |
Version abc71001
Diffstat (limited to 'src/sat/msat/msatClause.c')
-rw-r--r-- | src/sat/msat/msatClause.c | 529 |
1 files changed, 529 insertions, 0 deletions
diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c new file mode 100644 index 00000000..2ba8cd32 --- /dev/null +++ b/src/sat/msat/msatClause.c @@ -0,0 +1,529 @@ +/**CFile**************************************************************** + + FileName [msatClause.c] + + PackageName [A C version of SAT solver MINISAT, originally developed + in C++ by Niklas Een and Niklas Sorensson, Chalmers University of + Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] + + Synopsis [Procedures working with SAT clauses.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - January 1, 2004.] + + Revision [$Id: msatClause.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "msatInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +struct Msat_Clause_t_ +{ + int Num; // unique number of the clause + unsigned fLearned : 1; // 1 if the clause is learned + unsigned fMark : 1; // used to mark visited clauses during proof recording + unsigned fTypeA : 1; // used to mark clauses belonging to A for interpolant computation + unsigned nSize : 14; // the number of literals in the clause + unsigned nSizeAlloc : 15; // the number of bytes allocated for the clause + Msat_Lit_t pData[0]; +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates a new clause.] + + Description [Returns FALSE if top-level conflict detected (must be handled); + TRUE otherwise. 'pClause_out' may be set to NULL if clause is already + satisfied by the top-level assignment.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, Msat_Clause_t ** pClause_out ) +{ + int * pAssigns = Msat_SolverReadAssignsArray(p); + Msat_ClauseVec_t ** pvWatched; + Msat_Clause_t * pC; + int * pLits; + int nLits, i, j; + int nBytes; + Msat_Var_t Var; + bool Sign; + + *pClause_out = NULL; + + nLits = Msat_IntVecReadSize(vLits); + pLits = Msat_IntVecReadArray(vLits); + + if ( !fLearned ) + { + int * pSeen = Msat_SolverReadSeenArray( p ); + int nSeenId; + assert( Msat_SolverReadDecisionLevel(p) == 0 ); + // sorting literals makes the code trace-equivalent + // with to the original C++ solver + Msat_IntVecSort( vLits, 0 ); + // increment the counter of seen twice + nSeenId = Msat_SolverIncrementSeenId( p ); + nSeenId = Msat_SolverIncrementSeenId( p ); + // nSeenId - 1 stands for negative + // nSeenId stands for positive + // Remove false literals + + // there is a bug here!!!! + // when the same var in opposite polarities is given, it drops one polarity!!! + + for ( i = j = 0; i < nLits; i++ ) { + // get the corresponding variable + Var = MSAT_LIT2VAR(pLits[i]); + Sign = MSAT_LITSIGN(pLits[i]); // Sign=0 for positive + // check if we already saw this variable in the this clause + if ( pSeen[Var] >= nSeenId - 1 ) + { + if ( (pSeen[Var] != nSeenId) == Sign ) // the same lit + continue; + return 1; // two opposite polarity lits -- don't add the clause + } + // mark the variable as seen + pSeen[Var] = nSeenId - !Sign; + + // analize the value of this literal + if ( pAssigns[Var] != MSAT_VAR_UNASSIGNED ) + { + if ( pAssigns[Var] == pLits[i] ) + return 1; // the clause is always true -- don't add anything + // the literal has no impact - skip it + continue; + } + // otherwise, add this literal to the clause + pLits[j++] = pLits[i]; + } + Msat_IntVecShrink( vLits, j ); + nLits = j; +/* + // the problem with this code is that performance is very + // sensitive to the ordering of adjacency lits + // the best ordering requires fanins first, next fanouts + // this ordering is more convenient to make from FRAIG + + // create the adjacency information + if ( nLits > 2 ) + { + Msat_Var_t VarI, VarJ; + Msat_IntVec_t * pAdjI, * pAdjJ; + + for ( i = 0; i < nLits; i++ ) + { + VarI = MSAT_LIT2VAR(pLits[i]); + pAdjI = (Msat_IntVec_t *)p->vAdjacents->pArray[VarI]; + + for ( j = i+1; j < nLits; j++ ) + { + VarJ = MSAT_LIT2VAR(pLits[j]); + pAdjJ = (Msat_IntVec_t *)p->vAdjacents->pArray[VarJ]; + + Msat_IntVecPushUniqueOrder( pAdjI, VarJ, 1 ); + Msat_IntVecPushUniqueOrder( pAdjJ, VarI, 1 ); + } + } + } +*/ + } + // 'vLits' is now the (possibly) reduced vector of literals. + if ( nLits == 0 ) + return 0; + if ( nLits == 1 ) + return Msat_SolverEnqueue( p, pLits[0], NULL ); + + // Allocate clause: +// nBytes = sizeof(unsigned)*(nLits + 1 + (int)fLearned); + nBytes = sizeof(unsigned)*(nLits + 2 + (int)fLearned); +#ifdef USE_SYSTEM_MEMORY_MANAGEMENT + pC = (Msat_Clause_t *)ALLOC( char, nBytes ); +#else + pC = (Msat_Clause_t *)Msat_MmStepEntryFetch( Msat_SolverReadMem(p), nBytes ); +#endif + pC->Num = p->nClauses++; + pC->fTypeA = 0; + pC->fMark = 0; + pC->fLearned = fLearned; + pC->nSize = nLits; + pC->nSizeAlloc = nBytes; + memcpy( pC->pData, pLits, sizeof(int)*nLits ); + + // For learnt clauses only: + if ( fLearned ) + { + int * pLevel = Msat_SolverReadDecisionLevelArray( p ); + int iLevelMax, iLevelCur, iLitMax; + + // Put the second watch on the literal with highest decision level: + iLitMax = 1; + iLevelMax = pLevel[ MSAT_LIT2VAR(pLits[1]) ]; + for ( i = 2; i < nLits; i++ ) + { + iLevelCur = pLevel[ MSAT_LIT2VAR(pLits[i]) ]; + assert( iLevelCur != -1 ); + if ( iLevelMax < iLevelCur ) + // this is very strange - shouldn't it be??? + // if ( iLevelMax > iLevelCur ) + iLevelMax = iLevelCur, iLitMax = i; + } + pC->pData[1] = pLits[iLitMax]; + pC->pData[iLitMax] = pLits[1]; + + // Bumping: + // (newly learnt clauses should be considered active) + Msat_ClauseWriteActivity( pC, 0.0 ); + Msat_SolverClaBumpActivity( p, pC ); +// if ( nLits < 20 ) + for ( i = 0; i < nLits; i++ ) + { + Msat_SolverVarBumpActivity( p, pLits[i] ); +// Msat_SolverVarBumpActivity( p, pLits[i] ); +// p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++; + } + } + + // Store clause: + pvWatched = Msat_SolverReadWatchedArray( p ); + Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[0]) ], pC ); + Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[1]) ], pC ); + *pClause_out = pC; + return 1; +} + +/**Function************************************************************* + + Synopsis [Deallocates the clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched ) +{ + if ( fRemoveWatched ) + { + Msat_Lit_t Lit; + Msat_ClauseVec_t ** pvWatched; + pvWatched = Msat_SolverReadWatchedArray( p ); + Lit = MSAT_LITNOT( pC->pData[0] ); + Msat_ClauseRemoveWatch( pvWatched[Lit], pC ); + Lit = MSAT_LITNOT( pC->pData[1] ); + Msat_ClauseRemoveWatch( pvWatched[Lit], pC ); + } + +#ifdef USE_SYSTEM_MEMORY_MANAGEMENT + free( pC ); +#else + Msat_MmStepEntryRecycle( Msat_SolverReadMem(p), (char *)pC, pC->nSizeAlloc ); +#endif + +} + +/**Function************************************************************* + + Synopsis [Access the data field of the clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Msat_ClauseReadLearned( Msat_Clause_t * pC ) { return pC->fLearned; } +int Msat_ClauseReadSize( Msat_Clause_t * pC ) { return pC->nSize; } +int * Msat_ClauseReadLits( Msat_Clause_t * pC ) { return pC->pData; } +bool Msat_ClauseReadMark( Msat_Clause_t * pC ) { return pC->fMark; } +int Msat_ClauseReadNum( Msat_Clause_t * pC ) { return pC->Num; } +bool Msat_ClauseReadTypeA( Msat_Clause_t * pC ) { return pC->fTypeA; } + +void Msat_ClauseSetMark( Msat_Clause_t * pC, bool fMark ) { pC->fMark = fMark; } +void Msat_ClauseSetNum( Msat_Clause_t * pC, int Num ) { pC->Num = Num; } +void Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA ) { pC->fTypeA = fTypeA; } + +/**Function************************************************************* + + Synopsis [Checks whether the learned clause is locked.] + + Description [The clause may be locked if it is the reason of a + recent conflict. Such clause cannot be removed from the database.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC ) +{ + Msat_Clause_t ** pReasons = Msat_SolverReadReasonArray( p ); + return (bool)(pReasons[MSAT_LIT2VAR(pC->pData[0])] == pC); +} + +/**Function************************************************************* + + Synopsis [Reads the activity of the given clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Msat_ClauseReadActivity( Msat_Clause_t * pC ) +{ + return *((float *)(pC->pData + pC->nSize)); +} + +/**Function************************************************************* + + Synopsis [Sets the activity of the clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num ) +{ + *((float *)(pC->pData + pC->nSize)) = Num; +} + +/**Function************************************************************* + + Synopsis [Propages the assignment.] + + Description [The literal that has become true (Lit) is given to this + procedure. The array of current variable assignments is given for + efficiency. The output literal (pLit_out) can be the second watched + literal (if TRUE is returned) or the conflict literal (if FALSE is + returned). This messy interface is used to improve performance. + This procedure accounts for ~50% of the runtime of the solver.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out ) +{ + // make sure the false literal is pC->pData[1] + Msat_Lit_t LitF = MSAT_LITNOT(Lit); + if ( pC->pData[0] == LitF ) + pC->pData[0] = pC->pData[1], pC->pData[1] = LitF; + assert( pC->pData[1] == LitF ); + // if the 0-th watch is true, clause is already satisfied + if ( pAssigns[MSAT_LIT2VAR(pC->pData[0])] == pC->pData[0] ) + return 1; + // look for a new watch + if ( pC->nSize > 2 ) + { + int i; + for ( i = 2; i < (int)pC->nSize; i++ ) + if ( pAssigns[MSAT_LIT2VAR(pC->pData[i])] != MSAT_LITNOT(pC->pData[i]) ) + { + pC->pData[1] = pC->pData[i], pC->pData[i] = LitF; + *pLit_out = MSAT_LITNOT(pC->pData[1]); + return 1; + } + } + // clause is unit under assignment + *pLit_out = pC->pData[0]; + return 0; +} + +/**Function************************************************************* + + Synopsis [Simplifies the clause.] + + Description [Assumes everything has been propagated! (esp. watches + in clauses are NOT unsatisfied)] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns ) +{ + Msat_Var_t Var; + int i, j; + for ( i = j = 0; i < (int)pC->nSize; i++ ) + { + Var = MSAT_LIT2VAR(pC->pData[i]); + if ( pAssigns[Var] == MSAT_VAR_UNASSIGNED ) + { + pC->pData[j++] = pC->pData[i]; + continue; + } + if ( pAssigns[Var] == pC->pData[i] ) + return 1; + // otherwise, the value of the literal is false + // make sure, this literal is not watched + assert( i >= 2 ); + } + // if the size has changed, update it and move activity + if ( j < (int)pC->nSize ) + { + float Activ = Msat_ClauseReadActivity(pC); + pC->nSize = j; + Msat_ClauseWriteActivity(pC, Activ); + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Computes reason of conflict in the given clause.] + + Description [If the literal is unassigned, finds the reason by + complementing literals in the given cluase (pC). If the literal is + assigned, makes sure that this literal is the first one in the clause + and computes the complement of all other literals in the clause. + Returns the reason in the given array (vLits_out). If the clause is + learned, bumps its activity.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out ) +{ + int i; + // clear the reason + Msat_IntVecClear( vLits_out ); + assert( Lit == MSAT_LIT_UNASSIGNED || Lit == pC->pData[0] ); + for ( i = (Lit != MSAT_LIT_UNASSIGNED); i < (int)pC->nSize; i++ ) + { + assert( Msat_SolverReadAssignsArray(p)[MSAT_LIT2VAR(pC->pData[i])] == MSAT_LITNOT(pC->pData[i]) ); + Msat_IntVecPush( vLits_out, MSAT_LITNOT(pC->pData[i]) ); + } + if ( pC->fLearned ) + Msat_SolverClaBumpActivity( p, pC ); +} + +/**Function************************************************************* + + Synopsis [Removes the given clause from the watched list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC ) +{ + Msat_Clause_t ** pClauses; + int nClauses, i; + nClauses = Msat_ClauseVecReadSize( vClauses ); + pClauses = Msat_ClauseVecReadArray( vClauses ); + for ( i = 0; pClauses[i] != pC; i++ ) + assert( i < nClauses ); + for ( ; i < nClauses - 1; i++ ) + pClauses[i] = pClauses[i+1]; + Msat_ClauseVecPop( vClauses ); +} + +/**Function************************************************************* + + Synopsis [Prints the given clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Msat_ClausePrint( Msat_Clause_t * pC ) +{ + int i; + if ( pC == NULL ) + printf( "NULL pointer" ); + else + { + if ( pC->fLearned ) + printf( "Act = %.4f ", Msat_ClauseReadActivity(pC) ); + for ( i = 0; i < (int)pC->nSize; i++ ) + printf( " %s%d", ((pC->pData[i]&1)? "-": ""), pC->pData[i]/2 + 1 ); + } + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Writes the given clause in a file in DIMACS format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, bool fIncrement ) +{ + int i; + for ( i = 0; i < (int)pC->nSize; i++ ) + fprintf( pFile, "%s%d ", ((pC->pData[i]&1)? "-": ""), pC->pData[i]/2 + (int)(fIncrement>0) ); + if ( fIncrement ) + fprintf( pFile, "0" ); + fprintf( pFile, "\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints the given clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Msat_ClausePrintSymbols( Msat_Clause_t * pC ) +{ + int i; + if ( pC == NULL ) + printf( "NULL pointer" ); + else + { +// if ( pC->fLearned ) +// printf( "Act = %.4f ", Msat_ClauseReadActivity(pC) ); + for ( i = 0; i < (int)pC->nSize; i++ ) + printf(" "L_LIT, L_lit(pC->pData[i])); + } + printf( "\n" ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |