Generating de Bruijn sequences using Z3 SMT-solver

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

The following piece of quite esoteric code calculates number of leading zeroes:

int v[64]=
{ -1,31, 8,30, -1, 7,-1,-1, 29,-1,26, 6, -1,-1, 2,-1,
-1,28,-1,-1, -1,19,25,-1, 5,-1,17,-1, 23,14, 1,-1,
9,-1,-1,-1, 27,-1, 3,-1, -1,-1,20,-1, 18,24,15,10,
-1,-1, 4,-1, 21,-1,16,11, -1,22,-1,12, 13,-1, 0,-1 };

int LZCNT(uint32_t x)
{
x |= x >> 1;
x |= x >> 2;
x |= x >> 4;
x |= x >> 8;
x |= x >> 16;
return v[x >> 26];
}


Read more about it: https://yurichev.com/blog/de_bruijn/. The magic number used here is called "de Bruijn sequence", and I once used bruteforce to find it (the result was 0x4badf0d, which is used here). But what if we need magic number for 64-bit values? Bruteforce is not an option here.

If you alread read about this sequence in my blog or in other sources, you can see that the 32-bit magic number is a number consisting of 5-bit overlapping chunks, and all chunks must be unique, i.e., must not be repeating.

For 64-bit magic number, these are 6-bit overlapping chunks.

To find the magic number, one can find a Hamiltonian path of a de Bruijn graph. But I've found that Z3 is also can do this, though, overkill, but this is more illustrative.

#!/usr/bin/python
from z3 import *

out = BitVec('out', 64)

tmp=[]
for i in range(64):
tmp.append((out>>i)&0x3F)

s=Solver()

# all overlapping 6-bit chunks must be distinct:
# MSB must be zero:

print s.check()

result=s.model()[out].as_long()
print "0x%x" % result

# print overlapping 6-bit chunks:
for i in range(64):
t=(result>>i)&0x3F
print " "*(63-i) + format(t, 'b').zfill(6)


We just enumerate all overlapping 6-bit chunks and tell Z3 that they must be unique (see "Distinct"). Output:

sat
0x79c52dd0991abf60
100000
110000
011000
101100
110110
111011
111101
111110
111111
011111
101111
010111
101011
010101
101010
110101
011010
001101
000110
100011
010001
001000
100100
110010
011001
001100
100110
010011
001001
000100
000010
100001
010000
101000
110100
111010
011101
101110
110111
011011
101101
010110
001011
100101
010010
101001
010100
001010
000101
100010
110001
111000
011100
001110
100111
110011
111001
111100
011110
001111
000111
000011
000001
000000


Overlapping chunks are clearly visible. So the magic number is 0x79c52dd0991abf60. Let's check:

#include <stdint.h>
#include <stdio.h>
#include <assert.h>

#define MAGIC 0x79c52dd0991abf60

int magic_tbl[64];

// returns single bit position counting from LSB
// not working for i==0
int bitpos (uint64_t i)
{
return magic_tbl[(MAGIC/i) & 0x3F];
};

// trailing zeroes count
// not working for i==0
int tzcnt (uint64_t i)
{
uint64_t a=i & (-i);
return magic_tbl[(MAGIC/a) & 0x3F];
};

int main()
{
// construct magic table
// may be omitted in production code
for (int i=0; i<64; i++)
magic_tbl[(MAGIC/(1ULL<<i)) & 0x3F]=i;

// test
for (int i=0; i<64; i++)
{
printf ("input=0x%llx, result=%d\n", 1ULL<<i, bitpos (1ULL<<i));
assert(bitpos(1ULL<<i)==i);
};
assert(tzcnt (0xFFFF0000)==16);
assert(tzcnt (0xFFFF0010)==4);
};


That works!

My other notes about SAT/SMT: https://yurichev.com/writings/SAT_SMT_draft-EN.pdf.