Version abc80721

24 files changed, 1567 insertions, 93 deletions

diff --git a/abc.dsp b/abc.dsp
index 4469f3b3..228b163b 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -2902,6 +2902,10 @@ SOURCE=.\src\aig\aig\aigPartReg.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\aig\aigPartSat.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\aig\aigRepr.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 93ca298a..84c1e0b5 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -460,6 +460,7 @@ extern void            Aig_ManCutStop( Aig_ManCut_t * p );
 /*=== aigDfs.c ==========================================================*/
 extern int             Aig_ManVerifyTopoOrder( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfs( Aig_Man_t * p, int fNodesOnly );
+extern Vec_Ptr_t *     Aig_ManDfsPreorder( Aig_Man_t * p, int fNodesOnly );
 extern Vec_Vec_t *     Aig_ManLevelize( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *     Aig_ManDfsChoices( Aig_Man_t * p );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 47597f93..c9893ed2 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -166,6 +166,68 @@ Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p, int fNodesOnly )
 
 /**Function*************************************************************
 
+  Synopsis    [Collects internal nodes in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManDfsPreorder_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    if ( pObj == NULL )
+        return;
+    assert( !Aig_IsComplement(pObj) );
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    Vec_PtrPush( vNodes, pObj );
+    if ( p->pEquivs && Aig_ObjEquiv(p, pObj) )
+        Aig_ManDfs_rec( p, Aig_ObjEquiv(p, pObj), vNodes );
+    Aig_ManDfsPreorder_rec( p, Aig_ObjFanin0(pObj), vNodes );
+    Aig_ManDfsPreorder_rec( p, Aig_ObjFanin1(pObj), vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects objects of the AIG in the DFS order.]
+
+  Description [Works with choice nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManDfsPreorder( Aig_Man_t * p, int fNodesOnly )
+{
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManIncrementTravId( p );
+    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
+    // start the array of nodes
+    vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
+    // mark PIs if they should not be collected
+    if ( fNodesOnly )
+        Aig_ManForEachPi( p, pObj, i )
+            Aig_ObjSetTravIdCurrent( p, pObj );
+    else
+        Vec_PtrPush( vNodes, Aig_ManConst1(p) );
+    // collect nodes reachable in the DFS order
+    Aig_ManForEachPo( p, pObj, i )
+        Aig_ManDfsPreorder_rec( p, fNodesOnly? Aig_ObjFanin0(pObj): pObj, vNodes );
+    if ( fNodesOnly )
+        assert( Vec_PtrSize(vNodes) == Aig_ManNodeNum(p) );
+    else
+        assert( Vec_PtrSize(vNodes) == Aig_ManObjNum(p) );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Levelizes the nodes.]
 
   Description []
diff --git a/src/aig/aig/aigPartSat.c b/src/aig/aig/aigPartSat.c
new file mode 100644
index 00000000..2a3e975c
--- /dev/null
+++ b/src/aig/aig/aigPartSat.c
@@ -0,0 +1,612 @@
+/**CFile****************************************************************
+
+  FileName    [aigPartSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Partitioning for SAT solving.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigPartSat.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+#include "satSolver.h"
+#include "cnf.h"
+
+/* 
+
+The node partitioners defined in this file return array of intergers 
+mapping each AND node's ID into the 0-based number of its partition.
+The mapping of PIs/POs will be derived automatically in Aig_ManPartSplit().
+
+The partitions can be ordered in any way, but the recommended ordering
+is to first include partitions whose nodes are closer to the outputs.
+
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [No partitioning.]
+
+  Description [The partitioner ]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Aig_ManPartitionMonolithic( Aig_Man_t * p )
+{
+    Vec_Int_t * vId2Part;
+    vId2Part = Vec_IntStart( Aig_ManObjNumMax(p) );
+    return vId2Part;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Partitioning using levelized order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Aig_ManPartitionLevelized( Aig_Man_t * p, int nPartSize )
+{
+    Vec_Int_t * vId2Part;
+    Vec_Vec_t * vNodes;
+    Aig_Obj_t * pObj;
+    int i, k, Counter = 0;
+    vNodes = Aig_ManLevelize( p );
+    vId2Part = Vec_IntStart( Aig_ManObjNumMax(p) );
+    Vec_VecForEachEntryReverseReverse( vNodes, pObj, i, k )
+        Vec_IntWriteEntry( vId2Part, Aig_ObjId(pObj), Counter++/nPartSize );
+    Vec_VecFree( vNodes );
+    return vId2Part;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Partitioning using DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Aig_ManPartitionDfs( Aig_Man_t * p, int nPartSize, int fPreorder )
+{
+    Vec_Int_t * vId2Part; 
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+    vId2Part = Vec_IntStart( Aig_ManObjNumMax(p) );
+    if ( fPreorder )
+    {
+        vNodes = Aig_ManDfsPreorder( p, 1 );
+        Vec_PtrForEachEntry( vNodes, pObj, i )
+            Vec_IntWriteEntry( vId2Part, Aig_ObjId(pObj), Counter++/nPartSize );
+    }
+    else
+    {
+        vNodes = Aig_ManDfs( p, 1 );
+        Vec_PtrForEachEntryReverse( vNodes, pObj, i )
+            Vec_IntWriteEntry( vId2Part, Aig_ObjId(pObj), Counter++/nPartSize );
+    }
+    Vec_PtrFree( vNodes );
+    return vId2Part;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively constructs the partition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManPartSplitOne_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPio2Id )
+{
+    if ( !Aig_ObjIsTravIdCurrent( p, pObj ) )
+    { // new PI
+        Aig_ObjSetTravIdCurrent( p, pObj );
+/*
+        if ( pObj->fMarkA ) // const0
+            pObj->pData = Aig_ManConst0( pNew );
+        else if ( pObj->fMarkB ) // const1
+            pObj->pData = Aig_ManConst1( pNew );
+        else
+*/
+        {
+            pObj->pData = Aig_ObjCreatePi( pNew );
+            if ( pObj->fMarkA ) // const0
+                ((Aig_Obj_t *)pObj->pData)->fMarkA = 1;
+            else if ( pObj->fMarkB ) // const1
+                ((Aig_Obj_t *)pObj->pData)->fMarkB = 1;
+            Vec_IntPush( vPio2Id, Aig_ObjId(pObj) );
+        }
+        return;
+    }
+    if ( pObj->pData ) 
+        return;
+    Aig_ManPartSplitOne_rec( pNew, p, Aig_ObjFanin0(pObj), vPio2Id );
+    Aig_ManPartSplitOne_rec( pNew, p, Aig_ObjFanin1(pObj), vPio2Id );
+    pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Carves out one partition of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManPartSplitOne( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Int_t ** pvPio2Id )
+{
+    Vec_Int_t * vPio2Id;
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    // mark these nodes
+    Aig_ManIncrementTravId( p );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        Aig_ObjSetTravIdCurrent( p, pObj );
+        pObj->pData = NULL;
+    }
+    // add these nodes in a DFS order
+    pNew = Aig_ManStart( Vec_PtrSize(vNodes) );
+    vPio2Id = Vec_IntAlloc( 100 );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        Aig_ManPartSplitOne_rec( pNew, p, pObj, vPio2Id );
+    // add the POs
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        if ( Aig_ObjRefs(pObj->pData) != Aig_ObjRefs(pObj) )
+        {
+            assert( Aig_ObjRefs(pObj->pData) < Aig_ObjRefs(pObj) );
+            Aig_ObjCreatePo( pNew, pObj->pData );
+            Vec_IntPush( vPio2Id, Aig_ObjId(pObj) );
+        }
+    assert( Aig_ManNodeNum(pNew) == Vec_PtrSize(vNodes) );
+    *pvPio2Id = vPio2Id;
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives AIGs for each partition.]
+
+  Description [The first argument is a original AIG. The second argument
+  is the array mapping each AND-node's ID into the 0-based number of its
+  partition. The last argument is the array of arrays (one for each new AIG) 
+  mapping the index of each terminal in the new AIG (the index of each 
+  terminal is derived by ordering PIs followed by POs in their natural order) 
+  into the ID of the corresponding node in the original AIG. The returned 
+  value is the array of AIGs representing the partitions.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManPartSplit( Aig_Man_t * p, Vec_Int_t * vNode2Part, Vec_Ptr_t ** pvPio2Id, Vec_Ptr_t ** pvPart2Pos )
+{
+    Vec_Vec_t * vGroups, * vPart2Pos;
+    Vec_Ptr_t * vAigs, * vPio2Id, * vNodes;
+    Vec_Int_t * vPio2IdOne;
+    Aig_Man_t * pAig;
+    Aig_Obj_t * pObj, * pDriver;
+    int i, nodePart, nParts;
+    vAigs = Vec_PtrAlloc( 100 );
+    vPio2Id = Vec_PtrAlloc( 100 );
+    // put all nodes into levels according to their partition
+    nParts = Vec_IntFindMax(vNode2Part) + 1;
+    assert( nParts > 0 );
+    vGroups = Vec_VecAlloc( nParts );
+    Vec_IntForEachEntry( vNode2Part, nodePart, i )
+    {
+        pObj = Aig_ManObj( p, i );
+        if ( Aig_ObjIsNode(pObj) )
+            Vec_VecPush( vGroups, nodePart, pObj );
+    }
+
+    // label PIs that should be restricted to some values
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        pDriver = Aig_ObjFanin0(pObj);
+        if ( Aig_ObjIsPi(pDriver) )
+        {
+            if ( Aig_ObjFaninC0(pObj) )
+                pDriver->fMarkA = 1; // const0 PI
+            else
+                pDriver->fMarkB = 1; // const1 PI
+        }
+    }
+
+    // create partitions
+    Vec_VecForEachLevel( vGroups, vNodes, i )
+    {
+        if ( Vec_PtrSize(vNodes) == 0 )
+        {
+            printf( "Aig_ManPartSplit(): Skipping partition # %d without nodes (warning).\n", i );
+            continue;
+        }
+        pAig = Aig_ManPartSplitOne( p, vNodes, &vPio2IdOne );
+        Vec_PtrPush( vPio2Id, vPio2IdOne );
+        Vec_PtrPush( vAigs, pAig );
+    }
+    Vec_VecFree( vGroups );
+
+    // divide POs according to their partitions
+    vPart2Pos = Vec_VecStart( Vec_PtrSize(vAigs) );
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        pDriver = Aig_ObjFanin0(pObj);
+        if ( Aig_ObjIsPi(pDriver) )
+            pDriver->fMarkA = pDriver->fMarkB = 0;
+        else
+            Vec_VecPush( vPart2Pos, Vec_IntEntry(vNode2Part, Aig_ObjFaninId0(pObj)), pObj );
+    }
+
+    *pvPio2Id = vPio2Id;
+    *pvPart2Pos = (Vec_Ptr_t *)vPart2Pos;
+    return vAigs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resets node polarity to unbias the polarity of CNF variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManPartResetNodePolarity( Aig_Man_t * pPart )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManForEachObj( pPart, pObj, i )
+        pObj->fPhase = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets polarity according to the original nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManPartSetNodePolarity( Aig_Man_t * p, Aig_Man_t * pPart, Vec_Int_t * vPio2Id )
+{
+    Aig_Obj_t * pObj, * pObjInit;
+    int i;
+    Aig_ManConst1(pPart)->fPhase = 1;
+    Aig_ManForEachPi( pPart, pObj, i )
+    {
+        pObjInit = Aig_ManObj( p, Vec_IntEntry(vPio2Id, i) );
+        pObj->fPhase = pObjInit->fPhase;
+    }
+    Aig_ManForEachNode( pPart, pObj, i )
+        pObj->fPhase = (Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj)) & (Aig_ObjFanin1(pObj)->fPhase ^ Aig_ObjFaninC1(pObj));
+    Aig_ManForEachPo( pPart, pObj, i )
+    {
+        pObjInit = Aig_ManObj( p, Vec_IntEntry(vPio2Id, Aig_ManPiNum(pPart) + i) );
+        pObj->fPhase = (Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj));
+        assert( pObj->fPhase == pObjInit->fPhase );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets polarity according to the original nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManDeriveCounterExample( Aig_Man_t * p, Vec_Int_t * vNode2Var, sat_solver * pSat )
+{ 
+    Vec_Int_t * vPisIds;
+    Aig_Obj_t * pObj;
+    int i;
+    // collect IDs of PI variables
+    // (fanoutless PIs have SAT var 0, which is an unused in the SAT solver -> has value 0)
+    vPisIds = Vec_IntAlloc( Aig_ManPiNum(p) );
+    Aig_ManForEachPi( p, pObj, i )
+        Vec_IntPush( vPisIds, Vec_IntEntry(vNode2Var, Aig_ObjId(pObj)) );
+    // derive the SAT assignment
+    p->pData = Sat_SolverGetModel( pSat, vPisIds->pArray, vPisIds->nSize );
+    Vec_IntFree( vPisIds );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives CNF for the partition (pAig) and adds it to solver.]
+
+  Description [Array vPio2Id contains mapping of the PI/PO terminal of pAig
+  into the IDs of the corresponding original nodes. Array vNode2Var contains
+  mapping of the original nodes into their SAT variable numbers.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManAddNewCnfToSolver( sat_solver * pSat, Aig_Man_t * pAig, Vec_Int_t * vNode2Var, 
+                             Vec_Int_t * vPioIds, Vec_Ptr_t * vPartPos, int fAlignPol )
+{
+    Cnf_Dat_t * pCnf;
+    Aig_Obj_t * pObj;
+    int * pBeg, * pEnd;
+    int i, Lits[2], iSatVarOld, iNodeIdOld;
+    // derive CNF and express it using new SAT variables
+    pCnf = Cnf_Derive( pAig, Aig_ManPoNum(pAig) );
+    Cnf_DataTranformPolarity( pCnf, 1 );
+    Cnf_DataLift( pCnf, sat_solver_nvars(pSat) );
+    // create new variables in the SAT solver
+    sat_solver_setnvars( pSat, sat_solver_nvars(pSat) + pCnf->nVars );
+    // add clauses for this CNF
+    Cnf_CnfForClause( pCnf, pBeg, pEnd, i )
+        if ( !sat_solver_addclause( pSat, pBeg, pEnd ) )
+        {
+            assert( 0 ); // if it happens, can return 1 (unsatisfiable)
+            return 1;
+        }
+    // derive the connector clauses
+    Aig_ManForEachPi( pAig, pObj, i )
+    {
+        iNodeIdOld = Vec_IntEntry( vPioIds, i );
+        iSatVarOld = Vec_IntEntry( vNode2Var, iNodeIdOld );
+        if ( iSatVarOld == 0 ) // iNodeIdOld in the original AIG has no SAT var
+        { 
+            // map the corresponding original AIG node into this SAT var
+            Vec_IntWriteEntry( vNode2Var, iNodeIdOld, pCnf->pVarNums[Aig_ObjId(pObj)] );
+            continue;
+        }
+        // add connector clauses 
+        Lits[0] = toLitCond( iSatVarOld, 0 );
+        Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( iSatVarOld, 1 );
+        Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+    }
+    // derive the connector clauses
+    Aig_ManForEachPo( pAig, pObj, i )
+    {
+        iNodeIdOld = Vec_IntEntry( vPioIds, Aig_ManPiNum(pAig) + i );
+        iSatVarOld = Vec_IntEntry( vNode2Var, iNodeIdOld );
+        if ( iSatVarOld == 0 ) // iNodeIdOld in the original AIG has no SAT var
+        { 
+            // map the corresponding original AIG node into this SAT var
+            Vec_IntWriteEntry( vNode2Var, iNodeIdOld, pCnf->pVarNums[Aig_ObjId(pObj)] );
+            continue;
+        }
+        // add connector clauses 
+        Lits[0] = toLitCond( iSatVarOld, 0 );
+        Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( iSatVarOld, 1 );
+        Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+    }
+    // transfer the ID of constant 1 node
+    if ( Vec_IntEntry( vNode2Var, 0 ) == 0 )
+        Vec_IntWriteEntry( vNode2Var, 0, pCnf->pVarNums[0] );
+    // remove the CNF
+    Cnf_DataFree( pCnf );
+    // constrain the solver with the literals corresponding to the original POs
+    Vec_PtrForEachEntry( vPartPos, pObj, i )
+    {
+        iNodeIdOld = Aig_ObjFaninId0( pObj );
+        iSatVarOld = Vec_IntEntry( vNode2Var, iNodeIdOld );
+        assert( iSatVarOld != 0 );
+        // assert the original PO to be 1
+        Lits[0] = toLitCond( iSatVarOld, Aig_ObjFaninC0(pObj) );
+        // correct the polarity if polarity alignment is enabled
+        if ( fAlignPol && Aig_ObjFanin0(pObj)->fPhase ) 
+            Lits[0] = lit_neg( Lits[0] );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
+        {
+            assert( 0 ); // if it happens, can return 1 (unsatisfiable)
+            return 1;
+        }
+    }
+    // constrain some the primary inputs to constant values
+    Aig_ManForEachPi( pAig, pObj, i )
+    {
+        if ( !pObj->fMarkA && !pObj->fMarkB )
+            continue;
+        iNodeIdOld = Vec_IntEntry( vPioIds, i );
+        iSatVarOld = Vec_IntEntry( vNode2Var, iNodeIdOld );
+        Lits[0] = toLitCond( iSatVarOld, pObj->fMarkA );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
+        {
+            assert( 0 ); // if it happens, can return 1 (unsatisfiable)
+            return 1;
+        }
+        pObj->fMarkA = pObj->fMarkB = 0;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs partitioned SAT solving.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManPartitionedSat( Aig_Man_t * p, int nAlgo, int nPartSize, 
+    int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose )
+{
+    sat_solver * pSat;
+    Vec_Ptr_t * vAigs;
+    Vec_Vec_t * vPio2Id, * vPart2Pos;
+    Aig_Man_t * pAig, * pTemp;
+    Vec_Int_t * vNode2Part, * vNode2Var;
+    int nConfRemaining = nConfTotal, nNodes = 0;
+    int i, clk, status, RetValue;
+
+    // perform partitioning according to the selected algorithm
+    clk = clock();
+    switch ( nAlgo )
+    {
+    case 0: 
+        vNode2Part = Aig_ManPartitionMonolithic( p );
+        break;
+    case 1: 
+        vNode2Part = Aig_ManPartitionLevelized( p, nPartSize );
+        break;
+    case 2: 
+        vNode2Part = Aig_ManPartitionDfs( p, nPartSize, 0 );
+        break;
+    case 3: 
+        vNode2Part = Aig_ManPartitionDfs( p, nPartSize, 1 );
+        break;
+    default:
+        printf( "Unknown partitioning algorithm.\n" );
+        return -1;
+    }
+
+    if ( fVerbose )
+    {
+    printf( "Partitioning derived %d partitions. ", Vec_IntFindMax(vNode2Part) + 1 );
+    PRT( "Time", clock() - clk );
+    }
+
+    // split the original AIG into partition AIGs (vAigs)
+    // also, derives mapping of PIs/POs of partition AIGs into original nodes
+    // also, derives mapping of POs of the original AIG into partitions
+    vAigs = Aig_ManPartSplit( p, vNode2Part, (Vec_Ptr_t **)&vPio2Id, (Vec_Ptr_t **)&vPart2Pos );
+    Vec_IntFree( vNode2Part );
+
+    if ( fVerbose )
+    {
+    printf( "Partions were transformed into AIGs. " );
+    PRT( "Time", clock() - clk );
+    }
+
+    // synthesize partitions
+    if ( fSynthesize )
+    Vec_PtrForEachEntry( vAigs, pAig, i )
+    {
+        pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 );
+        Vec_PtrWriteEntry( vAigs, i, pAig );
+        Aig_ManStop( pTemp );
+    }
+
+    // start the SAT solver
+    pSat = sat_solver_new();
+//    pSat->verbosity = fVerbose;
+    // start mapping of the original AIG IDs into their SAT variable numbers
+    vNode2Var = Vec_IntStart( Aig_ManObjNumMax(p) );
+
+    // add partitions, one at a time, and run the SAT solver 
+    Vec_PtrForEachEntry( vAigs, pAig, i )
+    {
+clk = clock();
+        // transform polarity of the AIG
+        if ( fAlignPol )
+            Aig_ManPartSetNodePolarity( p, pAig, Vec_VecEntry(vPio2Id,i) );
+        else
+            Aig_ManPartResetNodePolarity( pAig );
+        // add CNF of this partition to the SAT solver
+        if ( Aig_ManAddNewCnfToSolver( pSat, pAig, vNode2Var, 
+            Vec_VecEntry(vPio2Id,i), Vec_VecEntry(vPart2Pos,i), fAlignPol ) )
+        {
+            RetValue = 1;
+            break;
+        }
+        // call the SAT solver
+        status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfRemaining, (sint64)0, (sint64)0, (sint64)0 );
+        if ( fVerbose )
+        {
+            printf( "%4d : Aig = %6d. Vs = %7d. RootCs = %7d. LearnCs = %6d. ",
+                i, nNodes += Aig_ManNodeNum(pAig), sat_solver_nvars(pSat), 
+                (int)pSat->stats.clauses, (int)pSat->stats.learnts );
+PRT( "Time", clock() - clk );
+        }
+        // analize the result
+        if ( status == l_False )
+        {
+            RetValue = 1;
+            break;
+        }
+        else if ( status == l_True )
+            RetValue = 0;
+        else
+            RetValue = -1;
+        nConfRemaining -= pSat->stats.conflicts;
+        if ( nConfRemaining <= 0 )
+        {
+            printf( "Exceeded the limit on the total number of conflicts (%d).\n", nConfTotal );
+            break;
+        }
+    }
+    if ( RetValue == 0 )
+        Aig_ManDeriveCounterExample( p, vNode2Var, pSat );
+    // cleanup
+    sat_solver_delete( pSat );
+    Vec_PtrForEachEntry( vAigs, pTemp, i )
+        Aig_ManStop( pTemp );
+    Vec_PtrFree( vAigs );
+    Vec_VecFree( vPio2Id );
+    Vec_VecFree( vPart2Pos );
+    Vec_IntFree( vNode2Var );
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index f1d018af..b1b8c5c2 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -13,6 +13,7 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigOrder.c \
     src/aig/aig/aigPart.c \
     src/aig/aig/aigPartReg.c \
+    src/aig/aig/aigPartSat.c \
     src/aig/aig/aigRepr.c \
     src/aig/aig/aigRet.c \
     src/aig/aig/aigRetF.c \
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index f4f782df..c9c5bce3 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -108,6 +108,10 @@ static inline void         Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut
 ///                           ITERATORS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+// iterator over the clauses
+#define Cnf_CnfForClause( p, pBeg, pEnd, i )                         \
+    for ( i = 0; i < p->nClauses && (pBeg = p->pClauses[i]) && (pEnd = p->pClauses[i+1]); i++ )
+
 // iterator over leaves of the cut
 #define Cnf_CutForEachLeaf( p, pCut, pLeaf, i )                         \
     for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )
@@ -142,7 +146,7 @@ extern void            Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, i
 extern void *          Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
 extern int             Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf );
 extern int             Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf );
-extern void            Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf );
+extern void            Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf, int fTransformPos );
 /*=== cnfMap.c ========================================================*/
 extern void            Cnf_DeriveMapping( Cnf_Man_t * p );
 extern int             Cnf_ManMapForCnf( Cnf_Man_t * p );
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index 1e650a05..9059b9e5 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -470,7 +470,7 @@ int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf )
   SeeAlso     []
 
 ***********************************************************************/
-void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf )
+void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf, int fTransformPos )
 {
     Aig_Obj_t * pObj;
     int * pVarToPol;
@@ -478,8 +478,12 @@ void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf )
     // create map from the variable number to its polarity
     pVarToPol = CALLOC( int, pCnf->nVars );
     Aig_ManForEachObj( pCnf->pMan, pObj, i )
-        if ( !Aig_ObjIsPo(pObj) && pCnf->pVarNums[pObj->Id] >= 0 )
+    {
+        if ( !fTransformPos && Aig_ObjIsPo(pObj) )
+            continue;
+        if ( pCnf->pVarNums[pObj->Id] >= 0 )
             pVarToPol[ pCnf->pVarNums[pObj->Id] ] = pObj->fPhase;
+    }
     // transform literals
     for ( i = 0; i < pCnf->nLiterals; i++ )
     {
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 1354e841..b27addd4 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -54,7 +54,7 @@ Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig )
 
 /**Function*************************************************************
 
-  Synopsis    [Reproduces script "compress2".]
+  Synopsis    [Reproduces script "rwsat".]
 
   Description []
                
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index e5940992..9046d574 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -55,7 +55,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFl
 //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
 
     if ( fFlipBits ) 
-        Cnf_DataTranformPolarity( pCnf );
+        Cnf_DataTranformPolarity( pCnf, 0 );
 
     // convert into SAT solver
     pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 1935bb7f..41f3ac59 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -530,7 +530,7 @@ p->timeTrav += clock() - clk2;
             pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
         else
             pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
-//        Cnf_DataTranformPolarity( pCnf );
+//        Cnf_DataTranformPolarity( pCnf, 0 );
 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
 
         p->pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 3aafeb18..04adb7e3 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -389,11 +389,11 @@ PRT( "Time", clock() - clkTotal );
 clk = clock();
     if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 )
     {
-        extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth );
+        extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth );
         int Depth;
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
-        RetValue = Saig_Interpolate( pNew, 5000, 40, 0, 1, 0, 1, 1, pParSec->fVeryVerbose, &Depth );
+        RetValue = Saig_Interpolate( pNew, 5000, 40, 0, 1, 0, 0, 0, 1, 1, pParSec->fVeryVerbose, &Depth );
         if ( pParSec->fVerbose )
         {
         if ( RetValue == 1 )
diff --git a/src/aig/hop/hopDfs.c b/src/aig/hop/hopDfs.c
index 29963f6d..bf196aea 100644
--- a/src/aig/hop/hopDfs.c
+++ b/src/aig/hop/hopDfs.c
@@ -394,7 +394,7 @@ Hop_Obj_t * Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, in
 
 /**Function*************************************************************
 
-  Synopsis    [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
+  Synopsis    [Remaps the AIG (pRoot) to have the given support (uSupp).]
 
   Description []
                
@@ -417,7 +417,7 @@ void Hop_Remap_rec( Hop_Man_t * p, Hop_Obj_t * pObj )
 
 /**Function*************************************************************
 
-  Synopsis    [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
+  Synopsis    [Remaps the AIG (pRoot) to have the given support (uSupp).]
 
   Description []
                
diff --git a/src/aig/mfx/mfxCore.c b/src/aig/mfx/mfxCore.c
index a7cd3e3c..d9f73c9d 100644
--- a/src/aig/mfx/mfxCore.c
+++ b/src/aig/mfx/mfxCore.c
@@ -205,7 +205,10 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib )
     int nTotalNodesBeg = Nwk_ManNodeNum(pNtk);
     int nTotalEdgesBeg = Nwk_ManGetTotalFanins(pNtk);
 
-//    assert( Nwk_ManCheck( pNtk ) );
+    // prepare the network for processing
+    Nwk_ManRemoveDupFanins( pNtk, 0 );
+    assert( Nwk_ManCheck( pNtk ) );
+
     // check limits on the number of fanins
     nFaninMax = Nwk_ManGetFaninMax(pNtk);
     if ( pPars->fResub )
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index f4d33cf1..79cd640a 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -803,6 +803,8 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan
         pNtk->pManTime = Tim_ManDup( pManTime, 0 );
     else
         pNtk->pManTime = Tim_ManDup( p->pManTime, 0 );
+//    Nwk_ManRemoveDupFanins( pNtk, 0 );
+//    assert( Nwk_ManCheck( pNtk ) );
     return pNtk;
 }
 
diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h
index 222130f3..603c1fb8 100644
--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -301,6 +301,7 @@ extern ABC_DLL void            Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileNa
 extern ABC_DLL void            Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk );
 extern ABC_DLL void            Nwk_ManCleanMarks( Nwk_Man_t * pNtk );
 extern ABC_DLL void            Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose );
+extern ABC_DLL void            Nwk_ManRemoveDupFanins( Nwk_Man_t * pNtk, int fVerbose );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/nwk/nwkCheck.c b/src/aig/nwk/nwkCheck.c
index 6922e439..0890ced8 100644
--- a/src/aig/nwk/nwkCheck.c
+++ b/src/aig/nwk/nwkCheck.c
@@ -41,7 +41,7 @@
 ***********************************************************************/
 int Nwk_ManCheck( Nwk_Man_t * p )
 {
-    Nwk_Obj_t * pObj;
+    Nwk_Obj_t * pObj, * pNext;
     int i, k, m;
     // check if the nodes have duplicated fanins
     Nwk_ManForEachNode( p, pObj, i )
@@ -51,7 +51,6 @@ int Nwk_ManCheck( Nwk_Man_t * p )
                 if ( pObj->pFanio[k] == pObj->pFanio[m] )
                     printf( "Node %d has duplicated fanin %d.\n", pObj->Id, pObj->pFanio[k]->Id );
     }
-/*
     // check if all nodes are in the correct fanin/fanout relationship
     Nwk_ManForEachObj( p, pObj, i )
     {
@@ -62,7 +61,6 @@ int Nwk_ManCheck( Nwk_Man_t * p )
             if ( Nwk_ObjFindFanin( pNext, pObj ) == -1 )
                 printf( "Nwk_ManCheck(): Object %d has fanout %d which does not have a corresponding fanin.\n", pObj->Id, pNext->Id );
     }
-*/
     return 1;
 }
 
diff --git a/src/aig/nwk/nwkFanio.c b/src/aig/nwk/nwkFanio.c
index 4068a1a5..56a13741 100644
--- a/src/aig/nwk/nwkFanio.c
+++ b/src/aig/nwk/nwkFanio.c
@@ -188,19 +188,25 @@ void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin )
 ***********************************************************************/
 void Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin )
 {
-    int i, k, Limit;
+    int i, k, Limit, fFound;
     // remove pFanin from the fanin list of pObj
     Limit = pObj->nFanins + pObj->nFanouts;
+    fFound = 0;
     for ( k = i = 0; i < Limit; i++ )
-        if ( pObj->pFanio[i] != pFanin )
+        if ( fFound || pObj->pFanio[i] != pFanin )
             pObj->pFanio[k++] = pObj->pFanio[i];
+        else
+            fFound = 1;
     assert( i == k + 1 ); // if it fails, likely because of duplicated fanin
     pObj->nFanins--;
     // remove pObj from the fanout list of pFanin
     Limit = pFanin->nFanins + pFanin->nFanouts;
+    fFound = 0;
     for ( k = i = pFanin->nFanins; i < Limit; i++ )
-        if ( pFanin->pFanio[i] != pObj )
+        if ( fFound || pFanin->pFanio[i] != pObj )
             pFanin->pFanio[k++] = pFanin->pFanio[i];
+        else
+            fFound = 1;
     assert( i == k + 1 ); // if it fails, likely because of duplicated fanout
     pFanin->nFanouts--; 
 }
diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c
index d6daca4e..fccac175 100644
--- a/src/aig/nwk/nwkUtil.c
+++ b/src/aig/nwk/nwkUtil.c
@@ -477,37 +477,116 @@ void Nwk_ManCleanMarks( Nwk_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose )
+int Nwk_ManMinimumBaseNode( Nwk_Obj_t * pObj, Vec_Int_t * vTruth, int fVerbose )
 {
     unsigned * pTruth;
+    Nwk_Obj_t * pFanin, * pObjNew;
+    Nwk_Man_t * pNtk = pObj->pMan;
+    int uSupp, nSuppSize, k, Counter = 0;
+    pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
+    nSuppSize = Kit_TruthSupportSize(pTruth, Nwk_ObjFaninNum(pObj));
+    if ( nSuppSize == Nwk_ObjFaninNum(pObj) )
+        return 0;
+    Counter++;
+    uSupp = Kit_TruthSupport( pTruth, Nwk_ObjFaninNum(pObj) );
+    // create new node with the given support
+    pObjNew = Nwk_ManCreateNode( pNtk, nSuppSize, Nwk_ObjFanoutNum(pObj) );
+    Nwk_ObjForEachFanin( pObj, pFanin, k )
+        if ( uSupp & (1 << k) )
+            Nwk_ObjAddFanin( pObjNew, pFanin );
+    pObjNew->pFunc = Hop_Remap( pNtk->pManHop, pObj->pFunc, uSupp, Nwk_ObjFaninNum(pObj) );
+    if ( fVerbose )
+        printf( "Reducing node %d fanins from %d to %d.\n", 
+            pObj->Id, Nwk_ObjFaninNum(pObj), Nwk_ObjFaninNum(pObjNew) );
+    Nwk_ObjReplace( pObj, pObjNew );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Minimizes the support of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose )
+{
     Vec_Int_t * vTruth;
-    Nwk_Obj_t * pObj, * pFanin, * pObjNew;
-    int uSupp, nSuppSize, i, k, Counter = 0;
+    Nwk_Obj_t * pObj;
+    int i, Counter = 0;
     vTruth = Vec_IntAlloc( 1 << 16 );
     Nwk_ManForEachNode( pNtk, pObj, i )
-    {
-        pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
-        nSuppSize = Kit_TruthSupportSize(pTruth, Nwk_ObjFaninNum(pObj));
-        if ( nSuppSize == Nwk_ObjFaninNum(pObj) )
-            continue;
-        Counter++;
-        uSupp = Kit_TruthSupport( pTruth, Nwk_ObjFaninNum(pObj) );
-        // create new node with the given support
-        pObjNew = Nwk_ManCreateNode( pNtk, nSuppSize, Nwk_ObjFanoutNum(pObj) );
-        Nwk_ObjForEachFanin( pObj, pFanin, k )
-            if ( uSupp & (1 << k) )
-                Nwk_ObjAddFanin( pObjNew, pFanin );
-        pObjNew->pFunc = Hop_Remap( pNtk->pManHop, pObj->pFunc, uSupp, Nwk_ObjFaninNum(pObj) );
-        if ( fVerbose )
-            printf( "Reducing node %d fanins from %d to %d.\n", 
-                pObj->Id, Nwk_ObjFaninNum(pObj), Nwk_ObjFaninNum(pObjNew) );
-        Nwk_ObjReplace( pObj, pObjNew );
-    }
+        Counter += Nwk_ManMinimumBaseNode( pObj, vTruth, fVerbose );
     if ( fVerbose && Counter )
         printf( "Support minimization reduced support of %d nodes.\n", Counter );
     Vec_IntFree( vTruth );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Minimizes the support of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManRemoveDupFaninsNode( Nwk_Obj_t * pObj, int iFan0, int iFan1, Vec_Int_t * vTruth )
+{
+    Hop_Man_t * pManHop = pObj->pMan->pManHop;
+//    Nwk_Obj_t * pFanin0 = pObj->pFanio[iFan0];
+//    Nwk_Obj_t * pFanin1 = pObj->pFanio[iFan1];
+    assert( pObj->pFanio[iFan0] == pObj->pFanio[iFan1] );
+    pObj->pFunc = Hop_Compose( pManHop, pObj->pFunc, Hop_IthVar(pManHop,iFan0), iFan1 );
+    Nwk_ManMinimumBaseNode( pObj, vTruth, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Minimizes the support of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManRemoveDupFanins( Nwk_Man_t * pNtk, int fVerbose )
+{
+    Vec_Int_t * vTruth;
+    Nwk_Obj_t * pObj;
+    int i, k, m, fFound;
+    // check if the nodes have duplicated fanins
+    vTruth = Vec_IntAlloc( 1 << 16 );
+    Nwk_ManForEachNode( pNtk, pObj, i )
+    {
+        fFound = 0;
+        for ( k = 0; k < pObj->nFanins; k++ )
+        {
+            for ( m = k + 1; m < pObj->nFanins; m++ )
+                if ( pObj->pFanio[k] == pObj->pFanio[m] )
+                {
+                    if ( fVerbose )
+                        printf( "Removing duplicated fanins of node %d (fanins %d and %d).\n", 
+                            pObj->Id, pObj->pFanio[k]->Id, pObj->pFanio[m]->Id );
+                    Nwk_ManRemoveDupFaninsNode( pObj, k, m, vTruth );
+                    fFound = 1;
+                    break;
+                }
+            if ( fFound )
+                break;
+        }
+    }
+    Vec_IntFree( vTruth );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 5a7beeec..e2fbda2d 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -85,7 +85,7 @@ extern Aig_Man_t *       Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSte
 extern void              Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 extern Aig_Man_t *       Saig_ManReadBlif( char * pFileName );
 /*=== saigInter.c ==========================================================*/
-extern int               Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth );
+extern int               Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth );
 /*=== saigMiter.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
 /*=== saigPhase.c ==========================================================*/
diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c
index 86982d46..65fe6d87 100644
--- a/src/aig/saig/saigInter.c
+++ b/src/aig/saig/saigInter.c
@@ -67,7 +67,7 @@ struct Saig_IntMan_t_
 };
 
 #ifdef ABC_USE_LIBRARIES
-static int Saig_M144pPerformOneStep( Saig_IntMan_t * p );
+static int Saig_M144pPerformOneStep( Saig_IntMan_t * p, int fUsePudlak, int fUseOther );
 #endif
 
 ////////////////////////////////////////////////////////////////////////
@@ -896,7 +896,7 @@ int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p, int fSubtractOld )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth )
+int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth )
 {
     extern int Saig_ManUniqueState( Aig_Man_t * pTrans, Vec_Ptr_t * vInters );
     Saig_IntMan_t * p;
@@ -982,8 +982,8 @@ p->timeCnf += clock() - clk;
             // perform interplation
             clk = clock();
 #ifdef ABC_USE_LIBRARIES
-            if ( fUseIp )
-                RetValue = Saig_M144pPerformOneStep( p );
+            if ( fUseMiniSat )
+                RetValue = Saig_M144pPerformOneStep( p, fUsePudlak, fUseOther );
             else
 #endif
                 RetValue = Saig_PerformOneStep( p, 0 );
@@ -1177,7 +1177,10 @@ M114p_Solver_t Saig_M144pDeriveSatSolver(
     {
         Vec_IntPush( *pvMapRoots, 1 );
         if ( !M114p_SolverAddClause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
-            assert( 0 );
+        {
+//            assert( 0 );
+            break;
+        }
     }
     // return clauses to the original state
     Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
@@ -1200,20 +1203,149 @@ M114p_Solver_t Saig_M144pDeriveSatSolver(
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
+void Saig_M144pInterpolateReport( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
 {
-    Aig_Man_t * p;
-    Aig_Obj_t * pInter, * pInter2, * pVar;
-    Vec_Ptr_t * vInters;
     Vec_Int_t * vASteps;
     int * pLits, * pClauses, * pVars;
     int nLits, nVars, i, k, iVar, haveASteps;
     int CountA, CountB, CountC, CountCsaved;
 
     assert( M114p_SolverProofIsReady(s) );
-    vInters = Vec_PtrAlloc( 1000 );
     vASteps = Vec_IntAlloc( 1000 );
     // process root clauses
+    M114p_SolverForEachRoot( s, &pLits, nLits, i )
+    {
+        if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
+        {
+        }
+        else // clause of A
+        {
+        }
+        Vec_IntPush( vASteps, Vec_IntEntry(vMapRoots, i) );
+    }
+//    assert( Vec_IntSize(vASteps) == Vec_IntSize(vMapRoots) );
+ 
+    // process learned clauses
+    CountA = CountB = CountC = CountCsaved = 0;
+    M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
+    {
+        haveASteps = Vec_IntEntry( vASteps, pClauses[0] );
+        for ( k = 0; k < nVars; k++ )
+        {
+            iVar = Vec_IntEntry( vMapVars, pVars[k] );
+            haveASteps |= Vec_IntEntry( vASteps, pClauses[k+1] );
+            if ( iVar == -1 ) // var of A
+            {
+                haveASteps = 1;
+            }
+            else // var of B or C
+            {
+            }
+
+            if ( iVar == -1 )
+                CountA++;
+            else if ( iVar == -2 )
+                CountB++;
+            else 
+            {
+                if ( haveASteps == 0 )
+                    CountCsaved++;
+                CountC++;
+            }
+        }
+        Vec_IntPush( vASteps, haveASteps );
+    }
+    assert( Vec_IntSize(vASteps) == M114p_SolverProofClauseNum(s) );
+
+    printf( "ResSteps: A = %6d. B = %6d. C = %6d. C_saved = %6d. (%6.2f %%)\n", 
+        CountA, CountB, CountC, CountCsaved, 100.0 * CountCsaved/CountC );
+    Vec_IntFree( vASteps );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes interpolant using MiniSat-1.14p.]
+
+  Description [Assumes that the solver returned UNSAT and proof
+  logging was enabled. Array vMapRoots maps number of each root clause 
+  into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
+  solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
+  where <num> is the var's 0-based number in the ordering of C variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_M144pInterpolateLastStep( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
+{
+    int * pLits, * pClauses, * pVars;
+    int nLits, nVars, i, k, iVar;
+    int nSteps, iStepA, iStepB;
+    assert( M114p_SolverProofIsReady(s) );
+    // process root clauses
+    M114p_SolverForEachRoot( s, &pLits, nLits, i )
+    {
+        if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
+        {
+        }
+        else // clause of A
+        {
+        }
+    }
+//    assert( Vec_IntSize(vASteps) == Vec_IntSize(vMapRoots) );
+    // process learned clauses
+    nSteps = 0;
+    M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
+    {
+        for ( k = 0; k < nVars; k++ )
+        {
+            iVar = Vec_IntEntry( vMapVars, pVars[k] );
+            if ( iVar == -1 ) // var of A
+            {
+                iStepA = nSteps;
+            }
+            else if ( iVar == -2 ) // var of B
+            {
+                iStepB = nSteps;
+            }
+            else // var of C
+            {
+            }
+            nSteps++;
+        }
+    }
+//    assert( Vec_IntSize(vASteps) == M114p_SolverProofClauseNum(s) );
+    if ( iStepA < iStepB )
+        return iStepB;
+    return iStepA;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes interpolant using MiniSat-1.14p.]
+
+  Description [Assumes that the solver returned UNSAT and proof
+  logging was enabled. Array vMapRoots maps number of each root clause 
+  into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
+  solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
+  where <num> is the var's 0-based number in the ordering of C variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
+{
+    Aig_Man_t * p;
+    Aig_Obj_t * pInter, * pInter2, * pVar;
+    Vec_Ptr_t * vInters;
+    int * pLits, * pClauses, * pVars;
+    int nLits, nVars, i, k, iVar;
+    assert( M114p_SolverProofIsReady(s) );
+    vInters = Vec_PtrAlloc( 1000 );
+    // process root clauses
     p = Aig_ManStart( 10000 );
     M114p_SolverForEachRoot( s, &pLits, nLits, i )
     {
@@ -1232,50 +1364,306 @@ Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_
             }
         }
         Vec_PtrPush( vInters, pInter );
-        Vec_IntPush( vASteps, 0 );
     }
-    assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
+//    assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
 
     // process learned clauses
-    CountA = CountB = CountC = CountCsaved = 0;
     M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
     {
         pInter = Vec_PtrEntry( vInters, pClauses[0] );
-        haveASteps = Vec_IntEntry( vASteps, pClauses[0] );
         for ( k = 0; k < nVars; k++ )
         {
             iVar = Vec_IntEntry( vMapVars, pVars[k] );
             pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
-            haveASteps |= Vec_IntEntry( vASteps, pClauses[k+1] );
             if ( iVar == -1 ) // var of A
-            {
-                haveASteps = 1;
                 pInter = Aig_Or( p, pInter, pInter2 );
-            }
             else // var of B or C
                 pInter = Aig_And( p, pInter, pInter2 );
+        }
+        Vec_PtrPush( vInters, pInter );
+    }
+    assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
+    Vec_PtrFree( vInters );
+    Aig_ObjCreatePo( p, pInter );
+    Aig_ManCleanup( p );
+    return p;
+}
 
-            if ( iVar == -1 )
-                CountA++;
-            else if ( iVar == -2 )
-                CountB++;
-            else 
+/**Function*************************************************************
+
+  Synopsis    [Performs one resolution step.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_M144pResolve( Vec_Int_t * vResolvent, int * pLits, int nLits, int iVar )
+{
+    int i, k, iLit = -1, fFound = 0;
+    // find the variable in the clause
+    for ( i = 0; i < vResolvent->nSize; i++ )
+        if ( lit_var(vResolvent->pArray[i]) == iVar )
+        {
+            iLit = vResolvent->pArray[i];
+            vResolvent->pArray[i] = vResolvent->pArray[--vResolvent->nSize];
+            break;
+        }
+    assert( iLit != -1 );
+    // add other variables
+    for ( i = 0; i < nLits; i++ )
+    {
+        if ( lit_var(pLits[i]) == iVar )
+        {
+            assert( iLit == lit_neg(pLits[i]) );
+            fFound = 1;
+            continue;
+        }
+        // check if this literal appears
+        for ( k = 0; k < vResolvent->nSize; k++ )
+            if ( vResolvent->pArray[k] == pLits[i] )
+                break;
+        if ( k < vResolvent->nSize )
+            continue;
+        // add this literal
+        Vec_IntPush( vResolvent, pLits[i] );
+    }
+    assert( fFound );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes interpolant using MiniSat-1.14p.]
+
+  Description [Assumes that the solver returned UNSAT and proof
+  logging was enabled. Array vMapRoots maps number of each root clause 
+  into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
+  solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
+  where <num> is the var's 0-based number in the ordering of C variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_M144pInterpolatePudlak( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
+{
+    Aig_Man_t * p;
+    Aig_Obj_t * pInter, * pInter2, * pVar;
+    Vec_Ptr_t * vInters;
+    Vec_Int_t * vLiterals, * vClauses, * vResolvent;
+    int * pLitsNext, nLitsNext, nOffset, iLit;
+    int * pLits, * pClauses, * pVars;
+    int nLits, nVars, i, k, v, iVar;
+    assert( M114p_SolverProofIsReady(s) );
+    vInters = Vec_PtrAlloc( 1000 );
+
+    vLiterals = Vec_IntAlloc( 10000 );
+    vClauses = Vec_IntAlloc( 1000 );
+    vResolvent = Vec_IntAlloc( 100 );
+
+    // create elementary variables
+    p = Aig_ManStart( 10000 );
+    Vec_IntForEachEntry( vMapVars, iVar, i )
+        if ( iVar >= 0 )
+            Aig_IthVar(p, iVar);
+    // process root clauses
+    M114p_SolverForEachRoot( s, &pLits, nLits, i )
+    {
+        if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
+            pInter = Aig_ManConst1(p);
+        else // clause of A
+            pInter = Aig_ManConst0(p);
+        Vec_PtrPush( vInters, pInter );
+
+        // save the root clause
+        Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
+        Vec_IntPush( vLiterals, nLits );
+        for ( v = 0; v < nLits; v++ )
+            Vec_IntPush( vLiterals, pLits[v] );
+    }
+    assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
+
+    // process learned clauses
+    M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
+    {
+        pInter = Vec_PtrEntry( vInters, pClauses[0] );
+
+        // initialize the resolvent
+        nOffset = Vec_IntEntry( vClauses, pClauses[0] );
+        nLitsNext = Vec_IntEntry( vLiterals, nOffset );
+        pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
+        Vec_IntClear( vResolvent );
+        for ( v = 0; v < nLitsNext; v++ )
+            Vec_IntPush( vResolvent, pLitsNext[v] );
+
+        for ( k = 0; k < nVars; k++ )
+        {
+            iVar = Vec_IntEntry( vMapVars, pVars[k] );
+            pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
+
+            // resolve it with the next clause
+            nOffset = Vec_IntEntry( vClauses, pClauses[k+1] );
+            nLitsNext = Vec_IntEntry( vLiterals, nOffset );
+            pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
+            Saig_M144pResolve( vResolvent, pLitsNext, nLitsNext, pVars[k] );
+
+            if ( iVar == -1 ) // var of A
+                pInter = Aig_Or( p, pInter, pInter2 );
+            else if ( iVar == -2 ) // var of B
+                pInter = Aig_And( p, pInter, pInter2 );
+            else // var of C
+            {
+                // check polarity of the pivot variable in the clause
+                for ( v = 0; v < nLitsNext; v++ )
+                    if ( lit_var(pLitsNext[v]) == pVars[k] )
+                        break;
+                assert( v < nLitsNext );
+                pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLitsNext[v]) );
+                pInter = Aig_Mux( p, pVar, pInter, pInter2 );
+            }
+        }
+        Vec_PtrPush( vInters, pInter );
+
+        // store the resulting clause
+        Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
+        Vec_IntPush( vLiterals, Vec_IntSize(vResolvent) );
+        Vec_IntForEachEntry( vResolvent, iLit, v )
+            Vec_IntPush( vLiterals, iLit );
+    }
+    assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
+    assert( Vec_IntSize(vResolvent) == 0 ); // the empty clause
+    Vec_PtrFree( vInters );
+    Vec_IntFree( vLiterals );
+    Vec_IntFree( vClauses );
+    Vec_IntFree( vResolvent );
+    Aig_ObjCreatePo( p, pInter );
+    Aig_ManCleanup( p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes interpolant using MiniSat-1.14p.]
+
+  Description [Assumes that the solver returned UNSAT and proof
+  logging was enabled. Array vMapRoots maps number of each root clause 
+  into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
+  solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
+  where <num> is the var's 0-based number in the ordering of C variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_M144pInterpolatePudlakASteps( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
+{
+    Aig_Man_t * p;
+    Aig_Obj_t * pInter, * pInter2, * pVar;
+    Vec_Ptr_t * vInters;
+    Vec_Int_t * vASteps;
+    Vec_Int_t * vLiterals, * vClauses, * vResolvent;
+    int * pLitsNext, nLitsNext, nOffset, iLit;
+    int * pLits, * pClauses, * pVars;
+    int nLits, nVars, i, k, v, iVar, haveASteps;
+    assert( M114p_SolverProofIsReady(s) );
+    vInters = Vec_PtrAlloc( 1000 );
+    vASteps = Vec_IntAlloc( 1000 );
+
+    vLiterals = Vec_IntAlloc( 10000 );
+    vClauses = Vec_IntAlloc( 1000 );
+    vResolvent = Vec_IntAlloc( 100 );
+
+    // create elementary variables
+    p = Aig_ManStart( 10000 );
+    Vec_IntForEachEntry( vMapVars, iVar, i )
+        if ( iVar >= 0 )
+            Aig_IthVar(p, iVar);
+    // process root clauses
+    M114p_SolverForEachRoot( s, &pLits, nLits, i )
+    {
+        if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
+            pInter = Aig_ManConst1(p);
+        else // clause of A
+            pInter = Aig_ManConst0(p);
+        Vec_PtrPush( vInters, pInter );
+        Vec_IntPush( vASteps, Vec_IntEntry(vMapRoots, i) );
+
+        // save the root clause
+        Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
+        Vec_IntPush( vLiterals, nLits );
+        for ( v = 0; v < nLits; v++ )
+            Vec_IntPush( vLiterals, pLits[v] );
+    }
+    assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
+
+    // process learned clauses
+    M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
+    {
+        pInter = Vec_PtrEntry( vInters, pClauses[0] );
+        haveASteps = Vec_IntEntry( vASteps, pClauses[0] );
+
+        // initialize the resolvent
+        nOffset = Vec_IntEntry( vClauses, pClauses[0] );
+        nLitsNext = Vec_IntEntry( vLiterals, nOffset );
+        pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
+        Vec_IntClear( vResolvent );
+        for ( v = 0; v < nLitsNext; v++ )
+            Vec_IntPush( vResolvent, pLitsNext[v] );
+
+        for ( k = 0; k < nVars; k++ )
+        {
+            iVar = Vec_IntEntry( vMapVars, pVars[k] );
+            pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
+            haveASteps |= Vec_IntEntry( vASteps, pClauses[k+1] );
+
+            // resolve it with the next clause
+            nOffset = Vec_IntEntry( vClauses, pClauses[k+1] );
+            nLitsNext = Vec_IntEntry( vLiterals, nOffset );
+            pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
+            Saig_M144pResolve( vResolvent, pLitsNext, nLitsNext, pVars[k] );
+
+            if ( iVar == -1 ) // var of A
+                pInter = Aig_Or( p, pInter, pInter2 ), haveASteps = 1;
+            else if ( iVar == -2 ) // var of B
+                pInter = Aig_And( p, pInter, pInter2 );
+            else // var of C
             {
                 if ( haveASteps == 0 )
-                    CountCsaved++;
-                CountC++;
+                    pInter = Aig_ManConst0(p);
+                else
+                {
+                    // check polarity of the pivot variable in the clause
+                    for ( v = 0; v < nLitsNext; v++ )
+                        if ( lit_var(pLitsNext[v]) == pVars[k] )
+                            break;
+                    assert( v < nLitsNext );
+                    pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLitsNext[v]) );
+                    pInter = Aig_Mux( p, pVar, pInter, pInter2 );
+                }
             }
         }
         Vec_PtrPush( vInters, pInter );
         Vec_IntPush( vASteps, haveASteps );
-    }
-//    printf( "ResSteps: A = %6d. B = %6d. C = %6d. C_saved = %6d. (%6.2f %%)\n", 
-//        CountA, CountB, CountC, CountCsaved, 100.0 * CountCsaved/CountC );
 
+        // store the resulting clause
+        Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
+        Vec_IntPush( vLiterals, Vec_IntSize(vResolvent) );
+        Vec_IntForEachEntry( vResolvent, iLit, v )
+            Vec_IntPush( vLiterals, iLit );
+    }
     assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
+    assert( Vec_IntSize(vResolvent) == 0 ); // the empty clause
     Vec_PtrFree( vInters );
     Vec_IntFree( vASteps );
 
+    Vec_IntFree( vLiterals );
+    Vec_IntFree( vClauses );
+    Vec_IntFree( vResolvent );
     Aig_ObjCreatePo( p, pInter );
     Aig_ManCleanup( p );
     return p;
@@ -1292,7 +1680,7 @@ Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_M144pPerformOneStep( Saig_IntMan_t * p )
+int Saig_M144pPerformOneStep( Saig_IntMan_t * p, int fUsePudlak, int fUseOther )
 {
     M114p_Solver_t pSat;
     Vec_Int_t * vMapRoots, * vMapVars;
@@ -1310,8 +1698,18 @@ p->timeSat += clock() - clk;
     if ( status == 0 )
     {
         RetValue = 1;
+
+        ///// report the savings of the modified Pudlak's approach
+        Saig_M144pInterpolateReport( pSat, vMapRoots, vMapVars );
+        /////
+
 clk = clock();
-        p->pInterNew = Saig_M144pInterpolate( pSat, vMapRoots, vMapVars );
+        if ( fUseOther )
+            p->pInterNew = Saig_M144pInterpolatePudlakASteps( pSat, vMapRoots, vMapVars );
+        else if ( fUsePudlak )
+            p->pInterNew = Saig_M144pInterpolatePudlak( pSat, vMapRoots, vMapVars );
+        else
+            p->pInterNew = Saig_M144pInterpolate( pSat, vMapRoots, vMapVars );
 p->timeInt += clock() - clk;
     }
     else if ( status == 1 )
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index e83bd132..fec01ef7 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -549,7 +549,7 @@ Vec_Ptr_t * Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll )
     }
     // collect dangling nodes if asked to
     if ( fCollectAll )
-    {
+    { 
         Abc_NtkForEachNode( pNtk, pObj, i )
             if ( !Abc_NodeIsTravIdCurrent(pObj) )
                 Abc_NtkDfs_iter( vStack, pObj, vNodes );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 264b1df4..b8a9cefe 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -200,6 +200,7 @@ static int Abc_CommandSec            ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandDSec           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSat            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDSat           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPSat           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandProve          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDebug          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -218,6 +219,7 @@ static int Abc_CommandAbc8Write      ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAbc8WriteLogic ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8ReadLut    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8PrintLut   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Check      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandAbc8Ps         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Pfan       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -458,6 +460,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "dprove",        Abc_CommandDProve,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "sat",           Abc_CommandSat,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "dsat",          Abc_CommandDSat,             0 );
+    Cmd_CommandAdd( pAbc, "Verification", "psat",          Abc_CommandPSat,             0 );
     Cmd_CommandAdd( pAbc, "Verification", "prove",         Abc_CommandProve,            1 );
     Cmd_CommandAdd( pAbc, "Verification", "iprove",        Abc_CommandIProve,           1 );
     Cmd_CommandAdd( pAbc, "Verification", "debug",         Abc_CommandDebug,            0 );
@@ -473,6 +476,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC8",         "*wlogic",       Abc_CommandAbc8WriteLogic,   0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*rlut",         Abc_CommandAbc8ReadLut,      0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*plut",         Abc_CommandAbc8PrintLut,     0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*check",        Abc_CommandAbc8Check,        0 );
 
     Cmd_CommandAdd( pAbc, "ABC8",         "*ps",           Abc_CommandAbc8Ps,           0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*pfan",         Abc_CommandAbc8Pfan,         0 );
@@ -6357,7 +6361,7 @@ int Abc_CommandTopAnd( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: topand [-h]\n" );
-    fprintf( pErr, "\t         AND-decomposition of single-output combinational miter\n" );
+    fprintf( pErr, "\t         performs AND-decomposition of single-output combinational miter\n" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     fprintf( pErr, "\tname   : the node name\n");
     return 1;
@@ -14196,7 +14200,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fPartition;
     int fMiter;
 
-    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
     extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -14850,14 +14854,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
     int RetValue;
-    int fFlipBits;
+    int fAlignPol;
     int fAndOuts;
     int fVerbose;
     int nConfLimit;
     int nInsLimit;
     int clk;
 
-    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
 
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -14865,13 +14869,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fFlipBits  = 0;
+    fAlignPol  = 0;
     fAndOuts   = 0;
     fVerbose   = 0;
     nConfLimit = 100000;   
     nInsLimit  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CIfavh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CIpavh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -14897,8 +14901,8 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nInsLimit < 0 ) 
                 goto usage;
             break;
-        case 'f':
-            fFlipBits ^= 1;
+        case 'p':
+            fAlignPol ^= 1;
             break;
         case 'a':
             fAndOuts ^= 1;
@@ -14937,7 +14941,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     clk = clock();
-    RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fFlipBits, fAndOuts, fVerbose );
+    RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fAlignPol, fAndOuts, fVerbose );
     // verify that the pattern is correct
     if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
     {
@@ -14970,13 +14974,177 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dsat [-C num] [-I num] [-favh]\n" );
+    fprintf( pErr, "usage: dsat [-C num] [-I num] [-pavh]\n" );
     fprintf( pErr, "\t         solves the combinational miter using SAT solver MiniSat-1.14\n" );
     fprintf( pErr, "\t         derives CNF from the current network and leave it unchanged\n" );
     fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
     fprintf( pErr, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
-    fprintf( pErr, "\t-f     : flip polarity of SAT variables [default = %s]\n", fFlipBits? "yes": "no" );  
-    fprintf( pErr, "\t-a     : constrain each output of multi-output miter [default = %s]\n", fAndOuts? "yes": "no" );  
+    fprintf( pErr, "\t-p     : alighn polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" );  
+    fprintf( pErr, "\t-a     : toggle ANDing/ORing of miter outputs [default = %s]\n", fAndOuts? "ANDing": "ORing" );  
+    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandPSat( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int RetValue;
+    int c, clk;
+    int nAlgo;
+    int nPartSize;
+    int nConfPart;
+    int nConfTotal;
+    int fAlignPol;
+    int fSynthesize;
+    int fVerbose;
+
+    extern int Abc_NtkPartitionedSat( Abc_Ntk_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nAlgo       =        0;
+    nPartSize   =    10000;
+    nConfPart   =        0;
+    nConfTotal  =  1000000;
+    fAlignPol   =        1;
+    fSynthesize =        0;
+    fVerbose    =        1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "APCpsvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'A':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-A\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nAlgo = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nAlgo < 0 ) 
+                goto usage;
+            break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nPartSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nPartSize < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfTotal = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfTotal < 0 ) 
+                goto usage;
+            break;
+        case 'p':
+            fAlignPol ^= 1;
+            break;
+        case 's':
+            fSynthesize ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkLatchNum(pNtk) > 0 )
+    {
+        fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
+        return 0;
+    } 
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+        return 0;
+    }
+
+    clk = clock();
+    RetValue = Abc_NtkPartitionedSat( pNtk, nAlgo, nPartSize, nConfPart, nConfTotal, fAlignPol, fSynthesize, fVerbose );
+    // verify that the pattern is correct
+    if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
+    {
+        //int i;
+        //Abc_Obj_t * pObj;
+        int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtk->pModel );
+        if ( pSimInfo[0] != 1 )
+            printf( "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" );
+        free( pSimInfo );
+        /*
+        // print model
+        Abc_NtkForEachPi( pNtk, pObj, i )
+        {
+            printf( "%d", (int)(pNtk->pModel[i] > 0) );
+            if ( i == 70 )
+                break;
+        }
+        printf( "\n" );
+        */
+    }
+
+    if ( RetValue == -1 )
+        printf( "UNDECIDED      " );
+    else if ( RetValue == 0 )
+        printf( "SATISFIABLE    " );
+    else
+        printf( "UNSATISFIABLE  " );
+    //printf( "\n" );
+    PRT( "Time", clock() - clk );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: psat [-APC num] [-psvh]\n" );
+    fprintf( pErr, "\t         solves the combinational miter using partitioning\n" );
+    fprintf( pErr, "\t         (derives CNF from the current network and leave it unchanged)\n" );
+    fprintf( pErr, "\t         for multi-output miters, tries to prove that the AND of POs is always 0\n" );
+    fprintf( pErr, "\t         (if POs should be ORed instead of ANDed, use command \"orpos\")\n" );
+    fprintf( pErr, "\t-A num : partitioning algorithm [default = %d]\n", nAlgo );
+    fprintf( pErr, "\t         0 : no partitioning\n" );
+    fprintf( pErr, "\t         1 : partitioning by level\n" );
+    fprintf( pErr, "\t         2 : DFS post-order\n" );
+    fprintf( pErr, "\t         3 : DFS pre-order\n" );
+    fprintf( pErr, "\t         4 : bit-slicing\n" );
+    fprintf( pErr, "\t         partitions are ordered by level (high level first)\n" );
+    fprintf( pErr, "\t-P num : limit on the partition size [default = %d]\n", nPartSize );
+    fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfTotal );
+    fprintf( pErr, "\t-p     : align polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" );  
+    fprintf( pErr, "\t-s     : apply logic synthesis to each partition [default = %s]\n", fSynthesize? "yes": "no" );  
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -15347,11 +15515,13 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fRewrite;
     int fTransLoop;
     int fUsePudlak;
+    int fUseOther;
+    int fUseMiniSat;
     int fCheckInd;
     int fCheckKstep;
     int fVerbose;
 
-    extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fCheckKstep, int fVerbose );
+    extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -15363,11 +15533,13 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     fRewrite   = 0;
     fTransLoop = 1;
     fUsePudlak = 0;
+    fUseOther  = 0;
+    fUseMiniSat= 0;
     fCheckInd  = 0;
     fCheckKstep= 0;
     fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpikvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpomikvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -15402,6 +15574,12 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             fUsePudlak ^= 1;
             break;
+        case 'o':
+            fUseOther ^= 1;
+            break;
+        case 'm':
+            fUseMiniSat ^= 1;
+            break;
         case 'i':
             fCheckInd ^= 1;
             break;
@@ -15437,18 +15615,19 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
         return 0;
     }
-    Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fCheckKstep, fVerbose );
+    Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fUseOther, fUseMiniSat, fCheckInd, fCheckKstep, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: int [-CF num] [-rtpikvh]\n" );
+    fprintf( pErr, "usage: int [-CF num] [-rtpomikvh]\n" );
     fprintf( pErr, "\t         uses interpolation to prove the property\n" );
     fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit );
     fprintf( pErr, "\t-F num : the limit on number of frames to unroll [default = %d]\n", nFramesMax );
     fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
     fprintf( pErr, "\t-t     : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" );
-//    fprintf( pErr, "\t-p     : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" );
-    fprintf( pErr, "\t-p     : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", fUsePudlak? "yes": "no" );
+    fprintf( pErr, "\t-p     : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" );
+    fprintf( pErr, "\t-o     : toggle using optimized Pudlak's interpolation procedure [default = %s]\n", fUseOther? "yes": "no" );
+    fprintf( pErr, "\t-m     : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", fUseMiniSat? "yes": "no" );
     fprintf( pErr, "\t-i     : toggle inductive containment checking [default = %s]\n", fCheckInd? "yes": "no" );
     fprintf( pErr, "\t-k     : toggle simple and k-step induction [default = %s]\n", fCheckKstep? "k-step": "simple" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -16364,6 +16543,55 @@ usage:
     return 1;       /* error exit */
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Command procedure to read LUT libraries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8Check( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    int c;
+    extern int Nwk_ManCheck( void * p );
+
+    // set the defaults
+    Extra_UtilGetoptReset();
+    while ( (c = Extra_UtilGetopt(argc, argv, "h")) != EOF ) 
+    {
+        switch (c) 
+        {
+            case 'h':
+                goto usage;
+                break;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( argc != globalUtilOptind )
+    {
+        goto usage;
+    }
+
+    // set the new network
+    if ( pAbc->pAbc8Nwk == NULL )
+        printf( "Abc_CommandAbc8Check(): There is no mapped network.\n" );
+    else
+        Nwk_ManCheck( pAbc->pAbc8Nwk );
+    return 0;
+
+usage:
+    fprintf( stdout, "\nusage: *check [-h]\n");
+    fprintf( stdout, "\t          checks if the current mapped network has duplicated fanins\n" );  
+    fprintf( stdout, "\t-h      : print the command usage\n");
+    return 1;       /* error exit */
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index e32dbce0..03790c4b 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -954,7 +954,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
 
     // derive CNF
     pCnf = Cnf_Derive( pMan, 0 );
-    Cnf_DataTranformPolarity( pCnf );
+    Cnf_DataTranformPolarity( pCnf, 0 );
 /*
     // write the network for verification
     pManCnf = Cnf_ManRead();
@@ -983,7 +983,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose )
+int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fAlignPol, int fAndOuts, int fVerbose )
 {
     Aig_Man_t * pMan;
     int RetValue;//, clk = clock();
@@ -991,7 +991,32 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFli
     assert( Abc_NtkLatchNum(pNtk) == 0 );
     assert( Abc_NtkPoNum(pNtk) == 1 );
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
-    RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fFlipBits, fAndOuts, fVerbose ); 
+    RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fAlignPol, fAndOuts, fVerbose ); 
+    pNtk->pModel = pMan->pData, pMan->pData = NULL;
+    Aig_ManStop( pMan );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solves combinational miter using a SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkPartitionedSat( Abc_Ntk_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose )
+{
+    extern int Aig_ManPartitionedSat( Aig_Man_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose );
+    Aig_Man_t * pMan;
+    int RetValue;//, clk = clock();
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( Abc_NtkLatchNum(pNtk) == 0 );
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
+    RetValue = Aig_ManPartitionedSat( pMan, nAlgo, nPartSize, nConfPart, nConfTotal, fAlignPol, fSynthesize, fVerbose ); 
     pNtk->pModel = pMan->pData, pMan->pData = NULL;
     Aig_ManStop( pMan );
     return RetValue;
@@ -1270,7 +1295,7 @@ PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fCheckKstep, int fVerbose )
+int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose )
 {
     Aig_Man_t * pMan;
     int RetValue, Depth, clk = clock();
@@ -1282,7 +1307,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fR
         return -1;
     }
     assert( pMan->nRegs > 0 );
-    RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fCheckKstep, fVerbose, &Depth );
+    RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fUseOther, fUseMiniSat, fCheckInd, fCheckKstep, fVerbose, &Depth );
     if ( RetValue == 1 )
         printf( "Property proved.  " );
     else if ( RetValue == 0 )
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 430b7b63..f20c7cc8 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -658,6 +658,52 @@ static inline int Vec_IntRemove( Vec_Int_t * p, int Entry )
 
 /**Function*************************************************************
 
+  Synopsis    [Find entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntFindMax( Vec_Int_t * p )
+{
+    int i, Best;
+    if ( p->nSize == 0 )
+        return 0;
+    Best = p->pArray[0];
+    for ( i = 1; i < p->nSize; i++ )
+        if ( Best < p->pArray[i] )
+            Best = p->pArray[i];
+    return Best;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntFindMin( Vec_Int_t * p )
+{
+    int i, Best;
+    if ( p->nSize == 0 )
+        return 0;
+    Best = p->pArray[0];
+    for ( i = 1; i < p->nSize; i++ )
+        if ( Best > p->pArray[i] )
+            Best = p->pArray[i];
+    return Best;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Comparison procedure for two integers.]
 
   Description []