Version abc50729

1 files changed, 466 insertions, 0 deletions

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