| /**CFile**************************************************************** |
| |
| FileName [msatOrder.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 [The manager of variable assignment.] |
| |
| Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - January 1, 2004.] |
| |
| Revision [$Id: msatOrder.c,v 1.0 2005/05/30 1:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "msatInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| /* |
| The J-boundary (justification boundary) is defined as a set of unassigned |
| variables belonging to the cone of interest, such that for each of them, |
| there exist an adjacent assigned variable in the cone of interest. |
| */ |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| typedef struct Msat_OrderVar_t_ Msat_OrderVar_t; |
| typedef struct Msat_OrderRing_t_ Msat_OrderRing_t; |
| |
| // the variable data structure |
| struct Msat_OrderVar_t_ |
| { |
| Msat_OrderVar_t * pNext; |
| Msat_OrderVar_t * pPrev; |
| int Num; |
| }; |
| |
| // the ring of variables data structure (J-boundary) |
| struct Msat_OrderRing_t_ |
| { |
| Msat_OrderVar_t * pRoot; |
| int nItems; |
| }; |
| |
| // the variable package data structure |
| struct Msat_Order_t_ |
| { |
| Msat_Solver_t * pSat; // the SAT solver |
| Msat_OrderVar_t * pVars; // the storage for variables |
| int nVarsAlloc; // the number of variables allocated |
| Msat_OrderRing_t rVars; // the J-boundary as a ring of variables |
| }; |
| |
| //The solver can communicate to the variable order the following parts: |
| //- the array of current assignments (pSat->pAssigns) |
| //- the array of variable activities (pSat->pdActivity) |
| //- the array of variables currently in the cone (pSat->vConeVars) |
| //- the array of arrays of variables adjucent to each(pSat->vAdjacents) |
| |
| #define Msat_OrderVarIsInBoundary( p, i ) ((p)->pVars[i].pNext) |
| #define Msat_OrderVarIsAssigned( p, i ) ((p)->pSat->pAssigns[i] != MSAT_VAR_UNASSIGNED) |
| #define Msat_OrderVarIsUsedInCone( p, i ) ((p)->pSat->vVarsUsed->pArray[i]) |
| |
| // iterator through the entries in J-boundary |
| #define Msat_OrderRingForEachEntry( pRing, pVar, pNext ) \ |
| for ( pVar = pRing, \ |
| pNext = pVar? pVar->pNext : NULL; \ |
| pVar; \ |
| pVar = (pNext != pRing)? pNext : NULL, \ |
| pNext = pVar? pVar->pNext : NULL ) |
| |
| static void Msat_OrderRingAddLast( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar ); |
| static void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar ); |
| |
| extern clock_t timeSelect; |
| extern clock_t timeAssign; |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Allocates the ordering structure.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat ) |
| { |
| Msat_Order_t * p; |
| p = ALLOC( Msat_Order_t, 1 ); |
| memset( p, 0, sizeof(Msat_Order_t) ); |
| p->pSat = pSat; |
| Msat_OrderSetBounds( p, pSat->nVarsAlloc ); |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Sets the bound of the ordering structure.] |
| |
| Description [Should be called whenever the SAT solver is resized.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax ) |
| { |
| int i; |
| // add variables if they are missing |
| if ( p->nVarsAlloc < nVarsMax ) |
| { |
| p->pVars = REALLOC( Msat_OrderVar_t, p->pVars, nVarsMax ); |
| for ( i = p->nVarsAlloc; i < nVarsMax; i++ ) |
| { |
| p->pVars[i].pNext = p->pVars[i].pPrev = NULL; |
| p->pVars[i].Num = i; |
| } |
| p->nVarsAlloc = nVarsMax; |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Cleans the ordering structure.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone ) |
| { |
| Msat_OrderVar_t * pVar, * pNext; |
| // quickly undo the ring |
| Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext ) |
| pVar->pNext = pVar->pPrev = NULL; |
| p->rVars.pRoot = NULL; |
| p->rVars.nItems = 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Checks that the J-boundary is okay.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Msat_OrderCheck( Msat_Order_t * p ) |
| { |
| Msat_OrderVar_t * pVar, * pNext; |
| Msat_IntVec_t * vRound; |
| int * pRound, nRound; |
| int * pVars, nVars, i, k; |
| int Counter = 0; |
| |
| // go through all the variables in the boundary |
| Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext ) |
| { |
| assert( !Msat_OrderVarIsAssigned(p, pVar->Num) ); |
| // go though all the variables in the neighborhood |
| // and check that it is true that there is least one assigned |
| vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVar->Num ); |
| nRound = Msat_IntVecReadSize( vRound ); |
| pRound = Msat_IntVecReadArray( vRound ); |
| for ( i = 0; i < nRound; i++ ) |
| { |
| if ( !Msat_OrderVarIsUsedInCone(p, pRound[i]) ) |
| continue; |
| if ( Msat_OrderVarIsAssigned(p, pRound[i]) ) |
| break; |
| } |
| // assert( i != nRound ); |
| // if ( i == nRound ) |
| // return 0; |
| if ( i == nRound ) |
| Counter++; |
| } |
| if ( Counter > 0 ) |
| printf( "%d(%d) ", Counter, p->rVars.nItems ); |
| |
| // we may also check other unassigned variables in the cone |
| // to make sure that if they are not in J-boundary, |
| // then they do not have an assigned neighbor |
| nVars = Msat_IntVecReadSize( p->pSat->vConeVars ); |
| pVars = Msat_IntVecReadArray( p->pSat->vConeVars ); |
| for ( i = 0; i < nVars; i++ ) |
| { |
| assert( Msat_OrderVarIsUsedInCone(p, pVars[i]) ); |
| // skip assigned vars, vars in the boundary, and vars not used in the cone |
| if ( Msat_OrderVarIsAssigned(p, pVars[i]) || |
| Msat_OrderVarIsInBoundary(p, pVars[i]) ) |
| continue; |
| // make sure, it does not have assigned neighbors |
| vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVars[i] ); |
| nRound = Msat_IntVecReadSize( vRound ); |
| pRound = Msat_IntVecReadArray( vRound ); |
| for ( k = 0; k < nRound; k++ ) |
| { |
| if ( !Msat_OrderVarIsUsedInCone(p, pRound[k]) ) |
| continue; |
| if ( Msat_OrderVarIsAssigned(p, pRound[k]) ) |
| break; |
| } |
| // assert( k == nRound ); |
| // if ( k != nRound ) |
| // return 0; |
| } |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Frees the ordering structure.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_OrderFree( Msat_Order_t * p ) |
| { |
| free( p->pVars ); |
| free( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Selects the next variable to assign.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Msat_OrderVarSelect( Msat_Order_t * p ) |
| { |
| Msat_OrderVar_t * pVar, * pNext, * pVarBest; |
| double * pdActs = p->pSat->pdActivity; |
| double dfActBest; |
| // clock_t clk = clock(); |
| |
| pVarBest = NULL; |
| dfActBest = -1.0; |
| Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext ) |
| { |
| if ( dfActBest < pdActs[pVar->Num] ) |
| { |
| dfActBest = pdActs[pVar->Num]; |
| pVarBest = pVar; |
| } |
| } |
| //timeSelect += clock() - clk; |
| //timeAssign += clock() - clk; |
| |
| //if ( pVarBest && pVarBest->Num % 1000 == 0 ) |
| //printf( "%d ", p->rVars.nItems ); |
| |
| // Msat_OrderCheck( p ); |
| if ( pVarBest ) |
| { |
| assert( Msat_OrderVarIsUsedInCone(p, pVarBest->Num) ); |
| return pVarBest->Num; |
| } |
| return MSAT_ORDER_UNKNOWN; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Updates J-boundary when the variable is assigned.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_OrderVarAssigned( Msat_Order_t * p, int Var ) |
| { |
| Msat_IntVec_t * vRound; |
| int i;//, clk = clock(); |
| |
| // make sure the variable is in the boundary |
| assert( Var < p->nVarsAlloc ); |
| // if it is not in the boundary (initial decision, random decision), do not remove |
| if ( Msat_OrderVarIsInBoundary( p, Var ) ) |
| Msat_OrderRingRemove( &p->rVars, &p->pVars[Var] ); |
| // add to the boundary those neighbors that are (1) unassigned, (2) not in boundary |
| // because for them we know that there is a variable (Var) which is assigned |
| vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var]; |
| for ( i = 0; i < vRound->nSize; i++ ) |
| { |
| if ( !Msat_OrderVarIsUsedInCone(p, vRound->pArray[i]) ) |
| continue; |
| if ( Msat_OrderVarIsAssigned(p, vRound->pArray[i]) ) |
| continue; |
| if ( Msat_OrderVarIsInBoundary(p, vRound->pArray[i]) ) |
| continue; |
| Msat_OrderRingAddLast( &p->rVars, &p->pVars[vRound->pArray[i]] ); |
| } |
| //timeSelect += clock() - clk; |
| // Msat_OrderCheck( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Updates the order after a variable is unassigned.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var ) |
| { |
| Msat_IntVec_t * vRound, * vRound2; |
| int i, k;//, clk = clock(); |
| |
| // make sure the variable is not in the boundary |
| assert( Var < p->nVarsAlloc ); |
| assert( !Msat_OrderVarIsInBoundary( p, Var ) ); |
| // go through its neigbors - if one of them is assigned add this var |
| // add to the boundary those neighbors that are not there already |
| // this will also get rid of variable outside of the current cone |
| // because they are unassigned in Msat_SolverPrepare() |
| vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var]; |
| for ( i = 0; i < vRound->nSize; i++ ) |
| if ( Msat_OrderVarIsAssigned(p, vRound->pArray[i]) ) |
| break; |
| if ( i != vRound->nSize ) |
| Msat_OrderRingAddLast( &p->rVars, &p->pVars[Var] ); |
| |
| // unassigning a variable may lead to its adjacents dropping from the boundary |
| for ( i = 0; i < vRound->nSize; i++ ) |
| if ( Msat_OrderVarIsInBoundary(p, vRound->pArray[i]) ) |
| { // the neighbor is in the J-boundary (and unassigned) |
| assert( !Msat_OrderVarIsAssigned(p, vRound->pArray[i]) ); |
| vRound2 = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[vRound->pArray[i]]; |
| // go through its neighbors and determine if there is at least one assigned |
| for ( k = 0; k < vRound2->nSize; k++ ) |
| if ( Msat_OrderVarIsAssigned(p, vRound2->pArray[k]) ) |
| break; |
| if ( k == vRound2->nSize ) // there is no assigned vars, delete this one |
| Msat_OrderRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] ); |
| } |
| //timeSelect += clock() - clk; |
| // Msat_OrderCheck( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Updates the order after a variable changed weight.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_OrderUpdate( Msat_Order_t * p, int Var ) |
| { |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Adds node to the end of the ring.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_OrderRingAddLast( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar ) |
| { |
| //printf( "adding %d\n", pVar->Num ); |
| // check that the node is not in a ring |
| assert( pVar->pPrev == NULL ); |
| assert( pVar->pNext == NULL ); |
| // if the ring is empty, make the node point to itself |
| pRing->nItems++; |
| if ( pRing->pRoot == NULL ) |
| { |
| pRing->pRoot = pVar; |
| pVar->pPrev = pVar; |
| pVar->pNext = pVar; |
| return; |
| } |
| // if the ring is not empty, add it as the last entry |
| pVar->pPrev = pRing->pRoot->pPrev; |
| pVar->pNext = pRing->pRoot; |
| pVar->pPrev->pNext = pVar; |
| pVar->pNext->pPrev = pVar; |
| |
| // move the root so that it points to the new entry |
| // pRing->pRoot = pRing->pRoot->pPrev; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Removes the node from the ring.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar ) |
| { |
| //printf( "removing %d\n", pVar->Num ); |
| // check that the var is in a ring |
| assert( pVar->pPrev ); |
| assert( pVar->pNext ); |
| pRing->nItems--; |
| if ( pRing->nItems == 0 ) |
| { |
| assert( pRing->pRoot == pVar ); |
| pVar->pPrev = NULL; |
| pVar->pNext = NULL; |
| pRing->pRoot = NULL; |
| return; |
| } |
| // move the root if needed |
| if ( pRing->pRoot == pVar ) |
| pRing->pRoot = pVar->pNext; |
| // move the root to the next entry after pVar |
| // this way all the additions to the list will be traversed first |
| // pRing->pRoot = pVar->pPrev; |
| // delete the node |
| pVar->pPrev->pNext = pVar->pNext; |
| pVar->pNext->pPrev = pVar->pPrev; |
| pVar->pPrev = NULL; |
| pVar->pNext = NULL; |
| } |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
