diff --git a/CMakeLists.txt b/CMakeLists.txt
index 05a47b82a..0b73b4cdd 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -13,6 +13,7 @@ option(BILL_Z3 "Enable Z3 interface for bill library" OFF)
 option(ENABLE_COVERAGE "Enable coverage reporting for gcc/clang" OFF)
 option(ENABLE_MATPLOTLIB "Enable matplotlib library in experiments" OFF)
 option(ENABLE_NAUTY "Enable the Nauty library for percy" OFF)
+option(ENABLE_ABC "Enable linking ABC as a static library" OFF)
 
 if(UNIX)
   # show quite some warnings (but remove some intentionally)
@@ -42,6 +43,12 @@ if(ENABLE_NAUTY)
   add_definitions(-DENABLE_NAUTY)
 endif()
 
+if (ENABLE_ABC)
+  if (NOT EXISTS ${PROJECT_SOURCE_DIR}/lib/abc_static/libabc.a)
+    message(FATAL_ERROR "Cannot find libabc.a in lib/abc_static/. For more info, see https://github.com/lsils/abc-staticlib")
+  endif()
+endif()
+
 if(MOCKTURTLE_EXAMPLES)
   add_subdirectory(examples)
 endif()
diff --git a/experiments/explorer.cpp b/experiments/explorer.cpp
new file mode 100644
index 000000000..fbe385e21
--- /dev/null
+++ b/experiments/explorer.cpp
@@ -0,0 +1,233 @@
+/* mockturtle: C++ logic network library
+ * Copyright (C) 2018-2022  EPFL
+ *
+ * Permission is hereby granted, free of charge, to any person
+ * obtaining a copy of this software and associated documentation
+ * files (the "Software"), to deal in the Software without
+ * restriction, including without limitation the rights to use,
+ * copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the
+ * Software is furnished to do so, subject to the following
+ * conditions:
+ *
+ * The above copyright notice and this permission notice shall be
+ * included in all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+ * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
+ * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
+ * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+ * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+ * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+ * OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+#ifdef ENABLE_ABC
+
+#include <lorina/aiger.hpp>
+#include <mockturtle/algorithms/explorer.hpp>
+#include <mockturtle/io/aiger_reader.hpp>
+#include <mockturtle/io/verilog_reader.hpp>
+#include <mockturtle/networks/mig.hpp>
+#include <mockturtle/networks/aig.hpp>
+#include <mockturtle/views/depth_view.hpp>
+#include <mockturtle/algorithms/aqfp/buffer_insertion.hpp>
+#include <mockturtle/algorithms/aqfp/buffer_verification.hpp>
+#include <mockturtle/networks/buffered.hpp>
+
+#include <experiments.hpp>
+#include <fmt/format.h>
+#include <string>
+
+using namespace mockturtle;
+
+static const std::string benchmark_repo_path = "../../SCE-benchmarks";
+
+/* AQFP benchmarks */
+std::vector<std::string> aqfp_benchmarks = {
+    "5xp1", "c1908", "c432", "c5315", "c880", "chkn", "count", "dist", "in5", "in6", "k2",
+    "m3", "max512", "misex3", "mlp4", "prom2", "sqr6", "x1dn" };
+
+std::string benchmark_aqfp_path( std::string const& benchmark_name )
+{
+  return fmt::format( "{}/MCNC/original/{}.v", benchmark_repo_path, benchmark_name );
+}
+
+mig_network ale_flow( aig_network const& ntk )
+{
+    aig_network aig = call_abc_script( ntk, "&c2rs" );
+    mig_network _ntk = cleanup_dangling<aig_network, mig_network>( aig );
+    mig_npn_resynthesis resyn{ true };
+    exact_library_params eps;
+    eps.np_classification = false;
+    eps.compute_dc_classes = true;
+    exact_library<mig_network> exact_lib( resyn, eps );
+    
+    map_params mps;
+    mps.skip_delay_round = true;
+    mps.required_time = std::numeric_limits<double>::max();
+    mps.ela_rounds = 2;
+    mps.enable_logic_sharing = true;
+    mps.use_dont_cares = true;
+    mps.window_size = 12;
+    mps.logic_sharing_cut_limit = 1;
+    mps.cut_enumeration_ps.cut_limit = 8;
+    
+    rewrite_params rwps;
+    rwps.allow_zero_gain = true;
+    rwps.window_size = 8;
+
+    resubstitution_params rsps;
+    rsps.max_inserts = 2;
+    rsps.max_pis = 8;
+    
+    for ( int i = 0; i < 3; ++i )
+    {
+      auto tmp = map( _ntk, exact_lib, mps );
+      if ( tmp.size() >= _ntk.size() )
+        break;
+      _ntk = tmp;
+    }
+
+    for ( int i = 0; i < 3; ++i )
+    {
+      rwps.use_dont_cares = i == 1;
+      auto size_before = _ntk.size();
+      rewrite( _ntk, exact_lib, rwps );
+      _ntk = cleanup_dangling( _ntk );
+      if ( _ntk.size() >= size_before )
+        break;
+    }
+
+    while ( true )
+    {
+      auto size_before = _ntk.size();
+      auto mig_resub = cleanup_dangling( _ntk );
+
+      depth_view depth_mig{ mig_resub };
+      fanout_view fanout_mig{ depth_mig };
+
+      mig_resubstitution( fanout_mig, rsps );
+      mig_resub = cleanup_dangling( mig_resub );
+
+      if ( mig_resub.size() >= size_before )
+        break;
+      _ntk = mig_resub;
+    }
+
+    rsps.max_inserts = std::numeric_limits<uint32_t>::max();
+    sim_resubstitution( _ntk, rsps );
+    _ntk = cleanup_dangling( _ntk );
+    return _ntk;
+}
+
+int main_aqfp( int argc, char* argv[] )
+{
+  using namespace experiments;
+
+  experiment<std::string, uint32_t, uint32_t, uint32_t, uint32_t, uint32_t, float, float, bool, bool> exp( "deepsyn_aqfp", "benchmark", "#JJ", "JJ depth", "JJ EDP", "MIG size", "MIG depth", "t total", "t eval", "cec", "verified" );
+
+  for ( auto const& benchmark : aqfp_benchmarks )
+  {
+    if ( argc == 2 && benchmark != std::string( argv[1] ) ) continue;
+    fmt::print( "[i] processing {}\n", benchmark );
+
+    mig_network ntk;
+    if ( lorina::read_verilog( benchmark_aqfp_path( benchmark ), verilog_reader( ntk ) ) != lorina::return_code::success )
+    {
+      std::cerr << "Cannot read " << benchmark << "\n";
+      return -1;
+    }
+
+    explorer_params ps;
+    explorer_stats st;
+    ps.num_restarts = 5;
+    ps.random_seed = 3252;
+    ps.max_steps_no_impr = 50;
+    ps.timeout = 100;
+    ps.compressing_scripts_per_step = 3;
+    ps.verbose = true;
+    //ps.very_verbose = true;
+
+    mig_network opt = deepsyn_aqfp( ntk, ps, &st );
+    depth_view d( opt );
+
+    aqfp_assumptions_legacy aqfp_ps;
+    aqfp_ps.splitter_capacity = 4;
+    aqfp_ps.branch_pis = true;
+    aqfp_ps.balance_pis = true;
+    aqfp_ps.balance_pos = true;
+
+    buffer_insertion_params bps;
+    bps.assume = legacy_to_realistic( aqfp_ps );
+    bps.scheduling = buffer_insertion_params::better_depth;
+    bps.optimization_effort = buffer_insertion_params::until_sat;
+    buffer_insertion buf_inst( opt, bps );
+
+    buffered_mig_network buffered_mig;
+    auto num_buffers = buf_inst.run( buffered_mig );
+    auto JJ_depth = buf_inst.depth();
+    auto JJ_count = opt.num_gates() * 6 + num_buffers * 2;
+    auto JJ_EDP = JJ_depth * JJ_count;
+    bool cec = abc_cec_impl( buffered_mig, benchmark_aqfp_path( benchmark ) );
+    bool bv = verify_aqfp_buffer( buffered_mig, bps.assume, buf_inst.pi_levels() );
+    //write_verilog( buffered_mig, benchmark + ".v" );
+
+    exp( benchmark, JJ_count, JJ_depth, JJ_EDP, opt.num_gates(), d.depth(), to_seconds(st.time_total), to_seconds(st.time_evaluate), cec, bv );
+  }
+
+  exp.save();
+  exp.table();
+
+  return 0;
+}
+
+int main( int argc, char* argv[] )
+{
+  using namespace experiments;
+  using namespace mockturtle;
+
+  experiment<std::string, uint32_t, uint32_t, uint32_t, float, bool> exp( "deepsyn_mig", "benchmark", "size_before", "size_after", "depth", "runtime", "cec" );
+
+  for ( auto const& benchmark : epfl_benchmarks() )
+  {
+    if ( argc == 2 && benchmark != std::string( argv[1] ) ) continue;
+    //if ( benchmark == "hyp" && argc == 1 ) continue;
+    fmt::print( "[i] processing {}\n", benchmark );
+
+    using Ntk = mig_network;
+    Ntk ntk;
+    if ( lorina::read_aiger( benchmark_path( benchmark ), aiger_reader( ntk ) ) != lorina::return_code::success )
+    {
+      std::cerr << "Cannot read " << benchmark << "\n";
+      return -1;
+    }
+
+    explorer_params ps;
+    ps.num_restarts = 4;
+    ps.random_seed = 42124;
+    ps.timeout = std::max(1000u, ntk.num_gates()/10);
+    ps.max_steps_no_impr = 50;
+    ps.compressing_scripts_per_step = 1;
+    ps.verbose = true;
+    //ps.very_verbose = true;
+
+    stopwatch<>::duration rt{0};
+    Ntk opt = call_with_stopwatch( rt, [&](){ return deepsyn_mig_v1( ntk, ps ); } );
+    //write_verilog( opt, "best_MIGs/" + benchmark + ".v" );
+    bool const cec = ( benchmark == "hyp" ) ? true : abc_cec_impl( opt, benchmark_path( benchmark ) );
+    depth_view d( opt );
+
+    exp( benchmark, ntk.num_gates(), opt.num_gates(), d.depth(), to_seconds(rt), cec );
+  }
+
+  exp.save();
+  exp.table();
+
+  return 0;
+}
+#else
+int main()
+{}
+#endif
diff --git a/include/CMakeLists.txt b/include/CMakeLists.txt
index 114d3492a..808310180 100644
--- a/include/CMakeLists.txt
+++ b/include/CMakeLists.txt
@@ -5,3 +5,9 @@ target_link_libraries(mockturtle INTERFACE kitty lorina parallel_hashmap percy j
 if(CMAKE_CXX_COMPILER_ID STREQUAL "GNU" AND CMAKE_CXX_COMPILER_VERSION VERSION_LESS 9)
 target_link_libraries(mockturtle INTERFACE stdc++fs)
 endif()
+
+if(ENABLE_ABC)
+target_link_libraries(mockturtle INTERFACE ${PROJECT_SOURCE_DIR}/lib/abc_static/libabc.a)
+target_link_libraries(mockturtle INTERFACE dl)
+target_compile_definitions(mockturtle INTERFACE ENABLE_ABC)
+endif()
\ No newline at end of file
diff --git a/include/mockturtle/algorithms/aig_resub.hpp b/include/mockturtle/algorithms/aig_resub.hpp
index 68f0dca30..d7eea28c5 100644
--- a/include/mockturtle/algorithms/aig_resub.hpp
+++ b/include/mockturtle/algorithms/aig_resub.hpp
@@ -179,14 +179,14 @@ struct aig_resub_functor
   {
   }
 
-  std::optional<signal> operator()( node const& root, TT care, uint32_t required, uint32_t max_inserts, uint32_t num_mffc, uint32_t& last_gain )
+  std::optional<signal> operator()( node const& root, TT care, uint32_t max_depth, uint32_t max_inserts, uint32_t num_mffc, uint32_t& last_gain )
   {
     (void)care;
     assert( is_const0( ~care ) );
 
     /* consider constants */
     auto g = call_with_stopwatch( st.time_resubC, [&]() {
-      return resub_const( root, required );
+      return resub_const( root );
     } );
     if ( g )
     {
@@ -197,7 +197,7 @@ struct aig_resub_functor
 
     /* consider equal nodes */
     g = call_with_stopwatch( st.time_resub0, [&]() {
-      return resub_div0( root, required );
+      return resub_div0( root, max_depth );
     } );
     if ( g )
     {
@@ -211,12 +211,12 @@ struct aig_resub_functor
 
     /* collect level one divisors */
     call_with_stopwatch( st.time_collect_unate_divisors, [&]() {
-      collect_unate_divisors( root, required );
+      collect_unate_divisors( root, max_depth );
     } );
 
     /* consider equal nodes */
     g = call_with_stopwatch( st.time_resub1, [&]() {
-      return resub_div1( root, required );
+      return resub_div1( root, max_depth );
     } );
     if ( g )
     {
@@ -229,7 +229,7 @@ struct aig_resub_functor
       return std::nullopt;
 
     /* consider triples */
-    g = call_with_stopwatch( st.time_resub12, [&]() { return resub_div12( root, required ); } );
+    g = call_with_stopwatch( st.time_resub12, [&]() { return resub_div12( root, max_depth ); } );
     if ( g )
     {
       ++st.num_div12_accepts;
@@ -239,11 +239,11 @@ struct aig_resub_functor
 
     /* collect level two divisors */
     call_with_stopwatch( st.time_collect_binate_divisors, [&]() {
-      collect_binate_divisors( root, required );
+      collect_binate_divisors( root, max_depth );
     } );
 
     /* consider two nodes */
-    g = call_with_stopwatch( st.time_resub2, [&]() { return resub_div2( root, required ); } );
+    g = call_with_stopwatch( st.time_resub2, [&]() { return resub_div2( root, max_depth ); } );
     if ( g )
     {
       ++st.num_div2_accepts;
@@ -255,7 +255,7 @@ struct aig_resub_functor
       return std::nullopt;
 
     /* consider three nodes */
-    g = call_with_stopwatch( st.time_resub3, [&]() { return resub_div3( root, required ); } );
+    g = call_with_stopwatch( st.time_resub3, [&]() { return resub_div3( root, max_depth ); } );
     if ( g )
     {
       ++st.num_div3_accepts;
@@ -266,9 +266,8 @@ struct aig_resub_functor
     return std::nullopt;
   }
 
-  std::optional<signal> resub_const( node const& root, uint32_t required ) const
+  std::optional<signal> resub_const( node const& root ) const
   {
-    (void)required;
     auto const tt = sim.get_tt( ntk.make_signal( root ) );
     if ( tt == sim.get_tt( ntk.get_constant( false ) ) )
     {
@@ -277,9 +276,9 @@ struct aig_resub_functor
     return std::nullopt;
   }
 
-  std::optional<signal> resub_div0( node const& root, uint32_t required ) const
+  std::optional<signal> resub_div0( node const& root, uint32_t max_depth ) const
   {
-    (void)required;
+    (void)max_depth;
     auto const tt = sim.get_tt( ntk.make_signal( root ) );
     for ( auto i = 0u; i < num_divs; ++i )
     {
@@ -287,13 +286,14 @@ struct aig_resub_functor
       if ( tt != sim.get_tt( ntk.make_signal( d ) ) )
         continue; /* next */
 
+      assert( ntk.level( d ) <= max_depth );
       return ( sim.get_phase( d ) ^ sim.get_phase( root ) ) ? !ntk.make_signal( d ) : ntk.make_signal( d );
     }
 
     return std::nullopt;
   }
 
-  void collect_unate_divisors( node const& root, uint32_t required )
+  void collect_unate_divisors( node const& root, uint32_t max_depth )
   {
     udivs.clear();
 
@@ -302,7 +302,7 @@ struct aig_resub_functor
     {
       auto const d = divs.at( i );
 
-      if ( ntk.level( d ) > required - 1 )
+      if ( ntk.level( d ) > max_depth - 1 )
         continue;
 
       auto const& tt_d = sim.get_tt( ntk.make_signal( d ) );
@@ -340,9 +340,9 @@ struct aig_resub_functor
     }
   }
 
-  std::optional<signal> resub_div1( node const& root, uint32_t required )
+  std::optional<signal> resub_div1( node const& root, uint32_t max_depth )
   {
-    (void)required;
+    (void)max_depth;
     auto const& tt = sim.get_tt( ntk.make_signal( root ) );
 
     /* check for positive unate divisors */
@@ -362,6 +362,7 @@ struct aig_resub_functor
           ++st.num_div1_or_accepts;
           auto const l = sim.get_phase( ntk.get_node( s0 ) ) ? !s0 : s0;
           auto const r = sim.get_phase( ntk.get_node( s1 ) ) ? !s1 : s1;
+          assert( ntk.level( ntk.get_node( l ) ) <= max_depth - 1 && ntk.level( ntk.get_node( r ) ) <= max_depth - 1 );
           return sim.get_phase( root ) ? !ntk.create_or( l, r ) : ntk.create_or( l, r );
         }
       }
@@ -384,6 +385,7 @@ struct aig_resub_functor
           ++st.num_div1_and_accepts;
           auto const l = sim.get_phase( ntk.get_node( s0 ) ) ? !s0 : s0;
           auto const r = sim.get_phase( ntk.get_node( s1 ) ) ? !s1 : s1;
+          assert( ntk.level( ntk.get_node( l ) ) <= max_depth - 1 && ntk.level( ntk.get_node( r ) ) <= max_depth - 1 );
           return sim.get_phase( root ) ? !ntk.create_and( l, r ) : ntk.create_and( l, r );
         }
       }
@@ -392,9 +394,8 @@ struct aig_resub_functor
     return std::nullopt;
   }
 
-  std::optional<signal> resub_div12( node const& root, uint32_t required )
+  std::optional<signal> resub_div12( node const& root, uint32_t max_depth )
   {
-    (void)required;
     auto const s = ntk.make_signal( root );
     auto const& tt = sim.get_tt( s );
 
@@ -420,7 +421,7 @@ struct aig_resub_functor
             auto const max_level = std::max( { ntk.level( ntk.get_node( s0 ) ),
                                                ntk.level( ntk.get_node( s1 ) ),
                                                ntk.level( ntk.get_node( s2 ) ) } );
-            assert( max_level <= required - 1 );
+            assert( max_level <= max_depth - 1 );
 
             signal max = s0;
             signal min0 = s1;
@@ -438,6 +439,9 @@ struct aig_resub_functor
               min1 = s1;
             }
 
+            if ( ntk.level( ntk.get_node( min0 ) ) > max_level - 2 || ntk.level( ntk.get_node( min1 ) ) > max_level - 2 )
+              continue;
+
             auto const a = sim.get_phase( ntk.get_node( max ) ) ? !max : max;
             auto const b = sim.get_phase( ntk.get_node( min0 ) ) ? !min0 : min0;
             auto const c = sim.get_phase( ntk.get_node( min1 ) ) ? !min1 : min1;
@@ -471,7 +475,7 @@ struct aig_resub_functor
             auto const max_level = std::max( { ntk.level( ntk.get_node( s0 ) ),
                                                ntk.level( ntk.get_node( s1 ) ),
                                                ntk.level( ntk.get_node( s2 ) ) } );
-            assert( max_level <= required - 1 );
+            assert( max_level <= max_depth - 1 );
 
             signal max = s0;
             signal min0 = s1;
@@ -489,6 +493,9 @@ struct aig_resub_functor
               min1 = s1;
             }
 
+            if ( ntk.level( ntk.get_node( min0 ) ) > max_level - 2 || ntk.level( ntk.get_node( min1 ) ) > max_level - 2 )
+              continue;
+
             auto const a = sim.get_phase( ntk.get_node( max ) ) ? !max : max;
             auto const b = sim.get_phase( ntk.get_node( min0 ) ) ? !min0 : min0;
             auto const c = sim.get_phase( ntk.get_node( min1 ) ) ? !min1 : min1;
@@ -503,7 +510,7 @@ struct aig_resub_functor
     return std::nullopt;
   }
 
-  void collect_binate_divisors( node const& root, uint32_t required )
+  void collect_binate_divisors( node const& root, uint32_t max_depth )
   {
     bdivs.clear();
 
@@ -511,13 +518,13 @@ struct aig_resub_functor
     for ( auto i = 0u; i < udivs.next_candidates.size(); ++i )
     {
       auto const& s0 = udivs.next_candidates.at( i );
-      if ( ntk.level( ntk.get_node( s0 ) ) > required - 2 )
+      if ( ntk.level( ntk.get_node( s0 ) ) > max_depth - 2 )
         continue;
 
       for ( auto j = i + 1; j < udivs.next_candidates.size(); ++j )
       {
         auto const& s1 = udivs.next_candidates.at( j );
-        if ( ntk.level( ntk.get_node( s1 ) ) > required - 2 )
+        if ( ntk.level( ntk.get_node( s1 ) ) > max_depth - 2 )
           continue;
 
         if ( bdivs.positive_divisors0.size() < 500 ) // ps.max_divisors2
@@ -581,9 +588,9 @@ struct aig_resub_functor
     }
   }
 
-  std::optional<signal> resub_div2( node const& root, uint32_t required )
+  std::optional<signal> resub_div2( node const& root, uint32_t max_depth )
   {
-    (void)required;
+    (void)max_depth;
     auto const s = ntk.make_signal( root );
     auto const& tt = sim.get_tt( s );
 
@@ -607,6 +614,8 @@ struct aig_resub_functor
         if ( ( tt_s0 | ( tt_s1 & tt_s2 ) ) == tt )
         {
           ++st.num_div2_or_and_accepts;
+          assert( ntk.level( ntk.get_node( a ) ) <= max_depth - 1 );
+          assert( ntk.level( ntk.get_node( b ) ) <= max_depth - 2 && ntk.level( ntk.get_node( c ) ) <= max_depth - 2 );
           return sim.get_phase( root ) ? !ntk.create_or( a, ntk.create_and( b, c ) ) : ntk.create_or( a, ntk.create_and( b, c ) );
         }
       }
@@ -632,6 +641,8 @@ struct aig_resub_functor
         if ( ( tt_s0 | ( tt_s1 & tt_s2 ) ) == tt )
         {
           ++st.num_div2_or_and_accepts;
+          assert( ntk.level( ntk.get_node( a ) ) <= max_depth - 1 );
+          assert( ntk.level( ntk.get_node( b ) ) <= max_depth - 2 && ntk.level( ntk.get_node( c ) ) <= max_depth - 2 );
           return sim.get_phase( root ) ? !ntk.create_and( a, ntk.create_or( b, c ) ) : ntk.create_and( a, ntk.create_or( b, c ) );
         }
       }
@@ -640,10 +651,9 @@ struct aig_resub_functor
     return std::nullopt;
   }
 
-  std::optional<signal> resub_div3( node const& root, uint32_t required )
+  std::optional<signal> resub_div3( node const& root, uint32_t max_depth )
   {
-    (void)required;
-
+    (void)max_depth;
     auto const s = ntk.make_signal( root );
     auto const& tt = sim.get_tt( s );
 
@@ -670,6 +680,8 @@ struct aig_resub_functor
           auto const d = sim.get_phase( ntk.get_node( s3 ) ) ? !s3 : s3;
 
           ++st.num_div3_and_2or_accepts;
+          assert( ntk.level( ntk.get_node( a ) ) <= max_depth - 2 && ntk.level( ntk.get_node( b ) ) <= max_depth - 2 );
+          assert( ntk.level( ntk.get_node( c ) ) <= max_depth - 2 && ntk.level( ntk.get_node( d ) ) <= max_depth - 2 );
           return sim.get_phase( root ) ? !ntk.create_and( ntk.create_or( a, b ), ntk.create_or( c, d ) ) : ntk.create_and( ntk.create_or( a, b ), ntk.create_or( c, d ) );
         }
       }
@@ -698,6 +710,8 @@ struct aig_resub_functor
           auto const d = sim.get_phase( ntk.get_node( s3 ) ) ? !s3 : s3;
 
           ++st.num_div3_or_2and_accepts;
+          assert( ntk.level( ntk.get_node( a ) ) <= max_depth - 2 && ntk.level( ntk.get_node( b ) ) <= max_depth - 2 );
+          assert( ntk.level( ntk.get_node( c ) ) <= max_depth - 2 && ntk.level( ntk.get_node( d ) ) <= max_depth - 2 );
           return sim.get_phase( root ) ? !ntk.create_or( ntk.create_and( a, b ), ntk.create_and( c, d ) ) : ntk.create_or( ntk.create_and( a, b ), ntk.create_and( c, d ) );
         }
       }
diff --git a/include/mockturtle/algorithms/cut_rewriting.hpp b/include/mockturtle/algorithms/cut_rewriting.hpp
index 0da9859c4..d58bbf8fd 100644
--- a/include/mockturtle/algorithms/cut_rewriting.hpp
+++ b/include/mockturtle/algorithms/cut_rewriting.hpp
@@ -860,6 +860,8 @@ Ntk cut_rewriting( Ntk const& ntk, RewritingFn const& rewriting_fn = {}, cut_rew
   {
     *pst = st;
   }
+
+  ntk.clear_values();
   return result;
 }
 
diff --git a/include/mockturtle/algorithms/explorer.hpp b/include/mockturtle/algorithms/explorer.hpp
new file mode 100644
index 000000000..1e27c6e07
--- /dev/null
+++ b/include/mockturtle/algorithms/explorer.hpp
@@ -0,0 +1,996 @@
+/* mockturtle: C++ logic network library
+ * Copyright (C) 2018-2023  EPFL
+ *
+ * Permission is hereby granted, free of charge, to any person
+ * obtaining a copy of this software and associated documentation
+ * files (the "Software"), to deal in the Software without
+ * restriction, including without limitation the rights to use,
+ * copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the
+ * Software is furnished to do so, subject to the following
+ * conditions:
+ *
+ * The above copyright notice and this permission notice shall be
+ * included in all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+ * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
+ * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
+ * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+ * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+ * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+ * OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+/*!
+  \file explorer.hpp
+  \brief Implements the design space explorer engine
+
+  \author Siang-Yun (Sonia) Lee
+*/
+
+#pragma once
+
+#include "lut_mapper.hpp"
+#include "collapse_mapped.hpp"
+#include "klut_to_graph.hpp"
+#include "cut_rewriting.hpp"
+#include "refactoring.hpp"
+#include "mig_algebraic_rewriting.hpp"
+#include "mapper.hpp"
+#include "rewrite.hpp"
+#include "node_resynthesis/mig_npn.hpp"
+#include "node_resynthesis/sop_factoring.hpp"
+#include "resubstitution.hpp"
+#include "aig_resub.hpp"
+#include "mig_resub.hpp"
+#include "sim_resub.hpp"
+#include "cleanup.hpp"
+#include "balancing.hpp"
+#include "balancing/sop_balancing.hpp"
+#include "aig_balancing.hpp"
+#include "miter.hpp"
+#include "equivalence_checking.hpp"
+#include "aqfp/buffer_insertion.hpp"
+#include "../networks/klut.hpp"
+#include "../networks/mig.hpp"
+#include "../views/mapping_view.hpp"
+#include "../io/write_verilog.hpp"
+#include "../io/write_aiger.hpp"
+#include "../io/verilog_reader.hpp"
+#include "../utils/stopwatch.hpp"
+#include "../utils/abc.hpp"
+
+#include <random>
+
+#define explorer_debug 0
+
+namespace mockturtle
+{
+
+struct explorer_params
+{
+  /*! \brief Number of iterations to run with different random seed, restarting from the original
+   * network (including the first iteration). */
+  uint32_t num_restarts{1u};
+
+  /*! \brief Initial random seed used to generate random seeds randomly. */
+  uint32_t random_seed{0u};
+
+  /*! \brief Maximum number of steps in each iteration. */
+  uint32_t max_steps{100000u};
+
+  /*! \brief Maximum number of steps without improvement in each iteration. */
+  uint32_t max_steps_no_impr{1000000u};
+
+  /*! \brief Number of compressing scripts to run per step. */
+  uint32_t compressing_scripts_per_step{3u};
+
+  /*! \brief Timeout per iteration in seconds. */
+  uint32_t timeout{30u};
+
+  /*! \brief Be verbose. */
+  bool verbose{false};
+
+  /*! \brief Be very verbose. */
+  bool very_verbose{false};
+};
+
+struct explorer_stats
+{
+  stopwatch<>::duration time_total{0};
+  stopwatch<>::duration time_evaluate{0};
+};
+
+template<class Ntk>
+using script_t = std::function<void( Ntk&, uint32_t, uint32_t )>;
+
+template<class Ntk>
+using cost_fn_t = std::function<uint32_t( Ntk const& )>;
+
+template<class Ntk>
+std::function<uint32_t( Ntk const& )> size_cost_fn = []( Ntk const& ntk ){ return ntk.num_gates(); };
+
+template<class Ntk>
+class explorer
+{
+public:
+  using RandEngine = std::default_random_engine;
+
+  explorer( explorer_params const& ps, explorer_stats& st, cost_fn_t<Ntk> const& cost_fn = size_cost_fn<Ntk> )
+      : _ps( ps ), _st( st ), cost( cost_fn )
+  {
+  }
+
+  void add_decompressing_script( script_t<Ntk> const& algo, float weight = 1.0 )
+  {
+    decompressing_scripts.emplace_back( std::make_pair( algo, total_weights_dec ) );
+    total_weights_dec += weight;
+  }
+
+  void add_compressing_script( script_t<Ntk> const& algo, float weight = 1.0 )
+  {
+    compressing_scripts.emplace_back( std::make_pair( algo, total_weights_com ) );
+    total_weights_com += weight;
+  }
+
+  Ntk run( Ntk const& ntk )
+  {
+    stopwatch t( _st.time_total );
+    if ( decompressing_scripts.size() == 0 )
+    {
+      std::cerr << "[e] No decompressing script provided.\n";
+      return ntk;
+    }
+    if ( compressing_scripts.size() == 0 )
+    {
+      std::cerr << "[e] No compressing script provided.\n";
+      return ntk;
+    }
+
+    RandEngine rnd( _ps.random_seed );
+    auto init_cost = call_with_stopwatch( _st.time_evaluate, [&](){ return cost( ntk ); } );
+    Ntk best = ntk.clone();
+    auto best_cost = init_cost;
+    for ( auto i = 0u; i < _ps.num_restarts; ++i )
+    {
+      Ntk current = ntk.clone();
+      auto new_cost = run_one_iteration( current, rnd(), init_cost );
+      if ( new_cost < best_cost )
+      {
+        best = current.clone();
+        best_cost = new_cost;
+      }
+      if ( _ps.verbose )
+        fmt::print( "[i] best cost in restart {}: {}, overall best cost: {}\n", i, new_cost, best_cost );
+    }
+    return best;
+  }
+
+private:
+  uint32_t run_one_iteration( Ntk& ntk, uint32_t seed, uint32_t init_cost )
+  {
+    if ( _ps.verbose )
+    {
+      fmt::print( "\n[i] new restart using seed {}, original cost = {}\n", seed, init_cost );
+    }
+ 
+    stopwatch<>::duration elapsed_time{0};
+    RandEngine rnd( seed );
+    Ntk best = ntk.clone();
+    auto best_cost = init_cost;
+    uint32_t last_update{0u};
+    for ( auto i = 0u; i < _ps.max_steps; ++i )
+    {
+    #if explorer_debug
+      Ntk backup = ntk.clone();
+    #endif
+
+      {
+        stopwatch t( elapsed_time );
+        decompress( ntk, rnd, i );
+        compress( ntk, rnd, i );
+      }
+      auto new_cost = call_with_stopwatch( _st.time_evaluate, [&](){ return cost( ntk ); } );
+      if ( _ps.very_verbose )
+        fmt::print( "[i] after step {}, cost = {}\n", i, new_cost );
+
+    #if explorer_debug
+      if ( !*equivalence_checking( *miter<Ntk>( ntk, best ) ) )
+      {
+        write_verilog( backup, "debug.v" );
+        write_verilog( ntk, "wrong.v" );
+        fmt::print( "NEQ at step {}!\n", i );
+        break;
+      }
+    #endif
+
+      if ( new_cost < best_cost )
+      {
+        best = ntk.clone();
+        best_cost = new_cost;
+        last_update = i;
+        if ( _ps.verbose )
+        {
+          fmt::print( "[i] updated new best at step {}: {}\n", i, best_cost );
+        }
+      }
+      if ( i - last_update >= _ps.max_steps_no_impr )
+      {
+        if ( _ps.verbose )
+          fmt::print( "[i] break restart at step {} after {} steps without improvement (elapsed time: {} secs)\n", i, _ps.max_steps_no_impr, to_seconds( elapsed_time ) );
+        break;
+      }
+      if ( to_seconds( elapsed_time ) >= _ps.timeout )
+      {
+        if ( _ps.verbose )
+          fmt::print( "[i] break restart at step {} after timeout of {} secs\n", i, to_seconds( elapsed_time ) );
+        break;
+      }
+    }
+    std::cout << std::flush;
+    ntk = best;
+    return best_cost;
+  }
+
+  void decompress( Ntk& ntk, RandEngine& rnd, uint32_t i )
+  {
+    std::uniform_real_distribution<> dis( 0.0, total_weights_dec );
+    float r = dis( rnd );
+    for ( auto it = decompressing_scripts.rbegin(); it != decompressing_scripts.rend(); ++it )
+    {
+      if ( r >= it->second )
+      {
+        it->first( ntk, i, rnd() );
+        break;
+      }
+    }
+  }
+
+  void compress( Ntk& ntk, RandEngine& rnd, uint32_t i )
+  {
+    std::uniform_real_distribution<> dis( 0.0, total_weights_com );
+    for ( auto j = 0u; j < _ps.compressing_scripts_per_step; ++j )
+    {
+      float r = dis( rnd );
+      for ( auto it = compressing_scripts.rbegin(); it != compressing_scripts.rend(); ++it )
+      {
+        if ( r >= it->second )
+        {
+          it->first( ntk, i, rnd() );
+          break;
+        }
+      }
+    }
+  }
+
+private:
+  const explorer_params _ps;
+  explorer_stats& _st;
+
+  std::vector<std::pair<script_t<Ntk>, float>> decompressing_scripts;
+  float total_weights_dec{0.0};
+  std::vector<std::pair<script_t<Ntk>, float>> compressing_scripts;
+  float total_weights_com{0.0};
+
+  cost_fn_t<Ntk> cost;
+};
+
+mig_network explore_mig( mig_network const& ntk, explorer_params const ps = {} )
+{
+  using Ntk = mig_network;
+
+  explorer_stats st;
+  explorer<Ntk> expl( ps, st );
+
+  expl.add_decompressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "decompressing with k-LUT mapping using random value {}, k = {}\n", rand, 2 + (rand % 5) );
+    lut_map_params mps;
+    mps.cut_enumeration_ps.cut_size = 3 + (rand & 0x3); //3 + (i % 4);
+    mapping_view<Ntk> mapped{ _ntk };
+    lut_map( mapped, mps );
+    const auto klut = *collapse_mapped_network<klut_network>( mapped );
+    
+    if ( (rand >> 2) & 0x1 )
+    {
+      _ntk = convert_klut_to_graph<Ntk>( klut );
+    }
+    else
+    {
+      sop_factoring<Ntk> resyn;
+      _ntk = node_resynthesis<Ntk>( klut, resyn );
+    }
+  } );
+
+  expl.add_decompressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "decompressing with break-MAJ using random value {}\n", rand );
+    std::mt19937 g( rand );
+    _ntk.foreach_gate( [&]( auto n ){
+      bool is_maj = true;
+      _ntk.foreach_fanin( n, [&]( auto fi ){
+        if ( _ntk.is_constant( _ntk.get_node( fi ) ) )
+          is_maj = false;
+        return;
+      });
+      if ( !is_maj )
+        return;
+      std::vector<typename Ntk::signal> fanins;
+      _ntk.foreach_fanin( n, [&]( auto fi ){
+        fanins.emplace_back( fi );
+      });
+
+      std::shuffle( fanins.begin(), fanins.end(), g );
+      _ntk.substitute_node( n, _ntk.create_or( _ntk.create_and( fanins[0], fanins[1] ), _ntk.create_and( fanins[2], !_ntk.create_and( !fanins[0], !fanins[1] ) ) ) );
+    });
+  } );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    mig_npn_resynthesis resyn{ true };
+    exact_library<mig_network> exact_lib( resyn );
+    map_params mps;
+    mps.skip_delay_round = true;
+    mps.required_time = std::numeric_limits<double>::max();
+    mps.area_flow_rounds = 1;
+    mps.enable_logic_sharing = rand & 0x1; /* high-effort remap */
+    _ntk = map( _ntk, exact_lib, mps );
+  } );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    resubstitution_params rps;
+    rps.max_inserts = rand & 0x7;
+    rps.max_pis = (rand >> 3) & 0x1 ? 6 : 8;
+    depth_view depth_mig{ _ntk };
+    fanout_view fanout_mig{ depth_mig };
+    mig_resubstitution2( fanout_mig, rps );
+    _ntk = cleanup_dangling( _ntk );
+  } );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    sop_rebalancing<mig_network> balance_fn;
+    balancing_params bps;
+    bps.cut_enumeration_ps.cut_size = 6u;
+    _ntk = balancing( _ntk, {balance_fn}, bps );
+  } );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    depth_view depth_mig{ _ntk };
+    mig_algebraic_depth_rewriting( depth_mig );
+    _ntk = cleanup_dangling( _ntk );
+  } );
+
+  return expl.run( ntk );
+}
+
+#ifdef ENABLE_ABC
+mig_network deepsyn_mig_v1( mig_network const& ntk, explorer_params const ps = {} )
+{
+  using Ntk = mig_network;
+
+  explorer_stats st;
+  explorer<Ntk> expl( ps, st );
+
+  expl.add_decompressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "decompressing with &if using random value {}\n", rand );
+    aig_network aig = cleanup_dangling<mig_network, aig_network>( _ntk );
+
+    std::string script = fmt::format(
+      "&dch{}; &if -a -K {}; &mfs -e -W 20 -L 20; &st",
+      (rand & 0x1) ? " -f" : "",
+      2 + (i % 5));
+    aig = call_abc_script( aig, script );
+
+    mig_npn_resynthesis resyn2{ true };
+    exact_library<mig_network> exact_lib( resyn2 );
+    map_params mps;
+    mps.skip_delay_round = true;
+    mps.required_time = std::numeric_limits<double>::max();
+    _ntk = map( aig, exact_lib, mps );
+  } );
+
+  expl.add_decompressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "decompressing with k-LUT mapping using random value {}, k = {}\n", rand, 2 + (rand % 5) );
+    lut_map_params mps;
+    mps.cut_enumeration_ps.cut_size = 3 + (rand & 0x3); //3 + (i % 4);
+    klut_network klut = lut_map( _ntk, mps );
+    
+    if ( (rand >> 2) & 0x1 )
+    {
+      _ntk = convert_klut_to_graph<Ntk>( klut );
+    }
+    else
+    {
+      sop_factoring<Ntk> resyn;
+      _ntk = node_resynthesis<Ntk>( klut, resyn );
+    }
+  } );
+
+  expl.add_decompressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "decompressing with break-MAJ using random value {}\n", rand );
+    std::mt19937 g( rand );
+    _ntk.foreach_gate( [&]( auto n ){
+      bool is_maj = true;
+      _ntk.foreach_fanin( n, [&]( auto fi ){
+        if ( _ntk.is_constant( _ntk.get_node( fi ) ) )
+          is_maj = false;
+        return;
+      });
+      if ( !is_maj )
+        return;
+      std::vector<typename Ntk::signal> fanins;
+      _ntk.foreach_fanin( n, [&]( auto fi ){
+        fanins.emplace_back( fi );
+      });
+
+      std::shuffle( fanins.begin(), fanins.end(), g );
+      _ntk.substitute_node( n, _ntk.create_or( _ntk.create_and( fanins[0], fanins[1] ), _ntk.create_and( fanins[2], !_ntk.create_and( !fanins[0], !fanins[1] ) ) ) );
+    });
+    _ntk = cleanup_dangling( _ntk );
+  } );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "compressing with resyn2rs using random value {}\n", rand );
+    aig_network aig = cleanup_dangling<mig_network, aig_network>( _ntk );
+    //std::string script = (rand & 0x1) ? "; &c2rs" : "; &dc2";
+    std::string script = "&put; resyn2rs; &get";
+
+    aig = call_abc_script( aig, script );
+    
+    mig_npn_resynthesis resyn{ true };
+    exact_library_params eps;
+    eps.np_classification = false;
+    eps.compute_dc_classes = rand & 0x2;
+    exact_library<mig_network> exact_lib( resyn, eps );
+    map_params mps;
+    mps.skip_delay_round = true;
+    mps.required_time = std::numeric_limits<double>::max();
+    mps.area_flow_rounds = 1;
+    mps.enable_logic_sharing = rand & 0x1; // high-effort remap
+    mps.use_dont_cares = rand & 0x2;
+    _ntk = map( aig, exact_lib, mps );
+  } );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "compressing with remapping using random value {}\n", rand );
+    mig_npn_resynthesis resyn{ true };
+    exact_library_params eps;
+    eps.np_classification = false;
+    eps.compute_dc_classes = rand & 0x2;
+    exact_library<mig_network> exact_lib( resyn, eps );
+    map_params mps;
+    mps.skip_delay_round = true;
+    mps.required_time = std::numeric_limits<double>::max();
+    mps.area_flow_rounds = 1;
+    mps.enable_logic_sharing = rand & 0x1; // high-effort remap
+    mps.use_dont_cares = rand & 0x2;
+    _ntk = map( _ntk, exact_lib, mps );
+  } );
+  
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "compressing with rewriting using random value {}\n", rand );
+    mig_npn_resynthesis resyn{ true };
+    exact_library_params eps;
+    eps.np_classification = false;
+    eps.compute_dc_classes = rand & 0x1;
+    exact_library<mig_network> exact_lib( resyn, eps );
+    rewrite_params rps;
+    rps.use_dont_cares = rand & 0x1;
+    rewrite( _ntk, exact_lib, rps );
+    _ntk = cleanup_dangling( _ntk );
+  } );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "compressing with resub using random value {}\n", rand );
+    resubstitution_params rps;
+    rps.max_inserts = (rand >> 1) & 0x7;
+    rps.max_pis = (rand >> 4) & 0x3 ? 6 : 8;
+    depth_view depth_mig{ _ntk };
+    fanout_view fanout_mig{ depth_mig };
+    mig_resubstitution2( fanout_mig, rps );
+    _ntk = cleanup_dangling( _ntk );
+  } );
+
+  return expl.run( ntk );
+}
+
+mig_network deepsyn_mig_v2( mig_network const& ntk, explorer_params const ps = {} )
+{
+  using Ntk = mig_network;
+
+  explorer_stats st;
+  explorer<Ntk> expl( ps, st );
+
+  expl.add_decompressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "decompressing with &if using random value {}\n", rand );
+    aig_network aig = cleanup_dangling<mig_network, aig_network>( _ntk );
+
+    std::string script = fmt::format(
+      "&dch{}; &if -a -K {}; &mfs -e -W 20 -L 20; &st",
+      (rand & 0x1) ? " -f" : "",
+      2 + (i % 5));
+    aig = call_abc_script( aig, script );
+
+    mig_npn_resynthesis resyn2{ true };
+    exact_library<mig_network> exact_lib( resyn2 );
+    map_params mps;
+    mps.skip_delay_round = true;
+    mps.required_time = std::numeric_limits<double>::max();
+    _ntk = map( aig, exact_lib, mps );
+  } );
+
+  expl.add_decompressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "decompressing with k-LUT mapping using random value {}, k = {}\n", rand, 2 + (rand % 5) );
+    lut_map_params mps;
+    mps.cut_enumeration_ps.cut_size = 3 + (rand & 0x3); //3 + (i % 4);
+    klut_network klut = lut_map( _ntk, mps );
+    
+    if ( (rand >> 2) & 0x1 )
+    {
+      _ntk = convert_klut_to_graph<Ntk>( klut );
+    }
+    else
+    {
+      sop_factoring<Ntk> resyn;
+      _ntk = node_resynthesis<Ntk>( klut, resyn );
+    }
+  } );
+
+  expl.add_decompressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "decompressing with break-MAJ using random value {}\n", rand );
+    std::mt19937 g( rand );
+    _ntk.foreach_gate( [&]( auto n ){
+      bool is_maj = true;
+      _ntk.foreach_fanin( n, [&]( auto fi ){
+        if ( _ntk.is_constant( _ntk.get_node( fi ) ) )
+          is_maj = false;
+        return;
+      });
+      if ( !is_maj )
+        return;
+      std::vector<typename Ntk::signal> fanins;
+      _ntk.foreach_fanin( n, [&]( auto fi ){
+        fanins.emplace_back( fi );
+      });
+
+      std::shuffle( fanins.begin(), fanins.end(), g );
+      _ntk.substitute_node( n, _ntk.create_or( _ntk.create_and( fanins[0], fanins[1] ), _ntk.create_and( fanins[2], !_ntk.create_and( !fanins[0], !fanins[1] ) ) ) );
+    });
+    _ntk = cleanup_dangling( _ntk );
+  } );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "compressing with resyn2rs using random value {}\n", rand );
+    aig_network aig = cleanup_dangling<mig_network, aig_network>( _ntk );
+    //std::string script = (rand & 0x1) ? "; &c2rs" : "; &dc2";
+    std::string script = "&put; resyn2rs; &get";
+
+    aig = call_abc_script( aig, script );
+    
+    mig_npn_resynthesis resyn{ true };
+    exact_library_params eps;
+    eps.np_classification = false;
+    eps.compute_dc_classes = rand & 0x2;
+    exact_library<mig_network> exact_lib( resyn, eps );
+    map_params mps;
+    mps.skip_delay_round = true;
+    mps.required_time = std::numeric_limits<double>::max();
+    mps.area_flow_rounds = 1;
+    mps.enable_logic_sharing = rand & 0x1; // high-effort remap
+    mps.use_dont_cares = rand & 0x2;
+    _ntk = map( aig, exact_lib, mps );
+  } );
+  
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "compressing with Ale flow using random value {}\n", rand );
+    //_ntk = cleanup_dangling( _ntk );
+
+    mig_npn_resynthesis resyn{ true };
+    exact_library_params eps;
+    eps.np_classification = false;
+    eps.compute_dc_classes = true;
+    exact_library<mig_network> exact_lib( resyn, eps );
+    
+    map_params mps;
+    mps.skip_delay_round = true;
+    mps.required_time = std::numeric_limits<double>::max();
+    mps.area_flow_rounds = 1;
+    mps.enable_logic_sharing = true; // high-effort remap
+    
+    rewrite_params rps;
+
+    resubstitution_params rsps;
+    rsps.max_inserts = 20;
+    rsps.max_pis = 8;
+    
+    mps.use_dont_cares = rand & 0x8;
+    _ntk = map( _ntk, exact_lib, mps );
+    mps.use_dont_cares = rand & 0xf;
+    _ntk = map( _ntk, exact_lib, mps );
+    mps.use_dont_cares = rand & 0x10;
+    _ntk = map( _ntk, exact_lib, mps );
+
+    rps.use_dont_cares = rand & 0x1;
+    rewrite( _ntk, exact_lib, rps );
+    _ntk = cleanup_dangling( _ntk );
+    rps.use_dont_cares = rand & 0x2;
+    rewrite( _ntk, exact_lib, rps );
+    _ntk = cleanup_dangling( _ntk );
+    rps.use_dont_cares = rand & 0x4;
+    rewrite( _ntk, exact_lib, rps );
+    _ntk = cleanup_dangling( _ntk );
+
+    depth_view depth_mig{ _ntk };
+    fanout_view fanout_mig{ depth_mig };
+    mig_resubstitution2( fanout_mig, rsps );
+    _ntk = cleanup_dangling( _ntk );
+  } );
+
+  return expl.run( ntk );
+}
+
+mig_network deepsyn_mig_depth( mig_network const& ntk, explorer_params const ps = {} )
+{
+  using Ntk = mig_network;
+
+  cost_fn_t<Ntk> depth_cost = []( Ntk const& _ntk ){
+    depth_view d{ _ntk };
+    return d.depth();
+  };
+
+  explorer_stats st;
+  explorer<Ntk> expl( ps, st, depth_cost );
+
+  expl.add_decompressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    aig_network aig = cleanup_dangling<mig_network, aig_network>( _ntk );
+
+    std::string script = fmt::format(
+      "&dch{} -m; &if -K {}; &mfs -e -W 20 {}",
+      (rand & 0x1) ? " -f" : "",
+      2 + (i % 5),
+      ((rand >> 2) & 0x1) ? "; &fx; &st" : "");
+    aig = call_abc_script( aig, script );
+
+    mig_npn_resynthesis resyn2{ true };
+    exact_library<mig_network> exact_lib( resyn2 );
+    map_params mps;
+    mps.skip_delay_round = false;
+    mps.required_time = std::numeric_limits<double>::max();
+    _ntk = map( aig, exact_lib, mps );
+  } );
+
+  expl.add_decompressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "decompressing with break-MAJ using random value {}\n", rand );
+    std::mt19937 g( rand );
+    _ntk.foreach_gate( [&]( auto n ){
+      bool is_maj = true;
+      _ntk.foreach_fanin( n, [&]( auto fi ){
+        if ( _ntk.is_constant( _ntk.get_node( fi ) ) )
+          is_maj = false;
+        return;
+      });
+      if ( !is_maj )
+        return;
+      std::vector<typename Ntk::signal> fanins;
+      _ntk.foreach_fanin( n, [&]( auto fi ){
+        fanins.emplace_back( fi );
+      });
+
+      std::shuffle( fanins.begin(), fanins.end(), g );
+      _ntk.substitute_node( n, _ntk.create_or( _ntk.create_and( fanins[0], fanins[1] ), _ntk.create_and( fanins[2], !_ntk.create_and( !fanins[0], !fanins[1] ) ) ) );
+    });
+    _ntk = cleanup_dangling( _ntk );
+  }, 0.3 );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    aig_network aig = cleanup_dangling<mig_network, aig_network>( _ntk );
+    std::string script = "&put; resyn2rs; &get";
+    aig = call_abc_script( aig, script );
+
+    mig_npn_resynthesis resyn2{ true };
+    exact_library<mig_network> exact_lib( resyn2 );
+    map_params mps;
+    mps.skip_delay_round = false;
+    mps.required_time = std::numeric_limits<double>::max();
+    _ntk = map( aig, exact_lib, mps );
+  } );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    mig_npn_resynthesis resyn{ true };
+    exact_library<mig_network> exact_lib( resyn );
+    map_params mps;
+    mps.skip_delay_round = false;
+    //mps.required_time = std::numeric_limits<double>::max();
+    mps.area_flow_rounds = 1;
+    mps.enable_logic_sharing = rand & 0x1; /* high-effort remap */
+    _ntk = map( _ntk, exact_lib, mps );
+  }, 0.5 );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    resubstitution_params rps;
+    rps.max_inserts = rand & 0x7;
+    rps.max_pis = (rand >> 3) & 0x1 ? 6 : 8;
+    depth_view depth_mig{ _ntk };
+    fanout_view fanout_mig{ depth_mig };
+    mig_resubstitution2( fanout_mig, rps );
+    _ntk = cleanup_dangling( _ntk );
+  }, 0.5 );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    sop_rebalancing<mig_network> balance_fn;
+    balancing_params bps;
+    bps.cut_enumeration_ps.cut_size = ( rand & 0x1 ) ? 8 : 10;
+    _ntk = balancing( _ntk, {balance_fn}, bps );
+  } );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    depth_view depth_mig{ _ntk };
+    mig_algebraic_depth_rewriting( depth_mig );
+    _ntk = cleanup_dangling( _ntk );
+  } );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    sop_factoring<Ntk> resyn;
+    refactoring( _ntk, resyn );
+    _ntk = cleanup_dangling( _ntk );
+  }, 0.5 );
+
+  return expl.run( ntk );
+}
+
+aig_network deepsyn_aig( aig_network const& ntk, explorer_params const ps = {} )
+{
+  using Ntk = aig_network;
+
+  explorer_stats st;
+  explorer<Ntk> expl( ps, st );
+
+  expl.add_decompressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    std::string script = fmt::format(
+      "&dch{}; &if -a -K {}; &mfs -e -W 20 -L 20{}",
+      (rand & 0x1) ? " -f" : "",
+      2 + (i % 5),
+      ((rand >> 2) & 0x1) ? "; &fx; &st" : "");
+    _ntk = call_abc_script( _ntk, script );
+  } );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    std::string script = (rand & 0x1) ? "; &c2rs" : "; &dc2";
+    _ntk = call_abc_script( _ntk, script );
+  } );
+
+  return expl.run( ntk );
+}
+
+mig_network deepsyn_aqfp( mig_network const& ntk, explorer_params const ps = {}, explorer_stats * pst = nullptr )
+{
+  using Ntk = mig_network;
+
+  cost_fn_t<Ntk> aqfp_cost = []( Ntk const& _ntk ){
+    buffer_insertion_params bps;
+    bps.assume.balance_cios = true;
+    bps.assume.splitter_capacity = 4;
+    bps.assume.ci_phases = {0};
+    bps.assume.num_phases = 1;
+    bps.scheduling = buffer_insertion_params::better_depth;
+    bps.optimization_effort = buffer_insertion_params::one_pass;
+    buffer_insertion buf_inst( _ntk, bps );
+    auto numbufs = buf_inst.dry_run();
+
+    //return (_ntk.num_gates() * 6 + numbufs * 2);
+    return (_ntk.num_gates() * 6 + numbufs * 2) * buf_inst.depth();
+  };
+
+  explorer_stats st;
+  explorer<Ntk> expl( ps, st, aqfp_cost );
+
+  expl.add_decompressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    aig_network aig = cleanup_dangling<mig_network, aig_network>( _ntk );
+
+    std::string script = fmt::format(
+      "&dch{}; &if -a -K {}; &mfs -e -W 20 -L 20{}",
+      (rand & 0x1) ? " -f" : "",
+      2 + (i % 5),
+      ((rand >> 2) & 0x1) ? "; &fx; &st" : "");
+    aig = call_abc_script( aig, script );
+
+    mig_npn_resynthesis resyn2{ true };
+    exact_library<mig_network> exact_lib( resyn2 );
+    map_params mps;
+    mps.skip_delay_round = true;
+    mps.required_time = std::numeric_limits<double>::max();
+    _ntk = map( aig, exact_lib, mps );
+  } );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    aig_network aig = cleanup_dangling<mig_network, aig_network>( _ntk );
+    std::string script = (rand & 0x1) ? "; &c2rs" : "; &dc2";
+    aig = call_abc_script( aig, script );
+
+    mig_npn_resynthesis resyn2{ true };
+    exact_library<mig_network> exact_lib( resyn2 );
+    map_params mps;
+    mps.skip_delay_round = true;
+    mps.required_time = std::numeric_limits<double>::max();
+    _ntk = map( aig, exact_lib, mps );
+  } );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    mig_npn_resynthesis resyn2{ true };
+    exact_library<mig_network> exact_lib( resyn2 );
+    map_params mps;
+    mps.skip_delay_round = true;
+    mps.required_time = std::numeric_limits<double>::max();
+    mps.area_flow_rounds = 1;
+    mps.enable_logic_sharing = rand & 0x1; /* high-effort remap */
+    _ntk = map( _ntk, exact_lib, mps );
+  } );
+
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    resubstitution_params rps;
+    rps.max_inserts = rand & 0x3;
+    depth_view depth_mig{ _ntk };
+    fanout_view fanout_mig{ depth_mig };
+    mig_resubstitution2( fanout_mig, rps );
+    _ntk = cleanup_dangling( _ntk );
+  } );
+
+  // balancing
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    sop_rebalancing<mig_network> balance_fn;
+    balancing_params bps;
+    bps.cut_enumeration_ps.cut_size = 6u;
+    _ntk = balancing( _ntk, {balance_fn}, bps );
+  } );
+
+  // algebraic depth optimization
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    depth_view depth_mig{ _ntk };
+    mig_algebraic_depth_rewriting( depth_mig );
+    _ntk = cleanup_dangling( _ntk );
+  } );
+
+  auto res = expl.run( ntk );
+  if ( pst )
+    *pst = st;
+  return res;
+}
+#endif
+
+void compress2rs_aig( aig_network& aig )
+{
+  xag_npn_resynthesis<aig_network> resyn;
+  cut_rewriting_params cps;
+  cps.cut_enumeration_ps.cut_size = 4;
+  resubstitution_params rps;
+  //sop_rebalancing<aig_network> balance_fn;
+  //balancing_params bps;
+  //bps.cut_enumeration_ps.cut_size = 6u;
+  aig_balancing_params abps;
+  refactoring_params fps;
+  sop_factoring<aig_network> resyn2;
+
+  /*abps.minimize_levels = true;*/ aig_balance( aig, abps ); // "b -l"
+  rps.max_pis = 6; rps.max_inserts = 1; /*rps.preserve_depth = true;*/ aig_resubstitution( aig, rps ); aig = cleanup_dangling( aig ); // "rs -K 6 -l"
+  /*cps.preserve_depth = true;*/ aig = cut_rewriting( aig, resyn, cps ); // "rw -l"
+  rps.max_pis = 6; rps.max_inserts = 2; aig_resubstitution( aig, rps ); aig = cleanup_dangling( aig ); // "rs -K 6 -N 2 -l"
+  /*fps.preserve_depth = true;*/ refactoring( aig, resyn2, fps ); aig = cleanup_dangling( aig ); // "rf -l"
+  rps.max_pis = 8; rps.max_inserts = 1; aig_resubstitution( aig, rps ); aig = cleanup_dangling( aig ); // "rs -K 8 -l"
+  aig_balance( aig, abps ); // "b -l"
+  rps.max_pis = 8; rps.max_inserts = 2; aig_resubstitution( aig, rps ); aig = cleanup_dangling( aig ); // "rs -K 8 -N 2 -l"
+  aig = cut_rewriting( aig, resyn, cps ); // "rw -l"
+  rps.max_pis = 10; rps.max_inserts = 1; aig_resubstitution( aig, rps ); aig = cleanup_dangling( aig ); // "rs -K 10 -l"
+  cps.allow_zero_gain = true; aig = cut_rewriting( aig, resyn, cps ); // "rwz -l"
+  rps.max_pis = 10; rps.max_inserts = 2; aig_resubstitution( aig, rps ); aig = cleanup_dangling( aig ); // "rs -K 10 -N 2 -l"
+  aig_balance( aig, abps ); // "b -l"
+  rps.max_pis = 12; rps.max_inserts = 1; aig_resubstitution( aig, rps ); aig = cleanup_dangling( aig ); // "rs -K 12 -l"
+  fps.allow_zero_gain = true; refactoring( aig, resyn2, fps ); aig = cleanup_dangling( aig ); // "rfz -l"
+  rps.max_pis = 12; rps.max_inserts = 2; aig_resubstitution( aig, rps ); aig = cleanup_dangling( aig ); // "rs -K 12 -N 2 -l"
+  aig = cut_rewriting( aig, resyn, cps ); // "rwz -l"
+  aig_balance( aig, abps ); // "b -l"
+}
+
+mig_network explore_aqfp( mig_network const& ntk, explorer_params const ps = {} )
+{
+  using Ntk = mig_network;
+
+  cost_fn_t<Ntk> aqfp_cost = []( Ntk const& _ntk ){
+    buffer_insertion_params bps;
+    bps.assume.balance_cios = true;
+    bps.assume.splitter_capacity = 4;
+    bps.assume.ci_phases = {0};
+    bps.scheduling = buffer_insertion_params::better_depth;
+    bps.optimization_effort = buffer_insertion_params::none;
+    buffer_insertion buf_inst( _ntk, bps );
+
+    return _ntk.num_gates() * 6 + buf_inst.dry_run() * 2;
+  };
+
+  explorer_stats st;
+  explorer<Ntk> expl( ps, st, aqfp_cost );
+
+  expl.add_decompressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "decompressing with k-LUT mapping using random value {}, k = {}\n", rand, 2 + (rand % 5) );
+    lut_map_params mps;
+    mps.cut_enumeration_ps.cut_size = 3 + (i & 0x3);
+    mapping_view<Ntk> mapped{ _ntk };
+    lut_map( mapped, mps );
+    const auto klut = *collapse_mapped_network<klut_network>( mapped );
+    
+    if ( (rand >> 2) & 0x1 )
+    {
+      _ntk = convert_klut_to_graph<Ntk>( klut );
+    }
+    else
+    {
+      sop_factoring<Ntk> resyn;
+      _ntk = node_resynthesis<Ntk>( klut, resyn );
+    }
+  } );
+
+  expl.add_decompressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    //fmt::print( "decompressing with break-MAJ using random value {}\n", rand );
+    std::mt19937 g( rand );
+    _ntk.foreach_gate( [&]( auto n ){
+      bool is_maj = true;
+      _ntk.foreach_fanin( n, [&]( auto fi ){
+        if ( _ntk.is_constant( _ntk.get_node( fi ) ) )
+          is_maj = false;
+        return;
+      });
+      if ( !is_maj )
+        return;
+      std::vector<typename Ntk::signal> fanins;
+      _ntk.foreach_fanin( n, [&]( auto fi ){
+        fanins.emplace_back( fi );
+      });
+
+      std::shuffle( fanins.begin(), fanins.end(), g );
+      _ntk.substitute_node( n, _ntk.create_or( _ntk.create_and( fanins[0], fanins[1] ), _ntk.create_and( fanins[2], !_ntk.create_and( !fanins[0], !fanins[1] ) ) ) );
+    });
+  }, 0.3 );
+
+  // high-effort AIG optimization + (50% chance high-effort) mapping
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    aig_network aig = cleanup_dangling<mig_network, aig_network>( _ntk );
+    compress2rs_aig( aig );
+
+    mig_npn_resynthesis resyn3{ true };
+    exact_library<mig_network> exact_lib( resyn3 );
+    map_params mps;
+    mps.skip_delay_round = false;
+    mps.required_time = std::numeric_limits<double>::max();
+    mps.area_flow_rounds = 1;
+    mps.enable_logic_sharing = rand & 0x1; /* high-effort remap */
+    _ntk = map( aig, exact_lib, mps );
+  } );
+
+  // high-effort MIG resub x1
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    resubstitution_params rps;
+    rps.max_inserts = rand & 0x7;
+    rps.max_pis = (rand >> 3) & 0x1 ? 6 : 8;
+    depth_view depth_mig{ _ntk };
+    fanout_view fanout_mig{ depth_mig };
+    mig_resubstitution2( fanout_mig, rps );
+    _ntk = cleanup_dangling( _ntk );
+  }, 0.5 );
+
+  // balancing
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    sop_rebalancing<mig_network> balance_fn;
+    balancing_params bps;
+    bps.cut_enumeration_ps.cut_size = 6u;
+    _ntk = balancing( _ntk, {balance_fn}, bps );
+  }, 0.5 );
+
+  // algebraic depth optimization
+  expl.add_compressing_script( []( Ntk& _ntk, uint32_t i, uint32_t rand ){
+    depth_view depth_mig{ _ntk };
+    mig_algebraic_depth_rewriting( depth_mig );
+    _ntk = cleanup_dangling( _ntk );
+  }, 0.5 );
+
+  return expl.run( ntk );
+}
+
+} // namespace mockturtle
diff --git a/include/mockturtle/algorithms/refactoring.hpp b/include/mockturtle/algorithms/refactoring.hpp
index 32113531e..dbdef7273 100644
--- a/include/mockturtle/algorithms/refactoring.hpp
+++ b/include/mockturtle/algorithms/refactoring.hpp
@@ -165,6 +165,11 @@ class refactoring_impl
       {
         return true;
       }
+
+      ntk.foreach_node( [&]( auto n ){
+        ntk.set_value( n, ntk.fanout_size( n ) );
+      });
+
       const auto mffc = make_with_stopwatch<mffc_view<Ntk>>( st.time_mffc, ntk, n );
 
       pbar( i, i, _candidates, _estimated_gain );
diff --git a/include/mockturtle/algorithms/resubstitution.hpp b/include/mockturtle/algorithms/resubstitution.hpp
index e5cfecd62..d8ed920a8 100644
--- a/include/mockturtle/algorithms/resubstitution.hpp
+++ b/include/mockturtle/algorithms/resubstitution.hpp
@@ -303,7 +303,7 @@ class default_divisor_collector
     auto max_depth = std::numeric_limits<uint32_t>::max();
     if ( ps.preserve_depth )
     {
-      max_depth = ntk.level( root ) - 1;
+      max_depth = ntk.level( root );
     }
     /* add the leaves of the cuts to the divisors */
     divs.clear();
@@ -531,7 +531,7 @@ class window_based_resub_engine
       auto max_depth = std::numeric_limits<uint32_t>::max();
       if ( ps.preserve_depth )
       {
-        max_depth = ntk.level( n ) - 1;
+        max_depth = ntk.level( n );
       }
       return resub_fn( n, care, max_depth, ps.max_inserts, potential_gain, last_gain );
     } );
diff --git a/include/mockturtle/algorithms/resyn_engines/mig_resyn.hpp b/include/mockturtle/algorithms/resyn_engines/mig_resyn.hpp
index 1655d218b..6684e517e 100644
--- a/include/mockturtle/algorithms/resyn_engines/mig_resyn.hpp
+++ b/include/mockturtle/algorithms/resyn_engines/mig_resyn.hpp
@@ -68,6 +68,7 @@ struct mig_resyn_static_params
 
 struct mig_resyn_stats
 {
+  void report() const {}
 };
 
 /*! \brief Logic resynthesis engine for MIGs with a bottom-up approach.
@@ -1340,4 +1341,4 @@ class mig_resyn_akers
 
   stats& st;
 }; /* mig_resyn_akers */
-} /* namespace mockturtle */
\ No newline at end of file
+} /* namespace mockturtle */
diff --git a/include/mockturtle/algorithms/sim_resub.hpp b/include/mockturtle/algorithms/sim_resub.hpp
index 7ac536abe..f1ab33d93 100644
--- a/include/mockturtle/algorithms/sim_resub.hpp
+++ b/include/mockturtle/algorithms/sim_resub.hpp
@@ -36,12 +36,14 @@
 #include "../io/write_patterns.hpp"
 #include "../networks/aig.hpp"
 #include "../networks/xag.hpp"
+#include "../networks/mig.hpp"
 #include "../utils/progress_bar.hpp"
 #include "../utils/stopwatch.hpp"
 #include "circuit_validator.hpp"
 #include "pattern_generation.hpp"
 #include "resubstitution.hpp"
 #include "resyn_engines/xag_resyn.hpp"
+#include "resyn_engines/mig_resyn.hpp"
 #include "simulation.hpp"
 
 #include <bill/bill.hpp>
@@ -366,7 +368,9 @@ void sim_resubstitution_run( Ntk& ntk, resubstitution_params const& ps, resubsti
 template<class Ntk>
 void sim_resubstitution( Ntk& ntk, resubstitution_params const& ps = {}, resubstitution_stats* pst = nullptr )
 {
-  static_assert( std::is_same_v<typename Ntk::base_type, aig_network> || std::is_same_v<typename Ntk::base_type, xag_network>, "Currently only supports AIG and XAG" );
+  static_assert( std::is_same_v<typename Ntk::base_type, aig_network> 
+                 || std::is_same_v<typename Ntk::base_type, xag_network>
+                 || std::is_same_v<typename Ntk::base_type, mig_network>, "Currently only supports AIG, XAG, and MIG" );
 
   using resub_view_t = fanout_view<depth_view<Ntk>>;
   depth_view<Ntk> depth_view{ ntk };
@@ -389,10 +393,27 @@ void sim_resubstitution( Ntk& ntk, resubstitution_params const& ps = {}, resubst
       detail::sim_resubstitution_run<resub_view_t, resub_impl_t>( resub_view, ps, pst );
     }
   }
-  else
+  else if constexpr ( std::is_same_v<typename Ntk::base_type, xag_network> )
   {
     using resyn_engine_t = xag_resyn_decompose<kitty::partial_truth_table, xag_resyn_static_params_for_sim_resub<resub_view_t>>;
 
+    if ( ps.odc_levels != 0 )
+    {
+      using validator_t = circuit_validator<resub_view_t, bill::solvers::bsat2, false, true, true>;
+      using resub_impl_t = typename detail::resubstitution_impl<resub_view_t, typename detail::simulation_based_resub_engine<resub_view_t, validator_t, resyn_engine_t>>;
+      detail::sim_resubstitution_run<resub_view_t, resub_impl_t>( resub_view, ps, pst );
+    }
+    else
+    {
+      using validator_t = circuit_validator<resub_view_t, bill::solvers::bsat2, false, true, false>;
+      using resub_impl_t = typename detail::resubstitution_impl<resub_view_t, typename detail::simulation_based_resub_engine<resub_view_t, validator_t, resyn_engine_t>>;
+      detail::sim_resubstitution_run<resub_view_t, resub_impl_t>( resub_view, ps, pst );
+    }
+  }
+  else if constexpr ( std::is_same_v<typename Ntk::base_type, mig_network> )
+  {
+    using resyn_engine_t = mig_resyn_topdown<kitty::partial_truth_table, mig_resyn_static_params>;
+
     if ( ps.odc_levels != 0 )
     {
       using validator_t = circuit_validator<resub_view_t, bill::solvers::bsat2, false, true, true>;
diff --git a/include/mockturtle/networks/gia.hpp b/include/mockturtle/networks/gia.hpp
new file mode 100644
index 000000000..64fed98af
--- /dev/null
+++ b/include/mockturtle/networks/gia.hpp
@@ -0,0 +1,269 @@
+#pragma once
+#ifdef ENABLE_ABC
+
+#include "detail/foreach.hpp"
+#include <kitty/dynamic_truth_table.hpp>
+
+namespace abc {
+  typedef struct Gia_Man_t_ Gia_Man_t;
+  typedef struct Gia_Obj_t_ Gia_Obj_t;
+  typedef struct Abc_Frame_t_ Abc_Frame_t;
+  
+  inline int      Abc_LitNot( int Lit )                  { assert(Lit >= 0); return Lit ^ 1;                           }
+  inline int      Abc_Lit2Var( int Lit )                 { assert(Lit >= 0); return Lit >> 1;                          }
+  inline int      Abc_LitRegular( int Lit )              { assert(Lit >= 0); return Lit & ~01;                         }
+
+  extern Gia_Obj_t * Gia_Regular( Gia_Obj_t * p );
+  extern Gia_Obj_t * Gia_Not( Gia_Obj_t * p );
+  extern Gia_Man_t * Gia_ManStart(int nObjsMax);
+  extern void        Gia_ManStop(Gia_Man_t * p);
+  extern int         Gia_ManAppendCi(Gia_Man_t * p);
+  extern int         Gia_ManAppendCo(Gia_Man_t * p, int iLit0);
+  extern int         Gia_ManAppendAnd2(Gia_Man_t * p, int iLit0, int iLit1);
+  extern Gia_Obj_t * Gia_ManObj(Gia_Man_t * p, int v);
+  extern int         Gia_ObjIsPi(Gia_Man_t * p, Gia_Obj_t * pObj);
+  extern int         Gia_ObjIsAnd(Gia_Obj_t * pObj);
+  extern int         Gia_IsComplement(Gia_Obj_t * p);
+  extern int         Gia_ManPiNum(Gia_Man_t * p);
+  extern int         Gia_ManPoNum(Gia_Man_t * p);
+  extern int         Gia_ManAndNum(Gia_Man_t * p);
+  extern int         Gia_ManObjNum(Gia_Man_t * p);
+  extern Gia_Obj_t * Gia_ManPi(Gia_Man_t * p, int v);
+  extern int         Gia_Obj2Lit(Gia_Man_t * p, Gia_Obj_t * pObj);
+  extern Gia_Obj_t * Gia_ManCi(Gia_Man_t * p, int v);
+  extern Gia_Obj_t * Gia_ManCo(Gia_Man_t * p, int v);
+  extern Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t * pObj);
+  extern Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t * pObj);
+  extern int Gia_ObjFaninC0(Gia_Obj_t * pObj);
+  extern int Gia_ObjFaninC1(Gia_Obj_t * pObj);
+  extern int         Gia_ManLevelNum( Gia_Man_t * p );
+  extern Gia_Obj_t * Gia_ManConst0( Gia_Man_t * p );
+  extern Gia_Obj_t * Gia_ManConst1( Gia_Man_t * p );
+  extern int Gia_ObjId( Gia_Man_t * p, Gia_Obj_t * pObj );
+  extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p );
+
+  extern Abc_Frame_t * Abc_FrameGetGlobalFrame();
+  extern void Abc_FrameUpdateGia( Abc_Frame_t * p, Gia_Man_t * pNew );
+  extern Gia_Man_t * Abc_FrameGetGia( Abc_Frame_t * p );
+  extern int Cmd_CommandExecute( Abc_Frame_t * pAbc, const char * sCommand );
+}
+
+#include <iostream>
+
+namespace mockturtle {
+
+class gia_network;
+  
+class gia_signal {
+  friend class gia_network;
+
+public:
+  explicit gia_signal() = default;
+  explicit gia_signal(abc::Gia_Obj_t * obj) : obj_(obj) {}
+ 
+  gia_signal operator!() const { return gia_signal(abc::Gia_Not(obj_)); }
+  gia_signal operator+() const { return gia_signal(abc::Gia_Regular(obj_)); }
+  gia_signal operator-() const { return gia_signal(abc::Gia_Not(abc::Gia_Regular(obj_))); }
+ 
+  bool operator==(const gia_signal& other) const { return obj_ == other.obj_; }
+  bool operator!=(const gia_signal& other) const { return !operator==(other); }
+  bool operator<(const gia_signal& other) const { return obj_ < other.obj_; }
+
+  abc::Gia_Obj_t * obj() const { return obj_; }
+  
+private:
+  abc::Gia_Obj_t * obj_;
+};
+  
+class gia_network {
+public:
+  static constexpr auto min_fanin_size = 2u;
+  static constexpr auto max_fanin_size = 2u;
+
+  using base_type = gia_network;
+  using node = int;
+  using signal = gia_signal;
+  using storage = abc::Gia_Man_t*;
+  
+  gia_network(int size)
+    : gia_(abc::Gia_ManStart(size)) /* doesn't automatically resize? */
+  {}
+
+  /* network does not implement constant value */
+  bool constant_value(node n) const { (void)n; return false; }
+
+  /* each node implements AND function */
+  kitty::dynamic_truth_table node_function(node n) const { (void)n; kitty::dynamic_truth_table tt(2); tt._bits[0] = 0x8; return tt; }
+
+  
+  signal get_constant(bool value) const {
+    return value ? signal(abc::Gia_ManConst1(gia_)) : signal(abc::Gia_ManConst0(gia_));
+  }
+  
+  signal create_pi() {
+    return signal(abc::Gia_ManObj(gia_, abc::Abc_Lit2Var(abc::Gia_ManAppendCi(gia_))));
+  }
+
+  void create_po(const signal& f) {
+    /* po_node = */abc::Gia_ManAppendCo(gia_, abc::Gia_Obj2Lit(gia_, f.obj()));
+  }
+
+  signal create_not(const signal& f) {
+    return !f;
+  }
+  
+  signal create_and(const signal& f, const signal& g) {
+    return signal(abc::Gia_ManObj(gia_, abc::Abc_Lit2Var(abc::Gia_ManAppendAnd2(gia_, abc::Gia_Obj2Lit(gia_, f.obj()), abc::Gia_Obj2Lit(gia_, g.obj())))));
+  }
+
+  bool is_constant(node n) const {
+    return n == 0;
+  }
+
+  node get_node(const signal& f) const {
+    return Gia_ObjId(gia_, f.obj());
+  }
+
+  bool is_pi(node const& n) const {
+    return abc::Gia_ObjIsPi(gia_, abc::Gia_ManObj(gia_, n));
+  }
+
+  bool is_complemented(const signal& f) const {
+    return Gia_IsComplement(f.obj());
+  }
+
+  template<typename Fn>
+  void foreach_pi(Fn&& fn) const {
+    abc::Gia_Obj_t * pObj;
+    for (int i = 0; (i < abc::Gia_ManPiNum(gia_)) && ((pObj) = abc::Gia_ManCi(gia_, i)); ++i) {
+      fn(Gia_ObjId(gia_, pObj));
+    }
+  }
+
+  template<typename Fn>
+  void foreach_po(Fn&& fn) const {
+    abc::Gia_Obj_t * pObj, * pFiObj;
+    for (int i = 0; (i < abc::Gia_ManPoNum(gia_)) && ((pObj) = abc::Gia_ManCo(gia_, i)); ++i) {
+      pFiObj = abc::Gia_ObjFanin0(pObj);
+      fn(abc::Gia_ObjFaninC0(pObj) ? !signal(pFiObj) : signal(pFiObj));
+    }
+  }
+
+  template<typename Fn>
+  void foreach_gate(Fn&& fn) const {
+    abc::Gia_Obj_t * pObj;
+    for (int i = 0; i < abc::Gia_ManObjNum(gia_) && ((pObj) = abc::Gia_ManObj(gia_, i)); ++i) {
+      if (abc::Gia_ObjIsAnd(pObj)) {
+        fn(Gia_ObjId(gia_, pObj));
+      }
+    }
+  }  
+
+  template<typename Fn>
+  void foreach_node(Fn&& fn) const {
+    abc::Gia_Obj_t * pObj;
+    for (int i = 0; i < abc::Gia_ManObjNum(gia_) && ((pObj) = abc::Gia_ManObj(gia_, i)); ++i) {
+      fn(signal(pObj));
+    }
+  }  
+
+  template<typename Fn>
+  void foreach_fanin(node n, Fn&& fn) const {
+    static_assert( detail::is_callable_without_index_v<Fn, signal, bool> ||
+                   detail::is_callable_with_index_v<Fn, signal, bool> ||
+                   detail::is_callable_without_index_v<Fn, signal, void> ||
+                   detail::is_callable_with_index_v<Fn, signal, void> );
+
+    if (n == 0 || is_pi(n)) { return; }    
+
+    abc::Gia_Obj_t * pObj = abc::Gia_ManObj(gia_, n);
+    if constexpr ( detail::is_callable_without_index_v<Fn, signal, bool> )
+    {
+      if (!fn(signal(abc::Gia_ObjFaninC0(pObj) ? Gia_Not(abc::Gia_ObjFanin0(pObj)) : abc::Gia_ObjFanin0(pObj)))) {
+        return;
+      }
+      fn(signal(abc::Gia_ObjFaninC1(pObj) ? Gia_Not(abc::Gia_ObjFanin1(pObj)) : abc::Gia_ObjFanin1(pObj)));
+    }
+    else if constexpr ( detail::is_callable_with_index_v<Fn, signal, bool> )
+    {
+      if (!fn(signal(abc::Gia_ObjFaninC0(pObj) ? Gia_Not(abc::Gia_ObjFanin0(pObj)) : abc::Gia_ObjFanin0(pObj))), 0) {
+        return;
+      }
+      fn(signal(abc::Gia_ObjFaninC1(pObj) ? Gia_Not(abc::Gia_ObjFanin1(pObj)) : abc::Gia_ObjFanin1(pObj)), 1);
+    }
+    else if constexpr ( detail::is_callable_without_index_v<Fn, signal, void> )
+    {
+      fn(signal(abc::Gia_ObjFaninC0(pObj) ? Gia_Not(abc::Gia_ObjFanin0(pObj)) : abc::Gia_ObjFanin0(pObj)));
+      fn(signal(abc::Gia_ObjFaninC1(pObj) ? Gia_Not(abc::Gia_ObjFanin1(pObj)) : abc::Gia_ObjFanin1(pObj)));
+    }
+    else if constexpr ( detail::is_callable_with_index_v<Fn, signal, void> )
+    {
+      fn(signal(abc::Gia_ObjFaninC0(pObj) ? Gia_Not(abc::Gia_ObjFanin0(pObj)) : abc::Gia_ObjFanin0(pObj)), 0);
+      fn(signal(abc::Gia_ObjFaninC1(pObj) ? Gia_Not(abc::Gia_ObjFanin1(pObj)) : abc::Gia_ObjFanin1(pObj)), 1);
+    }
+  }  
+
+  int literal(const signal& f) const
+  {
+    return (abc::Gia_ObjId(gia_, f.obj()) << 1) + abc::Gia_IsComplement(f.obj());
+  }
+  
+  int node_to_index(node n) const
+  {
+    return n;
+  }
+
+  auto num_pis() const { return abc::Gia_ManPiNum(gia_); }
+  auto num_pos() const { return abc::Gia_ManPoNum(gia_); }
+  auto num_gates() const { return abc::Gia_ManAndNum(gia_); }
+  auto num_levels() const { return abc::Gia_ManLevelNum(gia_); }
+  auto size() const { return abc::Gia_ManObjNum(gia_); }
+
+  bool load_rc() {
+    abc::Abc_Frame_t * abc = abc::Abc_FrameGetGlobalFrame();
+    const int success = abc::Cmd_CommandExecute(abc, default_rc);
+    if (success != 0) {
+      printf("syntax error in script\n");
+    }
+    return success == 0;
+  }
+
+  bool run_opt_script(const std::string &script) {
+    abc::Gia_Man_t * gia = abc::Gia_ManDup(gia_);
+    abc::Abc_Frame_t * abc = abc::Abc_FrameGetGlobalFrame();
+    abc::Abc_FrameUpdateGia(abc, gia);
+
+    const int success = abc::Cmd_CommandExecute(abc, script.c_str());
+    if (success != 0) {
+      printf("syntax error in script\n");
+    }
+
+    abc::Gia_Man_t * new_gia = abc::Abc_FrameGetGia(abc);
+    abc::Gia_ManStop(gia_);
+    gia_ = new_gia;
+    
+    return success == 0;
+  }
+
+private:
+  const char * default_rc =
+    "alias b balance;\n"
+    "alias rw rewrite;\n"
+    "alias rwz rewrite -z;\n"
+    "alias rf refactor;\n"
+    "alias rfz refactor -z;\n"
+    "alias rs resub;\n"
+    "alias rsz resub -z;\n"
+    "alias &r2rs '&put; b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b; &get';\n"
+    "alias &c2rs '&put; b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l; &get';\n"
+    "alias compress2rs 'b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l';\n"
+    "alias resyn2rs 'b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b;'\n"
+    "alias resyn2rs2 'b; rs -K 6; rw; rs -K 6 -N 2; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rs -K 12 -N 2; rwz; b;'\n";
+
+private:
+  abc::Gia_Man_t *gia_;
+}; // gia_network
+
+} // mockturtle
+
+#endif
diff --git a/include/mockturtle/utils/abc.hpp b/include/mockturtle/utils/abc.hpp
new file mode 100644
index 000000000..5988a1e2c
--- /dev/null
+++ b/include/mockturtle/utils/abc.hpp
@@ -0,0 +1,118 @@
+/* mockturtle: C++ logic network library
+ * Copyright (C) 2018-2023  EPFL
+ *
+ * Permission is hereby granted, free of charge, to any person
+ * obtaining a copy of this software and associated documentation
+ * files (the "Software"), to deal in the Software without
+ * restriction, including without limitation the rights to use,
+ * copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the
+ * Software is furnished to do so, subject to the following
+ * conditions:
+ *
+ * The above copyright notice and this permission notice shall be
+ * included in all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+ * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
+ * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
+ * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+ * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+ * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+ * OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+/*!
+  \file abc.hpp
+  \brief Utility functions for interfacing with ABC
+
+  \author Siang-Yun (Sonia) Lee
+*/
+
+#pragma once
+#ifdef ENABLE_ABC
+
+#include "../networks/aig.hpp"
+#include "../networks/gia.hpp"
+
+namespace mockturtle
+{
+
+void aig_to_gia(gia_network &gia, aig_network aig) {
+  using aig_node = aig_network::node;
+  using aig_signal = aig_network::signal;
+
+  std::vector<gia_signal> a_to_g(aig.size());
+
+  /* constant */
+  a_to_g[0] = gia.get_constant(false);
+
+  /* pis */
+  aig.foreach_pi([&](aig_node n) {
+    a_to_g[n] = gia.create_pi();
+  });
+
+  /* ands */
+  aig.foreach_gate([&](aig_node n){
+    std::array<gia_signal, 2u> fis;
+    aig.foreach_fanin(n, [&](aig_signal fi, int index){
+      fis[index] = aig.is_complemented(fi) ? !a_to_g[aig.get_node(fi)] : a_to_g[aig.get_node(fi)];
+    });
+    a_to_g[n] = gia.create_and(fis[0], fis[1]);
+  });
+
+  /* pos */
+  aig.foreach_po([&](aig_signal f){
+    gia.create_po(aig.is_complemented(f) ? !a_to_g[aig.get_node(f)] : a_to_g[aig.get_node(f)]);
+  });
+}
+
+void gia_to_aig(aig_network aig, const gia_network &gia) {
+  using gia_node = gia_network::node;
+  using gia_signal = gia_network::signal;
+
+  std::vector<aig_network::signal> g_to_a(gia.size());
+
+  /* constant */
+  g_to_a[0] = aig.get_constant(false);
+
+  /* pis */
+  gia.foreach_pi([&](gia_network::node n){
+    g_to_a[n] = aig.create_pi();
+  });
+
+  /* ands */
+  gia.foreach_gate([&](gia_network::node n){
+    std::array<aig_network::signal, 2u> fis;
+    gia.foreach_fanin(n, [&](gia_signal fi, int index){
+      fis[index] = gia.is_complemented(fi) ? !g_to_a[gia.get_node(fi)] : g_to_a[gia.get_node(fi)];
+    });
+    
+    g_to_a[n] = aig.create_and(fis[0], fis[1]);
+  });
+
+  /* pos */
+  gia.foreach_po([&](gia_network::signal f){
+    aig.create_po(gia.is_complemented(f) ? !g_to_a[gia.get_node(f)] : g_to_a[gia.get_node(f)]);
+  });
+}
+
+aig_network call_abc_script( aig_network const& aig, std::string const& script )
+{
+  gia_network gia( aig.size() << 1 );
+  aig_to_gia( gia, aig );
+
+  gia.load_rc();
+  gia.run_opt_script( script );
+
+  aig_network new_aig;
+  gia_to_aig( new_aig, gia );
+
+  new_aig = cleanup_dangling( new_aig );
+  return new_aig;
+}
+
+}
+
+#endif
\ No newline at end of file