How to model in Z3py

Question

I have a total of seven (A, B, C, D, E, r, c) Z3 Boolean variables, where A, B, C, D, E represent the edges from a point, represented as a black dot in the following Fig.1.

The remaining two variables, i.e, r and c are the variables for the black dot point, whose values depend on edges values as follows:

The conditions for variable ‘r’: Case1: If A is true then only one variable from C or D can be true Case2: Similarly, if B is true then only variable either C or D can be true. The variable r can be true only if one of the either Case 1 or Case 2 is true and r value should always be True. These conditions are solved in Z3 solver as:

s.add(Implies(A, Xor(C,D) ))
s.add(Implies(B, Xor(C,D) )) 
s.add(r1 == Xor(A, B) )
s.add(r1 == True)

Now I have to include the following conditions for variable ‘c’ in Z3 solver:

The variable ‘c’ can be true or false. And ‘c’ will be true only if any of the following conditions meet:

Case 3: if A and C are True then c will be true if both E and D are true

Case 4: if A and D are True then c will be true if both E and C are true

Case 5: if B and C are True then c will be true if both E and D are true

Case 6: if B and D are True then c will be true if both E and C are true

How to add these conditions as I am not able to model the conditions for ‘c’ variable in Z3 solver.

score 0 · Accepted Answer · answered Jan 04 '21 at 19:21

Your description is a bit hard to follow, but you should be able to express these almost literally as follows. (I added some inline comments so you can follow the coding logic and modify as appropriate.)

from z3 import *

A, B, C, D, E, r, c = Bools('A B C D E r c')

s = Solver()

# Case 1
Case1 = Implies(A, Xor(C,D))
s.add(Case1)

# Case 2
Case2 = Implies(B, Xor(C,D))
s.add(Case2)

# Conditions for r. Your description is a bit confusing here,
# as it says both `r` is true, and if one of Case1 or Case2
# is true. This suggests one of Case1 or Case2 must be true,
# though it's not clear to me why described it in this complex
# way. Modify accordingly.
s.add(r)
s.add(Or(Case1, Case2))

# Case 3: if A and C are True then c will be true if both E and D are true
s.add(Implies(And(A, C), Implies(And(E, D), c)))

# Case 4: if A and D are True then c will be true if both E and C are true
s.add(Implies(And(A, D), Implies(And(E, C), c)))

# Case 5: if B and C are True then c will be true if both E and D are true
s.add(Implies(And(B, C), Implies(And(E, D), c)))

# Case 6: if B and D are True then c will be true if both E and C are true
s.add(Implies(And(B, D), Implies(And(E, C), c)))

vars = [A, B, C, D, E, r, c]
while s.check() == sat:
    m = s.model()
    for v in vars:
      print("%s = %5s" % (v, m.evaluate(v, model_completion = True))),
    print
    s.add(Or([p != v for p, v in [(v, m.evaluate(v, model_completion = True)) for v in vars]]))

When run, this prints:

A = False B = False C = False D = False E = False r =  True c = False
A = False B = False C =  True D = False E = False r =  True c = False
A = False B = False C =  True D =  True E = False r =  True c = False
A = False B = False C = False D =  True E = False r =  True c =  True
A = False B = False C =  True D = False E = False r =  True c =  True
A = False B = False C =  True D =  True E = False r =  True c =  True
A = False B =  True C = False D =  True E = False r =  True c =  True
A = False B =  True C =  True D = False E = False r =  True c = False
A = False B =  True C =  True D = False E = False r =  True c =  True
A =  True B =  True C =  True D = False E = False r =  True c =  True
A =  True B = False C =  True D = False E =  True r =  True c =  True
A = False B =  True C =  True D = False E =  True r =  True c =  True
A =  True B =  True C =  True D = False E =  True r =  True c = False
A =  True B =  True C =  True D = False E =  True r =  True c =  True
A = False B =  True C = False D =  True E =  True r =  True c =  True
A = False B =  True C =  True D = False E =  True r =  True c = False
A = False B = False C =  True D = False E =  True r =  True c = False
A = False B = False C =  True D =  True E =  True r =  True c = False
A = False B = False C = False D =  True E = False r =  True c = False
A = False B = False C = False D =  True E =  True r =  True c = False
A = False B = False C = False D = False E =  True r =  True c = False
A = False B = False C = False D = False E =  True r =  True c =  True
A = False B = False C = False D = False E = False r =  True c =  True
A = False B = False C = False D =  True E =  True r =  True c =  True
A =  True B = False C = False D =  True E =  True r =  True c =  True
A =  True B = False C = False D =  True E =  True r =  True c = False
A =  True B =  True C = False D =  True E = False r =  True c = False
A =  True B =  True C = False D =  True E =  True r =  True c = False
A = False B =  True C = False D =  True E = False r =  True c = False
A =  True B =  True C = False D =  True E = False r =  True c =  True
A =  True B = False C = False D =  True E = False r =  True c =  True
A =  True B = False C =  True D = False E = False r =  True c =  True
A =  True B = False C =  True D = False E = False r =  True c = False
A =  True B = False C = False D =  True E = False r =  True c = False
A = False B =  True C = False D =  True E =  True r =  True c = False
A = False B = False C =  True D =  True E =  True r =  True c =  True
A = False B = False C =  True D = False E =  True r =  True c =  True
A =  True B =  True C =  True D = False E = False r =  True c = False
A =  True B = False C =  True D = False E =  True r =  True c = False
A =  True B =  True C = False D =  True E =  True r =  True c =  True

This prints all possible models. You can of course constrain it further.

How to model in Z3py

1 Answers1

Linked