How to distinguish between positive and negative integers for Binary Decision Diagrams

I have a CSV file with values and I am currently formulating a propositional formulae.

Here is a sample:

 x=6,y=-5,z=4.
 6 = 110
-5 = 1101 
 4 = 100

My formulae:

( (x2 and x1 and not (x0)) and (y3 and y2 and not(y1) and y0) and (z2 and not(z1) and not(z0)) )

Now I generate a BDD with the same. If I want a human/embedded system to understand from my diagram 1101 could be represented as 13 or -5. Any negative number can have 2 representations. Is there any way that I can make it only to one?

Solution

You have various possibilities. In the following, I mainly repeat the motivaton for two's complement representation of negative numbers (https://en.wikipedia.org/wiki/Two%27s_complement).

use the same number of bits for all numbers, e.g. write all numbers with 8 bits and then use the first bit for the sign
```
 6 = 00000110
-5 = 10000101 
 4 = 00000100
```

Number zero will have two representations: 00000000 and 10000000 (+0 and -0). If you use ZDDs (zero-suppressed BDDs) instead of ordinary ROBDDs you will get very compact representation.

use the last bit for the sign, this would be very tricky for performing arithmetic, but not a problem for the representation.
```
 6 = 1100 (110 + 0)
-5 = 1011 (101 + 1) 
 4 = 1000 (100 + 0)
```

You can set the rule, that the first (the left-most) bit must be always 1. In this case, number zero is uniquely represented as 1. ROBDDs will make this a compact representation.

use two's complement, please note, that this requires fixing the number of bits, the same as in the first proposal