OKlibrary  0.2.1.6

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:
• 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)\$

[X : bna_var_l('x,1,m), Y : bna_var_l('y,1,n),
Z : bna_var_l('z,1,max(m,n)+1)],
[append(X,Y,Z),create_list(
union(
i,0,2^length(X)-1,j,0,2^length(Y)-1)]\$

[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],
[V,listify(
```
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