From 27f2429d764d057c2e8cdc882332aa1583cee028 Mon Sep 17 00:00:00 2001
From: MyskYko <yoyuohlhjl@yahoo.co.jp>
Date: Sun, 6 Apr 2025 15:46:02 -0700
Subject: [PATCH] update rrr

---
 src/aig/gia/gia.h                     |   2 +-
 src/aig/gia/giaRrr.cpp                |  11 +-
 src/base/abci/abc.c                   |  44 ++-
 src/opt/rrr/rrr.h                     |  38 ++-
 src/opt/rrr/rrrAndNetwork.h           | 138 ++++++++-
 src/opt/rrr/rrrBddMspfAnalyzer.h      |   2 +-
 src/opt/rrr/rrrLevelBasePartitioner.h | 293 +++++++++++++++++++
 src/opt/rrr/rrrOptimizer.h            | 388 +++++++++++++++++++++++---
 src/opt/rrr/rrrParameter.h            |  11 +-
 src/opt/rrr/rrrPartitioner.h          | 277 +++++++++---------
 src/opt/rrr/rrrSatSolver.h            |   2 +-
 src/opt/rrr/rrrScheduler.h            | 145 +++++-----
 src/opt/rrr/rrrSimulator.h            |  58 +++-
 src/opt/rrr/rrrUtils.h                | 242 +++++++++++++---
 14 files changed, 1337 insertions(+), 314 deletions(-)
 create mode 100644 src/opt/rrr/rrrLevelBasePartitioner.h

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index b950da4be..273c530ec 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1808,7 +1808,7 @@ extern Gia_Man_t *         Gia_ManTransductionBdd( Gia_Man_t * pGia, int nType,
 extern Gia_Man_t *         Gia_ManTransductionTt( Gia_Man_t * pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t * pExdc, int fNewLine, int nVerbose );
 
 /*=== giaRrr.cpp ===========================================================*/
-extern Gia_Man_t *         Gia_ManRrr( Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int nSchedulerVerbose, int nPartitionerVerbose, int nOptimizerVerbose, int nAnalyzerVerbose, int nSimulatorVerbose, int nSatSolverVerbose, int fUseBddCspf, int fUseBddMspf, int nConflictLimit, int nSortType, int nOptimizerFlow, int nSchedulerFlow, int nDistance, int nRestarts, int nThreads, int nWindowSize, int fDeterministic );
+extern Gia_Man_t *         Gia_ManRrr( Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int nSchedulerVerbose, int nPartitionerVerbose, int nOptimizerVerbose, int nAnalyzerVerbose, int nSimulatorVerbose, int nSatSolverVerbose, int fUseBddCspf, int fUseBddMspf, int nConflictLimit, int nSortType, int nOptimizerFlow, int nSchedulerFlow, int nPartitionType, int nDistance, int nJobs, int nThreads, int nPartitionSize, int nPartitionSizeMin, int fDeterministic, int nParallelPartitions, int fOptOnInsert, int fGreedy );
 
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
diff --git a/src/aig/gia/giaRrr.cpp b/src/aig/gia/giaRrr.cpp
index df3b91e60..1eccd4dc2 100644
--- a/src/aig/gia/giaRrr.cpp
+++ b/src/aig/gia/giaRrr.cpp
@@ -5,7 +5,7 @@
 
 ABC_NAMESPACE_IMPL_START
 
-Gia_Man_t *Gia_ManRrr(Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int nSchedulerVerbose, int nPartitionerVerbose, int nOptimizerVerbose, int nAnalyzerVerbose, int nSimulatorVerbose, int nSatSolverVerbose, int fUseBddCspf, int fUseBddMspf, int nConflictLimit, int nSortType, int nOptimizerFlow, int nSchedulerFlow, int nDistance, int nRestarts, int nThreads, int nWindowSize, int fDeterministic) {
+Gia_Man_t *Gia_ManRrr(Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int nSchedulerVerbose, int nPartitionerVerbose, int nOptimizerVerbose, int nAnalyzerVerbose, int nSimulatorVerbose, int nSatSolverVerbose, int fUseBddCspf, int fUseBddMspf, int nConflictLimit, int nSortType, int nOptimizerFlow, int nSchedulerFlow, int nPartitionType, int nDistance, int nJobs, int nThreads, int nPartitionSize, int nPartitionSizeMin, int fDeterministic, int nParallelPartitions, int fOptOnInsert, int fGreedy) {
   rrr::AndNetwork ntk;
   ntk.Read(pGia, rrr::GiaReader<rrr::AndNetwork>);
   rrr::Parameter Par;
@@ -24,11 +24,16 @@ Gia_Man_t *Gia_ManRrr(Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int
   Par.nSortType = nSortType;
   Par.nOptimizerFlow = nOptimizerFlow;
   Par.nSchedulerFlow = nSchedulerFlow;
+  Par.nPartitionType = nPartitionType;
   Par.nDistance = nDistance;
-  Par.nRestarts = nRestarts;
+  Par.nJobs = nJobs;
   Par.nThreads = nThreads;
-  Par.nWindowSize = nWindowSize;
+  Par.nPartitionSize = nPartitionSize;
+  Par.nPartitionSizeMin = nPartitionSizeMin;
   Par.fDeterministic = fDeterministic;
+  Par.nParallelPartitions = nParallelPartitions;
+  Par.fOptOnInsert = fOptOnInsert;
+  Par.fGreedy = fGreedy;
   rrr::Perform(&ntk, &Par);
   Gia_Man_t *pNew = rrr::CreateGia(&ntk);
   return pNew;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4bf22bd88..2875b3a1b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -45457,9 +45457,9 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t *pNew;
     int c;
-    int iSeed = 0, nWords = 10, nTimeout = 0, nSchedulerVerbose = 1, nPartitionerVerbose = 0, nOptimizerVerbose = 0, nAnalyzerVerbose = 0, nSimulatorVerbose = 0, nSatSolverVerbose = 0, fUseBddCspf = 0, fUseBddMspf = 0, nConflictLimit = 0, nSortType = 12, nOptimizerFlow = 0, nSchedulerFlow = 0, nDistance = 0, nRestarts = 0, nThreads = 1, nWindowSize = 0, fDeterministic = 1;
+    int iSeed = 0, nWords = 10, nTimeout = 0, nSchedulerVerbose = 1, nPartitionerVerbose = 0, nOptimizerVerbose = 0, nAnalyzerVerbose = 0, nSimulatorVerbose = 0, nSatSolverVerbose = 0, fUseBddCspf = 0, fUseBddMspf = 0, nConflictLimit = 0, nSortType = -1, nOptimizerFlow = 0, nSchedulerFlow = 0, nPartitionType = 0, nDistance = 0, nJobs = 1, nThreads = 1, nPartitionSize = 0, nPartitionSizeMin = 0, fDeterministic = 1, nParallelPartitions = 1, fOptOnInsert = 0, fGreedy = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "XYNJKDRWTCGVPOAQSabdh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "XYZNJKLBDRWTCGVPOAQSabdegh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -45471,8 +45471,12 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
             nSchedulerFlow = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             break;
+        case 'Z':
+            nPartitionType = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
         case 'N':
-            nRestarts = atoi(argv[globalUtilOptind]);
+            nJobs = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             break;
         case 'J':
@@ -45480,7 +45484,15 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
             globalUtilOptind++;
             break;
         case 'K':
-            nWindowSize = atoi(argv[globalUtilOptind]);
+            nPartitionSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'L':
+            nPartitionSizeMin = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'B':
+            nParallelPartitions = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             break;
         case 'D':
@@ -45540,6 +45552,12 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             fDeterministic ^= 1;
             break;
+        case 'e':
+            fOptOnInsert ^= 1;
+            break;
+        case 'g':
+            fGreedy ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -45558,32 +45576,38 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     
-    pNew = Gia_ManRrr( pAbc->pGia, iSeed, nWords, nTimeout, nSchedulerVerbose, nPartitionerVerbose, nOptimizerVerbose, nAnalyzerVerbose, nSimulatorVerbose, nSatSolverVerbose, fUseBddCspf, fUseBddMspf, nConflictLimit, nSortType, nOptimizerFlow, nSchedulerFlow, nDistance, nRestarts, nThreads, nWindowSize, fDeterministic );
+    pNew = Gia_ManRrr( pAbc->pGia, iSeed, nWords, nTimeout, nSchedulerVerbose, nPartitionerVerbose, nOptimizerVerbose, nAnalyzerVerbose, nSimulatorVerbose, nSatSolverVerbose, fUseBddCspf, fUseBddMspf, nConflictLimit, nSortType, nOptimizerFlow, nSchedulerFlow, nPartitionType, nDistance, nJobs, nThreads, nPartitionSize, nPartitionSizeMin, fDeterministic, nParallelPartitions, fOptOnInsert, fGreedy );
 
     Abc_FrameUpdateGia( pAbc, pNew );
     
     return 0;
 
 usage:
-      Abc_Print( -2, "usage: rrr [-XYNJKDRWTCGVPOAQS num] [-abdh]\n" );
+      Abc_Print( -2, "usage: rrr [-XYZNJKLBDRWTCGVPOAQS num] [-abdegh]\n" );
       Abc_Print( -2, "\t        perform optimization\n" );
       Abc_Print( -2, "\t-X num : method [default = %d]\n", nOptimizerFlow );
       Abc_Print( -2, "\t                0: single-add resub\n" );
       Abc_Print( -2, "\t                1: multi-add resub\n" );
       Abc_Print( -2, "\t                2: repeat 0 and 1\n" );
+      Abc_Print( -2, "\t                3: random one meaningful resub\n" );
       Abc_Print( -2, "\t-Y num : flow [default = %d]\n", nSchedulerFlow );
       Abc_Print( -2, "\t                0: apply method once\n" );
       Abc_Print( -2, "\t                1: iterate like transtoch\n" );
       Abc_Print( -2, "\t                2: iterate like deepsyn\n" );
-      Abc_Print( -2, "\t-N num : number of restarts or windows [default = %d]\n", nRestarts );
+      Abc_Print( -2, "\t-Z num : partition [default = %d]\n", nPartitionType );
+      Abc_Print( -2, "\t                0: distance base\n" );
+      Abc_Print( -2, "\t                1: level base\n" );
+      Abc_Print( -2, "\t-N num : number of jobs to create by restarting or partitioning [default = %d]\n", nJobs );
       Abc_Print( -2, "\t-J num : number of threads [default = %d]\n", nThreads );
-      Abc_Print( -2, "\t-K num : window size (0 = no partitioning) [default = %d]\n", nWindowSize );
+      Abc_Print( -2, "\t-K num : partition size (0 = no partitioning) [default = %d]\n", nPartitionSize );
+      Abc_Print( -2, "\t-K num : minimum partition size [default = %d]\n", nPartitionSizeMin );
+      Abc_Print( -2, "\t-B num : max number of partitions in parallel [default = %d]\n", nParallelPartitions );
       Abc_Print( -2, "\t-D num : distance between nodes (0 = no limit) [default = %d]\n", nDistance );
       Abc_Print( -2, "\t-R num : random number generator seed [default = %d]\n", iSeed );
       Abc_Print( -2, "\t-W num : number of simulation words [default = %d]\n", nWords );
       Abc_Print( -2, "\t-T num : timeout in seconds (0 = no timeout) [default = %d]\n", nTimeout );
       Abc_Print( -2, "\t-C num : conflict limit (0 = no limit) [default = %d]\n", nConflictLimit );
-      Abc_Print( -2, "\t-G num : fanin cost function [default = %d]\n", nSortType );
+      Abc_Print( -2, "\t-G num : fanin cost function (-1 = random) [default = %d]\n", nSortType );
       Abc_Print( -2, "\t-V num : scheduler verbosity level [default = %d]\n", nSchedulerVerbose );
       Abc_Print( -2, "\t-P num : partitioner verbosity level [default = %d]\n", nPartitionerVerbose );
       Abc_Print( -2, "\t-O num : optimizer verbosity level [default = %d]\n", nOptimizerVerbose );
@@ -45593,6 +45617,8 @@ usage:
       Abc_Print( -2, "\t-a     : use BDD-based analyzer (CSPF) [default = %s]\n", fUseBddCspf? "yes": "no" );
       Abc_Print( -2, "\t-b     : use BDD-based analyzer (MSPF) [default = %s]\n", fUseBddMspf? "yes": "no" );
       Abc_Print( -2, "\t-d     : ensure deterministic execution [default = %s]\n", fDeterministic? "yes": "no" );
+      Abc_Print( -2, "\t-e     : apply c2rs; dc2 after importing changes of partitions [default = %s]\n", fOptOnInsert? "yes": "no" );
+      Abc_Print( -2, "\t-g     : discard changes that increased the cost [default = %s]\n", fGreedy? "yes": "no" );
       Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
diff --git a/src/opt/rrr/rrr.h b/src/opt/rrr/rrr.h
index f737b7ffc..c08d562ae 100644
--- a/src/opt/rrr/rrr.h
+++ b/src/opt/rrr/rrr.h
@@ -8,6 +8,8 @@
 #include "rrrAnalyzer.h"
 #include "rrrSatSolver.h"
 #include "rrrSimulator.h"
+#include "rrrPartitioner.h"
+#include "rrrLevelBasePartitioner.h"
 
 ABC_NAMESPACE_CXX_HEADER_START
 
@@ -16,15 +18,33 @@ namespace rrr {
   template <typename Ntk>
   void Perform(Ntk *pNtk, Parameter const *pPar) {
     assert(!pPar->fUseBddCspf || !pPar->fUseBddMspf);
-    if(pPar->fUseBddCspf) {
-      Scheduler<Ntk, rrr::Optimizer<Ntk, rrr::BddAnalyzer<Ntk>>> sch(pNtk, pPar);
-      sch.Run();
-    } else if(pPar->fUseBddMspf) {
-      Scheduler<Ntk, rrr::Optimizer<Ntk, rrr::BddMspfAnalyzer<Ntk>>> sch(pNtk, pPar);
-      sch.Run();
-    } else {
-      Scheduler<Ntk, rrr::Optimizer<Ntk, rrr::Analyzer<Ntk, rrr::Simulator<Ntk>, rrr::SatSolver<Ntk>>>> sch(pNtk, pPar);
-      sch.Run();
+    switch(pPar->nPartitionType) {
+    case 0:
+      if(pPar->fUseBddCspf) {
+        Scheduler<Ntk, Optimizer<Ntk, BddAnalyzer<Ntk>>, Partitioner<Ntk>> sch(pNtk, pPar);
+        sch.Run();
+      } else if(pPar->fUseBddMspf) {
+        Scheduler<Ntk, Optimizer<Ntk, BddMspfAnalyzer<Ntk>>, Partitioner<Ntk>> sch(pNtk, pPar);
+        sch.Run();
+      } else {
+        Scheduler<Ntk, Optimizer<Ntk, Analyzer<Ntk, Simulator<Ntk>, SatSolver<Ntk>>>, Partitioner<Ntk>> sch(pNtk, pPar);
+        sch.Run();
+      }
+      break;
+    case 1:
+      if(pPar->fUseBddCspf) {
+        Scheduler<Ntk, Optimizer<Ntk, BddAnalyzer<Ntk>>, LevelBasePartitioner<Ntk>> sch(pNtk, pPar);
+        sch.Run();
+      } else if(pPar->fUseBddMspf) {
+        Scheduler<Ntk, Optimizer<Ntk, BddMspfAnalyzer<Ntk>>, LevelBasePartitioner<Ntk>> sch(pNtk, pPar);
+        sch.Run();
+      } else {
+        Scheduler<Ntk, Optimizer<Ntk, Analyzer<Ntk, Simulator<Ntk>, SatSolver<Ntk>>>, LevelBasePartitioner<Ntk>> sch(pNtk, pPar);
+        sch.Run();
+      }
+      break;
+    default:
+      assert(0);
     }
   }
   
diff --git a/src/opt/rrr/rrrAndNetwork.h b/src/opt/rrr/rrrAndNetwork.h
index 00afd2386..f39bbdc4d 100644
--- a/src/opt/rrr/rrrAndNetwork.h
+++ b/src/opt/rrr/rrrAndNetwork.h
@@ -54,7 +54,7 @@ namespace rrr {
     void SortInts(itr it);
     unsigned StartTraversal(int n = 1);
     void EndTraversal();
-    void ForEachTfiRec(int id, std::function<void(int)> const &f);
+    void ForEachTfiRec(int id, std::function<void(int)> const &func);
     void TakenAction(Action const &action) const;
 
   public:
@@ -102,13 +102,15 @@ namespace rrr {
     int  FindFanin(int id, int fi) const;
     bool IsReconvergent(int id);
     std::vector<int> GetNeighbors(int id, bool fPis, int nHops);
-    template <template <typename...> typename Container, typename ... Ts, template <typename...> typename Container2, typename ... Ts2>
+    template <template <typename...> typename Container, typename... Ts, template <typename...> typename Container2, typename... Ts2>
     bool IsReachable(Container<Ts...> const &srcs, Container2<Ts2...> const &dsts);
-    template <template <typename...> typename Container, typename ... Ts, template <typename...> typename Container2, typename ... Ts2>
+    template <template <typename...> typename Container, typename... Ts, template <typename...> typename Container2, typename... Ts2>
     std::vector<int> GetInners(Container<Ts...> const &srcs, Container2<Ts2...> const &dsts);
+    std::set<int> GetExtendedFanins(int id);
 
     // network traversal
     void ForEachPi(std::function<void(int)> const &func) const;
+    void ForEachPiIdx(std::function<void(int, int)> const &func) const; // func(index, id)
     void ForEachInt(std::function<void(int)> const &func) const;
     void ForEachIntReverse(std::function<void(int)> const &func) const;
     void ForEachPiInt(std::function<void(int)> const &func) const;
@@ -124,18 +126,21 @@ namespace rrr {
     template <typename Func>
     void ForEachFanoutRidx(int id, bool fPos, Func const &func) const; // func(fo[, c], index of id in fanin list of fo)
     void ForEachTfi(int id, bool fPis, std::function<void(int)> const &func);
-    template <template <typename...> typename Container, typename ... Ts>
+    template <template <typename...> typename Container, typename... Ts>
     void ForEachTfiEnd(int id, Container<Ts...> const &ends, std::function<void(int)> const &func);
+    void ForEachTfiUpdate(int id, bool fPis, std::function<bool(int)> const &func);
+    template <template <typename...> typename Container, typename... Ts>
+    void ForEachTfisUpdate(Container<Ts...> const &ids, bool fPis, std::function<bool(int)> const &func);
     void ForEachTfo(int id, bool fPos, std::function<void(int)> const &func);
     void ForEachTfoReverse(int id, bool fPos, std::function<void(int)> const &func);
     void ForEachTfoUpdate(int id, bool fPos, std::function<bool(int)> const &func);
-    template <template <typename...> typename Container, typename ... Ts>
+    template <template <typename...> typename Container, typename... Ts>
     void ForEachTfos(Container<Ts...> const &ids, bool fPos, std::function<void(int)> const &func);
-    template <template <typename...> typename Container, typename ... Ts>
+    template <template <typename...> typename Container, typename... Ts>
     void ForEachTfosUpdate(Container<Ts...> const &ids, bool fPos, std::function<bool(int)> const &func);
 
     // extraction
-    template <template <typename...> typename Container, typename ... Ts>
+    template <template <typename...> typename Container, typename... Ts>
     AndNetwork *Extract(Container<Ts...> const &ids, std::vector<int> const &vInputs, std::vector<int> const &vOutputs);
 
     // actions
@@ -217,7 +222,7 @@ namespace rrr {
       ForEachTfiRec(fi, func);
     }
   }
-  
+
   inline void AndNetwork::TakenAction(Action const &action) const {
     for(Callback const &callback: vCallbacks) {
       callback(action);
@@ -552,7 +557,7 @@ namespace rrr {
     return v;
   }
 
-  template <template <typename...> typename Container, typename ... Ts, template <typename...> typename Container2, typename ... Ts2>
+  template <template <typename...> typename Container, typename... Ts, template <typename...> typename Container2, typename... Ts2>
   inline bool AndNetwork::IsReachable(Container<Ts...> const &srcs, Container2<Ts2...> const &dsts) {
     if(srcs.empty() || dsts.empty()) {
       return false;
@@ -607,7 +612,7 @@ namespace rrr {
     return false;
   }
 
-  template <template <typename...> typename Container, typename ... Ts, template <typename...> typename Container2, typename ... Ts2>
+  template <template <typename...> typename Container, typename... Ts, template <typename...> typename Container2, typename... Ts2>
   inline std::vector<int> AndNetwork::GetInners(Container<Ts...> const &srcs, Container2<Ts2...> const &dsts) {
     // this includes sources and destinations that are connected
     if(srcs.empty() || dsts.empty()) {
@@ -665,6 +670,43 @@ namespace rrr {
     return vInners;
   }
 
+  inline std::set<int> AndNetwork::GetExtendedFanins(int id) {
+    // go to the root of trivially collapsable nodes
+    while(GetNumFanouts(id) == 1) {
+      int id_new = -1;
+      ForEachFanout(id, false, [&](int fo, bool c) {
+        if(!c) {
+          id_new = fo;
+        }
+      });
+      if(id_new != -1) {
+        id = id_new;
+      } else {
+        break;
+      }
+    }
+    // emulate trivial collapse
+    std::vector<int> vFaninEdges = vvFaninEdges[id];
+    for(int idx = 0; idx < int_size(vFaninEdges);) {
+      int fi_edge = vFaninEdges[idx];
+      int fi = Edge2Node(fi_edge);
+      bool c = EdgeIsCompl(fi_edge);
+      if(!IsPi(fi) && !c && vRefs[fi] == 1) {
+        std::vector<int>::iterator it = vFaninEdges.begin() + idx;
+        it = vFaninEdges.erase(it);
+        vFaninEdges.insert(it, vvFaninEdges[fi].begin(), vvFaninEdges[fi].end());
+      } else {
+        idx++;
+      }
+    }
+    // create set
+    std::set<int> sFanins;
+    for(int fi_edge: vFaninEdges) {
+      sFanins.insert(Edge2Node(fi_edge));
+    }
+    return sFanins;
+  }
+
   /* }}} */
 
   /* {{{ Network traversal */
@@ -674,7 +716,13 @@ namespace rrr {
       func(pi);
     }
   }
-  
+
+  inline void AndNetwork::ForEachPiIdx(std::function<void(int, int)> const &func) const {
+    for(int idx = 0; idx < GetNumPis(); idx++) {
+      func(idx, GetPi(idx));
+    }
+  }
+
   inline void AndNetwork::ForEachInt(std::function<void(int)> const &func) const {
     for(int id: lInts) {
       func(id);
@@ -834,7 +882,7 @@ namespace rrr {
     EndTraversal();
   }
 
-  template <template <typename...> typename Container, typename ... Ts>
+  template <template <typename...> typename Container, typename... Ts>
   inline void AndNetwork::ForEachTfiEnd(int id, Container<Ts...> const &ends, std::function<void(int)> const &func) {
     // this does not include id itself
     StartTraversal();
@@ -845,6 +893,66 @@ namespace rrr {
     EndTraversal();
   }
 
+  inline void AndNetwork::ForEachTfiUpdate(int id, bool fPis, std::function<bool(int)> const &func) {
+    if(GetNumFanins(id) == 0) {
+      return;
+    }
+    StartTraversal();
+    for(int fi_edge: vvFaninEdges[id]) {
+      vTrav[Edge2Node(fi_edge)] = iTrav;
+    }
+    critr it = std::find(lInts.rbegin(), lInts.rend(), id);
+    assert(it != lInts.rend());
+    it++;
+    for(; it != lInts.rend(); it++) {
+      if(vTrav[*it] == iTrav) {
+        if(func(*it)) {
+          for(int fi_edge: vvFaninEdges[*it]) {
+            vTrav[Edge2Node(fi_edge)] = iTrav;
+          }
+        }
+      }
+    }
+    if(fPis) {
+      for(int pi: vPis) {
+        if(vTrav[pi] == iTrav) {
+          func(pi);
+        }
+      }
+    }
+    EndTraversal();
+  }
+
+  template <template <typename...> typename Container, typename... Ts>
+  inline void AndNetwork::ForEachTfisUpdate(Container<Ts...> const &ids, bool fPis, std::function<bool(int)> const &func) {
+    // this includes ids themselves
+    StartTraversal();
+    for(int id: ids) {
+      vTrav[id] = iTrav;
+    }
+    critr it = lInts.rbegin();
+    while(vTrav[*it] != iTrav && it != lInts.rend()) {
+      it++;
+    }
+    for(; it != lInts.rend(); it++) {
+      if(vTrav[*it] == iTrav) {
+        if(func(*it)) {
+          for(int fi_edge: vvFaninEdges[*it]) {
+            vTrav[Edge2Node(fi_edge)] = iTrav;
+          }
+        }
+      }
+    }
+    if(fPis) {
+      for(int pi: vPis) {
+        if(vTrav[pi] == iTrav) {
+          func(pi);
+        }
+      }
+    }
+    EndTraversal();
+  }
+
   inline void AndNetwork::ForEachTfo(int id, bool fPos, std::function<void(int)> const &func) {
     // this does not include id itself
     if(vRefs[id] == 0) {
@@ -951,7 +1059,7 @@ namespace rrr {
     EndTraversal();
   }
 
-  template <template <typename...> typename Container, typename ... Ts>
+  template <template <typename...> typename Container, typename... Ts>
   inline void AndNetwork::ForEachTfos(Container<Ts...> const &ids, bool fPos, std::function<void(int)> const &func) {
     // this includes ids themselves
     StartTraversal();
@@ -986,7 +1094,7 @@ namespace rrr {
     EndTraversal();
   }
   
-  template <template <typename...> typename Container, typename ... Ts>
+  template <template <typename...> typename Container, typename... Ts>
   inline void AndNetwork::ForEachTfosUpdate(Container<Ts...> const &ids, bool fPos, std::function<bool(int)> const &func) {
     // this includes ids themselves
     StartTraversal();
@@ -1033,7 +1141,7 @@ namespace rrr {
 
   /* {{{ Extraction */
 
-  template <template <typename...> typename Container, typename ... Ts>
+  template <template <typename...> typename Container, typename... Ts>
   AndNetwork *AndNetwork::Extract(Container<Ts...> const &ids, std::vector<int> const &vInputs, std::vector<int> const &vOutputs) {
     AndNetwork *pNtk = new AndNetwork;
     pNtk->Reserve(int_size(vInputs) + int_size(ids) + int_size(vOutputs));
diff --git a/src/opt/rrr/rrrBddMspfAnalyzer.h b/src/opt/rrr/rrrBddMspfAnalyzer.h
index 1634a5fd6..400fd9e6c 100644
--- a/src/opt/rrr/rrrBddMspfAnalyzer.h
+++ b/src/opt/rrr/rrrBddMspfAnalyzer.h
@@ -609,7 +609,7 @@ namespace rrr {
       NewBdd::Param Par;
       Par.nObjsMaxLog = 25;
       Par.nCacheMaxLog = 20;
-      Par.fCountOnes = true;
+      Par.fCountOnes = false;
       Par.nGbc = 1;
       Par.nReo = 4000;
       pBdd = new NewBdd::Man(pNtk->GetNumPis(), Par);
diff --git a/src/opt/rrr/rrrLevelBasePartitioner.h b/src/opt/rrr/rrrLevelBasePartitioner.h
new file mode 100644
index 000000000..5225cc5a7
--- /dev/null
+++ b/src/opt/rrr/rrrLevelBasePartitioner.h
@@ -0,0 +1,293 @@
+#pragma once
+
+#include <utility>
+#include <map>
+#include <tuple>
+#include <random>
+
+#include "rrrParameter.h"
+#include "rrrUtils.h"
+
+ABC_NAMESPACE_CXX_HEADER_START
+
+namespace rrr {
+
+  template <typename Ntk>
+  class LevelBasePartitioner {
+  private:
+    // pointer to network
+    Ntk *pNtk;
+
+    // parameters
+    int nVerbose;
+    int nPartitionSize;
+    int nPartitionSizeMin;
+    std::string strVerbosePrefix;
+
+    // data
+    int nMaxLevel;
+    std::vector<int> vLevels;
+    std::map<Ntk *, std::tuple<std::set<int>, std::vector<int>, std::vector<bool>, std::vector<int>>> mSubNtk2Io;
+    std::set<int> sBlocked;
+    std::vector<bool> vFailed;
+
+    // print
+    template<typename... Args>
+    void Print(int nVerboseLevel, Args... args);
+    
+    // subroutines
+    void ComputeLevel();
+    std::vector<int> GetIOI(int id, int nLevels);
+    Ntk *ExtractIOI(int id);
+    
+  public:
+    // constructors
+    LevelBasePartitioner(Parameter const *pPar);
+    void UpdateNetwork(Ntk *pNtk);
+
+    // APIs
+    Ntk *Extract(int iSeed);
+    void Insert(Ntk *pSubNtk);
+  };
+
+  /* {{{ Print */
+  
+  template <typename Ntk>
+  template <typename... Args>
+  inline void LevelBasePartitioner<Ntk>::Print(int nVerboseLevel, Args... args) {
+    if(nVerbose > nVerboseLevel) {
+      std::cout << strVerbosePrefix;
+      for(int i = 0; i < nVerboseLevel; i++) {
+        std::cout << "\t";
+      }
+      PrintNext(std::cout, args...);
+      std::cout << std::endl;
+    }
+  }
+
+  /* }}} */
+
+  /* {{{ Subroutines */
+
+  template <typename Ntk>
+  void LevelBasePartitioner<Ntk>::ComputeLevel() {
+    nMaxLevel = 0;
+    vLevels.clear();
+    vLevels.resize(pNtk->GetNumNodes());
+    pNtk->ForEachInt([&](int id) {
+      pNtk->ForEachFanin(id, [&](int fi) {
+        if(vLevels[id] < vLevels[fi]) {
+          vLevels[id] = vLevels[fi];
+        }
+      });
+      vLevels[id] += 1;
+      if(nMaxLevel < vLevels[id]) {
+        nMaxLevel = vLevels[id];
+      }
+    });
+  }
+
+  template <typename Ntk>
+  std::vector<int> LevelBasePartitioner<Ntk>::GetIOI(int id, int nLevels) {
+    std::vector<int> vNodes, vNodes2;
+    vNodes.push_back(id);
+    pNtk->ForEachTfiUpdate(id, false, [&](int fi) {
+      if(vLevels[fi] < vLevels[id] - nLevels) {
+        return false;
+      }
+      vNodes.push_back(fi);
+      return true;
+    });
+    pNtk->ForEachTfosUpdate(vNodes, false, [&](int fo) {
+      if(vLevels[fo] > vLevels[id] + nLevels) {
+        return false;
+      }
+      vNodes2.push_back(fo);
+      return true;
+    });
+    vNodes.clear();
+    pNtk->ForEachTfisUpdate(vNodes2, false, [&](int fi) {
+      if(vLevels[fi] < vLevels[id] - nLevels) {
+        return false;
+      }
+      vNodes.push_back(fi);
+      return true;
+    });
+    return vNodes;
+  }
+
+  template <typename Ntk>
+  Ntk *LevelBasePartitioner<Ntk>::ExtractIOI(int id) {
+    // collect IOI nodes
+    assert(!sBlocked.count(id));
+    int nLevels = 1;
+    std::vector<int> vNodes = GetIOI(id, nLevels);
+    Print(1, "level", NS(), nLevels, ":", "size =", int_size(vNodes));
+    std::vector<int> vNodesNew = GetIOI(id, nLevels + 1);
+    Print(1, "level", NS(), nLevels + 1, ":", "size =", int_size(vNodesNew));
+    // gradually increase level until it hits partition size limit
+    while(int_size(vNodesNew) < nPartitionSize) {
+      if(vLevels[id] - nLevels < 1 && vLevels[id] + nLevels >= nMaxLevel) { // already maximum
+        break;
+      }
+      vNodes = vNodesNew;
+      nLevels++;
+      vNodesNew = GetIOI(id, nLevels + 1);
+      Print(1, "level", NS(), nLevels + 1, ":", "size =", int_size(vNodesNew));
+    }
+    std::set<int> sNodes(vNodes.begin(), vNodes.end());
+    // remove nodes that are already blocked
+    for(std::set<int>::iterator it = sNodes.begin(); it != sNodes.end();) {
+      if(sBlocked.count(*it)) {
+        it = sNodes.erase(it);
+      } else {
+        it++;
+      }
+    }
+    Print(1, "checking:", "size =", int_size(sNodes));
+    // get partition IO
+    std::set<int> sInputs, sOutputs;
+    for(int id: sNodes) {
+      pNtk->ForEachFanin(id, [&](int fi) {
+        if(!sNodes.count(fi)) {
+          sInputs.insert(fi);
+        }
+      });
+      bool fOutput = false;
+      pNtk->ForEachFanout(id, true, [&](int fo) {
+        if(!sNodes.count(fo)) {
+          fOutput = true;
+        }
+      });
+      if(fOutput) {
+        sOutputs.insert(id);
+      }
+    }
+    Print(2, "nodes:", sNodes);
+    Print(2, "inputs:", sInputs);
+    Print(2, "outputs:", sOutputs);
+    if(int_size(sNodes) < nPartitionSizeMin) {
+      return NULL;
+    }
+    // check loops and just give up if any
+    std::set<int> sFanouts;
+    for(int id: sOutputs) {
+      pNtk->ForEachFanout(id, false, [&](int fo) {
+        if(!sNodes.count(fo)) {
+          sFanouts.insert(fo);
+        }
+      });
+    }
+    if(pNtk->IsReachable(sFanouts, sInputs)) {
+      return NULL;
+    }
+    for(auto const &entry: mSubNtk2Io) {
+      if(!pNtk->IsReachable(sOutputs, std::get<1>(entry.second))) {
+        continue;
+      }
+      if(!pNtk->IsReachable(std::get<3>(entry.second), sInputs)) {
+        continue;
+      }
+      return NULL;
+    }
+    // extract by inputs, internals, and outputs (no checks needed in ntk side)
+    std::vector<int> vInputs(sInputs.begin(), sInputs.end());
+    std::vector<int> vOutputs(sOutputs.begin(), sOutputs.end());
+    Ntk *pSubNtk = pNtk->Extract(sNodes, vInputs, vOutputs);
+    // return subntk to be modified, while remember IOs
+    for(int id: sNodes) {
+      sBlocked.insert(id);
+    }
+    mSubNtk2Io.emplace(pSubNtk, std::make_tuple(std::move(sNodes), std::move(vInputs), std::vector<bool>(vInputs.size()), std::move(vOutputs)));
+    return pSubNtk;
+  }
+  
+  /* }}} */
+
+  /* {{{ Constructors */
+  
+  template <typename Ntk>
+  LevelBasePartitioner<Ntk>::LevelBasePartitioner(Parameter const *pPar) :
+    nVerbose(pPar->nPartitionerVerbose),
+    nPartitionSize(pPar->nPartitionSize),
+    nPartitionSizeMin(pPar->nPartitionSizeMin) {
+  }
+
+  template <typename Ntk>
+  void LevelBasePartitioner<Ntk>::UpdateNetwork(Ntk *pNtk_) {
+    pNtk = pNtk_;
+    assert(mSubNtk2Io.empty());
+    assert(sBlocked.empty());
+    vFailed.clear();
+    vLevels.clear();
+  }
+
+  /* }}} */
+
+  /* {{{ APIs */
+  
+  template <typename Ntk>
+  Ntk *LevelBasePartitioner<Ntk>::Extract(int iSeed) {
+    // pick a center node from candidates that do not belong to any other ongoing partitions
+    vFailed.resize(pNtk->GetNumNodes());
+    if(vLevels.empty()) {
+      ComputeLevel();
+    }
+    std::mt19937 rng(iSeed);
+    std::vector<int> vInts = pNtk->GetInts();
+    std::shuffle(vInts.begin(), vInts.end(), rng);
+    for(int i = 0; i < int_size(vInts); i++) {
+      int id = vInts[i];
+      if(vFailed[id]) {
+        continue;
+      }
+      if(!sBlocked.count(id)) {
+        Print(0, "try partitioning with node", id, "(", i, "/", int_size(vInts), ")");
+        Ntk *pSubNtk = ExtractIOI(id);
+        if(pSubNtk) {
+          return pSubNtk;
+        }
+      }
+      vFailed[id] = true;
+    }
+    return NULL;
+  }
+
+  template <typename Ntk>
+  void LevelBasePartitioner<Ntk>::Insert(Ntk *pSubNtk) {
+    for(int i: std::get<0>(mSubNtk2Io[pSubNtk])) {
+      sBlocked.erase(i);
+    }
+    std::pair<std::vector<int>, std::vector<bool>> vNewSignals = pNtk->Insert(pSubNtk, std::get<1>(mSubNtk2Io[pSubNtk]), std::get<2>(mSubNtk2Io[pSubNtk]), std::get<3>(mSubNtk2Io[pSubNtk]));
+    std::vector<int> &vOldOutputs = std::get<3>(mSubNtk2Io[pSubNtk]);
+    std::vector<int> &vNewOutputs = vNewSignals.first;
+    std::vector<bool> &vNewCompls = vNewSignals.second;
+    // need to remap updated outputs that are used as inputs in other partitions
+    std::map<int, int> mOutput2Idx;
+    for(int idx = 0; idx < int_size(vOldOutputs); idx++) {
+      mOutput2Idx[vOldOutputs[idx]] = idx;
+    }
+    for(auto &entry: mSubNtk2Io) {
+      if(entry.first != pSubNtk) {
+        std::vector<int> &vInputs = std::get<1>(entry.second);
+        std::vector<bool> &vCompls = std::get<2>(entry.second);
+        for(int i = 0; i < int_size(vInputs); i++) {
+          if(mOutput2Idx.count(vInputs[i])) {
+            int idx = mOutput2Idx[vInputs[i]];
+            vInputs[i] = vNewOutputs[idx];
+            vCompls[i] = vCompls[i] ^ vNewCompls[idx];
+          }
+        }
+      }
+    }
+    delete pSubNtk;
+    mSubNtk2Io.erase(pSubNtk);
+    vFailed.clear(); // clear, there isn't really a way to track
+    vLevels.clear();
+  }
+
+  /* }}} */
+  
+}
+
+ABC_NAMESPACE_CXX_HEADER_END
diff --git a/src/opt/rrr/rrrOptimizer.h b/src/opt/rrr/rrrOptimizer.h
index 8d30368f1..831456295 100644
--- a/src/opt/rrr/rrrOptimizer.h
+++ b/src/opt/rrr/rrrOptimizer.h
@@ -12,6 +12,7 @@ ABC_NAMESPACE_CXX_HEADER_START
 
 namespace rrr {
 
+  // it is assumed that removing redundancy never degrades the cost in this optimizer
   template <typename Ntk, typename Ana>
   class Optimizer {
   private:
@@ -27,11 +28,14 @@ namespace rrr {
     // parameters
     int nVerbose;
     std::function<double(Ntk *)> CostFunction;
+    int nSortTypeOriginal;
     int nSortType;
     int nFlow;
     int nDistance;
     bool fCompatible;
+    bool fGreedy;
     seconds nTimeout; // assigned upon Run
+    std::string strVerbosePrefix;
 
     // data
     Ana ana;
@@ -47,6 +51,10 @@ namespace rrr {
     // marks
     int target;
     std::vector<bool> vTfoMarks;
+
+    // print
+    template<typename... Args>
+    void Print(int nVerboseLevel, Args... args);
     
     // callback
     void ActionCallback(Action const &action);
@@ -81,11 +89,21 @@ namespace rrr {
     int  MultiAdd(int id, std::vector<int> const &vCands, int nMax = 0);
 
     // resub
-    void SingleResub(int id, std::vector<int> const &vCands, bool fGreedy = true);
-    void MultiResub(int id, std::vector<int> const &vCands, bool fGreedy = true, int nMax = 0);
+    void SingleResub(int id, std::vector<int> const &vCands);
+    void MultiResub(int id, std::vector<int> const &vCands, int nMax = 0);
+
+    // resub stop
+    bool SingleResubStop(int id, std::vector<int> const &vCands);
+    bool MultiResubStop(int id, std::vector<int> const &vCands, int nMax = 0);
+
+    // multi-target resub
+    bool MultiTargetResub(std::vector<int> vTargets, int nMax = 0);
     
     // apply
     void ApplyReverseTopologically(std::function<void(int)> const &func);
+    void ApplyRandomlyStop(std::function<bool(int)> const &func);
+    void ApplyCombinationRandomlyStop(int k, std::function<bool(std::vector<int> const &)> const &func);
+    void ApplyCombinationSampledRandomlyStop(int k, int nSamples, std::function<bool(std::vector<int> const &)> const &func);
     
   public:
     // constructors
@@ -93,18 +111,39 @@ namespace rrr {
     void UpdateNetwork(Ntk *pNtk_, bool fSame = false);
 
     // run
-    void Run(seconds nTimeout_ = 0);
-    void ResetSeed(int iSeed);
-    void Randomize(int iSeed);
+    void Run(int iSeed = 0, seconds nTimeout_ = 0);
     
   };
 
+  /* {{{ Print */
+  
+  template <typename Ntk, typename Ana>
+  template <typename... Args>
+  inline void Optimizer<Ntk, Ana>::Print(int nVerboseLevel, Args... args) {
+    if(nVerbose > nVerboseLevel) {
+      std::cout << strVerbosePrefix;
+      for(int i = 0; i < nVerboseLevel; i++) {
+        std::cout << "\t";
+      }
+      PrintNext(std::cout, args...);
+      std::cout << std::endl;
+    }
+  }
+  
+  /* }}} */
+
   /* {{{ Callback */
   
   template <typename Ntk, typename Ana>
   void Optimizer<Ntk, Ana>::ActionCallback(Action const &action) {
-    if(nVerbose) {
-      PrintAction(action);
+    if(nVerbose > 2) {
+      std::stringstream ss = GetActionDescription(action);
+      std::string str;
+      std::getline(ss, str);
+      Print(2, str);
+      while(std::getline(ss, str)) {
+        Print(3, str);
+      }
     }
     switch(action.type) {
     case REMOVE_FANIN:
@@ -683,7 +722,7 @@ namespace rrr {
   /* {{{ Resub */
 
   template <typename Ntk, typename Ana>
-  void Optimizer<Ntk, Ana>::SingleResub(int id, std::vector<int> const &vCands, bool fGreedy) {
+  void Optimizer<Ntk, Ana>::SingleResub(int id, std::vector<int> const &vCands) {
     // NOTE: this assumes trivial collapse/decompose does not change cost
     // let us assume the node is not trivially redundant for now
     assert(pNtk->GetNumFanouts(id) != 0);
@@ -691,7 +730,7 @@ namespace rrr {
     // collapse
     pNtk->TrivialCollapse(id);
     // save if wanted
-    int slot;
+    int slot = -2;
     if(fGreedy) {
       slot = pNtk->Save();
     }
@@ -708,12 +747,11 @@ namespace rrr {
       if(it == vCands.end()) {
         break;
       }
+      Print(1, "cand", *it, "(", int_distance(vCands.begin(), it) + 1, "/", int_size(vCands), "):", "cost", "=", dCost);
       RemoveRedundancy();
       mapNewFanins.clear();
       double dNewCost = CostFunction(pNtk);
-      if(nVerbose) {
-        std::cout << "cost: " << dCost << " -> " << dNewCost << std::endl;
-      }
+      Print(2, "cost:", dCost, "->", dNewCost);
       if(fGreedy) {
         if(dNewCost <= dCost) {
           pNtk->Save(slot);
@@ -738,13 +776,13 @@ namespace rrr {
   }
 
   template <typename Ntk, typename Ana>
-  void Optimizer<Ntk, Ana>::MultiResub(int id, std::vector<int> const &vCands, bool fGreedy, int nMax) {
+  void Optimizer<Ntk, Ana>::MultiResub(int id, std::vector<int> const &vCands, int nMax) {
     // NOTE: this assumes trivial collapse/decompose does not change cost
     // let us assume the node is not trivially redundant for now
     assert(pNtk->GetNumFanouts(id) != 0);
     assert(pNtk->GetNumFanins(id) > 1);
     // save if wanted
-    int slot;
+    int slot = -2;
     if(fGreedy) {
       slot = pNtk->Save();
     }
@@ -755,16 +793,19 @@ namespace rrr {
     MultiAdd(id, vCands, nMax);
     RemoveRedundancy();
     mapNewFanins.clear();
+    // TODO: we could quit here if nothing has been removed
     RemoveRedundancy();
     double dNewCost = CostFunction(pNtk);
-    if(nVerbose) {
-      std::cout << "cost: " << dCost << " -> " << dNewCost << std::endl;
-    }
+    Print(1, "cost:", dCost, "->", dNewCost);
     if(fGreedy && dNewCost > dCost) {
       pNtk->Load(slot);
     }
     if(pNtk->IsInt(id)) {
       pNtk->TrivialDecompose(id);
+      SortFanins();
+      if(fCompatible) {
+        RemoveRedundancy();
+      }
     }
     if(fGreedy) {
       pNtk->PopBack();
@@ -773,6 +814,201 @@ namespace rrr {
   
   /* }}} */
 
+  /* {{{ Resub stop */
+
+  template <typename Ntk, typename Ana>
+  bool Optimizer<Ntk, Ana>::SingleResubStop(int id, std::vector<int> const &vCands) {
+    // stop whenever structure has changed without increasing cost and return true
+    // return false if no candidates are effective
+    // NOTE: this assumes trivial collapse/decompose does not change cost
+    // let us assume the node is not trivially redundant for now
+    assert(pNtk->GetNumFanouts(id) != 0);
+    assert(pNtk->GetNumFanins(id) > 1);
+    // save before trivial collapse
+    int slot0 = pNtk->Save();
+    // collapse
+    pNtk->TrivialCollapse(id);
+    // save after trivial collapse
+    int slot = pNtk->Save();
+    double dCost = CostFunction(pNtk);
+    // remember fanins
+    std::set<int> sFanins = pNtk->GetExtendedFanins(id);
+    Print(2, "extended fanins:", sFanins);
+    // main loop
+    for(citr it = vCands.begin(); it != vCands.end(); it++) {
+      if(Timeout()) {
+        break;
+      }
+      assert(pNtk->IsInt(id));
+      it = SingleAdd<citr>(id, it, vCands.end());
+      if(it == vCands.end()) {
+        break;
+      }
+      Print(1, "cand", *it, "(", int_distance(vCands.begin(), it) + 1, "/", int_size(vCands), "):", "cost", "=", dCost);
+      RemoveRedundancy();
+      mapNewFanins.clear();
+      double dNewCost = CostFunction(pNtk);
+      Print(2, "cost:", dCost, "->", dNewCost);
+      if(dNewCost <= dCost) {
+        bool fChanged = false;
+        if(dNewCost < dCost || !pNtk->IsInt(id)) {
+          fChanged = true;
+        } else {
+          std::set<int> sNewFanins = pNtk->GetExtendedFanins(id);
+          Print(2, "new extended fanins:", sNewFanins);
+          if(sFanins != sNewFanins) {
+            fChanged = true;
+          }
+        }
+        if(fChanged) {
+          if(pNtk->IsInt(id)) {
+            pNtk->TrivialDecompose(id);
+          }
+          pNtk->PopBack(); // slot
+          pNtk->PopBack(); // slot0
+          return true;
+        }
+      }
+      pNtk->Load(slot);
+    }
+    pNtk->PopBack(); // slot
+    pNtk->Load(slot0);
+    pNtk->PopBack(); // slot0
+    return false;
+  }
+
+  template <typename Ntk, typename Ana>
+  bool Optimizer<Ntk, Ana>::MultiResubStop(int id, std::vector<int> const &vCands, int nMax) {
+    // if structure has changed without increasing cost, return true
+    // otherwise, return false
+    // NOTE: this assumes trivial collapse/decompose does not change cost
+    // let us assume the node is not trivially redundant for now
+    assert(pNtk->GetNumFanouts(id) != 0);
+    assert(pNtk->GetNumFanins(id) > 1);
+    // save
+    int slot = pNtk->Save();
+    double dCost = CostFunction(pNtk);
+    // remember fanins
+    std::set<int> sFanins = pNtk->GetExtendedFanins(id);
+    Print(2, "extended fanins:", sFanins);
+    // collapse
+    pNtk->TrivialCollapse(id);
+    // resub
+    MultiAdd(id, vCands, nMax);
+    RemoveRedundancy();
+    mapNewFanins.clear();
+    // TODO: we could quit here if nothing has been removed
+    RemoveRedundancy();
+    double dNewCost = CostFunction(pNtk);
+    Print(1, "cost:", dCost, "->", dNewCost);
+    if(!fGreedy || dNewCost <= dCost) {
+      bool fChanged = false;
+      if(dNewCost < dCost || !pNtk->IsInt(id)) {
+        fChanged = true;
+      } else {
+        std::set<int> sNewFanins = pNtk->GetExtendedFanins(id);
+        Print(2, "new extended fanins:", sNewFanins);
+        if(sFanins != sNewFanins) {
+          fChanged = true;
+        }
+      }
+      if(fChanged) {
+        if(pNtk->IsInt(id)) {
+          pNtk->TrivialDecompose(id);
+        }
+        pNtk->PopBack();
+        return true;
+      }
+    }
+    pNtk->Load(slot);
+    pNtk->PopBack();
+    return false;
+  }
+  
+  /* }}} */
+
+  /* {{{ Multi-target resub */
+
+  template <typename Ntk, typename Ana>
+  bool Optimizer<Ntk, Ana>::MultiTargetResub(std::vector<int> vTargets, int nMax) {
+    // save
+    int slot = pNtk->Save();
+    double dCost = CostFunction(pNtk);
+    // remove targets that are trivially collapsed together
+    for(int id: vTargets) {
+      if(pNtk->IsInt(id)) {
+        pNtk->TrivialCollapse(id);
+      }
+    }
+    for(itr it = vTargets.begin(); it != vTargets.end();) {
+      if(!pNtk->IsInt(*it)) {
+        it = vTargets.erase(it);
+      } else {
+        it++;
+      }
+    }
+    // add while remembering extended fanins
+    Print(1, "targets:", vTargets);
+    std::vector<std::set<int>> vsFanins;
+    for(int id: vTargets) {
+      // get candidates
+      std::vector<int> vCands;
+      if(nDistance) {
+        vCands = pNtk->GetNeighbors(id, true, nDistance);
+      } else {
+        vCands = pNtk->GetPisInts();
+      }
+      std::shuffle(vCands.begin(), vCands.end(), rng);
+      // remember fanins
+      std::set<int> sFanins = pNtk->GetExtendedFanins(id);
+      Print(2, "extended fanins:", sFanins);
+      vsFanins.push_back(std::move(sFanins));
+      // add
+      MultiAdd(id, vCands, nMax);
+    }
+    // reduce
+    RemoveRedundancy();
+    mapNewFanins.clear();
+    // TODO: we could quit here if nothing has been removed
+    RemoveRedundancy();
+    double dNewCost = CostFunction(pNtk);
+    Print(1, "cost:", dCost, "->", dNewCost);
+    if(!fGreedy || dNewCost <= dCost) {
+      bool fChanged = false;
+      if(dNewCost < dCost) {
+        fChanged = true;
+      } else {
+        for(int id: vTargets) {
+          if(!pNtk->IsInt(id)) {
+            fChanged = true;
+            break;
+          }
+        }
+        for(int i = 0; !fChanged && i < int_size(vTargets); i++) {
+          std::set<int> sNewFanins = pNtk->GetExtendedFanins(vTargets[i]);
+          Print(2, "new extended fanins:", sNewFanins);
+          if(vsFanins[i] != sNewFanins) {
+            fChanged = true;
+          }
+        }
+      }
+      if(fChanged) {
+        for(int id: vTargets) {
+          if(pNtk->IsInt(id)) {
+            pNtk->TrivialDecompose(id);
+          }
+        }
+        pNtk->PopBack();
+        return true;
+      }
+    }
+    pNtk->Load(slot);
+    pNtk->PopBack();
+    return false;
+  }
+  
+  /* }}} */
+  
   /* {{{ Apply */
 
   template <typename Ntk, typename Ana>
@@ -785,12 +1021,73 @@ namespace rrr {
       if(!pNtk->IsInt(*it)) {
         continue;
       }
-      if(nVerbose) {
-        std::cout << "node " << *it << " (" << std::distance(vInts.crbegin(), it) + 1 << "/" << vInts.size() << ")" << std::endl;
-      }
+      Print(0, "node", *it, "(", int_distance(vInts.crbegin(), it) + 1, "/", int_size(vInts), "):", "cost", "=", CostFunction(pNtk));
       func(*it);
     }
   }
+
+  template <typename Ntk, typename Ana>
+  void Optimizer<Ntk, Ana>::ApplyRandomlyStop(std::function<bool(int)> const &func) {
+    std::vector<int> vInts = pNtk->GetInts();
+    std::shuffle(vInts.begin(), vInts.end(), rng);
+    for(citr it = vInts.begin(); it != vInts.end(); it++) {
+      if(Timeout()) {
+        break;
+      }
+      if(!pNtk->IsInt(*it)) {
+        continue;
+      }
+      Print(0, "node", *it, "(", int_distance(vInts.cbegin(), it) + 1, "/", int_size(vInts), "):", "cost", "=", CostFunction(pNtk));
+      if(func(*it)) {
+        break;
+      }
+    }
+  }
+
+  template <typename Ntk, typename Ana>
+  void Optimizer<Ntk, Ana>::ApplyCombinationRandomlyStop(int k, std::function<bool(std::vector<int> const &)> const &func) {
+    std::vector<int> vInts = pNtk->GetInts();
+    std::shuffle(vInts.begin(), vInts.end(), rng); // order is decided here, so it's not truely exhaustive
+    int nTried = 0;
+    int nCombs = k * (k - 1) / 2;
+    ForEachCombinationStop(int_size(vInts), k, [&](std::vector<int> const &vIdxs) {
+      Print(0, "comb", vIdxs, "(", ++nTried, "/", nCombs, ")");
+      assert(int_size(vIdxs) == k);
+      if(Timeout()) {
+        return true;
+      }
+      std::vector<int> vTargets(k);
+      for(int i = 0; i < k; i++) {
+        vTargets[i] = vInts[vIdxs[i]];
+      }
+      return func(vTargets);
+    });
+  }
+  
+  template <typename Ntk, typename Ana>
+  void Optimizer<Ntk, Ana>::ApplyCombinationSampledRandomlyStop(int k, int nSamples, std::function<bool(std::vector<int> const &)> const &func) {
+    std::vector<int> vInts = pNtk->GetInts();
+    for(int i = 0; i < nSamples; i++) {
+      if(Timeout()) {
+        break;
+      }
+      std::set<int> sIdxs;
+      while(int_size(sIdxs) < k) {
+        int idx = rng() % pNtk->GetNumInts();
+        sIdxs.insert(idx);
+      }
+      std::vector<int> vIdxs(sIdxs.begin(), sIdxs.end());
+      std::shuffle(vIdxs.begin(), vIdxs.end(), rng);
+      Print(0, "comb", vIdxs, "(", i + 1, "/", nSamples, ")");
+      std::vector<int> vTargets(k);
+      for(int i = 0; i < k; i++) {
+        vTargets[i] = vInts[vIdxs[i]];
+      }
+      if(func(vTargets)) {
+        break;
+      }
+    }
+  }
   
   /* }}} */
   
@@ -801,10 +1098,12 @@ namespace rrr {
     pNtk(NULL),
     nVerbose(pPar->nOptimizerVerbose),
     CostFunction(CostFunction),
+    nSortTypeOriginal(pPar->nSortType),
     nSortType(pPar->nSortType),
     nFlow(pPar->nOptimizerFlow),
     nDistance(pPar->nDistance),
     fCompatible(pPar->fUseBddCspf),
+    fGreedy(pPar->fGreedy),
     ana(pPar),
     target(-1) {
   }
@@ -822,7 +1121,14 @@ namespace rrr {
   /* {{{ Run */
 
   template <typename Ntk, typename Ana>
-  void Optimizer<Ntk, Ana>::Run(seconds nTimeout_) {
+  void Optimizer<Ntk, Ana>::Run(int iSeed, seconds nTimeout_) {
+    rng.seed(iSeed);
+    vRandPiOrder.clear();
+    vRandCosts.clear();
+    if(nSortTypeOriginal < 0) {
+      nSortType = rng() % 18;
+      Print(0, "sorttype =", nSortType);
+    }
     nTimeout = nTimeout_;
     start = GetCurrentTime();
     switch(nFlow) {
@@ -882,23 +1188,37 @@ namespace rrr {
       }
       break;
     }
+    case 3: {
+      RemoveRedundancy();
+      std::vector<int> vCands;
+      if(!nDistance) {
+        vCands = pNtk->GetPisInts();
+        std::shuffle(vCands.begin(), vCands.end(), rng);
+      }
+      ApplyRandomlyStop([&](int id) {
+        if(nDistance) {
+          vCands = pNtk->GetNeighbors(id, true, nDistance);
+          std::shuffle(vCands.begin(), vCands.end(), rng);
+        }
+        if(rng() & 1) {
+          return SingleResubStop(id, vCands);
+        } else {
+          return MultiResubStop(id, vCands);
+        }
+      });
+      break;
+    }
+    case 4: {
+      RemoveRedundancy();
+      ApplyCombinationSampledRandomlyStop(3, 100, [&](std::vector<int> const &vTargets) {
+        return MultiTargetResub(vTargets);
+      });
+      break;
+    }
     default:
       assert(0);
     }
   }
-
-  template <typename Ntk, typename Ana>
-  void Optimizer<Ntk, Ana>::ResetSeed(int iSeed) {
-    rng.seed(iSeed);
-    vRandPiOrder.clear();
-    vRandCosts.clear();
-  }
-  
-  template <typename Ntk, typename Ana>
-  void Optimizer<Ntk, Ana>::Randomize(int iSeed) {
-    ResetSeed(iSeed);
-    nSortType = rng() % 18;
-  }
   
   /* }}} */
   
diff --git a/src/opt/rrr/rrrParameter.h b/src/opt/rrr/rrrParameter.h
index 22429511b..e6b5ccb8c 100644
--- a/src/opt/rrr/rrrParameter.h
+++ b/src/opt/rrr/rrrParameter.h
@@ -17,14 +17,19 @@ namespace rrr {
     bool fUseBddCspf = false;
     bool fUseBddMspf = false;
     int nConflictLimit = 0;
-    int nSortType = 12;
+    int nSortType = -1;
     int nOptimizerFlow = 0;
     int nSchedulerFlow = 0;
+    int nPartitionType = 0;
     int nDistance = 0;
-    int nRestarts = 0;
+    int nJobs = 1;
     int nThreads = 1;
-    int nWindowSize = 0;
+    int nPartitionSize = 0;
+    int nPartitionSizeMin = 0;
     bool fDeterministic = true;
+    int nParallelPartitions = 1;
+    bool fOptOnInsert = false;
+    bool fGreedy = true;
   };
   
 }
diff --git a/src/opt/rrr/rrrPartitioner.h b/src/opt/rrr/rrrPartitioner.h
index a2993e8e8..16819f075 100644
--- a/src/opt/rrr/rrrPartitioner.h
+++ b/src/opt/rrr/rrrPartitioner.h
@@ -20,13 +20,23 @@ namespace rrr {
 
     // parameters
     int nVerbose;
-    int nWindowSize;
+    int nPartitionSize;
+    int nPartitionSizeMin;
+    std::string strVerbosePrefix;
 
     // data
     std::map<Ntk *, std::tuple<std::set<int>, std::vector<int>, std::vector<bool>, std::vector<int>>> mSubNtk2Io;
     std::set<int> sBlocked;
+    std::vector<bool> vFailed;
 
+    // print
+    template<typename... Args>
+    void Print(int nVerboseLevel, Args... args);
+    
     // subroutines
+    void GetIo(std::set<int> const &sNodes, std::set<int> &sInputs, std::set<int> &sOutputs);
+    std::set<int> GetFanouts(std::set<int> const &sNodes, std::set<int> const &sOutputs);
+    std::set<int> GetUnblockedNeighborsAndInners(int id, int nRadius);
     Ntk *ExtractDisjoint(int id);
     
   public:
@@ -39,45 +49,29 @@ namespace rrr {
     void Insert(Ntk *pSubNtk);
   };
 
+  /* {{{ Print */
+  
+  template <typename Ntk>
+  template <typename... Args>
+  inline void Partitioner<Ntk>::Print(int nVerboseLevel, Args... args) {
+    if(nVerbose > nVerboseLevel) {
+      std::cout << strVerbosePrefix;
+      for(int i = 0; i < nVerboseLevel; i++) {
+        std::cout << "\t";
+      }
+      PrintNext(std::cout, args...);
+      std::cout << std::endl;
+    }
+  }
+
+  /* }}} */
+
   /* {{{ Subroutines */
 
   template <typename Ntk>
-  Ntk *Partitioner<Ntk>::ExtractDisjoint(int id) {
-    // collect neighbor
-    assert(!sBlocked.count(id));
-    if(nVerbose) {
-      std::cout << "extracting with a center node " << id << std::endl;
-    }
-    int nRadius = 2;
-    std::vector<int> vNodes = pNtk->GetNeighbors(id, false, nRadius);
-    std::vector<int> vNodesNew = pNtk->GetNeighbors(id, false, nRadius + 1);
-    // gradually increase radius until it hits window size limit
-    while(int_size(vNodesNew) < nWindowSize) {
-      if(int_size(vNodes) == int_size(vNodesNew)) { // already maximum
-        break;
-      }
-      vNodes = vNodesNew;
-      nRadius++;
-      vNodesNew = pNtk->GetNeighbors(id, false, nRadius + 1);
-    }
-    std::set<int> sNodes(vNodes.begin(), vNodes.end());
-    sNodes.insert(id);
-    if(nVerbose) {
-      std::cout << "neighbors: " << sNodes << std::endl;
-    }
-    // remove nodes that are already blocked
-    for(std::set<int>::iterator it = sNodes.begin(); it != sNodes.end();) {
-      if(sBlocked.count(*it)) {
-        it = sNodes.erase(it);
-      } else {
-        it++;
-      }
-    }
-    if(nVerbose) {
-      std::cout << "disjoint neighbors: " << sNodes << std::endl;
-    }
-    // get tentative window IO
-    std::set<int> sInputs, sOutputs;
+  void Partitioner<Ntk>::GetIo(std::set<int> const &sNodes, std::set<int> &sInputs, std::set<int> &sOutputs) {
+    sInputs.clear();
+    sOutputs.clear();
     for(int id: sNodes) {
       pNtk->ForEachFanin(id, [&](int fi) {
         if(!sNodes.count(fi)) {
@@ -94,12 +88,10 @@ namespace rrr {
         sOutputs.insert(id);
       }
     }
-    if(nVerbose) {
-      std::cout << "\tinputs: " << sInputs << std::endl;
-      std::cout << "\toutputs: " << sOutputs << std::endl;
-    }
-    // prevent potential loops while ensuring disjointness
-    // first by including inner nodes
+  }
+
+  template <typename Ntk>
+  std::set<int> Partitioner<Ntk>::GetFanouts(std::set<int> const &sNodes, std::set<int> const &sOutputs) {
     std::set<int> sFanouts;
     for(int id: sOutputs) {
       pNtk->ForEachFanout(id, false, [&](int fo) {
@@ -108,89 +100,111 @@ namespace rrr {
         }
       });
     }
+    return sFanouts;
+  }
+
+  template <typename Ntk>
+  std::set<int> Partitioner<Ntk>::GetUnblockedNeighborsAndInners(int id, int nRadius) {
+    // return empty set on failure
+    // get neighbors
+    std::vector<int> vNodes = pNtk->GetNeighbors(id, false, nRadius);
+    vNodes.push_back(id);
+    std::set<int> sNodes(vNodes.begin(), vNodes.end());
+    Print(2, "radius", NS(), nRadius, ":", "size =", int_size(sNodes));
+    // remove nodes that are already blocked
+    for(std::set<int>::iterator it = sNodes.begin(); it != sNodes.end();) {
+      if(sBlocked.count(*it)) {
+        it = sNodes.erase(it);
+      } else {
+        it++;
+      }
+    }
+    Print(2, "unblocked:", "size =", int_size(sNodes));
+    if(int_size(sNodes) > nPartitionSize) {
+      // too large
+      return std::set<int>();
+    }
+    // get tentative partition IO
+    std::set<int> sInputs, sOutputs;
+    GetIo(sNodes, sInputs, sOutputs);
+    Print(3, "nodes:", sNodes);
+    Print(3, "inputs:", sInputs);
+    Print(3, "outputs:", sOutputs);
+    // include inner nodes
+    std::set<int> sFanouts = GetFanouts(sNodes, sOutputs);
     std::vector<int> vInners = pNtk->GetInners(sFanouts, sInputs);
     while(!vInners.empty()) {
-      if(nVerbose) {
-        std::cout << "inners: " << vInners << std::endl;
-      }
-      if(int_size(sNodes) + int_size(vInners) > 2 * nWindowSize) {
-        // TODO: parametrize
-        break;
-      }
-      bool fOverlap = false;
-      for(int i: vInners) {
-        if(sBlocked.count(i)) {
-          fOverlap = true;
-          break;
+      Print(2, "inner size =", int_size(vInners));
+      // check overlap
+      for(int id: vInners) {
+        if(sBlocked.count(id)) {
+          // overlapped
+          return std::set<int>();     
         }
       }
-      if(fOverlap) {
-        break;
-      }
+      // expand
       sNodes.insert(vInners.begin(), vInners.end());
-      if(nVerbose) {
-        std::cout << "new neighbors: " << sNodes << std::endl;
-      }
-      sInputs.clear();
-      sOutputs.clear();
-      for(int id: sNodes) {
-        pNtk->ForEachFanin(id, [&](int fi) {
-          if(!sNodes.count(fi)) {
-            sInputs.insert(fi);
-          }
-        });
-        bool fOutput = false;
-        pNtk->ForEachFanout(id, true, [&](int fo) {
-          if(!sNodes.count(fo)) {
-            fOutput = true;
-          }
-        });
-        if(fOutput) {
-          sOutputs.insert(id);
-        }
-      }
-      if(nVerbose) {
-        std::cout << "\tnew inputs: " << sInputs << std::endl;
-        std::cout << "\tnew outputs: " << sOutputs << std::endl;
-      }
-      sFanouts.clear();
-      for(int id: sOutputs) {
-        pNtk->ForEachFanout(id, false, [&](int fo) {
-          if(!sNodes.count(fo)) {
-            sFanouts.insert(fo);
-          }
-        });
+      Print(2, "expanded:", "size =", int_size(sNodes));
+      if(int_size(sNodes) > nPartitionSize) {
+        // too large
+        return std::set<int>();
       }
+      GetIo(sNodes, sInputs, sOutputs);
+      Print(3, "nodes:", sNodes);
+      Print(3, "inputs:", sInputs);
+      Print(3, "outputs:", sOutputs);
+      // recompute fanouts
+      sFanouts = GetFanouts(sNodes, sOutputs);
       vInners = pNtk->GetInners(sFanouts, sInputs);
     }
+    return sNodes;
+  }
+  
+  template <typename Ntk>
+  Ntk *Partitioner<Ntk>::ExtractDisjoint(int id) {
+    // collect neighbor
+    assert(!sBlocked.count(id));
+    int nRadius = 1;
+    std::set<int> sNodes = GetUnblockedNeighborsAndInners(id, nRadius);
+    Print(1, "radius", NS(), nRadius, ":", "size =", int_size(sNodes));
+    if(sNodes.empty()) {
+      return NULL;
+    }
+    std::set<int> sNodesNew = GetUnblockedNeighborsAndInners(id, nRadius + 1);
+    Print(1, "radius", NS(), nRadius + 1, ":", "size =", int_size(sNodesNew));
+    // gradually increase radius until it hits partition size limit
+    while(!sNodesNew.empty()) {
+      if(int_size(sNodes) == int_size(sNodesNew)) { // likely already maximum
+        break;
+      }
+      sNodes = sNodesNew;
+      nRadius++;
+      sNodesNew = GetUnblockedNeighborsAndInners(id, nRadius + 1);
+      Print(1, "radius", NS(), nRadius + 1, ":", "size =", int_size(sNodesNew));
+    }
+    if(int_size(sNodes) < nPartitionSizeMin) {
+      // too small
+      return NULL;
+    }
+    std::set<int> sInputs, sOutputs;
+    GetIo(sNodes, sInputs, sOutputs);
+    /* fall back method by removing TFI of outputs reachable to inputs
     if(!vInners.empty()) {
-      // fall back method by removing TFI of outputs reachable to inputs
       for(int id: sOutputs) {
         if(!sNodes.count(id)) { // already removed
           continue;
         }
-        sFanouts.clear();
-        pNtk->ForEachFanout(id, false, [&](int fo) {
-          if(!sNodes.count(fo)) {
-            sFanouts.insert(fo);
-          }
-        });
+        std::set<int> sFanouts = GetFanouts(sNodes, sOutputs);
         if(pNtk->IsReachable(sFanouts, sInputs)) {
-          if(nVerbose) {
-            std::cout << id << " is reachable to inputs" << std::endl;
-          }
+          Print(2, "node", id, "is reachable");
           sNodes.erase(id);
           pNtk->ForEachTfiEnd(id, sInputs, [&](int fi) {
             int r = sNodes.erase(fi);
             assert(r);
           });
-          if(nVerbose) {
-            std::cout << "new neighbors: " << sNodes << std::endl;
-          }
-          if(sNodes.empty()) {
-            if(nVerbose) {
-              std::cout << "IS EMPTY" << std::endl;
-            }
+          Print(1, "shrinking:", "size =", int_size(sNodes));
+          if(int_size(sNodes) < nPartitionSizeMin) {
+            // too small
             return NULL;
           }
           // recompute inputs
@@ -202,9 +216,8 @@ namespace rrr {
               }
             });
           }
-          if(nVerbose) {
-            std::cout << "\tnew inputs: " << sInputs << std::endl;
-          }
+          Print(3, "nodes:", sNodes);
+          Print(3, "inputs:", sInputs);
         }
       }
       // recompute outputs
@@ -215,11 +228,10 @@ namespace rrr {
           it++;
         }
       }
-      if(nVerbose) {
-        std::cout << "\tnew outputs: " << sOutputs << std::endl;
-      }
+      Print(3, "new outputs:", sOutputs);
     }
-    // ensure outputs of both windows do not reach each other's inputs at the same time
+    */
+    // ensure outputs of both partitions do not reach each other's inputs at the same time
     for(auto const &entry: mSubNtk2Io) {
       if(!pNtk->IsReachable(sOutputs, std::get<1>(entry.second))) {
         continue;
@@ -227,23 +239,20 @@ namespace rrr {
       if(!pNtk->IsReachable(std::get<3>(entry.second), sInputs)) {
         continue;
       }
-      if(nVerbose) {
-        std::cout << "POTENTIAL LOOPS" << std::endl;
-      }
-      return NULL;
-    }
-    if(int_size(sNodes) < nWindowSize / 2) {
-      // too small
-      // TODO: fix this parameterized
+      // if(nVerbose) {
+      //   std::cout << "POTENTIAL LOOPS" << std::endl;
+      // }
       return NULL;
     }
+    assert(int_size(sNodes) <= nPartitionSize);
+    assert(int_size(sNodes) >= nPartitionSizeMin);
     // extract by inputs, internals, and outputs (no checks needed in ntk side)
     std::vector<int> vInputs(sInputs.begin(), sInputs.end());
     std::vector<int> vOutputs(sOutputs.begin(), sOutputs.end());
     Ntk *pSubNtk = pNtk->Extract(sNodes, vInputs, vOutputs);
     // return subntk to be modified, while remember IOs
-    for(int i: sNodes) {
-      sBlocked.insert(i);
+    for(int id: sNodes) {
+      sBlocked.insert(id);
     }
     mSubNtk2Io.emplace(pSubNtk, std::make_tuple(std::move(sNodes), std::move(vInputs), std::vector<bool>(vInputs.size()), std::move(vOutputs)));
     return pSubNtk;
@@ -256,12 +265,16 @@ namespace rrr {
   template <typename Ntk>
   Partitioner<Ntk>::Partitioner(Parameter const *pPar) :
     nVerbose(pPar->nPartitionerVerbose),
-    nWindowSize(pPar->nWindowSize) {
+    nPartitionSize(pPar->nPartitionSize),
+    nPartitionSizeMin(pPar->nPartitionSizeMin) {
   }
 
   template <typename Ntk>
   void Partitioner<Ntk>::UpdateNetwork(Ntk *pNtk_) {
     pNtk = pNtk_;
+    assert(mSubNtk2Io.empty());
+    assert(sBlocked.empty());
+    vFailed.clear();
   }
 
   /* }}} */
@@ -270,17 +283,24 @@ namespace rrr {
   
   template <typename Ntk>
   Ntk *Partitioner<Ntk>::Extract(int iSeed) {
-    // pick a center node from candidates that do not belong to any other ongoing windows
+    // pick a center node from candidates that do not belong to any other ongoing partitions
+    vFailed.resize(pNtk->GetNumNodes());
     std::mt19937 rng(iSeed);
     std::vector<int> vInts = pNtk->GetInts();
     std::shuffle(vInts.begin(), vInts.end(), rng);
-    for(int id: vInts) {
+    for(int i = 0; i < int_size(vInts); i++) {
+      int id = vInts[i];
+      if(vFailed[id]) {
+        continue;
+      }
       if(!sBlocked.count(id)) {
+        Print(0, "try partitioning with node", id, "(", i, "/", int_size(vInts), ")");
         Ntk *pSubNtk = ExtractDisjoint(id);
         if(pSubNtk) {
           return pSubNtk;
         }
       }
+      vFailed[id] = true;
     }
     return NULL;
   }
@@ -294,7 +314,7 @@ namespace rrr {
     std::vector<int> &vOldOutputs = std::get<3>(mSubNtk2Io[pSubNtk]);
     std::vector<int> &vNewOutputs = vNewSignals.first;
     std::vector<bool> &vNewCompls = vNewSignals.second;
-    // need to remap updated outputs that are used as inputs in other windows
+    // need to remap updated outputs that are used as inputs in other partitions
     std::map<int, int> mOutput2Idx;
     for(int idx = 0; idx < int_size(vOldOutputs); idx++) {
       mOutput2Idx[vOldOutputs[idx]] = idx;
@@ -314,6 +334,7 @@ namespace rrr {
     }
     delete pSubNtk;
     mSubNtk2Io.erase(pSubNtk);
+    vFailed.clear(); // clear, there isn't really a way to track
   }
 
   /* }}} */
diff --git a/src/opt/rrr/rrrSatSolver.h b/src/opt/rrr/rrrSatSolver.h
index ac9fa4c45..b1bf01f35 100644
--- a/src/opt/rrr/rrrSatSolver.h
+++ b/src/opt/rrr/rrrSatSolver.h
@@ -108,7 +108,7 @@ namespace rrr {
   void SatSolver<Ntk>::EncodeNode(sat_solver *p, std::vector<int> const &v, int id, int to_negate) const {
     int RetValue;
     int x = -1, y = -1;
-    bool cx, cy;
+    bool cx = false, cy = false;
     assert(pNtk->GetNodeType(id) == AND);
     std::string delim;
     if(nVerbose) {
diff --git a/src/opt/rrr/rrrScheduler.h b/src/opt/rrr/rrrScheduler.h
index c8b5a16a0..ced6da047 100644
--- a/src/opt/rrr/rrrScheduler.h
+++ b/src/opt/rrr/rrrScheduler.h
@@ -11,16 +11,18 @@
 
 #include "rrrParameter.h"
 #include "rrrUtils.h"
-#include "rrrPartitioner.h"
 #include "rrrAbc.h"
 
 ABC_NAMESPACE_CXX_HEADER_START
 
 namespace rrr {
 
-  template <typename Ntk, typename Opt>
+  template <typename Ntk, typename Opt, typename Par>
   class Scheduler {
   private:
+    // aliases
+    static constexpr char *pCompress2rs = "balance -l; resub -K 6 -l; rewrite -l; resub -K 6 -N 2 -l; refactor -l; resub -K 8 -l; balance -l; resub -K 8 -N 2 -l; rewrite -l; resub -K 10 -l; rewrite -z -l; resub -K 10 -N 2 -l; balance -l; resub -K 12 -l; refactor -z -l; resub -K 12 -N 2 -l; rewrite -z -l; balance -l";
+    
     // job
     struct Job;
     struct CompareJobPointers;
@@ -32,18 +34,20 @@ namespace rrr {
     int nVerbose;
     int iSeed;
     int nFlow;
-    int nRestarts;
+    int nJobs;
     bool fMultiThreading;
     bool fPartitioning;
     bool fDeterministic;
+    int nParallelPartitions;
+    bool fOptOnInsert;
     seconds nTimeout;
     std::function<double(Ntk *)> CostFunction;
     
     // data
-    int nJobs;
+    int nCreatedJobs;
     int nFinishedJobs;
     time_point start;
-    Partitioner<Ntk> par;
+    Par par;
     std::queue<Job *> qPendingJobs;
     Opt *pOpt; // used only in case of single thread execution
 #ifdef ABC_USE_PTHREADS
@@ -86,8 +90,8 @@ namespace rrr {
 
   /* {{{ Job */
   
-  template <typename Ntk, typename Opt>
-  struct Scheduler<Ntk, Opt>::Job {
+  template <typename Ntk, typename Opt, typename Par>
+  struct Scheduler<Ntk, Opt, Par>::Job {
     // data
     int id;
     Ntk *pNtk;
@@ -101,8 +105,8 @@ namespace rrr {
     }
   };
 
-  template <typename Ntk, typename Opt>
-  struct Scheduler<Ntk, Opt>::CompareJobPointers {
+  template <typename Ntk, typename Opt, typename Par>
+  struct Scheduler<Ntk, Opt, Par>::CompareJobPointers {
     // smaller id comes first in priority_queue
     bool operator()(Job const *lhs, Job const *rhs) const {
       return lhs->id > rhs->id;
@@ -113,8 +117,8 @@ namespace rrr {
 
   /* {{{ Time */
 
-  template <typename Ntk, typename Opt>
-  seconds Scheduler<Ntk, Opt>::GetRemainingTime() const {
+  template <typename Ntk, typename Opt, typename Par>
+  seconds Scheduler<Ntk, Opt, Par>::GetRemainingTime() const {
     if(nTimeout == 0) {
       return 0;
     }
@@ -130,8 +134,8 @@ namespace rrr {
 
   /* {{{ Abc */
 
-  template <typename Ntk, typename Opt>
-  inline void Scheduler<Ntk, Opt>::CallAbc(Ntk *pNtk_, std::string Command) {
+  template <typename Ntk, typename Opt, typename Par>
+  inline void Scheduler<Ntk, Opt, Par>::CallAbc(Ntk *pNtk_, std::string Command) {
 #ifdef ABC_USE_PTHREADS
     if(fMultiThreading) {
       {
@@ -148,14 +152,13 @@ namespace rrr {
   
   /* {{{ Run jobs */
 
-  template <typename Ntk, typename Opt>
-  void Scheduler<Ntk, Opt>::RunJob(Opt &opt, Job const *pJob) {
+  template <typename Ntk, typename Opt, typename Par>
+  void Scheduler<Ntk, Opt, Par>::RunJob(Opt &opt, Job const *pJob) {
     opt.UpdateNetwork(pJob->pNtk);
     // start flow
     switch(nFlow) {
     case 0:
-      opt.ResetSeed(pJob->iSeed);
-      opt.Run(GetRemainingTime());
+      opt.Run(pJob->iSeed, GetRemainingTime());
       break;
     case 1: { // transtoch
       std::mt19937 rng(pJob->iSeed);
@@ -181,8 +184,7 @@ namespace rrr {
           if(GetRemainingTime() < 0) {
             break;
           }
-          opt.Randomize(rng());
-          opt.Run(GetRemainingTime());
+          opt.Run(rng(), GetRemainingTime());
           CallAbc(pJob->pNtk, "&dc2");
           double dNewCost = CostFunction(pJob->pNtk);
           if(nVerbose) {
@@ -221,7 +223,6 @@ namespace rrr {
         }
         // deepsyn
         int fUseTwo = 0;
-        std::string pCompress2rs = "balance -l; resub -K 6 -l; rewrite -l; resub -K 6 -N 2 -l; refactor -l; resub -K 8 -l; balance -l; resub -K 8 -N 2 -l; rewrite -l; resub -K 10 -l; rewrite -z -l; resub -K 10 -N 2 -l; balance -l; resub -K 12 -l; refactor -z -l; resub -K 12 -N 2 -l; rewrite -z -l; balance -l";
         unsigned Rand = rng();
         int fDch = Rand & 1;
         //int fCom = (Rand >> 1) & 3;
@@ -230,11 +231,11 @@ namespace rrr {
         int KLut = fUseTwo ? 2 + (i % 5) : 3 + (i % 4);
         std::string pComp;
         if ( fCom == 3 )
-          pComp = "; &put; " + pCompress2rs + "; " + pCompress2rs + "; " + pCompress2rs + "; &get";
+          pComp = std::string("; &put; ") + pCompress2rs + "; " + pCompress2rs + "; " + pCompress2rs + "; &get";
         else if ( fCom == 2 )
-          pComp = "; &put; " + pCompress2rs + "; " + pCompress2rs + "; &get";
+          pComp = std::string("; &put; ") + pCompress2rs + "; " + pCompress2rs + "; &get";
         else if ( fCom == 1 )
-          pComp = "; &put; " + pCompress2rs + "; &get";
+          pComp = std::string("; &put; ") + pCompress2rs + "; &get";
         else if ( fCom == 0 )
           pComp = "; &dc2";
         std::string Command = "&dch";
@@ -254,12 +255,11 @@ namespace rrr {
             break;
           }
           opt.UpdateNetwork(pJob->pNtk, true);
-          opt.Randomize(rng());
-          opt.Run(GetRemainingTime());
+          opt.Run(rng(), GetRemainingTime());
           if(rng() & 1) {
             CallAbc(pJob->pNtk, "&dc2");
           } else {
-            CallAbc(pJob->pNtk, "&put; " + pCompress2rs + "; &get");
+            CallAbc(pJob->pNtk, std::string("&put; ") + pCompress2rs + "; &get");
           }
           if(nVerbose) {
             std::cout << "\trrr " << std::setw(6) << j << ": cost = " << CostFunction(pJob->pNtk) << std::endl;
@@ -280,6 +280,10 @@ namespace rrr {
       }
       break;
     }
+    case 3:
+      opt.Run(pJob->iSeed, GetRemainingTime());
+      CallAbc(pJob->pNtk, std::string("&put; ") + pCompress2rs + "; dc2; &get");
+      break;
     default:
       assert(0);
     }
@@ -289,9 +293,9 @@ namespace rrr {
 
   /* {{{ Manage jobs */
 
-  template <typename Ntk, typename Opt>
-  void Scheduler<Ntk, Opt>::CreateJob(Ntk *pNtk_, int iSeed_) {
-    Job *pJob = new Job(nJobs++, pNtk_, iSeed_);
+  template <typename Ntk, typename Opt, typename Par>
+  void Scheduler<Ntk, Opt, Par>::CreateJob(Ntk *pNtk_, int iSeed_) {
+    Job *pJob = new Job(nCreatedJobs++, pNtk_, iSeed_);
 #ifdef ABC_USE_PTHREADS
     if(fMultiThreading) {
       {
@@ -305,8 +309,8 @@ namespace rrr {
     qPendingJobs.push(pJob);
   }
   
-  template <typename Ntk, typename Opt>
-  void Scheduler<Ntk, Opt>::OnJobEnd(std::function<void(Job *pJob)> const &func) {
+  template <typename Ntk, typename Opt, typename Par>
+  void Scheduler<Ntk, Opt, Par>::OnJobEnd(std::function<void(Job *pJob)> const &func) {
 #ifdef ABC_USE_PTHREADS
     if(fMultiThreading) {
       Job *pJob = NULL;
@@ -340,8 +344,8 @@ namespace rrr {
   /* {{{ Thread */
 
 #ifdef ABC_USE_PTHREADS
-  template <typename Ntk, typename Opt>
-  void Scheduler<Ntk, Opt>::Thread(Parameter const *pPar) {
+  template <typename Ntk, typename Opt, typename Par>
+  void Scheduler<Ntk, Opt, Par>::Thread(Parameter const *pPar) {
     Opt opt(pPar, CostFunction);
     while(true) {
       Job *pJob = NULL;
@@ -371,19 +375,21 @@ namespace rrr {
   /* }}} */
   
   /* {{{ Constructors */
-  
-  template <typename Ntk, typename Opt>
-  Scheduler<Ntk, Opt>::Scheduler(Ntk *pNtk, Parameter const *pPar) :
+
+  template <typename Ntk, typename Opt, typename Par>
+  Scheduler<Ntk, Opt, Par>::Scheduler(Ntk *pNtk, Parameter const *pPar) :
     pNtk(pNtk),
     nVerbose(pPar->nSchedulerVerbose),
     iSeed(pPar->iSeed),
     nFlow(pPar->nSchedulerFlow),
-    nRestarts(pPar->nRestarts),
+    nJobs(pPar->nJobs),
     fMultiThreading(pPar->nThreads > 1),
-    fPartitioning(pPar->nWindowSize > 0),
+    fPartitioning(pPar->nPartitionSize > 0),
     fDeterministic(pPar->fDeterministic),
+    nParallelPartitions(pPar->nParallelPartitions),
+    fOptOnInsert(pPar->fOptOnInsert),
     nTimeout(pPar->nTimeout),
-    nJobs(0),
+    nCreatedJobs(0),
     nFinishedJobs(0),
     par(pPar),
     pOpt(NULL) {
@@ -409,8 +415,8 @@ namespace rrr {
     pOpt = new Opt(pPar, CostFunction);
   }
 
-  template <typename Ntk, typename Opt>
-  Scheduler<Ntk, Opt>::~Scheduler() {
+  template <typename Ntk, typename Opt, typename Par>
+  Scheduler<Ntk, Opt, Par>::~Scheduler() {
 #ifdef ABC_USE_PTHREADS
     if(fMultiThreading) {
       {
@@ -430,45 +436,56 @@ namespace rrr {
   /* }}} */
 
   /* {{{ Run */
-  
-  template <typename Ntk, typename Opt>
-  void Scheduler<Ntk, Opt>::Run() {
+
+  template <typename Ntk, typename Opt, typename Par>
+  void Scheduler<Ntk, Opt, Par>::Run() {
     start = GetCurrentTime();
     if(fPartitioning) {
+      fDeterministic = false; // it is deterministic anyways as we wait until all jobs finish each round
       pNtk->Sweep();
       par.UpdateNetwork(pNtk);
-      while(nJobs < nRestarts) {
-        Ntk *pSubNtk = par.Extract(iSeed + nJobs);
-        if(pSubNtk == NULL) {
-          if(nJobs == nFinishedJobs) {
-            std::cout << "failed to extract a window" << std::endl;
-            break;
+      while(nCreatedJobs < nJobs) {
+        assert(nParallelPartitions > 0);
+        if(nCreatedJobs < nFinishedJobs + nParallelPartitions) {
+          Ntk *pSubNtk = par.Extract(iSeed + nCreatedJobs);
+          if(pSubNtk) {
+            CreateJob(pSubNtk, iSeed + nCreatedJobs);
+            std::cout << "job " << nCreatedJobs - 1 << " created (size = " << pSubNtk->GetNumInts() << ")" << std::endl;
+            continue;
           }
-          while(nFinishedJobs < nJobs) {
-            OnJobEnd([&](Job *pJob) {
-              std::cout << "job " << pJob->id << " finished (size = " << pJob->pNtk->GetNumInts() << ")" << std::endl;
-              par.Insert(pJob->pNtk);
-            });
-          }
-        } else {
-          CreateJob(pSubNtk, iSeed + nJobs);
-          std::cout << "job " << nJobs - 1 << " created (size = " << pSubNtk->GetNumInts() << ")" << std::endl;
+        }
+        if(nCreatedJobs == nFinishedJobs) {
+          std::cout << "failed to partition" << std::endl;
+          break;
+        }
+        while(nFinishedJobs < nCreatedJobs) {
+          OnJobEnd([&](Job *pJob) {
+            std::cout << "job " << pJob->id << " finished (size = " << pJob->pNtk->GetNumInts() << ")" << std::endl;
+            par.Insert(pJob->pNtk);
+          });
+        }
+        if(fOptOnInsert) {
+          CallAbc(pNtk, std::string("&put; ") + pCompress2rs + "; dc2; &get");
+          par.UpdateNetwork(pNtk);
         }
       }
-      while(nFinishedJobs < nJobs) {
+      while(nFinishedJobs < nCreatedJobs) {
         OnJobEnd([&](Job *pJob) {
           std::cout << "job " << pJob->id << " finished (size = " << pJob->pNtk->GetNumInts() << ")" << std::endl;
           par.Insert(pJob->pNtk);
         });
       }
-    } else if(nRestarts > 0) {
-      fDeterministic = false; // it is deterministic anyways
+      if(fOptOnInsert) {
+        CallAbc(pNtk, std::string("&put; ") + pCompress2rs + "; dc2; &get");
+        par.UpdateNetwork(pNtk);
+      }
+    } else if(nJobs > 1) {
       double dCost = CostFunction(pNtk);
-      for(int i = 0; i < 1 + nRestarts; i++) {
+      for(int i = 0; i < nJobs; i++) {
         Ntk *pCopy = new Ntk(*pNtk);
         CreateJob(pCopy, iSeed + i);
       }
-      for(int i = 0; i < 1 + nRestarts; i++) {
+      for(int i = 0; i < nJobs; i++) {
         OnJobEnd([&](Job *pJob) {
           double dNewCost = CostFunction(pJob->pNtk);
           if(nVerbose) {
diff --git a/src/opt/rrr/rrrSimulator.h b/src/opt/rrr/rrrSimulator.h
index 8d5c80c87..b1d7296e7 100644
--- a/src/opt/rrr/rrrSimulator.h
+++ b/src/opt/rrr/rrrSimulator.h
@@ -19,6 +19,7 @@ namespace rrr {
     using itr = std::vector<word>::iterator;
     using citr = std::vector<word>::const_iterator;
     static constexpr word one = 0xffffffffffffffff;
+    static constexpr bool fKeepStimula = true;
 
     // pointer to network
     Ntk *pNtk;
@@ -522,15 +523,54 @@ namespace rrr {
   void Simulator<Ntk>::Load(int slot) {
     assert(slot >= 0);
     assert(slot < int_size(vBackups));
-    nWords  = vBackups[slot].nWords;
-    target  = vBackups[slot].target;
-    vValues = vBackups[slot].vValues;
-    care    = vBackups[slot].care;
-    iPivot  = vBackups[slot].iPivot;
-    vAssignedStimuli = vBackups[slot].vAssignedStimuli;
     fUpdate = false;
     sUpdates.clear();
-    tmp.resize(nWords);
+    if(!fKeepStimula) {
+      nWords  = vBackups[slot].nWords;
+      target  = vBackups[slot].target;
+      vValues = vBackups[slot].vValues;
+      care    = vBackups[slot].care;
+      iPivot  = vBackups[slot].iPivot;
+      vAssignedStimuli = vBackups[slot].vAssignedStimuli;
+      tmp.resize(nWords);
+    } else {
+      std::vector<int> vOffsets;
+      for(int i = 0; i < vBackups[slot].nWords; i++) {
+        bool fDifferent = false;
+        pNtk->ForEachPi([&](int id) {
+          if(vValues[id * vBackups[slot].nWords + i] != vValues[id * nWords + i]) {
+            fDifferent = true;
+          }
+        });
+        if(fDifferent) {
+          vOffsets.push_back(i);
+        }
+      }
+      if(nWords == vBackups[slot].nWords) {
+        if(vOffsets.empty()) {
+          target  = vBackups[slot].target;
+          vValues = vBackups[slot].vValues;
+          care    = vBackups[slot].care;
+        } else {
+          target = -1;
+          std::vector<std::vector<word>> vInputStimuli(pNtk->GetNumPis());
+          pNtk->ForEachPiIdx([&](int idx, int id) {
+            vInputStimuli[idx].resize(nWords);
+            Copy(nWords, vInputStimuli[idx].begin(), vValues.begin() + id * nWords, false);
+          });
+          vValues = vBackups[slot].vValues;
+          pNtk->ForEachPiIdx([&](int idx, int id) {
+            Copy(nWords, vValues.begin() + id * nWords, vInputStimuli[idx].begin(), false);
+          });
+          for(int i: vOffsets) {
+            SimulateOneWord(i);
+          }
+        }
+      } else {
+        // when nWords has changed
+        assert(0);
+      }
+    }
   }
   
   /* }}} */
@@ -574,12 +614,13 @@ namespace rrr {
   void Simulator<Ntk>::UpdateNetwork(Ntk *pNtk_, bool fSame) {
     pNtk = pNtk_;
     pNtk->AddCallback(std::bind(&Simulator<Ntk>::ActionCallback, this, std::placeholders::_1));
+    // TODO: what if nWords has changed? shall we reset it to default?
     vValues.resize(nWords * pNtk->GetNumNodes());
     target = -1;
-    iPivot = 0;
     fUpdate = false;
     sUpdates.clear();
     if(!fSame) { // reset stimuli if network function changed
+      iPivot = 0;
       vAssignedStimuli.clear();
       vAssignedStimuli.resize(nWords * pNtk->GetNumPis());
       GenerateRandomStimuli();
@@ -771,6 +812,7 @@ namespace rrr {
       if(nVerbose) {
         std::cout << "recomputing careset of " << target << std::endl;
       }
+      vValues2.resize(vValues.size());
       pNtk->ForEachPi([&](int id) {
         vValues2[id * nWords + iWord] = vValues[id * nWords + iWord];
       });
diff --git a/src/opt/rrr/rrrUtils.h b/src/opt/rrr/rrrUtils.h
index f41593d52..b05a47625 100644
--- a/src/opt/rrr/rrrUtils.h
+++ b/src/opt/rrr/rrrUtils.h
@@ -2,6 +2,7 @@
 
 #include <iostream>
 #include <iomanip>
+#include <sstream>
 #include <vector>
 #include <set>
 #include <string>
@@ -30,13 +31,13 @@ namespace rrr {
 
   /* {{{ Int size */
   
-  template <template <typename...> typename Container, typename ... Ts>
+  template <template <typename...> typename Container, typename... Ts>
   static inline int int_size(Container<Ts...> const &c) {
     assert(c.size() <= (typename Container<Ts...>::size_type)std::numeric_limits<int>::max());
     return c.size();
   }
 
-  template <template <typename...> typename Container, typename ... Ts>
+  template <template <typename...> typename Container, typename... Ts>
   static inline bool check_int_size(Container<Ts...> const &c) {
     return c.size() <= (typename Container<Ts...>::size_type)std::numeric_limits<int>::max();
   }
@@ -44,11 +45,19 @@ namespace rrr {
   static inline bool check_int_max(int i) {
     return i == std::numeric_limits<int>::max();
   }
+
+  template <typename Iterator>
+  static inline int int_distance(Iterator begin, Iterator it) {
+    typename std::iterator_traits<Iterator>::difference_type d = std::distance(begin, it);
+    assert(d <= (typename std::iterator_traits<Iterator>::difference_type)std::numeric_limits<int>::max());
+    assert(d >= (typename std::iterator_traits<Iterator>::difference_type)std::numeric_limits<int>::lowest());
+    return d;
+  }
   
   /* }}} */
   
-  /* {{{ Print helpers */
-
+  /* {{{ Print containers */
+  
   template <typename T>
   std::ostream& operator<<(std::ostream& os, const std::vector<T>& v) {
     std::string delim;
@@ -83,6 +92,158 @@ namespace rrr {
     std::cout << "]";
   }
 
+  /* }}} */
+
+  /* {{{ Print next */
+
+  struct SW {
+    int width;
+  };
+
+  struct NS {}; // no space
+
+  template <typename T>
+  void PrintNext(std::ostream &os, T t);
+  template <typename T, typename... Args>
+  void PrintNext(std::ostream &os, T t, Args... args);
+  
+  static inline void PrintNext(std::ostream &os, bool arg) {
+    os << arg;
+  }
+  
+  template <typename... Args>
+  static inline void PrintNext(std::ostream &os, bool arg, Args... args) {
+    if(arg) {
+      os << "!";
+    } else {
+      os << " ";
+    }
+    PrintNext(os, args...);
+  }
+  
+  static inline void PrintNext(std::ostream &os, int t) {
+    os << std::setw(4) << t;
+  }
+
+  template <typename... Args>
+  static inline void PrintNext(std::ostream &os, int t, Args... args) {
+    os << std::setw(4) << t << " ";
+    PrintNext(os, args...);
+  }
+
+  static inline void PrintNext(std::ostream &os, double t) {
+    os << std::fixed << std::setprecision(2) << std::setw(8) << t;
+  }
+
+  template <typename... Args>
+  static inline void PrintNext(std::ostream &os, double t, Args... args) {
+    os << std::fixed << std::setprecision(2) << std::setw(8) << t << " ";
+    PrintNext(os, args...);
+  }
+
+  template <typename T>
+  static inline void PrintNext(std::ostream &os, SW sw, T arg) {
+    os << std::setw(sw.width) << arg;
+  }
+
+  template <typename T, typename... Args>
+  static inline void PrintNext(std::ostream &os, SW sw, T arg, Args... args) {
+    os << std::setw(sw.width) << arg << " ";
+    PrintNext(os, args...);
+  }
+
+  template <typename T, typename... Args>
+  static inline void PrintNext(std::ostream &os, NS ns, T arg, Args... args) {
+    (void)ns;
+    os << arg;
+    PrintNext(os, args...);
+  }
+  
+  template <typename T>
+  static inline void PrintNext(std::ostream& os, std::vector<T> const &arg) {
+    std::string delim;
+    os << "[";
+    for(T const &e: arg) {
+      os << delim;
+      PrintNext(os, e);
+      delim = ", ";
+    }
+    os << "]";
+  }
+
+  template <typename T, typename... Args>
+  static inline void PrintNext(std::ostream& os, std::vector<T> const &arg, Args... args) {
+    std::string delim;
+    os << "[";
+    for(T const &e: arg) {
+      os << delim;
+      PrintNext(os, e);
+      delim = ", ";
+    }
+    os << "] ";
+    PrintNext(os, args...);
+  }
+
+  template <typename T>
+  static inline void PrintNext(std::ostream& os, std::set<T> const &arg) {
+    std::string delim;
+    os << "{";
+    for(T const &e: arg) {
+      os << delim;
+      PrintNext(os, e);
+      delim = ", ";
+    }
+    os << "}";
+  }
+
+  template <typename T, typename... Args>
+  static inline void PrintNext(std::ostream& os, std::set<T> const &arg, Args... args) {
+    std::string delim;
+    os << "{";
+    for(T const &e: arg) {
+      os << delim;
+      PrintNext(os, e);
+      delim = ", ";
+    }
+    os << "} ";
+    PrintNext(os, args...);
+  }
+  
+  template <typename T>
+  void PrintNext(std::ostream &os, T t) {
+    os << t;
+  }
+
+  template <typename T, typename... Args>
+  void PrintNext(std::ostream &os, T t, Args... args) {
+    os << t << " ";
+    PrintNext(os, args...);
+  }  
+  
+  /* }}} */
+
+  /* {{{ Combination */
+
+  bool ForEachCombinationStopRec(std::vector<int> &v, int n, int k, std::function<bool(std::vector<int> const &)> const &func) {
+    if(k == 0) {
+      return func(v);
+    }
+    for(int i = v.back() + 1; i < n - k + 1; i++) {
+      v.push_back(i);
+      if(ForEachCombinationStopRec(v, n, k-1, func)) {
+        return true;
+      }
+      v.pop_back();
+    }
+    return false;
+  }
+  
+  static inline void ForEachCombinationStop(int n, int k, std::function<bool(std::vector<int> const &)> const &func) {
+    std::vector<int> v;
+    v.reserve(k);
+    ForEachCombinationStopRec(v, n, k, func);
+  }
+  
   /* }}} */
   
   /* {{{ VarValue functions */
@@ -102,6 +263,7 @@ namespace rrr {
     default:
       assert(0);
     }
+    return UNDEF;
   }
 
   static inline char GetVarValueChar(VarValue x) {
@@ -119,73 +281,77 @@ namespace rrr {
     default:
       assert(0);
     }
+    return 'X';
   }
 
   /* }}} */
 
   /* {{{ Action functions */
-
-  static inline void PrintAction(Action action) {
+  
+  static inline char const *GetActionTypeCstr(Action const &action) {
     switch(action.type) {
     case REMOVE_FANIN:
-      std::cout << "remove fanin";
-      break;
+      return "remove fanin";
     case REMOVE_UNUSED:
-      std::cout << "remove unused";
-      break;
+      return "remove unused";
     case REMOVE_BUFFER:
-      std::cout << "remove buffer";
-      break;
+      return "remove buffer";
     case REMOVE_CONST:
-      std::cout << "remove const";
-      break;
+      return "remove const";
     case ADD_FANIN:
-      std::cout << "add fanin";
-      break;
+      return "add fanin";
     case TRIVIAL_COLLAPSE:
-      std::cout << "trivial collapse";
-      break;
+      return "trivial collapse";
     case TRIVIAL_DECOMPOSE:
-      std::cout << "trivial decompose";
-      break;
+      return "trivial decompose";
     case SORT_FANINS:
-      std::cout << "sort fanins";
-      break;
+      return "sort fanins";
     case SAVE:
-      std::cout << "save";
-      break;
+      return "save";
     case LOAD:
-      std::cout << "load";
-      break;
+      return "load";
     case POP_BACK:
-      std::cout << "pop back";
-      break;
+      return "pop back";
     case INSERT:
-      std::cout << "insert";
-      break;
+      return "insert";
     default:
       assert(0);
     }
-    std::cout << ":";
+    return "";
+  }
+
+  static inline std::stringstream GetActionDescription(Action const &action) {
+    std::stringstream ss;
+    ss << GetActionTypeCstr(action);
+    std::string delim = ": ";
     if(action.id != -1) {
-      std::cout << " node " << action.id;
+      ss << delim;
+      PrintNext(ss, "node", action.id);
+      delim = ", ";
     }
     if(action.fi != -1) {
-      std::cout << " fanin " << (action.c? "!": "") << action.fi;
+      ss << delim;
+      PrintNext(ss, "fanin", (bool)action.c, action.fi);
+      delim = ", ";
     }
     if(action.idx != -1) {
-      std::cout << " index " << action.idx;
+      ss << delim;
+      PrintNext(ss, "index", action.idx);
     }
-    std::cout << std::endl;
+    ss << std::endl;
     if(!action.vFanins.empty()) {
-      std::cout << "\t" << "fanins: " << action.vFanins << std::endl;
+      ss << "fanins: ";
+      PrintNext(ss, action.vFanins);
     }
     if(!action.vIndices.empty()) {
-      std::cout << "\t" << "indices: " << action.vIndices << std::endl;
+      ss << "indices: ";
+      PrintNext(ss, action.vIndices);
     }
     if(!action.vFanouts.empty()) {
-      std::cout << "\t" << "fanouts: " << action.vFanouts << std::endl;
+      ss << "fanouts: ";
+      PrintNext(ss, action.vFanouts);
     }
+    return ss;
   }
 
   /* }}} */