SAT sweeping under constraints.

8 files changed, 1198 insertions, 0 deletions

diff --git a/src/proof/ssc/module.make b/src/proof/ssc/module.make
new file mode 100644
index 00000000..55e845f8
--- /dev/null
+++ b/src/proof/ssc/module.make
@@ -0,0 +1,5 @@
+SRC +=    src/proof/ssc/sscClass.c \
+    src/proof/ssc/sscCore.c \
+    src/proof/ssc/sscSat.c \
+    src/proof/ssc/sscSim.c \
+    src/proof/ssc/sscUtil.c
diff --git a/src/proof/ssc/ssc.h b/src/proof/ssc/ssc.h
new file mode 100644
index 00000000..de32ffc1
--- /dev/null
+++ b/src/proof/ssc/ssc.h
@@ -0,0 +1,76 @@
+/**CFile****************************************************************
+
+  FileName    [ssc.h] 
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT sweeping under constraints.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: ssc.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__aig__ssc__ssc_h
+#define ABC__aig__ssc__ssc_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// choicing parameters
+typedef struct Ssc_Pars_t_ Ssc_Pars_t;
+struct Ssc_Pars_t_
+{
+    int              nWords;        // the number of simulation words
+    int              nBTLimit;      // conflict limit at a node
+    int              nSatVarMax;    // the max number of SAT variables
+    int              nCallsRecycle; // calls to perform before recycling SAT solver
+    int              fVerbose;      // verbose stats
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== sscCore.c ==========================================================*/
+extern void          Ssc_ManSetDefaultParams( Ssc_Pars_t * p );
+extern Gia_Man_t *   Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars );
+extern Gia_Man_t *   Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars );
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/proof/ssc/sscClass.c b/src/proof/ssc/sscClass.c
new file mode 100644
index 00000000..a6d2b5e3
--- /dev/null
+++ b/src/proof/ssc/sscClass.c
@@ -0,0 +1,245 @@
+/**CFile****************************************************************
+
+  FileName    [sscClass.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT sweeping under constraints.]
+
+  Synopsis    [Equivalence classes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: sscClass.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sscInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes hash key of the simuation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ssc_GiaSimHashKey( Gia_Man_t * p, int iObj, int nTableSize )
+{
+    static int s_Primes[16] = { 
+        1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, 
+        4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
+    word * pSim = Gia_ObjSim( p, iObj );
+    unsigned uHash = 0;
+    int i, nWords = Gia_ObjSimWords(p);
+    if ( pSim[0] & 1 )
+        for ( i = 0; i < nWords; i++ )
+            uHash ^= ~pSim[i] * s_Primes[i & 0xf];
+    else
+        for ( i = 0; i < nWords; i++ )
+            uHash ^= pSim[i] * s_Primes[i & 0xf];
+    return (int)(uHash % nTableSize);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if sim patterns are equal up to the complement.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ssc_GiaSimIsConst0( Gia_Man_t * p, int iObj0 )
+{
+    int w, nWords = Gia_ObjSimWords(p);
+    word * pSim = Gia_ObjSim( p, iObj0 );
+    if ( pSim[0] & 1 )
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( ~pSim[w] )
+                return 0;
+    }
+    else
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( pSim[w] )
+                return 0;
+    }
+    return 1;
+}
+static inline int Ssc_GiaSimAreEqual( Gia_Man_t * p, int iObj0, int iObj1 )
+{
+    int w, nWords = Gia_ObjSimWords(p);
+    word * pSim0 = Gia_ObjSim( p, iObj0 );
+    word * pSim1 = Gia_ObjSim( p, iObj1 );
+    if ( (pSim0[0] & 1) != (pSim1[0] & 1) )
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( pSim0[w] != ~pSim1[w] )
+                return 0;
+    }
+    else
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( pSim0[w] != pSim1[w] )
+                return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines one equivalence class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssc_GiaSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
+{
+    int Repr = GIA_VOID, EntPrev = -1, Ent, i;
+    assert( Vec_IntSize(vClass) > 0 );
+    Vec_IntForEachEntry( vClass, Ent, i )
+    {
+        if ( i == 0 )
+        {
+            Repr = Ent;
+            Gia_ObjSetRepr( p, Ent, GIA_VOID );
+            EntPrev = Ent;
+        }
+        else
+        {
+            assert( Repr < Ent );
+            Gia_ObjSetRepr( p, Ent, Repr );
+            Gia_ObjSetNext( p, EntPrev, Ent );
+            EntPrev = Ent;
+        }
+    }
+    Gia_ObjSetNext( p, EntPrev, 0 );
+}
+int Ssc_GiaSimClassRefineOne( Gia_Man_t * p, int i )
+{
+    Gia_Obj_t * pObj;
+    int Ent;
+    Vec_IntClear( p->vClassOld );
+    Vec_IntClear( p->vClassNew );
+    Vec_IntPush( p->vClassOld, i );
+    pObj = Gia_ManObj(p, i);
+    Gia_ClassForEachObj1( p, i, Ent )
+    {
+        if ( Ssc_GiaSimAreEqual( p, i, Ent ) )
+            Vec_IntPush( p->vClassOld, Ent );
+        else
+            Vec_IntPush( p->vClassNew, Ent );
+    }
+    if ( Vec_IntSize( p->vClassNew ) == 0 )
+        return 0;
+    Ssc_GiaSimClassCreate( p, p->vClassOld );
+    Ssc_GiaSimClassCreate( p, p->vClassNew );
+    if ( Vec_IntSize(p->vClassNew) > 1 )
+        return 1 + Ssc_GiaSimClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
+    return 1;
+}
+void Ssc_GiaSimProcessRefined( Gia_Man_t * p, Vec_Int_t * vRefined )
+{
+    int * pTable, nTableSize, i, k, Key;
+    if ( Vec_IntSize(vRefined) == 0 )
+        return;
+    nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 );
+    pTable = ABC_CALLOC( int, nTableSize );
+    Vec_IntForEachEntry( vRefined, i, k )
+    {
+        assert( !Ssc_GiaSimIsConst0( p, i ) );
+        Key = Ssc_GiaSimHashKey( p, i, nTableSize );
+        if ( pTable[Key] == 0 )
+        {
+            assert( Gia_ObjRepr(p, i) == 0 );
+            assert( Gia_ObjNext(p, i) == 0 );
+            Gia_ObjSetRepr( p, i, GIA_VOID );
+        }
+        else
+        {
+            Gia_ObjSetNext( p, pTable[Key], i );
+            Gia_ObjSetRepr( p, i, Gia_ObjRepr(p, pTable[Key]) );
+            if ( Gia_ObjRepr(p, i) == GIA_VOID )
+                Gia_ObjSetRepr( p, i, pTable[Key] );
+            assert( Gia_ObjRepr(p, i) > 0 );
+        }
+        pTable[Key] = i;
+    }
+    Vec_IntForEachEntry( vRefined, i, k )
+        if ( Gia_ObjIsHead( p, i ) )
+            Ssc_GiaSimClassRefineOne( p, i );
+    ABC_FREE( pTable );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssc_GiaClassesRefine( Gia_Man_t * p )
+{
+    Vec_Int_t * vRefinedC;
+    Gia_Obj_t * pObj;
+    int i;
+    if ( p->pReprs == NULL )
+    {
+        assert( p->pReprs == NULL );
+        p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+        p->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
+        Gia_ManForEachObj( p, pObj, i )
+            Gia_ObjSetRepr( p, i, Gia_ObjIsCand(pObj) ? 0 : GIA_VOID );
+        if ( p->vClassOld == NULL )
+            p->vClassOld = Vec_IntAlloc( 100 );
+        if ( p->vClassNew == NULL )
+            p->vClassNew = Vec_IntAlloc( 100 );
+    }
+    vRefinedC = Vec_IntAlloc( 100 );
+    Gia_ManForEachCand( p, pObj, i )
+        if ( Gia_ObjIsTail(p, i) )
+            Ssc_GiaSimClassRefineOne( p, Gia_ObjRepr(p, i) );
+        else if ( Gia_ObjIsConst(p, i) && !Ssc_GiaSimIsConst0(p, i) )
+            Vec_IntPush( vRefinedC, i );
+    Ssc_GiaSimProcessRefined( p, vRefinedC );
+    Vec_IntFree( vRefinedC );
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c
new file mode 100644
index 00000000..f2cd810a
--- /dev/null
+++ b/src/proof/ssc/sscCore.c
@@ -0,0 +1,191 @@
+/**CFile****************************************************************
+
+  FileName    [sscCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT sweeping under constraints.]
+
+  Synopsis    [The core procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: sscCore.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sscInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssc_ManSetDefaultParams( Ssc_Pars_t * p )
+{
+    memset( p, 0, sizeof(Ssc_Pars_t) );
+    p->nWords         =     4;  // the number of simulation words
+    p->nBTLimit       =  1000;  // conflict limit at a node
+    p->nSatVarMax     =  5000;  // the max number of SAT variables
+    p->nCallsRecycle  =   100;  // calls to perform before recycling SAT solver
+    p->fVerbose       =     0;  // verbose stats
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssc_ManStop( Ssc_Man_t * p )
+{
+    if ( p->pSat )
+        sat_solver_delete( p->pSat );
+    Vec_IntFreeP( &p->vSatVars );
+    Gia_ManStopP( &p->pFraig );
+    Vec_IntFreeP( &p->vPivot );
+    ABC_FREE( p );
+}
+Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars )
+{
+    Ssc_Man_t * p;
+    p = ABC_CALLOC( Ssc_Man_t, 1 );
+    p->pPars  = pPars;
+    p->pAig   = pAig;
+    p->pCare  = pCare;
+    p->pFraig = Gia_ManDup( p->pCare );
+    Gia_ManInvertPos( p->pFraig );
+    Ssc_ManStartSolver( p );
+    if ( p->pSat == NULL )
+    {
+        printf( "Constraints are UNSAT after propagation.\n" );
+        Ssc_ManStop( p );
+        return NULL;
+    }
+    p->vPivot = Ssc_GiaFindPivotSim( p->pFraig );
+//    Vec_IntFreeP( &p->vPivot  );
+    if ( p->vPivot == NULL )
+        p->vPivot = Ssc_ManFindPivotSat( p );
+    if ( p->vPivot == NULL )
+    {
+        printf( "Constraints are UNSAT or conflict limit is too low.\n" );
+        Ssc_ManStop( p );
+        return NULL;
+    }
+    Vec_IntPrint( p->vPivot );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs computation of AIGs with choices.]
+
+  Description [Takes several AIGs and performs choicing.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars )
+{
+    Ssc_Man_t * p;
+    Gia_Man_t * pResult;
+    clock_t clk, clkTotal = clock();
+    int i;
+    assert( Gia_ManRegNum(pCare) == 0 );
+    assert( Gia_ManPiNum(pAig) == Gia_ManPiNum(pCare) );
+    assert( Gia_ManIsNormalized(pAig) );
+    assert( Gia_ManIsNormalized(pCare) );
+    // reset random numbers
+    Gia_ManRandom( 1 );
+    // sweeping manager
+    p = Ssc_ManStart( pAig, pCare, pPars );
+    if ( p == NULL )
+        return Gia_ManDup( pAig );
+    // perform simulation 
+clk = clock();
+    for ( i = 0; i < 16; i++ )
+    {
+        Ssc_GiaRandomPiPattern( pAig, 10, NULL );
+        Ssc_GiaSimRound( pAig );
+        Ssc_GiaClassesRefine( pAig );
+        Gia_ManEquivPrintClasses( pAig, 0, 0 );
+    }
+p->timeSimInit += clock() - clk;
+    // remember the resulting AIG
+    pResult = Gia_ManEquivReduce( pAig, 1, 0, 0 );
+    if ( pResult == NULL )
+    {
+        printf( "There is no equivalences.\n" );
+        pResult = Gia_ManDup( pAig );
+    }
+    Ssc_ManStop( p );
+    // count the number of representatives
+    if ( pPars->fVerbose ) 
+    {
+        Gia_ManEquivPrintClasses( pAig, 0, 0 );
+        Abc_Print( 1, "Reduction in AIG nodes:%8d  ->%8d.  ", Gia_ManAndNum(pAig), Gia_ManAndNum(pResult) );
+        Abc_PrintTime( 1, "Time", clock() - clkTotal );
+    }
+    return pResult;
+}
+Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
+{
+    Gia_Man_t * pAig, * pCare, * pResult;
+    int i;
+    if ( p->nConstrs == 0 )
+    {
+        pAig = Gia_ManDup( p );
+        pCare = Gia_ManStart( Gia_ManPiNum(p) + 2 );
+        pCare->pName = Abc_UtilStrsav( "care" );
+        for ( i = 0; i < Gia_ManPiNum(p); i++ )
+            Gia_ManAppendCi( pCare );
+        Gia_ManAppendCo( pCare, 1 );
+    }
+    else
+    {
+        Vec_Int_t * vOuts = Vec_IntStartNatural( Gia_ManPoNum(p) );
+        pAig = Gia_ManDupCones( p, Vec_IntArray(vOuts), Gia_ManPoNum(p) - p->nConstrs, 0 );
+        pCare = Gia_ManDupCones( p, Vec_IntArray(vOuts) + Gia_ManPoNum(p) - p->nConstrs, p->nConstrs, 0 );
+        Vec_IntFree( vOuts );
+    }
+    pResult = Ssc_PerformSweeping( pAig, pCare, pPars );
+    Gia_ManStop( pAig );
+    Gia_ManStop( pCare );
+    return pResult;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/ssc/sscInt.h b/src/proof/ssc/sscInt.h
new file mode 100644
index 00000000..21f5afc2
--- /dev/null
+++ b/src/proof/ssc/sscInt.h
@@ -0,0 +1,122 @@
+/**CFile****************************************************************
+
+  FileName    [sscInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Choice computation for tech-mapping.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: sscInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__aig__ssc__sscInt_h
+#define ABC__aig__ssc__sscInt_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig/gia/gia.h"
+#include "sat/bsat/satSolver.h"
+#include "ssc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// choicing manager
+typedef struct Ssc_Man_t_ Ssc_Man_t;
+struct Ssc_Man_t_
+{
+    // parameters
+    Ssc_Pars_t *     pPars;          // choicing parameters
+    Gia_Man_t *      pAig;           // subject AIG
+    Gia_Man_t *      pCare;          // care set AIG
+    Gia_Man_t *      pFraig;         // resulting AIG
+    Vec_Int_t *      vPivot;         // one SAT pattern
+    // SAT solving
+    sat_solver *     pSat;           // recyclable SAT solver
+    Vec_Int_t *      vSatVars;       // mapping of each node into its SAT var
+    Vec_Int_t *      vUsedNodes;     // nodes whose SAT vars are assigned
+    int              nRecycles;      // the number of times SAT solver was recycled
+    int              nCallsSince;    // the number of calls since the last recycle
+    Vec_Int_t *      vFanins;        // fanins of the CNF node
+    // SAT calls statistics
+    int              nSatCalls;      // the number of SAT calls
+    int              nSatProof;      // the number of proofs
+    int              nSatFailsReal;  // the number of timeouts
+    int              nSatCallsUnsat; // the number of unsat SAT calls
+    int              nSatCallsSat;   // the number of sat SAT calls
+    // runtime stats
+    clock_t          timeSimInit;    // simulation and class computation
+    clock_t          timeSimSat;     // simulation of the counter-examples
+    clock_t          timeSat;        // solving SAT
+    clock_t          timeSatSat;     // sat
+    clock_t          timeSatUnsat;   // unsat
+    clock_t          timeSatUndec;   // undecided
+    clock_t          timeChoice;     // choice computation
+    clock_t          timeOther;      // other runtime
+    clock_t          timeTotal;      // total runtime
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int  Ssc_ObjSatNum( Ssc_Man_t * p, Gia_Obj_t * pObj )             { return Vec_IntEntry(p->vSatVars, Gia_ObjId(p->pFraig, pObj));     }
+static inline void Ssc_ObjSetSatNum( Ssc_Man_t * p, Gia_Obj_t * pObj, int Num ) { Vec_IntWriteEntry(p->vSatVars, Gia_ObjId(p->pFraig, pObj), Num);  }
+
+static inline int  Ssc_ObjFraig( Ssc_Man_t * p, Gia_Obj_t * pObj )              { return pObj->Value;           }
+static inline void Ssc_ObjSetFraig( Gia_Obj_t * pObj, int iNode )               { pObj->Value = iNode;          }
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== sscClass.c =================================================*/
+extern int           Ssc_GiaClassesRefine( Gia_Man_t * p );
+/*=== sscCnf.c ===================================================*/
+extern void          Ssc_CnfNodeAddToSolver( Ssc_Man_t * p, Gia_Obj_t * pObj );
+/*=== sscCore.c ==================================================*/
+/*=== sscSat.c ===================================================*/
+extern int           Ssc_NodesAreEquiv( Ssc_Man_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );
+extern void          Ssc_ManSatSolverRecycle( Ssc_Man_t * p );
+extern void          Ssc_ManStartSolver( Ssc_Man_t * p );
+extern Vec_Int_t *   Ssc_ManFindPivotSat( Ssc_Man_t * p );
+/*=== sscSim.c ===================================================*/
+extern void          Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot );
+extern void          Ssc_GiaSimRound( Gia_Man_t * p );
+extern Vec_Int_t *   Ssc_GiaFindPivotSim( Gia_Man_t * p );
+/*=== sscUtil.c ===================================================*/
+extern Gia_Man_t *   Ssc_GenerateOneHot( int nVars );
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/proof/ssc/sscSat.c b/src/proof/ssc/sscSat.c
new file mode 100644
index 00000000..1519b89e
--- /dev/null
+++ b/src/proof/ssc/sscSat.c
@@ -0,0 +1,113 @@
+/**CFile****************************************************************
+
+  FileName    [sscSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT sweeping under constraints.]
+
+  Synopsis    [SAT procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: sscSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sscInt.h"
+#include "sat/cnf/cnf.h"
+#include "aig/gia/giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the SAT solver for constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssc_ManStartSolver( Ssc_Man_t * p )
+{
+    Aig_Man_t * pAig = Gia_ManToAig( p->pFraig, 0 );
+    Cnf_Dat_t * pDat = Cnf_Derive( pAig, 0 );
+    sat_solver * pSat;
+    int i, status;
+    assert( p->pSat == NULL && p->vSatVars == NULL );
+    assert( Aig_ManObjNumMax(pAig) == Gia_ManObjNum(p->pFraig) );
+    Aig_ManStop( pAig );
+//Cnf_DataWriteIntoFile( pDat, "dump.cnf", 1, NULL, NULL );
+    // save variable mapping
+    p->vSatVars = Vec_IntAllocArray( pDat->pVarNums, Gia_ManObjNum(p->pFraig) );  pDat->pVarNums = NULL;
+    // start the SAT solver
+    pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, pDat->nVars + 1000 );
+    for ( i = 0; i < pDat->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pDat->pClauses[i], pDat->pClauses[i+1] ) )
+        {
+            Cnf_DataFree( pDat );
+            sat_solver_delete( pSat );
+            return;
+        }
+    }
+    Cnf_DataFree( pDat );
+    status = sat_solver_simplify( pSat );
+    if ( status == 0 )
+    {
+        sat_solver_delete( pSat );
+        return;
+    }
+    p->pSat = pSat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p )
+{
+    Vec_Int_t * vInit;
+    Gia_Obj_t * pObj;
+    int i, status;
+    status = sat_solver_solve( p->pSat, NULL, NULL, p->pPars->nBTLimit, 0, 0, 0 );
+    if ( status != l_True ) // unsat or undec
+        return NULL;
+    vInit = Vec_IntAlloc( Gia_ManPiNum(p->pFraig) );
+    Gia_ManForEachPi( p->pFraig, pObj, i )
+        Vec_IntPush( vInit, sat_solver_var_value(p->pSat, Ssc_ObjSatNum(p, pObj)) );
+    return vInit;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/ssc/sscSim.c b/src/proof/ssc/sscSim.c
new file mode 100644
index 00000000..86837000
--- /dev/null
+++ b/src/proof/ssc/sscSim.c
@@ -0,0 +1,294 @@
+/**CFile****************************************************************
+
+  FileName    [sscSim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT sweeping under constraints.]
+
+  Synopsis    [Simulation procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: sscSim.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sscInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline word Ssc_Random()            { return ((word)Gia_ManRandom(0) << 32) | ((word)Gia_ManRandom(0) << 0);              }
+static inline word Ssc_Random1( int Bit )  { return ((word)Gia_ManRandom(0) << 32) | ((word)Gia_ManRandom(0) << 1) | (word)Bit;  }
+static inline word Ssc_Random2()           { return ((word)Gia_ManRandom(0) << 32) | ((word)Gia_ManRandom(0) << 2) | (word)2;    }
+
+static inline void Ssc_SimAnd( word * pSim, word * pSim0, word * pSim1, int nWords, int fComp0, int fComp1 )
+{
+    int w;
+    if ( fComp0 && fComp1 )
+        for ( w = 0; w < nWords; w++ )
+            pSim[w] = ~(pSim0[w] | pSim1[w]);
+    else if ( fComp0 )
+        for ( w = 0; w < nWords; w++ )
+            pSim[w] = ~pSim0[w] & pSim1[w];
+    else if ( fComp1 )
+        for ( w = 0; w < nWords; w++ )
+            pSim[w] = pSim0[w] & ~pSim1[w];
+    else
+        for ( w = 0; w < nWords; w++ )
+            pSim[w] = pSim0[w] & pSim1[w];
+}
+
+static inline void Ssc_SimDup( word * pSim, word * pSim0, int nWords, int fComp0 )
+{
+    int w;
+    if ( fComp0 )
+        for ( w = 0; w < nWords; w++ )
+            pSim[w] = ~pSim0[w];
+    else
+        for ( w = 0; w < nWords; w++ )
+            pSim[w] = pSim0[w];
+}
+
+static inline void Ssc_SimConst( word * pSim, int nWords, int fComp0 )
+{
+    int w;
+    if ( fComp0 )
+        for ( w = 0; w < nWords; w++ )
+            pSim[w] = ~(word)0;
+    else
+        for ( w = 0; w < nWords; w++ )
+            pSim[w] = 0;
+}
+
+static inline void Ssc_SimOr( word * pSim, word * pSim0, int nWords, int fComp0 )
+{
+    int w;
+    if ( fComp0 )
+        for ( w = 0; w < nWords; w++ )
+            pSim[w] |= ~pSim0[w];
+    else
+        for ( w = 0; w < nWords; w++ )
+            pSim[w] |= pSim0[w];
+}
+
+static inline int Ssc_SimFindBitWord( word t )
+{
+    int n = 0;
+    if ( t == 0 ) return -1;
+    if ( (t & 0x00000000FFFFFFFF) == 0 ) { n += 32; t >>= 32; }
+    if ( (t & 0x000000000000FFFF) == 0 ) { n += 16; t >>= 16; }
+    if ( (t & 0x00000000000000FF) == 0 ) { n +=  8; t >>=  8; }
+    if ( (t & 0x000000000000000F) == 0 ) { n +=  4; t >>=  4; }
+    if ( (t & 0x0000000000000003) == 0 ) { n +=  2; t >>=  2; }
+    if ( (t & 0x0000000000000001) == 0 ) { n++; }
+    return n;
+}
+static inline int Ssc_SimFindBit( word * pSim, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        if ( pSim[w] )
+            return 64*w + Ssc_SimFindBitWord(pSim[w]);
+    return -1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Vec_WrdDoubleSimInfo( Vec_Wrd_t * p, int nObjs )
+{
+    word * pArray = ABC_CALLOC( word, 2 * Vec_WrdSize(p) );
+    int i, nWords = Vec_WrdSize(p) / nObjs;
+    assert( Vec_WrdSize(p) % nObjs == 0 );
+    for ( i = 0; i < nObjs; i++ )
+        memcpy( pArray + 2*i*nWords, p->pArray + i*nWords, sizeof(word) * nWords );
+    ABC_FREE( p->pArray ); p->pArray = pArray;
+    p->nSize = p->nCap = 2*nWords*nObjs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssc_GiaResetPiPattern( Gia_Man_t * p, int nWords )
+{
+    p->iPatsPi = 0;
+    if ( p->vSimsPi == NULL )
+        p->vSimsPi = Vec_WrdStart(0);
+    Vec_WrdFill( p->vSimsPi, nWords * Gia_ManPiNum(p), 0 );
+    assert( nWords == Gia_ObjSimWords( p ) );
+}
+void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot )
+{
+    word * pSimPi;
+    int i, w;
+    Ssc_GiaResetPiPattern( p, nWords );
+    pSimPi = Gia_ObjSimPi( p, 0 );
+    for ( i = 0; i < Gia_ManPiNum(p); i++, pSimPi += nWords )
+    {
+        pSimPi[0] = vPivot ? Ssc_Random1(Vec_IntEntry(vPivot, i)) : Ssc_Random2();
+        for ( w = 1; w < nWords; w++ )
+            pSimPi[w] = Ssc_Random();
+//        if ( i < 10 )
+//            Extra_PrintBinary( stdout, (unsigned *)pSimPi, 64 ), printf( "\n" );
+    }
+}
+void Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat )
+{
+    word * pSimPi;
+    int i;
+    assert( Vec_IntSize(vPat) == Gia_ManPiNum(p) );
+    if ( p->iPatsPi == 64 * Gia_ObjSimWords(p) )
+        Vec_WrdDoubleSimInfo( p->vSimsPi, Gia_ManPiNum(p) );
+    assert( p->iPatsPi < 64 * Gia_ObjSimWords(p) );
+    pSimPi = Gia_ObjSimPi( p, 0 );
+    for ( i = 0; i < Gia_ManPiNum(p); i++, pSimPi += Gia_ObjSimWords(p) )
+        if ( Vec_IntEntry(vPat, i) )
+            Abc_InfoSetBit( (unsigned *)pSimPi, p->iPatsPi );
+    p->iPatsPi++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssc_GiaResetSimInfo( Gia_Man_t * p )
+{
+    assert( Vec_WrdSize(p->vSimsPi) % Gia_ManPiNum(p) == 0 );
+    if ( p->vSims == NULL )
+        p->vSims = Vec_WrdAlloc(0);
+    Vec_WrdFill( p->vSims, Gia_ObjSimWords(p) * Gia_ManObjNum(p), 0 );
+}
+void Ssc_GiaSimRound( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    word * pSim, * pSim0, * pSim1;
+    int i, nWords = Gia_ObjSimWords(p);
+    Ssc_GiaResetSimInfo( p );
+    assert( nWords == Vec_WrdSize(p->vSims) / Gia_ManObjNum(p) );
+    // constant node
+    Ssc_SimConst( Gia_ObjSim(p, 0), nWords, 0 );
+    // primary inputs
+    pSim = Gia_ObjSim( p, 1 );
+    pSim0 = Gia_ObjSimPi( p, 0 );
+    Gia_ManForEachPi( p, pObj, i )
+    {
+        assert( pSim == Gia_ObjSimObj( p, pObj ) );
+        Ssc_SimDup( pSim, pSim0, nWords, 0 );
+        pSim += nWords;
+        pSim0 += nWords;
+    }
+    // intermediate nodes
+    pSim = Gia_ObjSim( p, 1+Gia_ManPiNum(p) );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        assert( pSim == Gia_ObjSim( p, i ) );
+        pSim0 = pSim - pObj->iDiff0 * nWords;
+        pSim1 = pSim - pObj->iDiff1 * nWords;
+        Ssc_SimAnd( pSim, pSim0, pSim1, nWords, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj) );
+        pSim += nWords;
+    }
+    // primary outputs
+    pSim = Gia_ObjSim( p, Gia_ManObjNum(p) - Gia_ManPoNum(p) );
+    Gia_ManForEachPo( p, pObj, i )
+    {
+        assert( pSim == Gia_ObjSimObj( p, pObj ) );
+        pSim0 = pSim - pObj->iDiff0 * nWords;
+        Ssc_SimDup( pSim, pSim0, nWords, Gia_ObjFaninC0(pObj) );
+        pSim += nWords;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns one SAT assignment of the PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p )
+{
+    Vec_Int_t * vInit;
+    Gia_Obj_t * pObj;
+    int i, iBit, nWords = Gia_ObjSimWords( p );
+    word * pRes = ABC_FALLOC( word, nWords );
+    Gia_ManForEachPo( p, pObj, i )
+        Ssc_SimAnd( pRes, pRes, Gia_ObjSimObj(p, pObj), nWords, 0, 0 );
+    iBit = Ssc_SimFindBit( pRes, nWords );
+    ABC_FREE( pRes );
+    if ( iBit == -1 )
+        return NULL;
+    vInit = Vec_IntAlloc( 100 );
+    Gia_ManForEachPi( p, pObj, i )
+        Vec_IntPush( vInit, Abc_InfoHasBit((unsigned *)Gia_ObjSimObj(p, pObj), iBit) );
+    return vInit;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p )
+{
+    Vec_Int_t * vInit;
+    Ssc_GiaRandomPiPattern( p, 1, NULL );
+    Ssc_GiaSimRound( p );
+    vInit = Ssc_GiaGetOneSim( p );
+    return vInit;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/ssc/sscUtil.c b/src/proof/ssc/sscUtil.c
new file mode 100644
index 00000000..a96503d0
--- /dev/null
+++ b/src/proof/ssc/sscUtil.c
@@ -0,0 +1,152 @@
+/**CFile****************************************************************
+
+  FileName    [sscUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT sweeping under constraints.]
+
+  Synopsis    [Various utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: sscUtil.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sscInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Hsh_Obj_t_ Hsh_Obj_t;
+struct Hsh_Obj_t_
+{
+    int              iThis;
+    int              iNext;
+};
+
+typedef struct Hsh_Man_t_ Hsh_Man_t;
+struct Hsh_Man_t_
+{
+    unsigned *       pData;   // user's data
+    int *            pTable;  // hash table
+    Hsh_Obj_t *      pObjs;
+    int              nObjs;
+    int              nSize;
+    int              nTableSize;
+};
+
+static inline int *        Hsh_ObjData( Hsh_Man_t * p, int iThis )      { return p->pData + p->nSize * iThis;         }
+static inline Hsh_Obj_t *  Hsh_ObjGet( Hsh_Man_t * p, int iObj )        { return iObj == -1 ? NULL : p->pObjs + iObj;  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hsh_Man_t * Hsh_ManStart( unsigned * pData, int nDatas, int nSize )
+{
+    Hsh_Man_t * p;
+    p = ABC_CALLOC( Hsh_Man_t, 1 );
+    p->pData = pData;
+    p->nSize = nSize;
+    p->nTableSize = Abc_PrimeCudd( nDatas );
+    p->pTable = ABC_FALLOC( int, p->nTableSize );
+    p->pObjs  = ABC_FALLOC( Hsh_Obj_t, p->nTableSize );
+    return p;
+}
+void Hsh_ManStop( Hsh_Man_t * p )
+{
+    ABC_FREE( p->pObjs );
+    ABC_FREE( p->pTable );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Hsh_ManHash( unsigned * pData, int nSize, int nTableSize )
+{
+    static unsigned s_BigPrimes[7] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457};
+    unsigned char * pDataC = (unsigned char *)pData;
+    int c, nChars = nSize * 4, Key = 0;
+    for ( c = 0; c < nChars; c++ )
+        Key += pDataC[c] * s_BigPrimes[c % 7];
+    return Key % nTableSize;
+}
+int Hsh_ManAdd( Hsh_Man_t * p, int iThis )
+{
+    Hsh_Obj_t * pObj;
+    int * pThis = Hsh_ObjData( p, iThis );
+    int * pPlace = p->pTable + Hsh_ManHash( pThis, p->nSize, p->nTableSize );
+    for ( pObj = Hsh_ObjGet(p, *pPlace); pObj; pObj = Hsh_ObjGet(p, pObj->iNext) )
+        if ( !memcmp( pThis, Hsh_ObjData(p, pObj->iThis), sizeof(int) * p->nSize ) )
+            return pObj - p->pObjs;
+    assert( p->nObjs < p->nTableSize );
+    pObj = p->pObjs + p->nObjs;
+    pObj->iThis = iThis;
+    return (*pPlace = p->nObjs++);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Hashes data by value.]
+
+  Description [Array of 'nTotal' int entries, each of size 'nSize' ints,
+  is hashed and the resulting unique numbers is returned in the array.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Hsh_ManHashData( int * pData, int nDatas, int nSize, int nInts )
+{
+    Vec_Int_t * vRes;
+    Hsh_Man_t * p;
+    int i;
+    assert( nDatas * nSize == nInts );
+    p = Hsh_ManStart( pData, nDatas, nSize );
+    vRes = Vec_IntAlloc( 1000 );
+    for ( i = 0; i < nDatas; i++ )
+        Vec_IntPush( vRes, Hsh_ManAdd(p, i) );
+    Hsh_ManStop( p );
+    return vRes;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+