グレーコード

グレーコード#

グレーコードとは、隣接する値同士が1ビットだけ異なるように設計された数列であり、主に誤り訂正、エンコーディング、回路設計などで利用されます。一般的な二進数と異なり、1つの値から次の値への変化が最小限に抑えられるため、アナログ-デジタル変換などの用途でも重要な役割を果たします。

OrToolsでグレーコードを解く

from z3 import *

Int変数で解く#

以下は、Z3を用いて N ビットのグレイコードを生成するプログラムです。x % 2 ** (i + 1) - x % 2 ** i を用いて x の i 番目のビットを抽出し、2 つの整数から抽出したビットが一致しない数が 1 つだけであるという制約を課すことで、グレイコードの特性を満たすようにしています。

さらに、計算を高速化するために、連続する 2 つのコードの差分が 2 のべき乗であるという制約も追加しています。

def gray_code(nbits):
    n = 2 ** nbits
    codes = IntVector('code', n)
    solver = Solver()
    
    for c in codes:
        solver.add(0 <= c, c < n)
        
    solver.add(Distinct(codes))
    
    for c1, c2 in zip(codes, codes[1:] + codes[:1]):
        diff = Abs(c1 - c2)
        solver.add(Or([diff == 2**bit for bit in range(nbits)]))
        bit_diff = [c1 % 2**(i + 1) - c1 % 2**(i) != c2 % 2**(i + 1) - c2 % 2**(i) for i in range(nbits)]
        solver.add(Sum(bit_diff) == 1)
           
    solver.add(codes[0] == 0)
    solver.check()
    model = solver.model()
    return [model[c].as_long() for c in codes]

nbits = 4
%time codes = gray_code(nbits)
for c in codes:
    print(f'{c:0{nbits}b}')

CPU times: total: 7.33 s
Wall time: 7.95 s
0000
0100
0110
0111
0011
0010
1010
1110
1111
1011
1001
0001
0101
1101
1100
1000

BitVec変数で加速#

上記のコードは正しくグレーコードを生成できますが、整数 (Int) を使っているため、Z3 の制約解決が遅くなります。そこで、次に BitVec を用いてより効率的にグレーコードを生成する方法を示します。

Int の代わりに BitVec を使用し、前後の2つのコードの差分を XOR 演算子 (^) で求めます。グレーコードの隣接する値は1ビットだけ異なるため、この差分が「1が1つだけ立っている」ことを判定する必要があります。そのため、以下の条件を追加します。

diff = c1 ^ c2
solver.add(diff & (diff - 1) == 0, diff != 0)

これは、diff が 2 のべき乗であることを確認するための一般的なビット演算テクニックです。

def gray_code_bv(nbits):
    codes = [BitVec(f'code_{i}', nbits) for i in range(2**nbits)]
    solver = Solver()
    solver.add(Distinct(codes))
    
    for c1, c2 in zip(codes, codes[1:] + codes[:1]):
        diff = c1 ^ c2
        solver.add(diff & (diff - 1) == 0, diff != 0)
    
    solver.add(codes[0] == 0)
    
    solver.check()
    model = solver.model()
    return [model[c].as_long() for c in codes]

この方法では、BitVec を使用することで Z3 の処理が効率化され、整数 (Int) を使った場合と比べて数十倍高速にグレーコードを求めることができます。

%time codes = gray_code_bv(nbits)
for c in codes:
    print(f'{c:0{nbits}b}')

CPU times: total: 46.9 ms
Wall time: 79.9 ms
0000
0100
0110
0010
1010
1110
1100
1000
1001
1011
0011
0111
1111
1101
0101
0001
Contents