## Balanced Gray code and Z3 SMT solver

(The following text has been copypasted to the SAT/SMT by example.)

Suppose, you are making a rotary encoder. This is a device that can signal its angle in some form, like:

( Taken from Wikipedia: https://en.wikipedia.org/wiki/Gray_code )

This is a rotary (shaft) encoder: https://en.wikipedia.org/wiki/Rotary_encoder. This picture is a cropped and photoshopped version:

There are pins and tracks on rotating wheel. How would you do this? Easiest way is to use binary code. But it has a problem: when a wheel is rotating, in a moment of transition from one state to another, several bits may be changed, hence, undesirable state may be present for a short period of time. This is bad. To deal with it, Gray code was invented: only 1 bit is changed during rotation. Like:

Decimal Binary  Gray
0 	0000 	0000
1 	0001 	0001
2 	0010 	0011
3 	0011 	0010
4 	0100 	0110
5 	0101 	0111
6 	0110 	0101
7 	0111 	0100
8 	1000 	1100
9 	1001 	1101
10 	1010 	1111
11 	1011 	1110
12 	1100 	1010
13 	1101 	1011
14 	1110 	1001
15 	1111 	1000


Now the second problem. Look at the picture again. It has a lot of bit changes on the outer circles. And this is electromechanical device. Surely, you may want to make tracks as long as possible, to reduce wearing of both tracks and pins. This is a first problem. The second: wearing should be even across all tracks (this is balanced Gray code).

How we can find a table for all states using Z3:

#!/usr/bin/env python

from z3 import *

BITS=5

# how many times a run of bits for each bit can be changed (max).
# it can be 4 for 4-bit Gray code or 8 for 5-bit code.
# 12 for 6-bit code (maybe even less)
CHANGES_MAX=8

ROWS=2**BITS
MASK=ROWS-1 # 0x1f for 5 bits, 0xf for 4 bits, etc

def bool_to_int (b):
if b==True:
return 1
return 0

s=Solver()

# add a constraint: Hamming distance between two bitvectors must be 1
# i.e., two bitvectors can differ in only one bit.
# for 4 bits it works like that:
#        And(a3!=b3,a2==b2,a1==b1,a0==b0),
#        And(a3==b3,a2!=b2,a1==b1,a0==b0),
#        And(a3==b3,a2==b2,a1!=b1,a0==b0),
#        And(a3==b3,a2==b2,a1==b1,a0!=b0)))
def hamming1(l1, l2):
assert len(l1)==len(l2)
r=[]
for i in range(len(l1)):
t=[]
for j in range(len(l1)):
if i==j:
t.append(l1[j]!=l2[j])
else:
t.append(l1[j]==l2[j])
r.append(And(t))

# add a constraint: bitvectors must be different.
# for 4 bits works like this:
#    s.add(Or(a3!=b3, a2!=b2, a1!=b1, a0!=b0))
def not_eq(l1, l2):
assert len(l1)==len(l2)
t=[l1[i]!=l2[i] for i in range(len(l1))]

code=[[Bool('code_%d_%d' % (r,c)) for c in range(BITS)] for r in range(ROWS)]
ch=[[Bool('ch_%d_%d' % (r,c)) for c in range(BITS)] for r in range(ROWS)]

# each rows must be different from a previous one and a next one by 1 bit:
for i in range(ROWS):
# get bits of the current row:
lst1=[code[i][bit] for bit in range(BITS)]
# get bits of the next row.
# important: if the current row is the last one, (last+1)&MASK==0, so we overlap here:
lst2=[code[(i+1)&MASK][bit] for bit in range(BITS)]
hamming1(lst1, lst2)

# no row must be equal to any another row:
for i in range(ROWS):
for j in range(ROWS):
if i==j:
continue
lst1=[code[i][bit] for bit in range(BITS)]
lst2=[code[j][bit] for bit in range(BITS)]
not_eq(lst1, lst2)

# 1 in ch[] table means that run of 1's has been changed to run of 0's, or back.
# "run" change detected using simple XOR:
for i in range(ROWS):
for bit in range(BITS):
# row overlapping works here as well:

# only CHANGES_MAX of 1 bits is allowed in ch[] table for each bit:
for bit in range(BITS):
t=[ch[i][bit] for i in range(ROWS)]
# this is a dirty hack.
# AtMost() takes arguments like:
# AtMost(v1, v2, v3, v4, 2) <- this means, only 2 booleans (or less) from the list can be True.
# but we need to pass a list here.
# so a CHANGES_MAX number is appended to a list and a new list is then passed as arguments list:

result=s.check()
if result==unsat:
exit(0)
m=s.model()

# get the model.

print "code table:"

for i in range(ROWS):
for bit in range(BITS):
# comma at the end means "no newline":
print bool_to_int(is_true(m[code[i][BITS-1-bit]])),
print ""

print "ch table:"

stat={}

for i in range(ROWS):
for bit in range(BITS):
x=is_true(m[ch[i][BITS-1-bit]])
if x:
# increment if bit is present in dict, set 1 if not present
stat[bit]=stat.get(bit, 0)+1
# comma at the end means "no newline":
print bool_to_int(x),
print ""

print "stat (bit number: number of changes): ", stat



( The source code: https://github.com/DennisYurichev/yurichev.com/blob/master/blog/gray/gray.py )

For 4 bits, 4 changes is enough:

code table:
0 1 0 1
0 0 0 1
0 0 1 1
0 0 1 0
1 0 1 0
1 0 1 1
1 1 1 1
1 1 0 1
1 0 0 1
1 0 0 0
0 0 0 0
0 1 0 0
1 1 0 0
1 1 1 0
0 1 1 0
0 1 1 1
ch table:
0 1 0 0
0 0 1 0
0 0 0 1
1 0 0 0
0 0 0 1
0 1 0 0
0 0 1 0
0 1 0 0
0 0 0 1
1 0 0 0
0 1 0 0
1 0 0 0
0 0 1 0
1 0 0 0
0 0 0 1
0 0 1 0
stat (bit number: count of changes):  {0: 4, 1: 4, 2: 4, 3: 4}



8 changes for 5 bits: https://github.com/DennisYurichev/yurichev.com/blob/master/blog/gray/5.txt. 12 for 6 bits (or maybe even less): https://github.com/DennisYurichev/yurichev.com/blob/master/blog/gray/6.txt.

### Duke Nukem 3D from 1990s

Another application of Gray code:

with.inspiring@flair.and.erudition (Mike Naylor) wrote:

>In Duke Nukem, you often come upon panels that have four buttons in a row,
>all in their "off" position. Each time you "push" a button, it toggles from
>one state to the other. The object is to find the unique combination that
>unlocks something in the game.

>My question is: What is the most efficient order in which to push the
>buttons so that every combination is tested with no wasted effort?

A Gray Code. :-)

(Oh, you wanted to know what one would be?  How about:
0000
0001
0011
0010
0110
0111
0101
0100
1100
1101
1111
1110
1010
1000
1001
1011

Or, if you prefer, with buttons A,B,C,D: D,C,D,B,D,C,D,A,D,C,D,B,C,D,C
It isn't the "canonical" Gray code (or if it is, it is by Divine
Providence), but it works.

Douglas Limmer -- lim...@math.orst.edu
"No wonder these mathematical wizards were nuts - went off the beam -
he'd be pure squirrel-food if he had half that stuff in _his_ skull!"
E. E. "Doc" Smith, _Second Stage Lensmen_


Obviously, using our solution, you can minimize all movements in this ancient videogame, for 4 switches, that would be 4*4=16 switches. With our solution (balanced Gray code), wearing would be even across all 4 switches.

Please drop me email about any bug(s) and suggestion(s): dennis(@)yurichev.com.