Changes to CNF generation code.

7 files changed, 839 insertions, 18 deletions

diff --git a/abclib.dsp b/abclib.dsp
index f2dcbeb6..64867307 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -2971,6 +2971,10 @@ SOURCE=.\src\aig\cnf\cnfData.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\cnf\cnfFast.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\cnf\cnfMan.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index d57080cf..346302c5 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -410,24 +410,33 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
 // iterator over the primary inputs
 #define Aig_ManForEachPi( p, pObj, i )                                          \
     Vec_PtrForEachEntry( Aig_Obj_t *, p->vPis, pObj, i )
+#define Aig_ManForEachPiReverse( p, pObj, i )                                   \
+    Vec_PtrForEachEntryReverse( Aig_Obj_t *, p->vPis, pObj, i )
 // iterator over the primary outputs
 #define Aig_ManForEachPo( p, pObj, i )                                          \
     Vec_PtrForEachEntry( Aig_Obj_t *, p->vPos, pObj, i )
-// iterator over the assertions
-#define Aig_ManForEachAssert( p, pObj, i )                                      \
-    Vec_PtrForEachEntryStart( Aig_Obj_t *, p->vPos, pObj, i, Aig_ManPoNum(p)-p->nAsserts )
-// iterator over all objects, including those currently not used
+#define Aig_ManForEachPoReverse( p, pObj, i )                                   \
+    Vec_PtrForEachEntryReverse( Aig_Obj_t *, p->vPos, pObj, i )
+// iterators over all objects, including those currently not used
 #define Aig_ManForEachObj( p, pObj, i )                                         \
     Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
-// iterator over the objects whose IDs are stored in an array
-#define Aig_ManForEachObjVec( vIds, p, pObj, i )                               \
+#define Aig_ManForEachObjReverse( p, pObj, i )                                  \
+    Vec_PtrForEachEntryReverse( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
+// iterators over the objects whose IDs are stored in an array
+#define Aig_ManForEachObjVec( vIds, p, pObj, i )                                \
     for ( i = 0; i < Vec_IntSize(vIds) && (((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))), 1); i++ )
-// iterator over all nodes
+#define Aig_ManForEachObjVecReverse( vIds, p, pObj, i )                         \
+    for ( i = Vec_IntSize(vIds) - 1; i >= 0 && (((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))), 1); i-- )
+// iterators over all nodes
 #define Aig_ManForEachNode( p, pObj, i )                                        \
     Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
+#define Aig_ManForEachNodeReverse( p, pObj, i )                                 \
+    Vec_PtrForEachEntryReverse( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
 // iterator over all nodes
 #define Aig_ManForEachExor( p, pObj, i )                                        \
     Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsExor(pObj) ) {} else
+#define Aig_ManForEachExorReverse( p, pObj, i )                                 \
+    Vec_PtrForEachEntryReverse( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsExor(pObj) ) {} else
 
 // these two procedures are only here for the use inside the iterator
 static inline int     Aig_ObjFanout0Int( Aig_Man_t * p, int ObjId )  { assert(ObjId < p->nFansAlloc);  return p->pFanData[5*ObjId];                         }
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index 42dcd9a9..97111100 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -138,6 +138,8 @@ 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 ========================================================*/
+extern Cnf_Dat_t *     Cnf_DeriveFast( Aig_Man_t * p, int nOutputs );
 /*=== cnfMan.c ========================================================*/
 extern Cnf_Man_t *     Cnf_ManStart();
 extern void            Cnf_ManStop( Cnf_Man_t * p );
diff --git a/src/aig/cnf/cnfFast.c b/src/aig/cnf/cnfFast.c
new file mode 100644
index 00000000..83a273ae
--- /dev/null
+++ b/src/aig/cnf/cnfFast.c
@@ -0,0 +1,772 @@
+/**CFile****************************************************************
+
+  FileName    [cnfFast.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG-to-CNF conversion.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: cnfFast.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cnf.h"
+#include "kit.h"
+#include "satSolver.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Detects multi-input gate rooted at this node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_CollectSuper_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fStopCompl )
+{
+    if ( pRoot != pObj && (pObj->fMarkA || (fStopCompl && Aig_IsComplement(pObj))) )
+    {
+        Vec_PtrPushUnique( vSuper, fStopCompl ? pObj : Aig_Regular(pObj) );
+        return;
+    }
+    assert( Aig_ObjIsNode(pObj) );
+    if ( fStopCompl )
+    {
+        Cnf_CollectSuper_rec( pRoot, Aig_ObjChild0(pObj), vSuper, 1 );
+        Cnf_CollectSuper_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 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Detects multi-input gate rooted at this node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_CollectSuper( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper, int fStopCompl )
+{
+    assert( !Aig_IsComplement(pRoot) );
+    Vec_PtrClear( vSuper );
+    Cnf_CollectSuper_rec( pRoot, pRoot, vSuper, fStopCompl );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes inside the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_CollectVolume_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
+        return;
+    Aig_ObjSetTravIdCurrent( p, pObj );
+    assert( Aig_ObjIsNode(pObj) );
+    Cnf_CollectVolume_rec( p, Aig_ObjFanin0(pObj), vNodes );
+    Cnf_CollectVolume_rec( p, Aig_ObjFanin1(pObj), vNodes );
+    Vec_PtrPush( vNodes, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes inside the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_CollectVolume( Aig_Man_t * p, Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManIncrementTravId( p );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
+        Aig_ObjSetTravIdCurrent( p, pObj );
+    Vec_PtrClear( vNodes );
+    Cnf_CollectVolume_rec( p, pRoot, vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+word Cnf_CutDeriveTruth( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes )
+{
+    static word Truth6[6] = {
+        0xAAAAAAAAAAAAAAAA,
+        0xCCCCCCCCCCCCCCCC,
+        0xF0F0F0F0F0F0F0F0,
+        0xFF00FF00FF00FF00,
+        0xFFFF0000FFFF0000,
+        0xFFFFFFFF00000000
+    };
+    static word C[2] = { 0, ~0 };
+    static word S[256];
+    Aig_Obj_t * pObj;
+    int i;
+    assert( Vec_PtrSize(vLeaves) <= 6 && Vec_PtrSize(vNodes) > 0 );
+    assert( Vec_PtrSize(vLeaves) + Vec_PtrSize(vNodes) <= 256 );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
+    {
+        pObj->iData    = i;
+        S[pObj->iData] = Truth6[i];
+    }
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+    {
+        pObj->iData    = Vec_PtrSize(vLeaves) + i;
+        S[pObj->iData] = (S[Aig_ObjFanin0(pObj)->iData] ^ C[Aig_ObjFaninC0(pObj)]) & 
+                         (S[Aig_ObjFanin1(pObj)->iData] ^ C[Aig_ObjFaninC1(pObj)]);
+    }
+    return S[pObj->iData];
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Marks AIG for CNF computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_DeriveFastMark_( Aig_Man_t * p )
+{
+    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;
+
+
+    // mark roots/leaves of MUX/XOR with MarkA
+    // mark internal nodes of MUX/XOR with MarkB
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        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;
+    }
+
+    // mark nodes with many fanouts or pointed to by a complemented edge
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        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;
+    }
+
+    // clean internal nodes of MUX/XOR
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        if ( pObj->fMarkB )
+            pObj->fMarkB = pObj->fMarkA = 0;
+//            pObj->fMarkB = 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;
+/*
+    // 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 )
+    {
+        int fChanges = 0;
+        Aig_ManForEachNode( p, pObj, i )
+        {
+            if ( !pObj->fMarkA )
+                continue;
+            if ( Aig_ObjRefs(pObj) == 1 )
+                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;
+            }
+        }
+        printf( "Round 1 \n" );
+        if ( !fChanges )
+            break;
+    }
+*/
+    while ( 1 )
+    {
+        int fChanges = 0;
+        Aig_ManForEachNode( p, pObj, i )
+        {
+            if ( !pObj->fMarkA )
+                continue;
+            Cnf_CollectSuper( pObj, vLeaves, 0 );
+            if ( Vec_PtrSize(vLeaves) <= 6 )
+                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;
+                }
+            }
+        }
+        printf( "Round 2\n" );
+        if ( !fChanges )
+            break;
+    }
+
+
+    Vec_PtrFree( vLeaves );
+    Vec_PtrFree( vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks AIG for CNF computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_DeriveFastMark( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vLeaves, * vNodes;
+    Aig_Obj_t * pObj, * pObjC, * pObj0, * pObj1;
+    int i, k, Counter;
+    Aig_ManCleanMarkAB( p );
+
+    // mark CIs
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->fMarkA = 1;
+
+    // mark CO drivers
+    Aig_ManForEachPo( p, pObj, i )
+        Aig_ObjFanin0(pObj)->fMarkA = 1;
+
+    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) )
+            Aig_ObjFanin0(pObj)->fMarkA = 1;
+        if ( Aig_ObjFaninC1(pObj) )
+            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
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        if ( !pObj->fMarkB )
+            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->fMarkA )
+                continue;
+            Cnf_CollectSuper( pObj, vLeaves, 0 );
+            if ( Vec_PtrSize(vLeaves) <= 6 )
+                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) );
+                    nChanges++;
+                }
+                if ( Aig_ObjFaninC1(pObjC) && !Aig_ObjFanin1(pObjC)->fMarkA )
+                {
+                    Aig_ObjFanin1(pObjC)->fMarkA = 1;
+//                    printf( "%d ", Aig_ObjFaninId1(pObjC) );
+                    nChanges++;
+                }
+            }
+        }
+        printf( "Made %d gate changes\n", nChanges );
+        if ( !nChanges )
+            break;
+    }
+
+    // check CO drivers
+    Counter = 0;
+    Aig_ManForEachPo( p, pObj, i )
+        Counter += !Aig_ObjFanin0(pObj)->fMarkA;
+    printf( "PO-driver rule is violated %d times.\n", Counter );
+
+    // check that the AND-gates are fine
+    Counter = 0;
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        assert( pObj->fMarkB == 0 );
+        if ( !pObj->fMarkA )
+            continue;
+        Cnf_CollectSuper( pObj, vLeaves, 0 );
+        if ( Vec_PtrSize(vLeaves) <= 6 )
+            continue;
+        Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
+        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj1, k )
+        {
+            if ( Aig_ObjFaninC0(pObj1) && !Aig_ObjFanin0(pObj1)->fMarkA )
+                Counter++;
+            if ( Aig_ObjFaninC1(pObj1) && !Aig_ObjFanin1(pObj1)->fMarkA )
+                Counter++;
+        }
+    }
+    Vec_PtrFree( vLeaves );
+    Vec_PtrFree( vNodes );
+
+    printf( "AND-gate rule is violated %d times.\n", Counter );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cnf_CutCountClauses( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Int_t * vCover )
+{
+    word Truth;
+    Aig_Obj_t * pObj;
+    int i, RetValue, nSize = 0;
+    if ( Vec_PtrSize(vLeaves) > 6 )
+    {
+        // make sure this is an AND gate
+        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+        {
+            if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFanin0(pObj)->fMarkA )
+                printf( "Unusual 1!\n" );
+            if ( Aig_ObjFaninC1(pObj) && !Aig_ObjFanin1(pObj)->fMarkA )
+                printf( "Unusual 2!\n" );
+            continue;
+
+            assert( !Aig_ObjFaninC0(pObj) || Aig_ObjFanin0(pObj)->fMarkA );
+            assert( !Aig_ObjFaninC1(pObj) || Aig_ObjFanin1(pObj)->fMarkA );
+        }
+        return Vec_PtrSize(vLeaves) + 1;
+    }
+    Truth = Cnf_CutDeriveTruth( p, vLeaves, vNodes );
+
+    RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
+    assert( RetValue >= 0 );
+    nSize += Vec_IntSize(vCover);
+
+    Truth = ~Truth;
+
+    RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
+    assert( RetValue >= 0 );
+    nSize += Vec_IntSize(vCover);
+    return nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the size of the CNF, assuming marks are set.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cnf_CountCnfSize( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vLeaves, * vNodes;
+    Vec_Int_t * vCover;
+    Aig_Obj_t * pObj;
+    int nVars = 0, nClauses = 0;
+    int i, nSize;
+
+    vLeaves = Vec_PtrAlloc( 100 );
+    vNodes  = Vec_PtrAlloc( 100 );
+    vCover  = Vec_IntAlloc( 1 << 16 );
+
+    Aig_ManForEachObj( p, pObj, i )
+        nVars += pObj->fMarkA;
+
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        if ( !pObj->fMarkA )
+            continue;
+        Cnf_CollectSuper( pObj, vLeaves, 0 );
+        Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
+        assert( pObj == Vec_PtrEntryLast(vNodes) );
+
+        nSize = Cnf_CutCountClauses( p, vLeaves, vNodes, vCover );
+//        printf( "%d(%d) ", Vec_PtrSize(vLeaves), nSize );
+
+        nClauses += nSize;
+    }
+//    printf( "\n" );
+    printf( "Vars = %d  Clauses = %d\n", nVars, nClauses );
+
+    Vec_PtrFree( vLeaves );
+    Vec_PtrFree( vNodes );
+    Vec_IntFree( vCover );
+    return nClauses;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives CNF from the marked AIG.]
+
+  Description [Assumes that marking is such that when we traverse from each
+  marked node, the logic cone has 6 inputs or less, or it is a multi-input AND.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs )
+{
+    Cnf_Dat_t * pCnf;
+    Vec_Int_t * vLits, * vClas, * vMap;
+    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;
+
+    vLits = Vec_IntAlloc( 1 << 16 );
+    vClas = Vec_IntAlloc( 1 << 12 );
+    vMap  = Vec_IntStartFull( Aig_ManObjNumMax(p) );
+
+    // assign variables for the outputs
+    nVars = 1;
+    if ( nOutputs )
+    {
+        if ( Aig_ManRegNum(p) == 0 )
+        {
+            assert( nOutputs == Aig_ManPoNum(p) );
+            Aig_ManForEachPo( p, pObj, i )
+                Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
+        }
+        else
+        {
+            assert( nOutputs == Aig_ManRegNum(p) );
+            Aig_ManForEachLiSeq( p, pObj, i )
+                Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
+        }
+    }
+    // assign variables to the internal nodes
+    Aig_ManForEachNodeReverse( p, pObj, i )
+        if ( pObj->fMarkA )
+            Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
+    // assign variables to the PIs and constant node
+    Aig_ManForEachPi( p, pObj, i )
+        Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
+    Vec_IntWriteEntry( vMap, Aig_ObjId(Aig_ManConst1(p)), nVars++ );
+
+    // create clauses
+    vLeaves = Vec_PtrAlloc( 100 );
+    vNodes  = Vec_PtrAlloc( 100 );
+    vCover  = Vec_IntAlloc( 1 << 16 );
+    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_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 )
+            {
+                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 ) );
+            }
+        }
+    }
+    Vec_PtrFree( vLeaves );
+    Vec_PtrFree( vNodes );
+    Vec_IntFree( vCover );
+
+    // create clauses for the outputs
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        DriLit = toLitCond( Vec_IntEntry(vMap, Aig_ObjFaninId0(pObj)), Aig_ObjFaninC0(pObj) );
+        if ( i < Aig_ManPoNum(p) - nOutputs )
+        {
+            Vec_IntPush( vClas, Vec_IntSize(vLits) );
+            Vec_IntPush( vLits, DriLit );
+        }
+        else
+        {
+            OutLit = toLit( Vec_IntEntry(vMap, Aig_ObjId(pObj)) );
+            // first clause
+            Vec_IntPush( vClas, Vec_IntSize(vLits) );
+            Vec_IntPush( vLits, OutLit );
+            Vec_IntPush( vLits, lit_neg(DriLit) );
+            // second clause
+            Vec_IntPush( vClas, Vec_IntSize(vLits) );
+            Vec_IntPush( vLits, lit_neg(OutLit) );
+            Vec_IntPush( vLits, DriLit );
+        }
+    }
+ 
+    // write the constant literal
+    OutLit = toLit( Vec_IntEntry(vMap, Aig_ObjId(Aig_ManConst1(p))) );
+    Vec_IntPush( vClas, Vec_IntSize(vLits) );
+    Vec_IntPush( vLits, OutLit );
+
+    // create structure
+    pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
+    pCnf->pMan = p;
+    pCnf->nVars = nVars;
+    pCnf->nLiterals = Vec_IntSize( vLits );
+    pCnf->nClauses  = Vec_IntSize( vClas );
+    pCnf->pClauses  = ABC_ALLOC( int *, pCnf->nClauses + 1 );
+    pCnf->pClauses[0] = Vec_IntReleaseArray( vLits );
+    Vec_IntForEachEntry( vClas, Entry, i )
+        pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
+    pCnf->pClauses[pCnf->nClauses] = pCnf->pClauses[0] + pCnf->nLiterals;
+    pCnf->pVarNums  = Vec_IntReleaseArray( vMap );
+
+    // cleanup
+    Vec_IntFree( vLits );
+    Vec_IntFree( vClas );
+    Vec_IntFree( vMap );
+    return pCnf;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fast CNF computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cnf_Dat_t * Cnf_DeriveFast( Aig_Man_t * p, int nOutputs )
+{
+    Cnf_Dat_t * pCnf = NULL;
+    int clk, clkTotal = clock();
+    printf( "\n" );
+    Aig_ManCleanMarkAB( p );
+    // create initial marking
+    clk = clock();
+    Cnf_DeriveFastMark( p );
+    Abc_PrintTime( 1, "Marking", clock() - clk );
+    // compute CNF size
+    clk = clock();
+    pCnf = Cnf_DeriveFastClauses( p, nOutputs );
+    Abc_PrintTime( 1, "Clauses", clock() - clk );
+    // derive the resulting CNF
+    Aig_ManCleanMarkA( p );
+    Abc_PrintTime( 1, "TOTAL  ", clock() - clkTotal );
+
+    printf( "Vars = %6d. Clauses = %7d. Literals = %8d.   \n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
+
+//    Cnf_DataFree( pCnf );
+//    pCnf = NULL;
+    return pCnf;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/cnf/module.make b/src/aig/cnf/module.make
index dbcaeba4..596fe31b 100644
--- a/src/aig/cnf/module.make
+++ b/src/aig/cnf/module.make
@@ -1,6 +1,7 @@
 SRC +=    src/aig/cnf/cnfCore.c \
     src/aig/cnf/cnfCut.c \
     src/aig/cnf/cnfData.c \
+    src/aig/cnf/cnfFast.c \
     src/aig/cnf/cnfMan.c \
     src/aig/cnf/cnfMap.c \
     src/aig/cnf/cnfPost.c \
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 7efc062e..13aeaaa0 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1172,13 +1172,14 @@ Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
+Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo, int fChangePol, int fVerbose )
 {
     Vec_Ptr_t * vMapped = NULL;
     Aig_Man_t * pMan;
     Cnf_Man_t * pManCnf = NULL;
     Cnf_Dat_t * pCnf;
     Abc_Ntk_t * pNtkNew = NULL;
+    int clk = clock();
     assert( Abc_NtkIsStrash(pNtk) );
 
     // convert to the AIG manager
@@ -1192,12 +1193,25 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
         return NULL;
     }
     // perform balance
+    if ( fVerbose )
     Aig_ManPrintStats( pMan );
 
     // derive CNF
-    pCnf = Cnf_Derive( pMan, 0 );
-    Cnf_DataTranformPolarity( pCnf, 0 );
-    printf( "Vars = %6d. Clauses = %7d. Literals = %8d.\n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
+    if ( fFastAlgo )
+        pCnf = Cnf_DeriveFast( pMan, 0 );
+    else
+        pCnf = Cnf_Derive( pMan, 0 );
+
+    // adjust polarity
+    if ( fChangePol )
+        Cnf_DataTranformPolarity( pCnf, 0 );
+
+    // print stats
+    if ( fVerbose )
+    {
+        printf( "Vars = %6d. Clauses = %7d. Literals = %8d.   ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
+        Abc_PrintTime( 1, "Time", clock() - clk );
+    }
 
 /*
     // write the network for verification
@@ -1210,7 +1224,6 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
     Cnf_DataWriteIntoFile( pCnf, pFileName, 0 );
     Cnf_DataFree( pCnf );
     Cnf_ClearMemory();
-
     Aig_ManStop( pMan );
     return pNtkNew;
 }
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 3b85a020..60085168 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1865,23 +1865,38 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * pFileName;
     int c;
-    int fAllPrimes;
     int fNewAlgo;
-    extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
+    int fFastAlgo;
+    int fAllPrimes;
+    int fChangePol;
+    int fVerbose;
+    extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo, int fChangePol, int fVerbose );
 
     fNewAlgo = 1;
+    fFastAlgo = 0;
     fAllPrimes = 0;
+    fChangePol = 1;
+    fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "nph" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "nfpcvh" ) ) != EOF )
     {
         switch ( c )
         {
             case 'n':
                 fNewAlgo ^= 1;
                 break;
+            case 'f':
+                fFastAlgo ^= 1;
+                break;
             case 'p':
                 fAllPrimes ^= 1;
                 break;
+            case 'c':
+                fChangePol ^= 1;
+                break;
+            case 'v':
+                fVerbose ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -1904,8 +1919,10 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
         printf( "Warning: Selected option to write all primes has no effect when deriving CNF from AIG.\n" );
     }
     // call the corresponding file writer
-    if ( fNewAlgo )
-        Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName );
+    if ( fFastAlgo )
+        Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName, 1, fChangePol, fVerbose );
+    else if ( fNewAlgo )
+        Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName, 0, fChangePol, fVerbose );
     else if ( fAllPrimes )
         Io_WriteCnf( pAbc->pNtkCur, pFileName, 1 );
     else
@@ -1913,10 +1930,13 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_cnf [-nph] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_cnf [-nfpcvh] <file>\n" );
     fprintf( pAbc->Err, "\t         writes the miter cone into a CNF file\n" );
     fprintf( pAbc->Err, "\t-n     : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes" : "no" );
+    fprintf( pAbc->Err, "\t-f     : toggle using fast algorithm [default = %s]\n", fFastAlgo? "yes" : "no" );
     fprintf( pAbc->Err, "\t-p     : toggle using all primes to enhance implicativity [default = %s]\n", fAllPrimes? "yes" : "no" );
+    fprintf( pAbc->Err, "\t-c     : toggle adjasting polarity of internal variables [default = %s]\n", fChangePol? "yes" : "no" );
+    fprintf( pAbc->Err, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes" : "no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
     return 1;