Experiments with circuit-based SAT.

src/aig/gia/gia.c

@@ -26,6 +26,43 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
+ 
+typedef struct Slv_Man_t_ Slv_Man_t;
+struct Slv_Man_t_
+{
+    Vec_Int_t      vCis;
+    Vec_Int_t      vCos;
+    Vec_Int_t      vFanins;
+    Vec_Int_t      vFanoutN;
+    Vec_Int_t      vFanout0;
+    Vec_Str_t      vValues;
+    Vec_Int_t      vCopies;
+};
+
+static inline int  Slv_ManObjNum       ( Slv_Man_t * p )                      { return Vec_IntSize(&p->vFanins)/2;                       }
+
+static inline int  Slv_ObjFaninLit     ( Slv_Man_t * p, int iObj, int f )     { return Vec_IntEntry(&p->vFanins, Abc_Var2Lit(iObj, f));  }
+static inline int  Slv_ObjFanin        ( Slv_Man_t * p, int iObj, int f )     { return Abc_Lit2Var(Slv_ObjFaninLit(p, iObj, f));         }
+static inline int  Slv_ObjFaninC       ( Slv_Man_t * p, int iObj, int f )     { return Abc_LitIsCompl(Slv_ObjFaninLit(p, iObj, f));      }
+
+static inline int  Slv_ObjIsCi         ( Slv_Man_t * p, int iObj )            { return !Slv_ObjFaninLit(p, iObj, 0) &&  Slv_ObjFaninLit(p, iObj, 1);  }
+static inline int  Slv_ObjIsCo         ( Slv_Man_t * p, int iObj )            { return  Slv_ObjFaninLit(p, iObj, 0) && !Slv_ObjFaninLit(p, iObj, 1);  }
+static inline int  Slv_ObjIsAnd        ( Slv_Man_t * p, int iObj )            { return  Slv_ObjFaninLit(p, iObj, 0) &&  Slv_ObjFaninLit(p, iObj, 1);  }
+
+static inline int  Slv_ObjFanout0      ( Slv_Man_t * p, int iObj )            { return Vec_IntEntry(&p->vFanout0, iObj);      }
+static inline void Slv_ObjSetFanout0   ( Slv_Man_t * p, int iObj, int iLit )  { Vec_IntWriteEntry(&p->vFanout0, iObj, iLit);  }
+
+static inline int  Slv_ObjNextFanout   ( Slv_Man_t * p, int iLit )            { return Vec_IntEntry(&p->vFanoutN, iLit);      }
+static inline void Slv_ObjSetNextFanout( Slv_Man_t * p, int iLit, int iLitF ) { Vec_IntWriteEntry(&p->vFanoutN, iLit, iLitF); }
+
+static inline int  Slv_ObjCopyLit      ( Slv_Man_t * p, int iObj )            { return Vec_IntEntry(&p->vCopies, iObj);       }
+static inline void Slv_ObjSetCopyLit   ( Slv_Man_t * p, int iObj, int iLit )  { Vec_IntWriteEntry(&p->vCopies, iObj, iLit);   }
+
+#define Slv_ManForEachObj( p, iObj )                                  \
+    for ( iObj = 1; iObj < Slv_ManObjNum(p); iObj++ )
+
+#define Slv_ObjForEachFanout( p, iObj, iFanLit )                      \
+    for ( iFanLit = Slv_ObjFanout0(p, iObj); iFanLit; iFanLit = Slv_ObjNextFanout(p, iFanLit) )
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -42,6 +79,128 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+Slv_Man_t * Slv_ManAlloc( int nObjs )
+{
+    Slv_Man_t * p = ABC_CALLOC( Slv_Man_t, 1 );
+    Vec_IntGrow( &p->vCis,     100 );
+    Vec_IntGrow( &p->vCos,     100 );
+    Vec_IntGrow( &p->vFanins,  2*nObjs );
+    Vec_IntGrow( &p->vFanoutN, 2*nObjs );
+    Vec_IntGrow( &p->vFanout0, nObjs );
+    Vec_StrGrow( &p->vValues,  nObjs );
+    // constant node
+    Vec_IntFill( &p->vFanins,  2, 0 );
+    Vec_IntFill( &p->vFanoutN, 2, 0 );
+    Vec_IntFill( &p->vFanout0, 1, 0 );
+    return p;
+}
+void Slv_ManFree( Slv_Man_t * p )
+{
+    Vec_IntErase( &p->vCis     );
+    Vec_IntErase( &p->vCos     );
+    Vec_IntErase( &p->vFanins  );
+    Vec_IntErase( &p->vFanoutN );
+    Vec_IntErase( &p->vFanout0 );
+    Vec_StrErase( &p->vValues  );
+    Vec_IntErase( &p->vCopies  );
+    ABC_FREE( p );
+}
+void Slv_ManPrintFanouts( Slv_Man_t * p )
+{
+    int iObj, iFanLit;
+    Slv_ManForEachObj( p, iObj )
+    {
+        printf( "Fanouts of node %d: ", iObj );
+        Slv_ObjForEachFanout( p, iObj, iFanLit )
+            printf( "%d ", Abc_Lit2Var(iFanLit) );
+        printf( "\n" );
+    }
+}
+static inline int Slv_ManAppendObj( Slv_Man_t * p, int iLit0, int iLit1 )
+{
+    int iObj = Slv_ManObjNum(p);
+    Vec_StrPush( &p->vValues,  0 );
+    Vec_IntPush( &p->vFanout0, 0 );
+    Vec_IntPushTwo( &p->vFanoutN, 0, 0 );
+    if ( !iLit0 )  // primary input
+        assert(!iLit1), iLit1 = Vec_IntSize(&p->vCis)+1, Vec_IntPush(&p->vCis, iObj);
+    else if ( !iLit1 )  // primary output
+        assert(iLit0), Vec_IntPush(&p->vCos, iObj);
+    else
+    {
+        Slv_ObjSetNextFanout( p, Abc_Var2Lit(iObj, 0), Slv_ObjFanout0(p, Abc_Lit2Var(iLit0)) );
+        Slv_ObjSetNextFanout( p, Abc_Var2Lit(iObj, 1), Slv_ObjFanout0(p, Abc_Lit2Var(iLit1)) );
+        Slv_ObjSetFanout0( p, Abc_Lit2Var(iLit0), Abc_Var2Lit(iObj, 0) );
+        Slv_ObjSetFanout0( p, Abc_Lit2Var(iLit1), Abc_Var2Lit(iObj, 1) );
+    }
+    Vec_IntPushTwo( &p->vFanins, iLit0, iLit1 );
+    return Abc_Var2Lit( iObj, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Slv_Man_t * Slv_ManFromGia( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj; int i;
+    Slv_Man_t * pNew = Slv_ManAlloc( Gia_ManObjNum(p) );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Slv_ManAppendObj( pNew, Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj)), Abc_LitNotCond(Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj)) );
+        else if ( Gia_ObjIsCo(pObj) )
+            pObj->Value = Slv_ManAppendObj( pNew, Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj)), 0 );
+        else if ( Gia_ObjIsCi(pObj) )
+            pObj->Value = Slv_ManAppendObj( pNew, 0, 0 );
+        else
+            assert( 0 );
+    }
+    assert( Gia_ManObjNum(p) == Slv_ManObjNum(pNew) );
+    return pNew;
+}
+Gia_Man_t * Slv_ManToGia( Slv_Man_t * p )
+{
+    int iObj;
+    Gia_Man_t * pNew = Gia_ManStart( Slv_ManObjNum(p) ); 
+    Vec_IntFill( &p->vCopies,  Slv_ManObjNum(p), 0 );
+    Slv_ManForEachObj( p, iObj )
+        if ( Slv_ObjIsCi(p, iObj) )
+            Slv_ObjSetCopyLit( p, iObj, Gia_ManAppendCi(pNew) );
+        else if ( Slv_ObjIsCo(p, iObj) )
+        {
+            int iLit0 = Abc_LitNotCond( Slv_ObjCopyLit(p, Slv_ObjFanin(p, iObj, 0)), Slv_ObjFaninC(p, iObj, 0) );
+            Slv_ObjSetCopyLit( p, iObj, Gia_ManAppendCo(pNew, iLit0) );
+        }
+        else if ( Slv_ObjIsAnd(p, iObj) )
+        {
+            int iLit0 = Abc_LitNotCond( Slv_ObjCopyLit(p, Slv_ObjFanin(p, iObj, 0)), Slv_ObjFaninC(p, iObj, 0) );
+            int iLit1 = Abc_LitNotCond( Slv_ObjCopyLit(p, Slv_ObjFanin(p, iObj, 1)), Slv_ObjFaninC(p, iObj, 1) );
+            Slv_ObjSetCopyLit( p, iObj, Gia_ManAppendAnd(pNew, iLit0, iLit1) );
+        }
+        else assert(0);
+    assert( Gia_ManObjNum(pNew) == Slv_ManObjNum(p) );
+    return pNew;
+}
+
+Gia_Man_t * Slv_ManToAig( Gia_Man_t * pGia )
+{
+    Slv_Man_t * p = Slv_ManFromGia( pGia );
+    Gia_Man_t * pNew = Slv_ManToGia( p );
+    pNew->pName = Abc_UtilStrsav( pGia->pName );
+    pNew->pSpec = Abc_UtilStrsav( pGia->pSpec );
+    Slv_ManPrintFanouts( p );
+    Slv_ManFree( p );
+    return pNew;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/aig/gia/giaCSat.c

@@ -285,6 +285,7 @@ static inline int Cbs_QueIsEmpty( Cbs_Que_t * p )
 ***********************************************************************/
 static inline void Cbs_QuePush( Cbs_Que_t * p, Gia_Obj_t * pObj )
 {
+    assert( !Gia_IsComplement(pObj) );
     if ( p->iTail == p->nSize )
     {
         p->nSize *= 2;

src/aig/gia/module.make

@@ -13,6 +13,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaCone.c \
     src/aig/gia/giaCSatOld.c \
     src/aig/gia/giaCSat.c \
+    src/aig/gia/giaCSat2.c \
     src/aig/gia/giaCTas.c \
     src/aig/gia/giaCut.c \
     src/aig/gia/giaDfs.c \

src/base/abci/abc.c

@@ -33640,13 +33640,14 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    extern Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
     Cec_ParSat_t ParsSat, * pPars = &ParsSat;
     Gia_Man_t * pTemp;
     int c;
-    int fCSat = 0;
+    int fNewSolver = 0, fCSat = 0;
     Cec_ManSatSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CSNnmtcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CSNanmtcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -33683,6 +33684,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nCallsRecycle < 0 )
                 goto usage;
             break;
+        case 'a':
+            fNewSolver ^= 1;
+            break;
         case 'n':
             pPars->fNonChrono ^= 1;
             break;
@@ -33711,7 +33715,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         Vec_Int_t * vCounters;
         Vec_Str_t * vStatus;
-        if ( pPars->fLearnCls )
+        if ( fNewSolver )
+            vCounters = Cbs2_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose );
+        else if ( pPars->fLearnCls )
             vCounters = Tas_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose );
         else if ( pPars->fNonChrono )
             vCounters = Cbs_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose );
@@ -33728,11 +33734,12 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &sat [-CSN <num>] [-nmctvh]\n" );
+    Abc_Print( -2, "usage: &sat [-CSN <num>] [-anmctvh]\n" );
     Abc_Print( -2, "\t         performs SAT solving for the combinational outputs\n" );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
     Abc_Print( -2, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
+    Abc_Print( -2, "\t-a     : toggle using new solver [default = %s]\n", fNewSolver? "yes": "no" );
     Abc_Print( -2, "\t-n     : toggle using non-chronological backtracking [default = %s]\n", pPars->fNonChrono? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
     Abc_Print( -2, "\t-c     : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" );
@@ -44856,6 +44863,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Gia_ParTest( pAbc->pGia, nWords, nProcs );
 //    Gia_StoComputeCuts( pAbc->pGia );
 //    printf( "\nThis command is currently disabled.\n\n" );
+/*
     {
         char Buffer[10];
         extern void Gia_DumpLutSizeDistrib( Gia_Man_t * p, char * pFileName );
@@ -44863,6 +44871,9 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( pAbc->pGia )
             Gia_DumpLutSizeDistrib( pAbc->pGia, Buffer );
     }
+*/
+//    pTemp = Slv_ManToAig( pAbc->pGia );
+//    Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 usage:
     Abc_Print( -2, "usage: &test [-FW num] [-svh]\n" );

src/proof/cec/cecCore.c

@@ -48,7 +48,7 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
     p->nBTLimit       =     100;  // conflict limit at a node
     p->nSatVarMax     =    2000;  // the max number of SAT variables
     p->nCallsRecycle  =     200;  // calls to perform before recycling SAT solver
-    p->fNonChrono     =       0;  // use non-chronological backtracling (for circuit SAT only)
+    p->fNonChrono     =       1;  // use non-chronological backtracling (for circuit SAT only)
     p->fPolarFlip     =       1;  // flops polarity of variables
     p->fCheckMiter    =       0;  // the circuit is the miter
 //    p->fFirstStop     =       0;  // stop on the first sat output