Changes to CNF generation code.

3 files changed, 178 insertions, 265 deletions

diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index 97111100..d0011700 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -138,7 +138,10 @@ extern void            Cnf_CutUpdateRefs( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_C
 extern Cnf_Cut_t *     Cnf_CutCompose( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, int iFan );
 /*=== cnfData.c ========================================================*/
 extern void            Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops );
-/*=== cnfData.c ========================================================*/
+/*=== cnfFast.c ========================================================*/
+extern void            Cnf_CollectLeaves( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper, int fStopCompl );
+extern void            Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, 
+                           Vec_Ptr_t * vNodes, Vec_Int_t * vMap, Vec_Int_t * vCover, Vec_Int_t * vClauses );
 extern Cnf_Dat_t *     Cnf_DeriveFast( Aig_Man_t * p, int nOutputs );
 /*=== cnfMan.c ========================================================*/
 extern Cnf_Man_t *     Cnf_ManStart();
diff --git a/src/aig/cnf/cnfFast.c b/src/aig/cnf/cnfFast.c
index 83a273ae..c602c882 100644
--- a/src/aig/cnf/cnfFast.c
+++ b/src/aig/cnf/cnfFast.c
@@ -43,7 +43,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Cnf_CollectSuper_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fStopCompl )
+void Cnf_CollectLeaves_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fStopCompl )
 {
     if ( pRoot != pObj && (pObj->fMarkA || (fStopCompl && Aig_IsComplement(pObj))) )
     {
@@ -53,13 +53,13 @@ void Cnf_CollectSuper_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSup
     assert( Aig_ObjIsNode(pObj) );
     if ( fStopCompl )
     {
-        Cnf_CollectSuper_rec( pRoot, Aig_ObjChild0(pObj), vSuper, 1 );
-        Cnf_CollectSuper_rec( pRoot, Aig_ObjChild1(pObj), vSuper, 1 );
+        Cnf_CollectLeaves_rec( pRoot, Aig_ObjChild0(pObj), vSuper, 1 );
+        Cnf_CollectLeaves_rec( pRoot, Aig_ObjChild1(pObj), vSuper, 1 );
     }
     else
     {
-        Cnf_CollectSuper_rec( pRoot, Aig_ObjFanin0(pObj), vSuper, 0 );
-        Cnf_CollectSuper_rec( pRoot, Aig_ObjFanin1(pObj), vSuper, 0 );
+        Cnf_CollectLeaves_rec( pRoot, Aig_ObjFanin0(pObj), vSuper, 0 );
+        Cnf_CollectLeaves_rec( pRoot, Aig_ObjFanin1(pObj), vSuper, 0 );
     }
 }
 
@@ -74,11 +74,11 @@ void Cnf_CollectSuper_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSup
   SeeAlso     []
 
 ***********************************************************************/
-void Cnf_CollectSuper( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper, int fStopCompl )
+void Cnf_CollectLeaves( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper, int fStopCompl )
 {
     assert( !Aig_IsComplement(pRoot) );
     Vec_PtrClear( vSuper );
-    Cnf_CollectSuper_rec( pRoot, pRoot, vSuper, fStopCompl );
+    Cnf_CollectLeaves_rec( pRoot, pRoot, vSuper, fStopCompl );
 }
 
 /**Function*************************************************************
@@ -169,7 +169,7 @@ word Cnf_CutDeriveTruth( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes
 
 /**Function*************************************************************
 
-  Synopsis    [Marks AIG for CNF computation.]
+  Synopsis    [Collects nodes inside the cone.]
 
   Description []
                
@@ -178,136 +178,94 @@ word Cnf_CutDeriveTruth( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes
   SeeAlso     []
 
 ***********************************************************************/
-void Cnf_DeriveFastMark_( Aig_Man_t * p )
+void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot, 
+    Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Int_t * vMap, Vec_Int_t * vCover, Vec_Int_t * vClauses )
 {
-    Vec_Ptr_t * vLeaves, * vNodes;
-    Aig_Obj_t * pObj, * pObjC, * pObj0, * pObj1;
-    int i, k;
-    // mark CIs
-    Aig_ManForEachPi( p, pObj, i )
-        pObj->fMarkA = 1;
-    // mark CO drivers
-    Aig_ManForEachPo( p, pObj, i )
-        Aig_ObjFanin0(pObj)->fMarkA = 1;
+    Aig_Obj_t * pLeaf;
+    int c, k, Cube, OutLit, RetValue;
+    word Truth;
+    assert( pRoot->fMarkA );
 
+    Vec_IntClear( vClauses );
 
-    // mark roots/leaves of MUX/XOR with MarkA
-    // mark internal nodes of MUX/XOR with MarkB
-    Aig_ManForEachNode( p, pObj, i )
+    OutLit = toLit( Vec_IntEntry(vMap, Aig_ObjId(pRoot)) );
+    // detect cone
+    Cnf_CollectLeaves( pRoot, vLeaves, 0 );
+    Cnf_CollectVolume( p, pRoot, vLeaves, vNodes );
+    assert( pObj == Vec_PtrEntryLast(vNodes) );
+    // check if this is an AND-gate
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pLeaf, k )
     {
-        if ( !Aig_ObjIsMuxType(pObj) )
-            continue;
-        pObjC = Aig_ObjRecognizeMux( pObj, &pObj1, &pObj0 );
-        Aig_Regular(pObjC)->fMarkA = 1;
-        Aig_Regular(pObj1)->fMarkA = 1;
-        Aig_Regular(pObj0)->fMarkA = 1;
-
-        Aig_ObjFanin0(pObj)->fMarkB = 1;
-        Aig_ObjFanin1(pObj)->fMarkB = 1;
+        if ( Aig_ObjFaninC0(pLeaf) && !Aig_ObjFanin0(pLeaf)->fMarkA )
+            break;
+        if ( Aig_ObjFaninC1(pLeaf) && !Aig_ObjFanin1(pLeaf)->fMarkA )
+            break;
     }
-
-    // mark nodes with many fanouts or pointed to by a complemented edge
-    Aig_ManForEachNode( p, pObj, i )
+    if ( k == Vec_PtrSize(vNodes) )
     {
-        if ( Aig_ObjRefs(pObj) > 1 )
-            pObj->fMarkA = 1;
-        if ( Aig_ObjFaninC0(pObj) )
-            Aig_ObjFanin0(pObj)->fMarkA = 1;
-        if ( Aig_ObjFaninC1(pObj) )
-            Aig_ObjFanin1(pObj)->fMarkA = 1;
+        Cnf_CollectLeaves( pRoot, vLeaves, 1 );
+        // write big clause
+        Vec_IntPush( vClauses, 0 );
+        Vec_IntPush( vClauses, OutLit );
+        Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k )
+            Vec_IntPush( vClauses, toLitCond(Vec_IntEntry(vMap, Aig_ObjId(Aig_Regular(pLeaf))), !Aig_IsComplement(pLeaf)) );
+        // write small clauses
+        Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k )
+        {
+            Vec_IntPush( vClauses, 0 );
+            Vec_IntPush( vClauses, lit_neg(OutLit) );
+            Vec_IntPush( vClauses, toLitCond(Vec_IntEntry(vMap, Aig_ObjId(Aig_Regular(pLeaf))), Aig_IsComplement(pLeaf)) );
+        }
+        return;
     }
+    if ( Vec_PtrSize(vLeaves) > 6 )
+        printf( "FastCnfGeneration:  Internal error!!!\n" );
+    assert( Vec_PtrSize(vLeaves) <= 6 );
 
-    // clean internal nodes of MUX/XOR
-    Aig_ManForEachNode( p, pObj, i )
+    Truth = Cnf_CutDeriveTruth( p, vLeaves, vNodes );
+    if ( Truth == 0 || Truth == ~0 )
     {
-        if ( pObj->fMarkB )
-            pObj->fMarkB = pObj->fMarkA = 0;
-//            pObj->fMarkB = 0;
+        assert( RetValue == 0 );
+        Vec_IntPush( vClauses, 0 );
+        Vec_IntPush( vClauses, (Truth == 0) ? lit_neg(OutLit) : OutLit );
+        return;
     }
-    // remove nodes those fanins are used
-    Aig_ManForEachNode( p, pObj, i )
-        if ( pObj->fMarkA && Aig_ObjFanin0(pObj)->fMarkA && Aig_ObjFanin1(pObj)->fMarkA )
-            pObj->fMarkA = 0;
 
-    // mark CO drivers
-    Aig_ManForEachPo( p, pObj, i )
-        Aig_ObjFanin0(pObj)->fMarkA = 1;
-/*
-    // if node has multiple fanout
-    Aig_ManForEachNode( p, pObj, i )
-    {
-        if ( Aig_ObjRefs(pObj) == 1 )
-            continue;
-        if ( Aig_ObjRefs(pObj) == 2 && Aig_ObjFanin0(pObj)->fMarkA && Aig_ObjFanin1(pObj)->fMarkA )
-            continue;
-        pObj->fMarkA = 1;
-    }
-*/
-    // consider large cuts and mark inputs that are
-    vLeaves = Vec_PtrAlloc( 100 );
-    vNodes  = Vec_PtrAlloc( 100 );
-/*
-    while ( 1 )
+    RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
+    assert( RetValue >= 0 );
+
+    Vec_IntForEachEntry( vCover, Cube, c )
     {
-        int fChanges = 0;
-        Aig_ManForEachNode( p, pObj, i )
+        Vec_IntPush( vClauses, 0 );
+        Vec_IntPush( vClauses, OutLit );
+        for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 )
         {
-            if ( !pObj->fMarkA )
-                continue;
-            if ( Aig_ObjRefs(pObj) == 1 )
+            if ( (Cube & 3) == 0 )
                 continue;
-
-            Cnf_CollectSuper( pObj, vLeaves, 1 );
-            if ( Vec_PtrSize(vLeaves) <= 6 )
-                continue;
-            Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObjC, k )
-            {
-                if ( Aig_Regular(pObjC)->fMarkA == 0 )
-                    fChanges = 1;
-                Aig_Regular(pObjC)->fMarkA = 1;
-            }
+            assert( (Cube & 3) != 3 );
+            Vec_IntPush( vClauses, toLitCond( Vec_IntEntry(vMap, Aig_ObjId(Vec_PtrEntry(vLeaves,k))), (Cube&3)!=1 ) );
         }
-        printf( "Round 1 \n" );
-        if ( !fChanges )
-            break;
     }
-*/
-    while ( 1 )
+
+    Truth = ~Truth;
+
+    RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
+    assert( RetValue >= 0 );
+    Vec_IntForEachEntry( vCover, Cube, c )
     {
-        int fChanges = 0;
-        Aig_ManForEachNode( p, pObj, i )
+        Vec_IntPush( vClauses, 0 );
+        Vec_IntPush( vClauses, lit_neg(OutLit) );
+        for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 )
         {
-            if ( !pObj->fMarkA )
-                continue;
-            Cnf_CollectSuper( pObj, vLeaves, 0 );
-            if ( Vec_PtrSize(vLeaves) <= 6 )
+            if ( (Cube & 3) == 0 )
                 continue;
-            Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
-            Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObjC, k )
-            {
-                if ( Aig_ObjFaninC0(pObjC) && !Aig_ObjFanin0(pObjC)->fMarkA )
-                {
-                    Aig_ObjFanin0(pObjC)->fMarkA = 1;
-//                    printf( "%d ", Aig_ObjFaninId0(pObjC) );
-                    fChanges = 1;
-                }
-                if ( Aig_ObjFaninC1(pObjC) && !Aig_ObjFanin1(pObjC)->fMarkA )
-                {
-                    Aig_ObjFanin1(pObjC)->fMarkA = 1;
-//                    printf( "%d ", Aig_ObjFaninId1(pObjC) );
-                    fChanges = 1;
-                }
-            }
+            assert( (Cube & 3) != 3 );
+            Vec_IntPush( vClauses, toLitCond( Vec_IntEntry(vMap, Aig_ObjId(Vec_PtrEntry(vLeaves,k))), (Cube&3)!=1 ) );
         }
-        printf( "Round 2\n" );
-        if ( !fChanges )
-            break;
     }
+}
 
 
-    Vec_PtrFree( vLeaves );
-    Vec_PtrFree( vNodes );
-}
 
 /**Function*************************************************************
 
@@ -322,10 +280,14 @@ void Cnf_DeriveFastMark_( Aig_Man_t * p )
 ***********************************************************************/
 void Cnf_DeriveFastMark( Aig_Man_t * p )
 {
+    Vec_Int_t * vSupps;
     Vec_Ptr_t * vLeaves, * vNodes;
-    Aig_Obj_t * pObj, * pObjC, * pObj0, * pObj1;
-    int i, k, Counter;
-    Aig_ManCleanMarkAB( p );
+    Aig_Obj_t * pObj, * pTemp, * pObjC, * pObj0, * pObj1;
+    int i, k, nFans, Counter;
+
+    vLeaves = Vec_PtrAlloc( 100 );
+    vNodes  = Vec_PtrAlloc( 100 );
+    vSupps  = Vec_IntStart( Aig_ManObjNumMax(p) );
 
     // mark CIs
     Aig_ManForEachPi( p, pObj, i )
@@ -335,90 +297,99 @@ void Cnf_DeriveFastMark( Aig_Man_t * p )
     Aig_ManForEachPo( p, pObj, i )
         Aig_ObjFanin0(pObj)->fMarkA = 1;
 
+    // mark MUX/XOR nodes
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        assert( !pObj->fMarkB );
+        if ( !Aig_ObjIsMuxType(pObj) )
+            continue;
+        pObj0 = Aig_ObjFanin0(pObj);
+        if ( pObj0->fMarkB || Aig_ObjRefs(pObj0) > 1 )
+            continue;
+        pObj1 = Aig_ObjFanin1(pObj);
+        if ( pObj1->fMarkB || Aig_ObjRefs(pObj1) > 1 )
+            continue;
+        // mark nodes
+        pObj->fMarkB = 1;
+        pObj0->fMarkB = 1;
+        pObj1->fMarkB = 1;
+        // mark inputs and outputs
+        pObj->fMarkA = 1;
+        Aig_ObjFanin0(pObj0)->fMarkA = 1;
+        Aig_ObjFanin1(pObj0)->fMarkA = 1;
+        Aig_ObjFanin0(pObj1)->fMarkA = 1;
+        Aig_ObjFanin1(pObj1)->fMarkA = 1;
+    }
+
+    // mark nodes with multiple fanouts and pointed to by complemented edges
     Aig_ManForEachNode( p, pObj, i )
     {
         // mark nodes with many fanouts
         if ( Aig_ObjRefs(pObj) > 1 )
             pObj->fMarkA = 1;
         // mark nodes pointed to by a complemented edge
-        if ( Aig_ObjFaninC0(pObj) )
+        if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFanin0(pObj)->fMarkB )
             Aig_ObjFanin0(pObj)->fMarkA = 1;
-        if ( Aig_ObjFaninC1(pObj) )
+        if ( Aig_ObjFaninC1(pObj) && !Aig_ObjFanin1(pObj)->fMarkB )
             Aig_ObjFanin1(pObj)->fMarkA = 1;
-
-        // mark roots/leaves of MUX/XOR with MarkA
-        // mark internal nodes of MUX/XOR with MarkB
-        if ( !Aig_ObjIsMuxType(pObj) )
-            continue;
-
-        pObjC = Aig_ObjRecognizeMux( pObj, &pObj1, &pObj0 );
-        Aig_Regular(pObjC)->fMarkA = 1;
-        Aig_Regular(pObj1)->fMarkA = 1;
-        Aig_Regular(pObj0)->fMarkA = 1;
-
-        Aig_ObjFanin0(pObj)->fMarkB = 1;
-        Aig_ObjFanin1(pObj)->fMarkB = 1;
     }
 
-    // clean internal nodes of MUX/XOR
+    // compute supergate size for internal marked nodes
     Aig_ManForEachNode( p, pObj, i )
     {
-        if ( !pObj->fMarkB )
+        if ( !pObj->fMarkA )
             continue;
-        pObj->fMarkB = 0;
-        if ( Aig_ObjRefs(pObj) == 1 )
-            pObj->fMarkA = 0;
-    }
-
-    // remove nodes those fanins are used
-    Aig_ManForEachNode( p, pObj, i )
-        if ( pObj->fMarkA && Aig_ObjFanin0(pObj)->fMarkA && Aig_ObjFanin1(pObj)->fMarkA )
-            pObj->fMarkA = 0;
-
-    // mark CO drivers
-    Aig_ManForEachPo( p, pObj, i )
-        Aig_ObjFanin0(pObj)->fMarkA = 1;
-
-
-    vLeaves = Vec_PtrAlloc( 100 );
-    vNodes  = Vec_PtrAlloc( 100 );
-
-    while ( 1 )
-    {
-        int nChanges = 0;
-        Aig_ManForEachNode( p, pObj, i )
+        if ( pObj->fMarkB )
         {
-            if ( !pObj->fMarkA )
+            if ( !Aig_ObjIsMuxType(pObj) )
                 continue;
-            Cnf_CollectSuper( pObj, vLeaves, 0 );
-            if ( Vec_PtrSize(vLeaves) <= 6 )
+            pObjC = Aig_ObjRecognizeMux( pObj, &pObj1, &pObj0 );
+            pObj0 = Aig_Regular(pObj0);
+            pObj1 = Aig_Regular(pObj1);
+            assert( pObj0->fMarkA );
+            assert( pObj1->fMarkA );
+//            if ( pObj0 == pObj1 )
+//                continue;
+            nFans = 1 + (pObj0 == pObj1);
+            if ( !pObj0->fMarkB && !Aig_ObjIsPi(pObj0) && Aig_ObjRefs(pObj0) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj0)) < 3 )
+            {
+                pObj0->fMarkA = 0;
                 continue;
-            Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
-            Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObjC, k )
+            }
+            if ( !pObj1->fMarkB && !Aig_ObjIsPi(pObj1) && Aig_ObjRefs(pObj1) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj1)) < 3 )
             {
-                if ( Aig_ObjFaninC0(pObjC) && !Aig_ObjFanin0(pObjC)->fMarkA )
-                {
-                    Aig_ObjFanin0(pObjC)->fMarkA = 1;
-//                    printf( "%d ", Aig_ObjFaninId0(pObjC) );
-                    nChanges++;
-                }
-                if ( Aig_ObjFaninC1(pObjC) && !Aig_ObjFanin1(pObjC)->fMarkA )
-                {
-                    Aig_ObjFanin1(pObjC)->fMarkA = 1;
-//                    printf( "%d ", Aig_ObjFaninId1(pObjC) );
-                    nChanges++;
-                }
+                pObj1->fMarkA = 0;
+                continue;
             }
+            continue;
         }
-        printf( "Made %d gate changes\n", nChanges );
-        if ( !nChanges )
+
+        Cnf_CollectLeaves( pObj, vLeaves, 1 );
+        Vec_IntWriteEntry( vSupps, Aig_ObjId(pObj), Vec_PtrSize(vLeaves) );
+        if ( Vec_PtrSize(vLeaves) >= 6 )
+            continue;
+        Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pTemp, k )
+        {
+            pTemp = Aig_Regular(pTemp);
+            assert( pTemp->fMarkA );
+            if ( pTemp->fMarkB || Aig_ObjIsPi(pTemp) || Aig_ObjRefs(pTemp) > 1 )
+                continue;
+            assert( Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) > 0 );
+            if ( Vec_PtrSize(vLeaves) - 1 + Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) > 6 )
+                continue;
+            pTemp->fMarkA = 0;
+            Vec_IntWriteEntry( vSupps, Aig_ObjId(pObj), 6 );
+//printf( "%d %d   ", Vec_PtrSize(vLeaves), Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) );
             break;
+        }
     }
+    Aig_ManCleanMarkB( p );
 
     // check CO drivers
     Counter = 0;
     Aig_ManForEachPo( p, pObj, i )
         Counter += !Aig_ObjFanin0(pObj)->fMarkA;
+    if ( Counter )
     printf( "PO-driver rule is violated %d times.\n", Counter );
 
     // check that the AND-gates are fine
@@ -428,22 +399,24 @@ void Cnf_DeriveFastMark( Aig_Man_t * p )
         assert( pObj->fMarkB == 0 );
         if ( !pObj->fMarkA )
             continue;
-        Cnf_CollectSuper( pObj, vLeaves, 0 );
+        Cnf_CollectLeaves( pObj, vLeaves, 0 );
         if ( Vec_PtrSize(vLeaves) <= 6 )
             continue;
         Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
-        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj1, k )
+        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pTemp, k )
         {
-            if ( Aig_ObjFaninC0(pObj1) && !Aig_ObjFanin0(pObj1)->fMarkA )
+            if ( Aig_ObjFaninC0(pTemp) && !Aig_ObjFanin0(pTemp)->fMarkA )
                 Counter++;
-            if ( Aig_ObjFaninC1(pObj1) && !Aig_ObjFanin1(pObj1)->fMarkA )
+            if ( Aig_ObjFaninC1(pTemp) && !Aig_ObjFanin1(pTemp)->fMarkA )
                 Counter++;
         }
     }
+    if ( Counter )
+    printf( "AND-gate rule is violated %d times.\n", Counter );
+
     Vec_PtrFree( vLeaves );
     Vec_PtrFree( vNodes );
-
-    printf( "AND-gate rule is violated %d times.\n", Counter );
+    Vec_IntFree( vSupps );
 }
 
 
@@ -523,7 +496,7 @@ int Cnf_CountCnfSize( Aig_Man_t * p )
     {
         if ( !pObj->fMarkA )
             continue;
-        Cnf_CollectSuper( pObj, vLeaves, 0 );
+        Cnf_CollectLeaves( pObj, vLeaves, 0 );
         Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
         assert( pObj == Vec_PtrEntryLast(vNodes) );
 
@@ -556,12 +529,11 @@ int Cnf_CountCnfSize( Aig_Man_t * p )
 Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs )
 {
     Cnf_Dat_t * pCnf;
-    Vec_Int_t * vLits, * vClas, * vMap;
+    Vec_Int_t * vLits, * vClas, * vMap, * vTemp;
     Vec_Ptr_t * vLeaves, * vNodes;
     Vec_Int_t * vCover;
-    Aig_Obj_t * pObj, * pLeaf;
-    int i, c, k, nVars, Cube, Entry, OutLit, DriLit, RetValue;
-    word Truth;
+    Aig_Obj_t * pObj;
+    int i, k, nVars, Entry, OutLit, DriLit;
 
     vLits = Vec_IntAlloc( 1 << 16 );
     vClas = Vec_IntAlloc( 1 << 12 );
@@ -597,87 +569,24 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs )
     vLeaves = Vec_PtrAlloc( 100 );
     vNodes  = Vec_PtrAlloc( 100 );
     vCover  = Vec_IntAlloc( 1 << 16 );
+    vTemp   = Vec_IntAlloc( 100 );
     Aig_ManForEachNodeReverse( p, pObj, i )
     {
         if ( !pObj->fMarkA )
             continue;
-        OutLit = toLit( Vec_IntEntry(vMap, Aig_ObjId(pObj)) );
-        // detect cone
-        Cnf_CollectSuper( pObj, vLeaves, 0 );
-        Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
-        assert( pObj == Vec_PtrEntryLast(vNodes) );
-        // check if this is an AND-gate
-        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pLeaf, k )
-        {
-            if ( Aig_ObjFaninC0(pLeaf) && !Aig_ObjFanin0(pLeaf)->fMarkA )
-                break;
-            if ( Aig_ObjFaninC1(pLeaf) && !Aig_ObjFanin1(pLeaf)->fMarkA )
-                break;
-        }
-        if ( k == Vec_PtrSize(vNodes) )
+        Cnf_ComputeClauses( p, pObj, vLeaves, vNodes, vMap, vCover, vTemp );
+        Vec_IntForEachEntry( vTemp, Entry, k )
         {
-            Cnf_CollectSuper( pObj, vLeaves, 1 );
-            // write big clause
-            Vec_IntPush( vClas, Vec_IntSize(vLits) );
-            Vec_IntPush( vLits, OutLit );
-            Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k )
-                Vec_IntPush( vLits, toLitCond(Vec_IntEntry(vMap, Aig_ObjId(Aig_Regular(pLeaf))), !Aig_IsComplement(pLeaf)) );
-            // write small clauses
-            Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k )
-            {
+            if ( Entry == 0 )
                 Vec_IntPush( vClas, Vec_IntSize(vLits) );
-                Vec_IntPush( vLits, lit_neg(OutLit) );
-                Vec_IntPush( vLits, toLitCond(Vec_IntEntry(vMap, Aig_ObjId(Aig_Regular(pLeaf))), Aig_IsComplement(pLeaf)) );
-            }
-            continue;
-        }
-        assert( Vec_PtrSize(vLeaves) <= 6 );
-
-        Truth = Cnf_CutDeriveTruth( p, vLeaves, vNodes );
-        if ( Truth == 0 || Truth == ~0 )
-        {
-            assert( RetValue == 0 );
-            Vec_IntPush( vClas, Vec_IntSize(vLits) );
-            Vec_IntPush( vLits, (Truth == 0) ? lit_neg(OutLit) : OutLit );
-            continue;
-        }
-
-        RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
-        assert( RetValue >= 0 );
-
-        Vec_IntForEachEntry( vCover, Cube, c )
-        {
-            Vec_IntPush( vClas, Vec_IntSize(vLits) );
-            Vec_IntPush( vLits, OutLit );
-            for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 )
-            {
-                if ( (Cube & 3) == 0 )
-                    continue;
-                assert( (Cube & 3) != 3 );
-                Vec_IntPush( vLits, toLitCond( Vec_IntEntry(vMap, Aig_ObjId(Vec_PtrEntry(vLeaves,k))), (Cube&3)!=1 ) );
-            }
-        }
-
-        Truth = ~Truth;
-
-        RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
-        assert( RetValue >= 0 );
-        Vec_IntForEachEntry( vCover, Cube, c )
-        {
-            Vec_IntPush( vClas, Vec_IntSize(vLits) );
-            Vec_IntPush( vLits, lit_neg(OutLit) );
-            for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 )
-            {
-                if ( (Cube & 3) == 0 )
-                    continue;
-                assert( (Cube & 3) != 3 );
-                Vec_IntPush( vLits, toLitCond( Vec_IntEntry(vMap, Aig_ObjId(Vec_PtrEntry(vLeaves,k))), (Cube&3)==1 ) );
-            }
-        }
+            else
+                Vec_IntPush( vLits, Entry );
+        }       
     }
     Vec_PtrFree( vLeaves );
     Vec_PtrFree( vNodes );
     Vec_IntFree( vCover );
+    Vec_IntFree( vTemp );
 
     // create clauses for the outputs
     Aig_ManForEachPo( p, pObj, i )
@@ -742,21 +651,21 @@ Cnf_Dat_t * Cnf_DeriveFast( Aig_Man_t * p, int nOutputs )
 {
     Cnf_Dat_t * pCnf = NULL;
     int clk, clkTotal = clock();
-    printf( "\n" );
+//    printf( "\n" );
     Aig_ManCleanMarkAB( p );
     // create initial marking
     clk = clock();
     Cnf_DeriveFastMark( p );
-    Abc_PrintTime( 1, "Marking", clock() - clk );
+//    Abc_PrintTime( 1, "Marking", clock() - clk );
     // compute CNF size
     clk = clock();
     pCnf = Cnf_DeriveFastClauses( p, nOutputs );
-    Abc_PrintTime( 1, "Clauses", clock() - clk );
+//    Abc_PrintTime( 1, "Clauses", clock() - clk );
     // derive the resulting CNF
     Aig_ManCleanMarkA( p );
-    Abc_PrintTime( 1, "TOTAL  ", clock() - clkTotal );
+//    Abc_PrintTime( 1, "TOTAL  ", clock() - clkTotal );
 
-    printf( "Vars = %6d. Clauses = %7d. Literals = %8d.   \n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
+//    printf( "Vars = %6d. Clauses = %7d. Literals = %8d.   \n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
 
 //    Cnf_DataFree( pCnf );
 //    pCnf = NULL;
diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c
index 75af32f1..574371ff 100644
--- a/src/aig/saig/saigAbsPba.c
+++ b/src/aig/saig/saigAbsPba.c
@@ -269,7 +269,8 @@ clk = clock();
 if ( fVerbose )
 Aig_ManPrintStats( pFrames );
 //    pCnf = Cnf_DeriveSimple( pFrames, 0 );
-    pCnf = Cnf_Derive( pFrames, 0 );
+//    pCnf = Cnf_Derive( pFrames, 0 );
+    pCnf = Cnf_DeriveFast( pFrames, 0 );
     pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     if ( pSat == NULL )
     {