(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 )

Click on bigger image: https://raw.githubusercontent.com/DennisYurichev/yurichev.com/master/blog/gray/Gray_code_rotary_encoder_13-track_opened.jpg.

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

( Source: http://homepages.dordt.edu/~ddeboer//S10/304/c_at_d/304S10_RC_TRK.HTM )

Click on bigger one: https://raw.githubusercontent.com/DennisYurichev/yurichev.com/master/blog/gray/Rotary_Encoder_track_detail.gif.

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: # s.add(Or( # 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)) s.add(Or(r)) # 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))] s.add(Or(t)) 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: s.add(ch[i][bit]==Xor(code[i][bit],code[(i+1)&MASK][bit])) # 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: s.add(AtMost(*(t+[CHANGES_MAX]))) 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.

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_

( https://groups.google.com/forum/#!topic/rec.puzzles/Dh2H-pGJcbI )

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):