1
Vote

Strange/Wrong result

description

I am testing z3 for the following problem, when I am trying to find unknown values in the model it returns me unsat. But when I am giving it exact values for the for the unknown parameters for which model is SAT, it still returns me unsat. I have tested 4.3.2 on windows and 4.4 on linux they both give me wrong result. What can be the reason for that? is there any way to find out the conflict between constraint due to which result is unsat? without using "assert_and_track()". I have tried to solve this problem with hand and with other solvers, basically we know the analytical solution, but z3 is returning UNSAT. which is not correct. Please have a look into it: To use exact values for which model is SAT please uncomment the values of a,b,c,d,e,f,g,h,i,j,k1,l, m1 and comment the section which has range of values.
from z3 import*
import time


start_time= time.time()
a,b,c,d,e,f,g,h,i,j,k1,l, m1 = Reals('a b c d e f g h i j k1 l m1')

k = [ [Real("k_%s_%s" %(i+1, j+1))  for j in range(6) ] for i in range(6)] 
m = [ [Real("m_%s_%s" %(i+1, j+1))  for j in range(6) ] for i in range(6)]
psi = [ [Real("psi_%s_%s" %(i+1, j+1))  for j in range(6) ] for i in range(6)]
omg = [ [Real("omg_%s_%s" %(i+1, j+1))  for j in range(6) ] for i in range(6)]
mul = [ [Real("mul_%s_%s" %(i+1, j+1))  for j in range(6) ] for i in range(6)]



k_psi= [[sum(a*b for a,b in zip(k_row,psi_col)) for psi_col in zip(*psi)] for k_row in k]
m_psi= [[sum(a*b for a,b in zip(m_row, psi_col)) for psi_col in zip(*psi)] for m_row in m]
m_psi_omg= [[sum(a*b for a,b in zip(m_psi_row,omg_col)) for omg_col in zip(*omg)] for m_psi_row in m_psi]

result = [  (mul[i][j]==(k_psi[i][j] - m_psi_omg[i][j])) for i in range (6) for j in range(6)]


s = Solver()



s.add(a>=0)
s.add(b>=0)
s.add(c>=0)
s.add(d>=0)
s.add(e>=0)
s.add(f>=0)
s.add(g>=0)
s.add(a<=500)
s.add(b<=500)
s.add(c<=500)
s.add(d<=500)
s.add(e<=500)
s.add(f<=500)
s.add(g<=500)
s.add(h>=0)
s.add(i>=0)
s.add(j>0)
s.add(k1>=0)
s.add(l>0)
s.add(m1>=0)
s.add(h<=1)
s.add(i<=1)
s.add(j<=1)
s.add(k1<=1)
s.add(l<=1)
s.add(m1<=1)
s.add((h+i+j+k1+l+m1)==2.25)

"""
s.add(a==200)
s.add(b==300)
s.add(c==300)
s.add(d==375)
s.add(e==200)
s.add(f==250)
s.add(g==125)
s.add(h==0.24)
s.add(i==0.31)
s.add(j==0.17)
s.add(k1==0.12)
s.add(l==0.85)
s.add(m1==0.56)
"""

s.add(result)

s.add(k[0][0]==a + b + d)
s.add(k[0][1]==-b)
s.add(k[0][2]==-d)
s.add(k[0][3]== 0)
s.add(k[0][4]==0)
s.add(k[0][5]==0)
s.add(k[1][0]==-b)
s.add(k[1][1]==b + c)
s.add(k[1][2]==-c)
s.add(k[1][3]==0)
s.add(k[1][4]==0)
s.add(k[1][5]==0)
s.add(k[2][0]==-d)
s.add(k[2][1]==-c)
s.add(k[2][2]==c + d + e)
s.add(k[2][3]==-e)
s.add(k[2][4]==0)
s.add(k[2][5]==0)
s.add(k[3][0]==0)
s.add(k[3][1]==0)
s.add(k[3][2]==-e)
s.add(k[3][3]==(e+f))
s.add(k[3][4]==-f)
s.add(k[3][5]==0)
s.add(k[4][0]==0)
s.add(k[4][1]==0)
s.add(k[4][2]==0)
s.add(k[4][3]==-f)
s.add(k[4][4]== f+g)
s.add(k[4][5]==-g)
s.add(k[5][0]==0)
s.add(k[5][1]==0)
s.add(k[5][2]==0)
s.add(k[5][3]==0)
s.add(k[5][4]==-g)
s.add(k[5][5]==g)

s.add(m[0][0]==h)
s.add(m[0][1]==0)
s.add(m[0][2]==0)
s.add(m[0][3]==0)
s.add(m[0][4]==0)
s.add(m[0][5]==0)
s.add(m[1][0]==0)
s.add(m[1][1]==i)
s.add(m[1][2]==0)
s.add(m[1][3]==0)
s.add(m[1][4]==0)
s.add(m[1][5]==0)
s.add(m[2][0]==0)
s.add(m[2][1]==0)
s.add(m[2][2]==j)
s.add(m[2][3]==0)
s.add(m[2][4]==0)
s.add(m[2][5]==0)
s.add(m[3][0]==0)
s.add(m[3][1]==0)
s.add(m[3][2]==0)
s.add(m[3][3]==k1)
s.add(m[3][4]==0)
s.add(m[3][5]==0)
s.add(m[4][0]==0)
s.add(m[4][1]==0)
s.add(m[4][2]==0)
s.add(m[4][3]==0)
s.add(m[4][4]==l)
s.add(m[4][5]==0)
s.add(m[5][0]==0)
s.add(m[5][1]==0)
s.add(m[5][2]==0)
s.add(m[5][3]==0)
s.add(m[5][4]==0)
s.add(m[5][5]==m1)


s.add(psi[0][0]==-0.29462279543992203612)
s.add(psi[0][1]==-0.79078221481674182414)
s.add(psi[0][2]==0.75534135855179973529)
s.add(psi[0][3]==0.21116735598066815882)
s.add(psi[0][4]==0.96993759493551989781)
s.add(psi[0][5]==-0.4337175318369222432)
s.add(psi[1][0]==-0.35306760795528230323)
s.add(psi[1][1]==-1)
s.add(psi[1][2]==1)
s.add(psi[1][3]==-0.47014632232760678043)
s.add(psi[1][4]==-0.48226340764609254563)
s.add(psi[1][5]==-0.1096723188102655816)
s.add(psi[2][0]==-0.39803202612065768928)
s.add(psi[2][1]==-0.88767490355683298375)
s.add(psi[2][2]==0.71439112846711949611)
s.add(psi[2][3]==0.42914165674611098877)
s.add(psi[2][4]==0.10656842365141939999)
s.add(psi[2][5]==1)
s.add(psi[3][0]==-0.64687006248760992033)
s.add(psi[3][1]==-0.66607552014599125112)
s.add(psi[3][2]==-0.10241254986014626527)
s.add(psi[3][3]==1)
s.add(psi[3][4]==-1)
s.add(psi[3][5]==-0.53974847242042967022)
s.add(psi[4][0]==-0.83446787254965248959)
s.add(psi[4][1]==-0.38930973836405058375)
s.add(psi[4][2]==-0.73062945726975181415)
s.add(psi[4][3]==-0.10498663551466924648)
s.add(psi[4][4]==0.08066814925499826705)
s.add(psi[4][5]==0.02447475459544082993)
s.add(psi[5][0]==-1)
s.add(psi[5][1]==0.98798550662681383638)
s.add(psi[5][2]==0.56246993127549760327)
s.add(psi[5][3]==0.0077334703222273117745)
s.add(psi[5][4]==-0.0046498326038086346124)
s.add(psi[5][5]==-0.00081428285654484573296)


s.add(omg[0][0]==6.078580064)
s.add(omg[0][1]==0)
s.add(omg[0][2]==0)
s.add(omg[0][3]==0)
s.add(omg[0][4]==0)
s.add(omg[0][5]==0)
s.add(omg[1][0]==0)
s.add(omg[1][1]==17.64002638)
s.add(omg[1][2]==0)
s.add(omg[1][3]==0)
s.add(omg[1][4]==0)
s.add(omg[1][5]==0)
s.add(omg[2][0]==0)
s.add(omg[2][1]==0)
s.add(omg[2][2]==22.65308167)
s.add(omg[2][3]==0)
s.add(omg[2][4]==0)
s.add(omg[2][5]==0)
s.add(omg[3][0]==0)
s.add(omg[3][1]==0)
s.add(omg[3][2]==0)
s.add(omg[3][3]==57.03933785)
s.add(omg[3][4]==0)
s.add(omg[3][5]==0)
s.add(omg[4][0]==0)
s.add(omg[4][1]==0)
s.add(omg[4][2]==0)
s.add(omg[4][3]==0)
s.add(omg[4][4]==63.99744279)
s.add(omg[4][5]==0)
s.add(omg[5][0]==0)
s.add(omg[5][1]==0)
s.add(omg[5][2]==0)
s.add(omg[5][3]==0)
s.add(omg[5][4]==0)
s.add(omg[5][5]==83.26059249)


s.add(mul[0][0]==0)
s.add(mul[0][1]==0)
s.add(mul[0][2]==0)
s.add(mul[0][3]==0)
s.add(mul[0][4]==0)
s.add(mul[0][5]==0)

s.add(mul[1][0]==0)
s.add(mul[1][1]==0)
s.add(mul[1][2]==0)
s.add(mul[1][3]==0)
s.add(mul[1][4]==0)
s.add(mul[1][5]==0)

s.add(mul[2][0]==0)
s.add(mul[2][1]==0)
s.add(mul[2][2]==0)
s.add(mul[2][3]==0)
s.add(mul[2][4]==0)
s.add(mul[2][5]==0)


s.add(mul[3][0]==0)
s.add(mul[3][1]==0)
s.add(mul[3][2]==0)
s.add(mul[3][3]==0)
s.add(mul[3][4]==0)
s.add(mul[3][5]==0)


s.add(mul[4][0]==0)
s.add(mul[4][1]==0)
s.add(mul[4][2]==0)
s.add(mul[4][3]==0)
s.add(mul[4][4]==0)
s.add(mul[4][5]==0)

s.add(mul[5][0]==0)
s.add(mul[5][1]==0)
s.add(mul[5][2]==0)
s.add(mul[5][3]==0)
s.add(mul[5][4]==0)
s.add(mul[5][5]==0)

r=s.check()
if (r==sat):
    total_time = time.time() - start_time
    
    m =s.model()
    print  r,'\n',m,'\n'
    r=[[ m.evaluate(mul[i][j]) for i in range (2)] for j in range (2)]
    print r, '\n'
    print total_time,
if (r==unsat):
    total_time = time.time() - start_time
    print "UNSAT, no model exists",'\n', total_time, s.check()

comments

wintersteiger wrote Apr 15, 2015 at 3:44 PM

There is no convenient way of finding a subset of unsatisfiable constraints without using assert_and_track (or simulating it). You can try getting a full proof instead of an unsat core, but that's likely less readable. We don't have magical debugging techniques either, so we would also have to do exactly that.

One "quick and dirty" way of getting a little bit more information is by simply removing a random subset of the constraints and checking whether it's still unsat. You can also try to do a binary search for a core that way.

UR85 wrote Apr 28, 2015 at 5:33 PM

Perhaps its not feasible to remove constraints randomly. Is it possible to create multiple backtracking points? using push() function?

wintersteiger wrote Apr 30, 2015 at 10:45 AM

Yes, using multiple push/pops is possible, but the solver may behave differently. At the first push/pop that it sees, it may have to switch to a different solver that supports incremental solving features.