Hybrid exact spectral classification. (#96)

docs/canonization.rst

@@ -16,6 +16,7 @@ based on spectral transformations.
 .. doc_brief_table::
    exact_spectral_canonization
    exact_spectral_canonization_limit
+   hybrid_exact_spectral_canonization
    print_spectrum
    rademacher_walsh_spectrum
    autocorrelation_spectrum

docs/changelog.rst

@@ -31,6 +31,9 @@ v0.7 (Not yet released)
 * Constructor: ``nth_var``
   `#95 <https://github.com/msoeken/kitty/pull/95>`_
 
+* Spectral classification: ``hybrid_exact_spectral_canonization``
+  `#96 <https://github.com/msoeken/kitty/pull/96>`_
+
 v0.6 (June 2, 2019)
 -------------------
 

include/kitty/detail/constants.hpp

@@ -183,6 +183,14 @@ static constexpr uint16_t primes[] = {2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31,
                                       937, 941, 947, 953, 967, 971, 977, 983,
                                       991, 997, 1009, 1013, 1019, 1021, 1031};
 
+static constexpr int8_t log2[] = {-1, 0, 1, -1, 2, -1, -1, -1, 3, -1,
+                                  -1, -1, -1, -1, -1, -1, 4, -1, -1, -1,
+                                  -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
+                                  -1, -1, 5, -1, -1, -1, -1, -1, -1, -1,
+                                  -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
+                                  -1, -1, -1, -1, -1, -1, -1, -1, -1, -1,
+                                  -1, -1, -1, -1, 6};
+
 } // namespace detail
 } // namespace kitty
 /*! \endcond */

include/kitty/spectral.hpp

@@ -40,6 +40,7 @@
 
 #include "bit_operations.hpp"
 #include "constructors.hpp"
+#include "esop.hpp"
 #include "detail/mscfix.hpp"
 
 #include <cmath>
@@ -598,7 +599,7 @@ inline TT exact_spectral_canonization( const TT& tt, Callback&& fn = detail::exa
   entry is the representative, and the second entry indicates whether the
   solution is known to be exact or not.
 
-  The function can be passed as second argument a callback that is called with a
+  A function can be passed as second argument that is callback called with a
   vector of spectral operations necessary to transform the input function into
   the representative.
 
@@ -614,6 +615,243 @@ inline std::pair<TT, bool> exact_spectral_canonization_limit( const TT& tt, unsi
   return impl.run( fn );
 }
 
+namespace detail
+{
+
+template<class TT>
+struct anf_spectrum
+{
+public:
+  explicit anf_spectrum( const TT& tt )
+    : _anf( detail::algebraic_normal_form( tt ) ),
+      _khots( tt.num_vars() + 1, tt.construct() )
+  {
+    for ( auto i = 0; i <= tt.num_vars(); ++i )
+    {
+      create_equals( _khots[i], i );
+    }
+  }
+
+private:
+  auto permutation( unsigned i, unsigned j )
+  {
+    spectral_operation op( spectral_operation::kind::permutation, 1 << i, 1 << j );
+
+    swap_inplace( _anf, i, j );
+
+    return op;
+  }
+
+  auto input_negation( unsigned i )
+  {
+    spectral_operation op( spectral_operation::kind::input_negation, 1 << i );
+
+    _anf ^= cofactor1( _anf, i ) & nth_var<TT>( _anf.num_vars(), i, true );
+
+    return op;
+  }
+
+  auto output_negation()
+  {
+    flip_bit( _anf, 0 );
+
+    return spectral_operation( spectral_operation::kind::output_negation );
+  }
+
+  auto spectral_translation( int i, int j )
+  {
+    spectral_operation op( spectral_operation::kind::spectral_translation, 1 << i, 1 << j );
+
+    _anf ^= ( cofactor1( _anf, i ) ^ cofactor0( cofactor1( _anf, i ), j ) ) & nth_var<TT>( _anf.num_vars(), j ) & nth_var<TT>( _anf.num_vars(), i, true );
+
+    return op;
+  }
+
+  auto disjoint_translation( int i )
+  {
+    spectral_operation op( spectral_operation::kind::disjoint_translation, 1 << i );
+
+    flip_bit( _anf, 1 << i );
+
+    return op;
+  }
+
+  template<class Fn>
+  void foreach_term_of_size( uint32_t k, Fn&& fn, int64_t start = 0 )
+  {
+    auto term = find_first_one_bit( _anf & _khots[k], start );
+
+    while ( term != -1 )
+    {
+      fn( term );
+      term = find_first_one_bit( _anf & _khots[k], term + 1 );
+    }
+  }
+
+  void insert( const spectral_operation& op )
+  {
+    _transforms.push_back( op );
+  }
+
+public:
+  bool classify()
+  {
+    bool repeat = true;
+    auto rounds = 0u;
+    while ( repeat && rounds++ < 2u )
+    {
+      if ( count_ones( _anf ) < 2 )
+      {
+        break;
+      }
+
+      repeat = false;
+      for ( auto k = 2; k < _anf.num_vars(); ++k )
+      {
+        foreach_term_of_size( k, [&]( auto term ) {
+          auto mask = _anf.construct();
+          create_from_cubes( mask, {cube( term, term )} );
+
+          const auto i = find_first_one_bit( _anf & _khots[k + 1] & mask );
+          if ( i != -1 )
+          {
+            insert( input_negation( detail::log2[i & ~term] ) );
+            repeat = true;
+          }
+          else
+          {
+            foreach_term_of_size( k, [&]( auto term2 ) {
+              if ( __builtin_popcount( term ^ term2 ) == 2 )
+              {
+                const auto vari = detail::log2[term & ~term2];
+                const auto varj = detail::log2[term2 & ~term];
+
+                insert( spectral_translation( vari, varj ) );
+                repeat = true;
+              }
+            }, term + 1 );
+          }
+        } );
+      }
+    }
+
+    if ( get_bit( _anf, 0 ) )
+    {
+      insert( output_negation() );
+    }
+
+    for ( auto i = 0; i < _anf.num_vars(); ++i )
+    {
+      if ( get_bit( _anf, 1 << i ) )
+      {
+        insert( disjoint_translation( i ) );
+      }
+    }
+
+    auto mask = 0u;
+    bool disjoint = true;
+    for_each_one_bit( _anf, [&]( auto word ) {
+      if ( word & mask ) {
+        disjoint = false;
+      } else {
+        mask |= word;
+      }
+    });
+
+    if ( disjoint )
+    {
+      auto dest_var = 0;
+      for ( auto k = 2; k < _anf.num_vars(); ++k )
+      {
+        foreach_term_of_size( k, [&]( auto term ) {
+          while ( term != 0 )
+          {
+            const auto vari = detail::log2[term & ~( term - 1 )];
+
+            // swap i with dest_var
+            if ( vari != dest_var )
+            {
+              insert( permutation( vari, dest_var ) );
+            }
+            ++dest_var;
+
+            term &= ( term - 1 );
+          }
+        } );
+      }
+
+      return true;
+    }
+
+    return false;
+  }
+
+  const TT& anf() const
+  {
+    return _anf;
+  }
+
+  TT truth_table() const
+  {
+    return detail::algebraic_normal_form( _anf );
+  }
+
+  template<class Callback>
+  void get_transformations( Callback&& fn ) const
+  {
+    fn( _transforms );
+  }
+
+private:
+  TT _anf;
+  std::vector<TT> _khots;
+  std::vector<spectral_operation> _transforms;
+};
+
+}
+
+/*! \brief Exact spectral canonization (with Reed-Muller preprocessor)
+
+  A function can be passed as second argument that is callback called with a
+  vector of spectral operations necessary to transform the input function into
+  the representative.
+
+  The algorithm is based on the paper: M. Soeken, E. Testa, D.M. Miller: A
+  hybrid spectral method for checking Boolean function equivalence, PACRIM 2019.
+
+  \param tt Truth table
+  \param fn Callback to retrieve list of transformations (optional)
+ */
+template<typename TT, typename Callback = decltype( detail::exact_spectral_canonization_null_callback )>
+inline TT hybrid_exact_spectral_canonization( const TT& tt, Callback&& fn = detail::exact_spectral_canonization_null_callback )
+{
+  (void)fn;
+
+  std::vector<detail::spectral_operation> transforms;
+
+  detail::anf_spectrum<TT> anf( tt );
+
+  bool is_disjoint = anf.classify();
+  anf.get_transformations( [&]( const auto& t ) { std::copy( t.begin(), t.end(), std::back_inserter( transforms ) ); } );
+
+  if ( !is_disjoint )
+  {
+    const auto miller_repr = exact_spectral_canonization( anf.truth_table(), [&]( const auto& t ) {
+      std::copy( t.begin(), t.end(), std::back_inserter( transforms ) );
+    } );
+    detail::anf_spectrum<TT> anf_post( miller_repr );
+    anf_post.classify();
+    anf_post.get_transformations( [&]( const auto& t ) { std::copy( t.begin(), t.end(), std::back_inserter( transforms ) ); } );
+    fn( transforms );
+    return anf_post.truth_table();
+  }
+  else
+  {
+    fn( transforms );
+    return anf.truth_table();
+  }
+}
+
 /*! \brief Print spectral representation of a function in RW order
 
   \param tt Truth table

test/spectral.cpp

@@ -187,14 +187,14 @@ TEST_F( SpectralTest, distribution_test )
 TEST_F( SpectralTest, spectral_class )
 {
   const auto test_one = []( uint32_t num_vars, uint64_t word, uint32_t index ) {
-    kitty::dynamic_truth_table func( num_vars );
-    kitty::create_from_words( func, &word, &word + 1 );
+    dynamic_truth_table func( num_vars );
+    create_from_words( func, &word, &word + 1 );
     EXPECT_EQ( get_spectral_class( func ), index );
   };
 
   for ( auto v = 0u; v <= 5u; ++v )
   {
-    const auto& repr = kitty::detail::spectral_repr[v];
+    const auto& repr = detail::spectral_repr[v];
     for ( auto c = 0u; c < repr.size(); ++c )
     {
       test_one( v, repr[c], c );
@@ -212,7 +212,7 @@ TEST_F( SpectralTest, spectral_representative )
 
   for ( auto v = 0u; v <= 5u; ++v )
   {
-    const auto& repr = kitty::detail::spectral_repr[v];
+    const auto& repr = detail::spectral_repr[v];
     for ( auto c = 0u; c < repr.size(); ++c )
     {
       test_one( v, repr[c] );
@@ -244,3 +244,48 @@ TEST_F( SpectralTest, algebraic_normal_form )
   algebraic_normal_form_test<6>();
   algebraic_normal_form_test<7>();
 }
+
+template<int NumVars>
+void hybrid_exact_spectral_canonization()
+{
+  const auto& repr = detail::spectral_repr[NumVars];
+  for ( auto word : repr ) {
+    static_truth_table<NumVars> tt1;
+    create_from_words( tt1, &word, &word + 1 );
+    const auto tt2 = exact_spectral_canonization( tt1 );
+    const auto tt3 = hybrid_exact_spectral_canonization( tt1 );
+    const auto tt4 = hybrid_exact_spectral_canonization( tt2 );
+    EXPECT_EQ( tt3, tt4 );
+  }
+}
+
+TEST_F( SpectralTest, hybrid_exact_spectral_canonization )
+{
+  hybrid_exact_spectral_canonization<3>();
+  hybrid_exact_spectral_canonization<4>();
+  //hybrid_exact_spectral_canonization<5>();
+}
+
+TEST_F( SpectralTest, hybrid_exact_spectral_canonization_with_transformation )
+{
+  static_truth_table<5> tt;
+  std::vector<detail::spectral_operation> transforms;
+
+  for ( auto i = 0; i < 100; ++i )
+  {
+    create_random( tt );
+    const auto r = hybrid_exact_spectral_canonization( tt, [&]( const auto& _transforms ) { transforms = _transforms; } );
+
+    auto s = detail::spectrum::from_truth_table( tt );
+    std::for_each( transforms.begin(), transforms.end(), [&s]( const auto& t ) { s.apply( t ); } );
+    auto tt2 = tt.construct();
+    s.to_truth_table( tt2 );
+    EXPECT_EQ( r, tt2 );
+
+    s = detail::spectrum::from_truth_table( tt2 );
+    std::for_each( transforms.rbegin(), transforms.rend(), [&s]( const auto& t ) { s.apply( t ); } );
+
+    s.to_truth_table( tt2 );
+    EXPECT_EQ( tt, tt2 );
+  }
+}