Z3 giving unsat result for equation Solving

Question

Given a set of possible values for each variable and two equations, I wrote the below code to get the exact variable values. But Z3 is giving Unsat results.

I have created 7 instances and combined them to make a single one. And passed the instance to the z3 solver. But getting unsat result as a response but clearly it can be seen there exists a valid solution. Below is the code I have written:

from z3 import *
import sys
import io
import math
import copy

X0 = Int('X0')
X1 = Int('X1')
X2 = Int('X2')
X3 = Int('X3')
X4 = Int('X4')
P0 = Int('P0')
P1 = Int('P1')
P2 = Int('P2')
P3 = Int('P3')
P4 = Int('P4')

I =  IntSort()
P = Array('P', I, I)

P0 = 10
P1 = 20
P2 = 30
P3 = 40
P4 = 50

s = Solver()

X0_ =[1,2,6]
X1_ =[2,6,7,8]
X2_ =[2,3,6,7]
X3_ =[2,4,8,9]
X4_ =[5,6,7,8,9]
X_Con1 = [(Or([X0 == i for i in X0_]))]
X_Con2 = [(Or([X1 == i for i in X1_]))]
X_Con3 = [(Or([X2 == i for i in X2_]))]
X_Con4 = [(Or([X3 == i for i in X3_]))]
X_Con5 = [(Or([X4 == i for i in X4_]))]
S_Con = [(X0 + X1 + X2 + X3 + X4 == 15)]
P_Con = [(P0*X0 + P1*X1 + P2*X2 + P3*X3 + P4*X4 == 520)]
Solve =   X_Con1 + X_Con2 + X_Con3 + X_Con4 + X_Con5 + S_Con + P_Con
s.add(Solve)
print(Solve)
if s.check() == sat:
    m = s.model()
    r = [m.evaluate(X0,X1,X2,X3,X4)]
    print(r)
else:
    print "unsat"

Answer 1

[...] clearly it can be seen there exists a valid solution.

Actually, there isn't.

Let's modify the problem slightly and replace 520 with a fresh free variable called PFREE.

from z3 import *
import sys
import io
import math
import copy

X0 = Int('X0')
X1 = Int('X1')
X2 = Int('X2')
X3 = Int('X3')
X4 = Int('X4')
P0 = Int('P0')
P1 = Int('P1')
P2 = Int('P2')
P3 = Int('P3')
P4 = Int('P4')

PFREE = Int('PFREE')

I =  IntSort()
P = Array('P', I, I)

P0 = 10
P1 = 20
P2 = 30
P3 = 40
P4 = 50

s = Solver()

X0_ =[1,2,6]
X1_ =[2,6,7,8]
X2_ =[2,3,6,7]
X3_ =[2,4,8,9]
X4_ =[5,6,7,8,9]
X_Con1 = [(Or([X0 == i for i in X0_]))]
X_Con2 = [(Or([X1 == i for i in X1_]))]
X_Con3 = [(Or([X2 == i for i in X2_]))]
X_Con4 = [(Or([X3 == i for i in X3_]))]
X_Con5 = [(Or([X4 == i for i in X4_]))]
S_Con = [(X0 + X1 + X2 + X3 + X4 == 15)]
P_Con = [(P0*X0 + P1*X1 + P2*X2 + P3*X3 + P4*X4 == PFREE)]
Solve =   X_Con1 + X_Con2 + X_Con3 + X_Con4 + X_Con5 + S_Con + P_Con
s.add(Solve)

while s.check() == sat:
    m = s.model()
    print(m)
    blocking_clause = Or([x != m.evaluate(x) for x in [X0, X1, X2, X3, X4]])
    s.add(blocking_clause)

If we enumerate all possible solutions, none of these verifies PFREE = 520:

~$ python test.py 
[X0 = 2, X1 = 2, X2 = 2, X3 = 4, X4 = 5, PFREE = 530]
[X0 = 2, X1 = 2, X2 = 3, X3 = 2, X4 = 6, PFREE = 530]
[X0 = 1, X1 = 2, X2 = 3, X3 = 4, X4 = 5, PFREE = 550]
[X0 = 2, X1 = 2, X2 = 2, X3 = 2, X4 = 7, PFREE = 550]
[X0 = 1, X1 = 2, X2 = 2, X3 = 4, X4 = 6, PFREE = 570]
[X0 = 1, X1 = 2, X2 = 3, X3 = 2, X4 = 7, PFREE = 570]
[X0 = 1, X1 = 2, X2 = 2, X3 = 2, X4 = 8, PFREE = 590]