From 888e5bed5d7f56a5d86d91a6e8e88f3e5a3454dc Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 29 Jul 2005 08:01:00 -0700 Subject: Version abc50729 --- src/sat/msat/msatOrderJ.c | 466 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 466 insertions(+) create mode 100644 src/sat/msat/msatOrderJ.c (limited to 'src/sat/msat/msatOrderJ.c') diff --git a/src/sat/msat/msatOrderJ.c b/src/sat/msat/msatOrderJ.c new file mode 100644 index 00000000..6067b40f --- /dev/null +++ b/src/sat/msat/msatOrderJ.c @@ -0,0 +1,466 @@ +/**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 ] + + 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" + +/* +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 int timeSelect; +extern int timeAssign; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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; + + // 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; + } + + // 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 ( 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; + } + 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; + int 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 ); + + 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->pNext; + // delete the node + pVar->pPrev->pNext = pVar->pNext; + pVar->pNext->pPrev = pVar->pPrev; + pVar->pPrev = NULL; + pVar->pNext = NULL; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + -- cgit v1.2.3