Generating Hamming Codes

Problem Specification

Generate a Hamming code that fits in b - bit words to code n symbols where the Hamming distance between every two symbol codes is at least b. The Hamming distance between two words is the number of bit positions where they differ.

Viewpoint and Constraints

A b - bit word is modeled by a set s $\subseteq$ {1,...,b} where e$\in$ s means that the bit at position e is set (resp. unset otherwise). The Hamming distance h(a, b) between two words a and b represented as sets s_a and s_b can be computed by subtracting from the word size b the number of elements that is contained ( #(s_a $\cap$ s_b)) resp. is not contained ( #({1,..., b} $\setminus$ s_a $\cup$ s_b)) in both sets. Thus, the Hamming distance results in

h(a, b) = s_b - # ( s_a $\cap$ s_b) - #({1,...,b \s_a $\cup$ s_b).

Script

 
fun hamming bits distance numsymbols space =
    let
       val xs = List.tabulate(numsymbols,(fn x => 
                    FS.upperBound(space,#[(1,bits)])))
       val tmp = FS.Value.make(space,#[(1,bits)])
       fun minDist(x,y)= 
           let
              val tmp1 = FS.setvar space
              val tmp2 = FS.setvar space
              val tmp3 = FS.setvar space
              val tmp4 = FD.intvar(space,#[(0,bits)])
              val tmp5 = FD.intvar(space,#[(0,bits)])
           in
             (FS.relOp(space,x,FS.INTER,y,FS.SEQ,tmp1);
              FS.relOp(space,x,FS.UNION,y,FS.SEQ,tmp2);
              FS.relOp(space,tmp,FS.MINUS,tmp2,FS.SEQ,tmp3);
              FS.cardinality(space,tmp1,tmp4);
              FS.cardinality(space,tmp3,tmp5);
              post(space,`bits `- FD(tmp4) `- FD(tmp5) 
                         `>= `distance,FD.DOM))
           end 
       fun forallTail([y])= ()
         | forallTail(y::ys) = (List.app(fn x => 
                          minDist(y,x))(ys);forallTail ys)
    in
       forallTail(xs);
       FS.setvarbranch(space,Vector.fromList xs,
                             FS.FSB_NONE,FS.FSB_MIN);
       xs
    end

The Script in Listing 27 generates a Hamming code for numsymbols symbols in words with bits bits and a Hamming distance of distance. The procedure minDist implements the constraint that the Hamming distance does not exceed the value of distance. The list xs holds the sets representing the single codes. The nested loop forallTail imposes minDist on all pairwise distinct elements of xs. The branching employs straightforwardly a naive strategy.

The following code generates a Hamming code for 16 symbols using 7 bit words and ensures a Hamming distance of 2.

val distance = 2
val bits = 7
val numsymbols = 16 

let 
    val(s,r) = valOf(Search.searchOne
                (hamming bits distance numsymbols))
in
    List.map(fn y => domainToList y)
     (List.map(fn x =>FS.Reflect.upperBound(s,x))r)
end