var L = sat.L 

var t1=time(),t2,t3

var m = sat.solver()

var i,j,i2,j2,row
var locations=[]
for (i=0;i<9;i++) {
  row=[]
  for(j=0;j<9;j++) {
    row.push(sat.L.variableBits([i,j], 4));
  }
  locations.push(row)
}


var bits = []
for(i=0;i<10;i++) bits[i]= L.constantBits(i);


for (i=0;i<9;i++) {
  for (j=0;j<9;j++) {
    sat.R(m,L.greaterThanOrEqual(locations[i][j], bits[1]))
    sat.R(m,L.lessThanOrEqual(locations[i][j], bits[9]))
    for(j2=0;j2<9;j2++) {
      if (j !== j2) {
        sat.F(m,L.equalBits(locations[i][j], locations[i][j2]))
      }       
    }
  }
  for(i2=0;i2<9;i2++) {
    for (j=0;j<9;j++) {
      if (i !== i2) {
        sat.F(m,L.equalBits(locations[i][j], locations[i2][j]))
      } 
    }       
  }
}

// Presets
sat.R(m,L.equalBits(locations[0][0],bits[2]))
sat.R(m,L.equalBits(locations[1][0],bits[3]))
sat.R(m,L.equalBits(locations[0][1],bits[3]))
sat.R(m,L.equalBits(locations[8][8],bits[3]))

t2=time()
sat.solve(m)
t3=time()
for (i=0;i<9;i++) {
  var row=''
  for (j=0;j<9;j++) {
    row = row + ' ' + sat.eval(m,locations[i][j]);
  }
  print(row)
}

print()
print('Setup  time: '+(t2-t1)+' ms')
print('Solver time: '+(t3-t2)+' ms')