OKlibrary  0.2.1.6
BinaryAddition.hpp File Reference

Investigations regarding the presentation of binary addition. More...

Go to the source code of this file.


Detailed Description

Investigations regarding the presentation of binary addition.

Todo:
Boolean functions representing binary addition
  • Consider n in NN_0.
  • "Boolean literals x_1, ..., x_{m} represent 0 <= k <= 2^m-1 in binary" is defined by the condition (as constraint) that sum(x_{i} * 2^(i-1),i, 1,m) = m.
  • Note here that the variables map to binary digits from the right. This allows CNF/DNF translations of binary addition of smaller numbers to be extended to addition on larger numbers, by adding variables and clauses, rather than having to rename them.
  • For m, n in NN, that a boolean function f in m+n+max(m,n)+1 variables x_1, ..., x_{m}, y_1, ..., y_{m}, z_1, ..., z_{max(m,n)+1} represents binary addition of numbers up to 2^m - 1, 2^n - 1 is defined by the following conditions:
    1. Let x, y, z be the tuples of variables.
    2. Consider x representing 0 <= p <= 2^m - 1 in (reverse) binary and y representing 0 <= q <= 2^n - 1 in (reverse) binary.
    3. Then for z representing p+q in (reverse) binary we have f(x,y,z)=1, while for all other z we have f(x,y,z)=0. This covers all cases.
Todo:
CNF and DNF representations of binary addition
  • What variables to use?
    • Perhaps bna('x,i), bna('y,i) and bna(z',i), each representing the i-th variable in the two input and then output variable lists respectively, where "bna" stands for "binary number addition".
  • At first, given p > 0 and q > 0 where m and m are the number of bits in the two input numbers, we have the full CNF and DNF representations generated by
    declare(bna,noun)$
    declare(bna,posfun)$
    bna_var(v,i) := apply(nounify(bna),[v,i])$
    bna_var_l(v,a,b) := create_list(bna_var(v,i),i,a,b)$
    
    bin_add_full_dnf_fcl_std(m,n) := block( 
      [X : bna_var_l('x,1,m), Y : bna_var_l('y,1,n),
       Z : bna_var_l('z,1,max(m,n)+1)],
      bin_add_full_dnf_fcl(X,Y,Z))$
    bin_add_full_dnf_fcl(X,Y,Z) := 
      [append(X,Y,Z),create_list(
        union(
          bv2c_wv(reverse(int2polyadic_padd(i,2,length(X))),X),
          bv2c_wv(reverse(int2polyadic_padd(j,2,length(Y))),Y),
          bv2c_wv(reverse(int2polyadic_padd(i+j,2,length(Z))),Z)),
        i,0,2^length(X)-1,j,0,2^length(Y)-1)]$
    
    bin_add_full_cnf_fcl_std(m,n) := block(
      [X : bna_var_l('x,1,m), Y : bna_var_l('y,1,n),
       Z : bna_var_l('z,1, max(m,n)+1),V],
      bin_add_full_cnf_fcl(X,Y,Z))$
    bin_add_full_cnf_fcl(X,Y,Z) := block([V : append(X,Y,Z)],
      [V,listify(
          map(comp_sl,setdifference(all_tass(V),setify(bin_add_full_dnf_fcl(X,Y,Z)[2]))))])$
       
Todo:
Smallest prime CNF-representation
  • Computing all minimum CNF representations using all_minequiv_bvsr_sub_cs gives
    1. n=1, m=1
      all_minequiv_bvsr_cs(setify(bin_add_full_cnf_fcl_std(1,1)[2]));
      [{{-bna(x,1),-bna(y,1),-bna(z,1)},{-bna(x,1),bna(y,1),bna(z,1)},
        {bna(x,1),bna(y,1),-bna(z,1)},{bna(x,1),-bna(z,2)},
        {-bna(y,1),bna(z,1),bna(z,2)},{bna(y,1),-bna(z,2)}},
       {{-bna(x,1),-bna(y,1),-bna(z,1)},
        {-bna(x,1),bna(y,1),bna(z,1)},
        {bna(x,1),bna(y,1),-bna(z,1)},
        {bna(x,1),-bna(z,2)},{-bna(y,1),bna(z,1),bna(z,2)},
        {-bna(z,1),-bna(z,2)}},
       {{-bna(x,1),-bna(y,1),-bna(z,1)},
        {-bna(x,1),bna(z,1),bna(z,2)},
        {bna(x,1),-bna(y,1),bna(z,1)},
        {bna(x,1),bna(y,1),-bna(z,1)},
        {bna(x,1),-bna(z,2)},{bna(y,1),-bna(z,2)}},
       {{-bna(x,1),-bna(y,1),-bna(z,1)},
        {-bna(x,1),bna(z,1),bna(z,2)},
        {bna(x,1),-bna(y,1),bna(z,1)},
        {bna(x,1),bna(y,1),-bna(z,1)},{bna(y,1),-bna(z,2)},{-bna(z,1),-bna(z,2)}},
       {{-bna(x,1),-bna(y,1),-bna(z,1)},{-bna(x,1),bna(z,1),bna(z,2)},
        {bna(x,1),bna(y,1),-bna(z,1)},{bna(x,1),-bna(z,2)},
        {-bna(y,1),bna(z,1),bna(z,2)},{bna(y,1),-bna(z,2)}},
       {{-bna(x,1),-bna(y,1),bna(z,2)},{-bna(x,1),bna(y,1),bna(z,1)},
        {bna(x,1),-bna(y,1),bna(z,1)},{bna(x,1),bna(y,1),-bna(z,1)},
        {bna(x,1),-bna(z,2)},{-bna(z,1),-bna(z,2)}},
       {{-bna(x,1),-bna(y,1),bna(z,2)},{-bna(x,1),bna(y,1),bna(z,1)},
        {bna(x,1),-bna(y,1),bna(z,1)},{bna(x,1),bna(y,1),-bna(z,1)},
        {bna(y,1),-bna(z,2)},{-bna(z,1),-bna(z,2)}},
       {{-bna(x,1),-bna(y,1),bna(z,2)},{-bna(x,1),bna(y,1),bna(z,1)},
        {bna(x,1),bna(y,1),-bna(z,1)},
        {bna(x,1),-bna(z,2)},{-bna(y,1),bna(z,1),bna(z,2)},{-bna(z,1),-bna(z,2)}},
       {{-bna(x,1),-bna(y,1),bna(z,2)},{-bna(x,1),bna(z,1),bna(z,2)},
        {bna(x,1),-bna(y,1),bna(z,1)},{bna(x,1),bna(y,1),-bna(z,1)},
        {bna(y,1),-bna(z,2)},{-bna(z,1),-bna(z,2)}}]
           
      with
      minBinCNFs : all_minequiv_bvsr_cs(setify(bin_add_full_cnf_fcl_std(1,1)[2]))$
      length(minBinCNFs);
      9
      length(minBinCNFs[1]);
      6
           
    2. n=2, m=1
      minBinCNFs : all_minequiv_bvsr_cs(setify(bin_add_full_cnf_fcl_std(2,1)[2]));
      length(minBinCNFs);
      84
      length(minBinCNFs[1]);
      11
      minBinCNFs[1];
      {{-bna(x,1),-bna(y,1),-bna(z,1)},{-bna(x,1),bna(y,1),bna(z,1)},
              {bna(x,1),-bna(x,2),bna(z,2)},{bna(x,1),bna(x,2),-bna(z,2)},{bna(x,1),bna(y,1),-bna(z,1)},
              {-bna(x,2),-bna(y,1),bna(z,1),-bna(z,2)},{-bna(x,2),bna(y,1),bna(z,2)},
              {bna(x,2),bna(y,1),-bna(z,2)},{bna(x,2),-bna(z,3)},{-bna(y,1),bna(z,1),bna(z,2),bna(z,3)},
              {-bna(z,2),-bna(z,3)}}
           
    3. n=2, m=2
      minBinCNFs : all_minequiv_bvsr_cs(setify(bin_add_full_cnf_fcl_std(2,2)[2]));
      length(minBinCNFs);
      144
      length(minBinCNFs[1]);
      17
      A[1];
      {{-bna(x,1),-bna(x,2),-bna(y,2),bna(z,2)},{-bna(x,1),-bna(x,2),bna(z,3)},
       {-bna(x,1),bna(x,2),-bna(y,2),-bna(z,2)},{-bna(x,1),bna(x,2),bna(y,2),bna(z,2)},
       {-bna(x,1),-bna(y,1),bna(z,1)},{-bna(x,1),bna(y,1),-bna(z,1)},
       {bna(x,1),-bna(x,2),bna(y,1),-bna(y,2),-bna(z,2)},
       {bna(x,1),-bna(x,2),bna(y,1),bna(y,2),bna(z,2)},
       {bna(x,1),bna(x,2),bna(y,1),bna(y,2),-bna(z,2)},{bna(x,1),bna(x,2),bna(y,1),-bna(z,3)},
       {bna(x,1),-bna(y,1),-bna(z,1)},{-bna(x,2),-bna(y,2),bna(z,1),bna(z,2)},
       {-bna(x,2),bna(z,1),bna(z,3)},{bna(x,2),-bna(y,2),bna(z,1),-bna(z,2)},
       {bna(x,2),bna(y,2),bna(z,1),bna(z,2)},{-bna(y,2),bna(z,2),bna(z,3)},
       {bna(y,2),-bna(z,2),-bna(z,3)}}
           
    4. n=3, m=2?
Todo:
Smallest r_1-based CNF representation
Todo:
Smallest r_2-based CNF representation

Definition in file BinaryAddition.hpp.