Version abc80721

19 files changed, 1240 insertions, 69 deletions

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 )