Experiments with SAT-based collapsing.

5 files changed, 132 insertions, 53 deletions

diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index bb960ddc..e1b042b8 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -970,7 +970,7 @@ Vec_Int_t * Abc_NtkNodeSupportInt( Abc_Ntk_t * pNtk, int iCo )
 int Abc_NtkFunctionalIsoGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode )
 {
     int iLit0, iLit1;
-    if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 )
+    if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 || Abc_ObjIsCi(pNode) )
         return pNode->iTemp;
     assert( Abc_ObjIsNode( pNode ) );
     Abc_NodeSetTravIdCurrent( pNode );
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index e8ab3f7a..1536fe0c 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -256,7 +256,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
 int Abc_NtkClpOneGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode )
 {
     int iLit0, iLit1;
-    if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 )
+    if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 || Abc_ObjIsCi(pNode) )
         return pNode->iTemp;
     assert( Abc_ObjIsNode( pNode ) );
     Abc_NodeSetTravIdCurrent( pNode );
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c
index d0948176..15cac4bb 100644
--- a/src/sat/bmc/bmcClp.c
+++ b/src/sat/bmc/bmcClp.c
@@ -38,7 +38,7 @@ extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfOb
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Performs one round of removing literals.]
 
   Description []
                
@@ -47,7 +47,7 @@ extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfOb
   SeeAlso     []
 
 ***********************************************************************/
-int Bmc_CollapseExpandCanon( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit )
+int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon )
 {
     int k, n, iLit, status;
     // try removing one literal at a time
@@ -56,6 +56,26 @@ int Bmc_CollapseExpandCanon( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * v
         int Save = Vec_IntEntry( vLits, k );
         if ( Save == -1 )
             continue;
+        // check if this literal when expanded overlaps with the on-set
+        if ( pSatOn )
+        {
+            // it is ok to skip the first round if the literal is positive
+            if ( fCanon && !Abc_LitIsCompl(Save) )
+                continue;
+            // put into new array
+            Vec_IntClear( vTemp );
+            Vec_IntForEachEntry( vLits, iLit, n )
+                if ( iLit != -1 )
+                    Vec_IntPush( vTemp, Abc_LitNotCond(iLit, k==n) );
+            // check against onset
+            status = sat_solver_solve( pSatOn, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 );
+            if ( status == l_Undef )
+                return -1;
+            //printf( "%d", status == l_True );
+            if ( status == l_False )
+                continue;
+            // otherwise keep trying to remove it
+        }
         Vec_IntWriteEntry( vLits, k, -1 );
         // put into new array
         Vec_IntClear( vTemp );
@@ -69,6 +89,8 @@ int Bmc_CollapseExpandCanon( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * v
         if ( status == l_True )
             Vec_IntWriteEntry( vLits, k, Save );
     }
+//    if ( pSatOn )
+//    printf( "\n" );
     // put into new array
     Vec_IntClear( vNums );
     Vec_IntForEachEntry( vLits, iLit, n )
@@ -79,7 +101,7 @@ int Bmc_CollapseExpandCanon( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * v
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Expends minterm into a cube.]
 
   Description []
                
@@ -88,44 +110,73 @@ int Bmc_CollapseExpandCanon( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * v
   SeeAlso     []
 
 ***********************************************************************/
-int Bmc_CollapseExpand( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit )
+int Bmc_CollapseExpand( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon )
 {
-    int i, k, iLit, status, nFinal, * pFinal;
-    // check against offset
-    status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
-    if ( status == l_Undef )
-        return -1;
-    assert( status == l_False );
-    // get subset of literals
-    nFinal = sat_solver_final( pSat, &pFinal );
-/*
-    // collect literals
-    Vec_IntClear( vNums );
-    for ( i = 0; i < nFinal; i++ )
+    // perform one quick reduction if it is non-canonical
+    if ( !fCanon )
     {
-        iLit = Vec_IntFind( vLits, Abc_LitNot(pFinal[i]) );
-        assert( iLit >= 0 );
-        Vec_IntPush( vNums, iLit );
-    }
-*/
-    // mark unused literals
-    Vec_IntForEachEntry( vLits, iLit, i )
-    {
-        for ( k = 0; k < nFinal; k++ )
-            if ( iLit == Abc_LitNot(pFinal[k]) )
-                break;
-        if ( k == nFinal )
-            Vec_IntWriteEntry( vLits, i, -1 );
+        int i, k, iLit, status, nFinal, * pFinal;
+        // check against offset
+        status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
+        if ( status == l_Undef )
+            return -1;
+        assert( status == l_False );
+        // get subset of literals
+        nFinal = sat_solver_final( pSat, &pFinal );
+        // mark unused literals
+        Vec_IntForEachEntry( vLits, iLit, i )
+        {
+            for ( k = 0; k < nFinal; k++ )
+                if ( iLit == Abc_LitNot(pFinal[k]) )
+                    break;
+            if ( k == nFinal )
+                Vec_IntWriteEntry( vLits, i, -1 );
+        }
     }
-    Bmc_CollapseExpandCanon( pSat, vLits, vNums, vTemp, nBTLimit );
+    Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon );
+    Bmc_CollapseExpandRound( pSat, NULL,   vLits, vNums, vTemp, nBTLimit, fCanon );
+    return 0;
+}
 
-/*
-    int i;
-    Vec_IntClear( vNums );
+/**Function*************************************************************
+
+  Synopsis    [Returns SAT solver in the 'sat' state with the given assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bmc_ComputeCanonical( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTemp, int nBTLimit )
+{
+    int i, k, iLit, status = l_Undef;
     for ( i = 0; i < Vec_IntSize(vLits); i++ )
-        Vec_IntPush( vNums, i );
-*/
-    return 0;
+    {
+        // copy the first i+1 literals
+        Vec_IntClear( vTemp );
+        Vec_IntForEachEntryStop( vLits, iLit, k, i+1 )
+            Vec_IntPush( vTemp, iLit );
+        // check if it satisfies the on-set
+        status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 );
+        if ( status == l_Undef )
+            return l_Undef;
+        if ( status == l_True )
+            continue;
+        // if it is UNSAT, try the opposite literal
+        iLit = Vec_IntEntry( vLits, i );
+        // if literal is positive, there is no way to flip it
+        if ( !Abc_LitIsCompl(iLit) )
+            return l_False;
+        Vec_IntWriteEntry( vLits, i, Abc_LitNot(iLit) );
+        Vec_IntForEachEntryStart( vLits, iLit, k, i+1 )
+            Vec_IntWriteEntry( vLits, k, Abc_LitNot(Abc_LitRegular(iLit)) );
+        // recheck
+        i--;
+    }
+    assert( status == l_True );
+    return status;
 }
 
 /**Function*************************************************************
@@ -145,6 +196,7 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
     int nVars = Gia_ManCiNum(p);
     Vec_Int_t * vVars = Vec_IntAlloc( nVars );
     Vec_Int_t * vLits = Vec_IntAlloc( nVars );
+    Vec_Int_t * vLitsC= Vec_IntAlloc( nVars );
     Vec_Int_t * vNums = Vec_IntAlloc( nVars );
     Vec_Int_t * vCube = Vec_IntAlloc( nVars );
     Vec_Str_t * vSop  = Vec_StrAlloc( 100 );
@@ -152,9 +204,10 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
 
     // create SAT solver
     Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
-    sat_solver * pSat[2] = { 
+    sat_solver * pSat[3] = { 
         (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), 
-        (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) 
+        (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0),
+        fCanon ? (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) : NULL
     };
 
     // collect CI variables
@@ -162,14 +215,18 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
     for ( n = 0; n < nVars; n++ )
         Vec_IntPush( vVars, iCiVarBeg + n );
 
+    // start with all negative literals
+    Vec_IntForEachEntry( vVars, iVar, n )
+        Vec_IntPush( vLitsC, Abc_Var2Lit(iVar, 1) );
+
     // check that on-set/off-set is sat
-    for ( n = 0; n < 2; n++ )
+    for ( n = 0; n < 2 + fCanon; n++ )
     {
-        iLit = Abc_Var2Lit( iOut + 1, n ); // n=0 => F=1   n=1 => F=0
+        iLit = Abc_Var2Lit( iOut + 1, n&1 ); // n=0 => F=1   n=1 => F=0
         status = sat_solver_addclause( pSat[n], &iLit, &iLit + 1 );
         if ( status == 0 )
         {
-            Vec_StrPrintStr( vSop, (n ^ fCompl) ? " 1\n" : " 0\n" );
+            Vec_StrPrintStr( vSop, ((n&1) ^ fCompl) ? " 1\n" : " 0\n" );
             Vec_StrPush( vSop, '\0' );
             goto cleanup; // const0/1
         }
@@ -181,7 +238,7 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
         }
         if ( status == l_False )
         {
-            Vec_StrPrintStr( vSop, (n ^ fCompl) ? " 1\n" : " 0\n" );
+            Vec_StrPrintStr( vSop, ((n&1) ^ fCompl) ? " 1\n" : " 0\n" );
             Vec_StrPush( vSop, '\0' );
             goto cleanup; // const0/1
         }
@@ -189,13 +246,19 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
     Vec_StrPush( vSop, '\0' );
 
     // prepare on-set for solving
-    if ( fCanon )
-        sat_solver_prepare_enum( pSat[0], Vec_IntArray(vVars), Vec_IntSize(vVars) );
+//    if ( fCanon )
+//        sat_solver_prepare_enum( pSat[0], Vec_IntArray(vVars), Vec_IntSize(vVars) );
     Count = 0;
     while ( 1 )
     {
         // get the assignment
-        status = sat_solver_solve( pSat[0], NULL, NULL, 0, 0, 0, 0 );
+        if ( fCanon )
+            status = Bmc_ComputeCanonical( pSat[0], vLitsC, vCube, nBTLimit );
+        else
+        {
+            sat_solver_clean_polarity( pSat[0], Vec_IntArray(vVars), Vec_IntSize(vVars) );
+            status = sat_solver_solve( pSat[0], NULL, NULL, 0, 0, 0, 0 );
+        }
         if ( status == l_Undef )
         {
             Vec_StrFreeP( &vSop );
@@ -212,8 +275,13 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
         }
         // collect values
         Vec_IntClear( vLits );
+        Vec_IntClear( vLitsC );
         Vec_IntForEachEntry( vVars, iVar, n )
-            Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[0], iVar)) );
+        {
+            iLit = Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[0], iVar));
+            Vec_IntPush( vLits, iLit );
+            Vec_IntPush( vLitsC, iLit );
+        }
         // print minterm
         if ( fPrintMinterm )
         {
@@ -223,10 +291,7 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
             printf( "\n" );
         }
         // expand the values
-        if ( fCanon )
-            status = Bmc_CollapseExpandCanon( pSat[1], vLits, vNums, vCube, nBTLimit );
-        else
-            status = Bmc_CollapseExpand( pSat[1], vLits, vNums, vCube, nBTLimit );
+        status = Bmc_CollapseExpand( pSat[1], fCanon ? pSat[2] : pSat[0], vLits, vNums, vCube, nBTLimit, fCanon );
         if ( status < 0 )
         {
             Vec_StrFreeP( &vSop );
@@ -254,15 +319,22 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
         status = sat_solver_addclause( pSat[0], Vec_IntArray(vCube), Vec_IntLimit(vCube) );
         if ( status == 0 )
             break;
+        // add cube
+        if ( fCanon )
+            status = sat_solver_addclause( pSat[2], Vec_IntArray(vCube), Vec_IntLimit(vCube) );
+        assert( status == 1 );
     }
     //printf( "Finished enumerating %d assignments.\n", Count );
 cleanup:
     Vec_IntFree( vVars );
     Vec_IntFree( vLits );
+    Vec_IntFree( vLitsC );
     Vec_IntFree( vNums );
     Vec_IntFree( vCube );
     sat_solver_delete( pSat[0] );
     sat_solver_delete( pSat[1] );
+    if ( fCanon )
+    sat_solver_delete( pSat[2] );
     Cnf_DataFree( pCnf );
     return vSop;
 }
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 053b0587..24c60dac 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1861,7 +1861,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
             int fConfl = sat_solver_propagate(s);
             if (fConfl){
                 sat_solver_analyze_final(s, fConfl, 0);
-                assert(s->conf_final.size > 0);
+                //assert(s->conf_final.size > 0);
                 sat_solver_canceluntil(s, 0);
                 return l_False; }
         }
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 8e171031..89391d2d 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -234,6 +234,13 @@ static void sat_solver_prepare_enum(sat_solver* s, int * pVars, int nVars )
     for ( v = 0; v < nVars; v++ )
         veci_push(&s->vDeciVars,pVars[v]);
 }
+static void sat_solver_clean_polarity(sat_solver* s, int * pVars, int nVars )
+{
+    int i;
+    assert( veci_size(&s->vDeciVars) == 0 );
+    for ( i = 0; i < nVars; i++ )
+        s->polarity[pVars[i]] = 0;
+}
 
 static int sat_solver_final(sat_solver* s, int ** ppArray)
 {