/**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