word.mod

// A matrix model for the word design problem
// Brahim Hnich

//the number of words! Increase this to get better solutions!
int m =60;


range letter 0..3;
range word 1..8;
range size 1..m;




struct adj { int a; int b;};
{adj} adjacent = {<i,j> | ordered i,j in size};



var letter M[size,word];
var letter MC[size,word];


struct s { int a1; int a2; int a3; int a4; int a5; int a6;int a7; int a8; };
{s} allowed  = ...;
predicate allow(int a1, int a2, int a3, int a4, int a5, int a6,int a7, int a8) 
in allowed;


struct comp { int a; int b;};
{comp} Comps = { <0,2>, <1,3>, <2,0>, <3,1> };

predicate link(int a, int b) in Comps;

solve {
   
  
//channeling constraints
forall(j in word, i in size)
   link(M[i,j],MC[i,j]);



//This constraint restricts the words to be a member of the set "allowed".
//Each tuple a in allowed
//satisfies the following properties:
//1- the reverse of a and the complement of a differ in at least 4 positions;
//2- 0 and 2 occur together 4 times in a;
//3- 1 and 3 occur together 4 times in a.


forall(i in size)
 allow(M[i,1],M[i,2],M[i,3],M[i,4],M[i,5],M[i,6],M[i,7],M[i,8] );  



//This constraint enforces each pair of distinct words to
//differ in at least 4 positions
forall(ordered i,j in size)
   sum(k in word)  (M[i,k]=M[j,k]) <= 4 ;

//This constraint ensures that the reverse of a word and the
//complement of any other word differ in at least 4 positions
forall(ordered i,j in size)  
  sum(k in word) (M[i,9-k]=MC[j,k]) <= 4;

//Lex order the rows to break row symmetry
forall(ordered i,j in size)
 M[i,1]*16384 + M[i,2]*4096 + M[i,3]*1024 + M[i,4]*256 + M[i,5]*64 + M[i,6]*16 + M[i,7]*4 + M[i,8] <
 M[j,1]*16384 + M[j,2]*4096 + M[j,3]*1024 + M[j,4]*256 + M[j,5]*64 + M[j,6]*16 + M[j,7]*4 + M[j,8];



};
search{

//row-wise labeling
forall(i in size)
   forall( j in word)   
     tryall(v in letter) M[i,j]=v;
 
 };

// 

/*
// A solution with 112 words 
[Found using a greedy algorithm due to Emmanuel Hebrard, 
Brahim Hnich, and Toby Walsh]
G=[
[0, 0, 1, 1, 1, 3, 0, 2],
[0, 0, 1, 1, 3, 1, 2, 0],
[0, 0, 3, 3, 1, 3, 2, 0],
[0, 0, 3, 3, 3, 1, 0, 2],
[0, 2, 1, 3, 1, 1, 0, 0],
[2, 0, 1, 3, 3, 3, 0, 0],
[0, 2, 3, 1, 3, 3, 0, 0],
[2, 0, 3, 1, 1, 1, 0, 0],
[0, 1, 0, 1, 1, 0, 3, 2],
[0, 1, 0, 1, 3, 2, 1, 0],
[0, 3, 0, 3, 1, 2, 3, 0],
[2, 1, 0, 3, 3, 0, 3, 0],
[0, 1, 2, 3, 1, 0, 1, 0],
[0, 3, 0, 3, 3, 0, 1, 2],
[0, 3, 2, 1, 3, 0, 3, 0],
[2, 3, 0, 1, 1, 0, 1, 0],
[0, 1, 1, 0, 2, 1, 3, 0],
[0, 3, 3, 0, 2, 3, 1, 0],
[0, 1, 1, 0, 0, 3, 1, 2],
[2, 1, 1, 2, 2, 3, 1, 0],
[0, 1, 3, 2, 2, 1, 1, 2],
[2, 1, 3, 0, 0, 1, 1, 0],
[0, 1, 3, 2, 0, 3, 3, 0],
[0, 3, 1, 2, 0, 1, 1, 0],
[1, 0, 0, 1, 1, 0, 2, 3],
[1, 2, 0, 3, 3, 0, 0, 3],
[1, 1, 0, 0, 2, 0, 1, 3],
[1, 0, 1, 0, 2, 1, 0, 3],
[1, 1, 2, 2, 0, 2, 1, 3],
[1, 0, 3, 2, 0, 3, 0, 3],
[1, 0, 0, 1, 3, 2, 0, 1],
[1, 2, 0, 3, 1, 2, 2, 1],
[1, 1, 0, 0, 0, 2, 3, 1],
[1, 0, 1, 0, 0, 3, 2, 1],
[1, 2, 3, 0, 0, 1, 0, 1],
[1, 3, 0, 2, 2, 2, 1, 1],
[1, 0, 3, 2, 2, 1, 2, 1],
[1, 2, 1, 2, 2, 3, 0, 1],
[3, 0, 1, 2, 0, 1, 0, 1],
[3, 0, 3, 0, 2, 3, 0, 1],
[1, 0, 2, 3, 1, 0, 0, 1],
[1, 1, 2, 2, 2, 0, 3, 1],
[1, 2, 2, 1, 3, 0, 2, 1],
[1, 3, 2, 0, 0, 0, 1, 1],
[3, 0, 0, 3, 3, 0, 2, 1],
[3, 1, 0, 2, 0, 0, 1, 1],
[3, 1, 2, 0, 2, 2, 1, 1],
[3, 2, 0, 1, 1, 0, 0, 1],
[0, 0, 0, 0, 1, 1, 1, 1],
[0, 0, 2, 2, 3, 3, 1, 1],
[0, 2, 0, 2, 3, 1, 3, 1],
[1, 3, 3, 1, 0, 2, 2, 0],
[0, 2, 2, 0, 1, 3, 3, 1],
[1, 1, 1, 1, 0, 0, 0, 0],
[1, 1, 3, 3, 2, 2, 0, 0],
[1, 3, 1, 3, 2, 0, 2, 0],
[0, 0, 0, 0, 3, 3, 3, 3],
[0, 0, 2, 2, 1, 1, 3, 3],
[0, 2, 0, 2, 1, 3, 1, 3],
[2, 0, 0, 2, 1, 3, 3, 1],
[0, 2, 2, 0, 3, 1, 1, 3],
[2, 0, 2, 0, 3, 1, 3, 1],
[2, 2, 0, 0, 3, 3, 1, 1],
[2, 2, 2, 2, 1, 1, 1, 1],
[0, 0, 1, 1, 0, 0, 1, 1],
[0, 0, 1, 1, 2, 2, 3, 3],
[0, 0, 3, 3, 0, 0, 3, 3],
[1, 1, 2, 2, 3, 3, 0, 0],
[0, 2, 1, 3, 0, 2, 1, 3],
[0, 2, 1, 3, 2, 0, 3, 1],
[0, 2, 3, 1, 0, 2, 3, 1],
[0, 2, 3, 1, 2, 0, 1, 3],
[1, 1, 0, 0, 1, 1, 0, 0],
[1, 3, 0, 2, 3, 1, 2, 0],
[2, 0, 1, 3, 0, 2, 3, 1],
[2, 2, 1, 1, 2, 2, 1, 1],
[0, 0, 3, 3, 2, 2, 1, 1],
[1, 3, 2, 0, 1, 3, 2, 0],
[2, 0, 3, 1, 2, 0, 3, 1],
[2, 2, 3, 3, 0, 0, 1, 1],
[0, 1, 0, 1, 0, 1, 0, 1],
[0, 1, 0, 1, 2, 3, 2, 3],
[0, 1, 2, 3, 0, 1, 2, 3],
[1, 0, 3, 2, 3, 2, 1, 0],
[0, 3, 0, 3, 0, 3, 0, 3],
[0, 3, 0, 3, 2, 1, 2, 1],
[0, 3, 2, 1, 0, 3, 2, 1],
[0, 3, 2, 1, 2, 1, 0, 3],
[1, 0, 1, 0, 1, 0, 1, 0],
[1, 2, 1, 2, 3, 0, 3, 0],
[2, 1, 0, 3, 0, 3, 2, 1],
[2, 3, 0, 1, 2, 3, 0, 1],
[0, 1, 2, 3, 2, 3, 0, 1],
[1, 2, 3, 0, 1, 2, 3, 0],
[2, 1, 2, 1, 2, 1, 2, 1],
[2, 3, 2, 3, 0, 1, 0, 1],
[0, 1, 1, 0, 1, 0, 0, 1],
[0, 1, 1, 0, 3, 2, 2, 3],
[0, 1, 3, 2, 1, 0, 2, 3],
[1, 0, 2, 3, 2, 3, 1, 0],
[0, 3, 1, 2, 1, 2, 0, 3],
[0, 3, 1, 2, 3, 0, 2, 1],
[0, 3, 3, 0, 1, 2, 2, 1],
[0, 3, 3, 0, 3, 0, 0, 3],
[1, 0, 0, 1, 0, 1, 1, 0],
[1, 2, 0, 3, 2, 1, 3, 0],
[2, 1, 1, 2, 1, 2, 2, 1],
[2, 3, 1, 0, 3, 2, 0, 1],
[0, 1, 3, 2, 3, 2, 0, 1],
[1, 2, 2, 1, 0, 3, 3, 0],
[2, 1, 3, 0, 3, 0, 2, 1],
[2, 3, 3, 2, 1, 0, 0, 1]
];

*/
/* A solution with 107 words 
G=[
[0, 0, 1, 1, 1, 3, 0, 2],
[0, 0, 1, 1, 3, 1, 2, 0],
[0, 0, 3, 3, 1, 3, 2, 0],
[0, 0, 3, 3, 3, 1, 0, 2],
[0, 2, 1, 3, 1, 1, 0, 0],
[2, 0, 1, 3, 3, 3, 0, 0],
[0, 2, 3, 1, 3, 3, 0, 0],
[2, 0, 3, 1, 1, 1, 0, 0],
[0, 1, 0, 1, 1, 2, 3, 0],
[0, 1, 2, 3, 3, 0, 3, 0],
[0, 1, 0, 1, 3, 0, 1, 2],
[0, 1, 2, 3, 1, 2, 1, 2],
[2, 1, 0, 3, 1, 0, 1, 0],
[0, 3, 0, 3, 3, 2, 1, 0],
[2, 1, 2, 1, 3, 2, 1, 0],
[0, 3, 2, 1, 1, 0, 1, 0],
[0, 1, 1, 0, 2, 1, 3, 0],
[0, 3, 3, 0, 2, 3, 1, 0],
[0, 1, 1, 0, 0, 3, 1, 2],
[2, 1, 1, 2, 2, 3, 1, 0],
[0, 1, 3, 2, 2, 1, 1, 2],
[2, 1, 3, 0, 0, 1, 1, 0],
[0, 1, 3, 2, 0, 3, 3, 0],
[0, 3, 1, 2, 0, 1, 1, 0],
[0, 0, 0, 0, 1, 1, 1, 1],
[0, 0, 3, 3, 2, 2, 1, 1],
[0, 3, 0, 3, 2, 1, 2, 1],
[0, 3, 3, 0, 1, 2, 2, 1],
[2, 0, 0, 1, 2, 1, 3, 1],
[2, 1, 0, 0, 3, 1, 2, 1],
[2, 0, 3, 0, 3, 2, 3, 1],
[2, 1, 3, 1, 2, 2, 2, 1],
[0, 0, 0, 1, 2, 3, 1, 3],
[0, 3, 1, 1, 2, 2, 2, 3],
[0, 0, 1, 0, 3, 2, 1, 3],
[0, 3, 0, 0, 3, 3, 2, 3],
[1, 0, 0, 3, 2, 3, 3, 0],
[1, 1, 0, 0, 1, 3, 2, 0],
[1, 0, 1, 0, 1, 2, 3, 0],
[1, 1, 1, 3, 2, 2, 2, 0],
[0, 0, 0, 2, 3, 3, 3, 1],
[0, 0, 1, 1, 0, 2, 3, 1],
[0, 1, 0, 1, 0, 3, 2, 1],
[0, 1, 1, 2, 3, 2, 2, 1],
[2, 0, 0, 3, 0, 3, 1, 1],
[2, 3, 1, 3, 0, 2, 2, 1],
[2, 0, 1, 2, 1, 2, 1, 1],
[2, 3, 0, 2, 1, 3, 2, 1],
[0, 0, 0, 3, 0, 1, 3, 3],
[0, 1, 3, 3, 0, 2, 2, 3],
[0, 0, 3, 2, 1, 2, 3, 3],
[0, 1, 0, 2, 1, 1, 2, 3],
[1, 0, 0, 1, 0, 1, 1, 0],
[1, 3, 3, 1, 0, 2, 2, 0],
[1, 0, 3, 2, 3, 2, 1, 0],
[1, 3, 0, 2, 3, 1, 2, 0],
[1, 0, 0, 1, 1, 2, 2, 1],
[1, 0, 1, 0, 0, 1, 2, 3],
[3, 0, 1, 2, 2, 1, 2, 1],
[1, 1, 0, 0, 0, 2, 1, 3],
[3, 1, 0, 2, 2, 2, 1, 1],
[1, 0, 1, 0, 2, 3, 0, 1],
[1, 2, 3, 0, 2, 1, 2, 1],
[1, 1, 0, 0, 2, 0, 3, 1],
[1, 3, 2, 0, 2, 2, 1, 1],
[1, 0, 3, 2, 0, 1, 0, 1],
[1, 1, 2, 2, 0, 2, 3, 1],
[1, 2, 1, 2, 0, 3, 2, 1],
[1, 3, 0, 2, 0, 0, 1, 1],
[1, 0, 0, 3, 3, 0, 0, 1],
[1, 2, 2, 3, 3, 2, 2, 1],
[1, 0, 2, 1, 3, 2, 0, 3],
[3, 0, 2, 3, 1, 2, 0, 1],
[1, 2, 0, 0, 1, 1, 0, 3],
[1, 0, 2, 0, 1, 0, 1, 3],
[3, 0, 2, 1, 2, 0, 1, 1],
[3, 2, 0, 0, 3, 3, 0, 1],
[1, 2, 2, 1, 1, 0, 0, 1],
[1, 2, 3, 1, 2, 0, 1, 0],
[1, 2, 2, 0, 3, 1, 1, 0],
[1, 3, 3, 0, 3, 0, 0, 0],
[1, 3, 2, 1, 2, 1, 0, 0],
[0, 2, 2, 2, 3, 1, 3, 3],
[0, 2, 3, 1, 0, 0, 3, 3],
[2, 2, 1, 1, 0, 0, 1, 1],
[2, 2, 2, 2, 3, 3, 1, 1],
[0, 3, 2, 1, 0, 3, 0, 3],
[0, 2, 1, 3, 2, 0, 1, 3],
[0, 3, 1, 2, 3, 0, 0, 3],
[1, 2, 1, 3, 0, 0, 3, 0],
[0, 3, 2, 2, 1, 1, 0, 1],
[0, 3, 3, 3, 0, 0, 0, 1],
[1, 2, 2, 2, 1, 3, 3, 0],
[2, 1, 3, 2, 3, 0, 0, 1],
[2, 1, 2, 1, 0, 1, 0, 1],
[2, 2, 2, 0, 1, 1, 3, 1],
[0, 2, 3, 2, 1, 0, 1, 1],
[1, 1, 2, 3, 0, 3, 0, 0],
[0, 1, 2, 3, 2, 1, 0, 3],
[0, 2, 1, 0, 3, 0, 3, 1],
[0, 1, 3, 0, 1, 0, 0, 3],
[2, 2, 3, 3, 2, 0, 3, 1],
[2, 3, 1, 0, 1, 0, 0, 1],
[2, 3, 2, 3, 2, 3, 0, 1],
[0, 2, 2, 1, 2, 3, 3, 1],
[0, 2, 2, 3, 0, 1, 1, 1],
[1, 1, 1, 2, 1, 0, 0, 0]
];
*/