title: Checking satisfiability for matrix valued function
body: <p>I am trying to multiply 2 matrices of 2*2 order. One of the matrix contains an unknown parameter "k1". I want to check a satisfiable solution that for which value of k1. The product of two matrices will be equal to the third one. 
  Note: I dont want to convert the multiplication into a linear relation or set of equation I want to manipulate it as matrices.</p>
  
  <p>Here is where I am stuck.</p>
  
  <pre><code>k1 = Int ('k1')
  
  x = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(2) ] 
       for i in range(2) ]
  
  a =((1,k1),(3,4))
  
  b =((1,1),(1,1))
  
  c= ((3,3),(7,7))
  
  s = Solver()
  s.add(a[0][1]&gt;0)
  s.add(a*b==c)
  if s.check() == sat:
  m = s.model()
  r = [ [ m.evaluate(x[i][j]) for j in range(2) ] 
        for i in range(2) ]
  print_matrix(r)
  else:
  print "failed to solve"
  </code></pre>
  
  <p>Any way Out?</p>