From 089ff5570b335574a548f77542182cd2f2085b89 Mon Sep 17 00:00:00 2001 From: Karel Peeters Date: Fri, 18 Dec 2020 15:16:13 +0100 Subject: [PATCH 1/2] Initial working implementation. --- include/kitty/threshold_identification.hpp | 167 +++++++++++++++++++-- 1 file changed, 156 insertions(+), 11 deletions(-) diff --git a/include/kitty/threshold_identification.hpp b/include/kitty/threshold_identification.hpp index 02533d8e..e7eaca52 100755 --- a/include/kitty/threshold_identification.hpp +++ b/include/kitty/threshold_identification.hpp @@ -33,12 +33,33 @@ #pragma once #include -// #include /* uncomment this line to include lp_solve */ +#include #include "traits.hpp" +#include "isop.hpp" namespace kitty { +namespace util +{ + +//TODO start using this again +/// Returns 1 for pos unate, -1 for neg unate and 0 for binate +template::value>> +int is_unate( const TT& tt, uint8_t var_index ) +{ + auto const tt0 = cofactor0( tt, var_index ); + auto const tt1 = cofactor1( tt, var_index ); + + if ( is_const0( tt0 & ~tt1 ) ) + return 1; + if ( is_const0( tt1 & ~tt0 ) ) + return -1; + return 0; +} + +} // namespace util + /*! \brief Threshold logic function identification Given a truth table, this function determines whether it is a threshold logic function (TF) @@ -56,21 +77,145 @@ namespace kitty \return `true` if `tt` is a TF; `false` if `tt` is a non-TF. */ template::value>> -bool is_threshold( const TT& tt, std::vector* plf = nullptr ) +bool is_threshold( const TT& tt_orig, std::vector* plf = nullptr ) { - std::vector linear_form; + auto num_vars = tt_orig.num_vars(); - /* TODO */ - /* if tt is non-TF: */ - return false; + //convert to positive unate + auto tt_star( tt_orig ); + std::vector flipped; - /* if tt is TF: */ - /* push the weight and threshold values into `linear_form` */ - if ( plf ) + for ( uint8_t var_index = 0u; var_index < num_vars; var_index++ ) { - *plf = linear_form; + auto const tt0 = cofactor0( tt_star, var_index ); + auto const tt1 = cofactor1( tt_star, var_index ); + + if ( is_const0( tt0 & ~tt1 ) ) + { + //pos unate + flipped.push_back( false ); + } + else if ( is_const0( tt1 & ~tt0 ) ) + { + //neg unate + flip_inplace( tt_star, var_index ); + flipped.push_back( true ); + } + else + { + //binate + return false; + } + } + + //construct ILP + lprec* lp = make_lp( 0, num_vars + 1 ); + set_col_name(lp, 1, "T"); + for (int i = 0; i < num_vars + 1; i++) { + set_int(lp, i + 1, true); + } + + auto col_indices = new int[num_vars+1]; + auto row_values = new double[num_vars+1]; + + //-T as first col + col_indices[0] = 1; + row_values[0] = -1; + + set_add_rowmode( lp, true ); + + std::vector on_sets = isop( tt_star ); + std::vector off_sets = isop( ~tt_star ); + + for ( auto on_cube : on_sets ) + { + std::cout << "on cube: "; + on_cube.print(num_vars); + std::cout << std::endl; + + int j = 1; + + for ( int i = 0; i < num_vars; i++ ) + { + if ( on_cube.get_mask( i ) && on_cube.get_bit( i ) ) + { + col_indices[j] = i + 2; + row_values[j] = 1; + j++; + } + } + + add_constraintex( lp, j, row_values, col_indices, GE, 0 ); } - return true; + + for ( auto off_cube : off_sets ) + { + int j = 1; + + std::cout << "off cube: "; + off_cube.print(num_vars); + std::cout << std::endl; + + for ( int i = 0; i < num_vars; i++ ) + { + if ( !off_cube.get_mask( i ) && !off_cube.get_bit( i ) ) + { + col_indices[j] = i + 2; + row_values[j] = 1; + j++; + } + } + + add_constraintex( lp, j, row_values, col_indices, LE, -1 ); + } + + set_add_rowmode( lp, false ); + + //add objective + set_minim( lp ); + for ( int i = 0; i < num_vars + 1; i++ ) + { + col_indices[i] = i + 1; + row_values[i] = 1; + } + set_obj_fnex( lp, num_vars + 1, row_values, col_indices ); + + write_LP( lp, stdout ); + + auto result = solve(lp); + bool solved = false; + + if (result == OPTIMAL) { + + print_solution(lp, num_vars+1); + + solved = true; + if (plf) { + plf->clear(); + get_variables(lp, row_values); + auto t_result = row_values[0]; + for (int i = 0; i < num_vars; i++) { + plf->push_back((int64_t) row_values[i + 1]); + if (flipped[i]) { + t_result -= plf->back(); + plf->back() *= -1; + } + } + plf->push_back((int64_t) t_result); + } + + std::cout << "Linear form: "; + for (auto x : *plf) { + std::cout << x << ", "; + } + std::cout << std::endl; + + } + + delete[] col_indices; + delete[] row_values; + + return solved; } } /* namespace kitty */ From 13055179d09b38e7cd7187830674d9fdcca99f07 Mon Sep 17 00:00:00 2001 From: Karel Peeters Date: Sat, 19 Dec 2020 14:36:25 +0100 Subject: [PATCH 2/2] Extract utility function and reformat code. --- include/kitty/threshold_identification.hpp | 64 ++++++++++------------ 1 file changed, 28 insertions(+), 36 deletions(-) diff --git a/include/kitty/threshold_identification.hpp b/include/kitty/threshold_identification.hpp index e7eaca52..569ac38b 100755 --- a/include/kitty/threshold_identification.hpp +++ b/include/kitty/threshold_identification.hpp @@ -87,36 +87,29 @@ bool is_threshold( const TT& tt_orig, std::vector* plf = nullptr ) for ( uint8_t var_index = 0u; var_index < num_vars; var_index++ ) { - auto const tt0 = cofactor0( tt_star, var_index ); - auto const tt1 = cofactor1( tt_star, var_index ); + auto x = util::is_unate( tt_orig, var_index ); - if ( is_const0( tt0 & ~tt1 ) ) + if ( x == 0 ) { - //pos unate - flipped.push_back( false ); + return false; } - else if ( is_const0( tt1 & ~tt0 ) ) + else if ( x == -1 ) { - //neg unate flip_inplace( tt_star, var_index ); - flipped.push_back( true ); - } - else - { - //binate - return false; } + flipped.push_back(x == -1); } //construct ILP lprec* lp = make_lp( 0, num_vars + 1 ); - set_col_name(lp, 1, "T"); - for (int i = 0; i < num_vars + 1; i++) { - set_int(lp, i + 1, true); + set_col_name( lp, 1, "T" ); + for ( int i = 0; i < num_vars + 1; i++ ) + { + set_int( lp, i + 1, true ); } - auto col_indices = new int[num_vars+1]; - auto row_values = new double[num_vars+1]; + auto col_indices = new int[num_vars + 1]; + auto row_values = new double[num_vars + 1]; //-T as first col col_indices[0] = 1; @@ -130,7 +123,7 @@ bool is_threshold( const TT& tt_orig, std::vector* plf = nullptr ) for ( auto on_cube : on_sets ) { std::cout << "on cube: "; - on_cube.print(num_vars); + on_cube.print( num_vars ); std::cout << std::endl; int j = 1; @@ -153,7 +146,7 @@ bool is_threshold( const TT& tt_orig, std::vector* plf = nullptr ) int j = 1; std::cout << "off cube: "; - off_cube.print(num_vars); + off_cube.print( num_vars ); std::cout << std::endl; for ( int i = 0; i < num_vars; i++ ) @@ -182,34 +175,33 @@ bool is_threshold( const TT& tt_orig, std::vector* plf = nullptr ) write_LP( lp, stdout ); - auto result = solve(lp); + //solve LP + auto result = solve( lp ); bool solved = false; - if (result == OPTIMAL) { + if ( result == OPTIMAL ) + { - print_solution(lp, num_vars+1); + print_solution( lp, num_vars + 1 ); solved = true; - if (plf) { + if ( plf ) + { + //convert solution to expected return format plf->clear(); - get_variables(lp, row_values); + get_variables( lp, row_values ); auto t_result = row_values[0]; - for (int i = 0; i < num_vars; i++) { - plf->push_back((int64_t) row_values[i + 1]); - if (flipped[i]) { + for ( int i = 0; i < num_vars; i++ ) + { + plf->push_back( (int64_t)row_values[i + 1] ); + if ( flipped[i] ) + { t_result -= plf->back(); plf->back() *= -1; } } - plf->push_back((int64_t) t_result); - } - - std::cout << "Linear form: "; - for (auto x : *plf) { - std::cout << x << ", "; + plf->push_back( (int64_t)t_result ); } - std::cout << std::endl; - } delete[] col_indices;