2

Please consider the following problem

(declare-fun x1 () Bool)
(declare-fun x2 () Bool)
(declare-fun x3 () Bool)
(declare-fun x4 () Bool)
(define-fun conjecture () Bool
(and (= (and x2 x3) x1) (= (and x1 (not x4)) x2) (= x2 x3) (= (not x3) x4)))
(assert conjecture)
(check-sat)
(get-model)
(assert (= x4 false))
(check-sat)
(get-model)

and the corresponding output is

sat 
  (model 
    (define-fun x2 () Bool false) 
    (define-fun x4 () Bool true) 
    (define-fun x1 () Bool false) 
    (define-fun x3 () Bool false) ) 

sat 
  (model 
    (define-fun x3 () Bool true) 
    (define-fun x2 () Bool true) 
    (define-fun x1 () Bool true) 
    (define-fun x4 () Bool false) )

This problem has two solutions. But, please let me know how to determine automatically the number of the possible solutions.

Other example:

(declare-fun x1 () Bool)
(declare-fun x2 () Bool)
(declare-fun x3 () Bool)
(declare-fun x4 () Bool)
(declare-fun x5 () Bool)
(define-fun conjecture () Bool
   (and (= (and x2 x3 (not x4)) x1) (= (and x1 (not x4) (not x5)) x2) 
   (= (and x2 (not x5)) x3) (= (and (not x3) x1) x4) (= (and x2 x3 (not x4)) x5)))
(assert conjecture)
(check-sat)
(get-model)

The output is:

sat 
(model 
  (define-fun x3 () Bool false) 
  (define-fun x1 () Bool false) 
  (define-fun x4 () Bool false) 
  (define-fun x5 () Bool false) 
  (define-fun x2 () Bool false) )

How I can to know if this solution is the only solution?

Other example online here

I am trying to apply the method proposed at Z3-number of solutions. Such method performs well in the following example:

Code:

def add_constraints(s, model):

x = Bool('x')
s.add(Or(x, False) == True)

notAgain = []
i = 0
for val in model:
  notAgain.append(x != model[val])

  i = i + 1
if len(notAgain) > 0:
  s.add(Or(notAgain))
  print Or(notAgain)
return s

s = Solver()
i = 0
add_constraints(s, [])
while s.check() == sat:
print s.model()
i = i + 1
add_constraints(s, s.model())
print i # solutions

Output : 

[x = True]
x ≠ True
1

Run this example online here.

But the method fails online in the following example

def add_constraints(s, model):

x = Bool('x')
s.add(Or(x, True) == True)

notAgain = []
i = 0
for val in model:
  notAgain.append(x != model[val])

  i = i + 1
if len(notAgain) > 0:
  s.add(Or(notAgain))
  print Or(notAgain)
return s

s = Solver()
i = 0
add_constraints(s, [])
while s.check() == sat:
print s.model()
i = i + 1
add_constraints(s, s.model())
print i # solutions

Output:

F:\Applications\Rise4fun\Tools\Z3Py timed out

Run this example online here

For this last example the correct answer is 2. Please can you tell me why such method fails in this case?

Other example with the modified Taylor`s code:

def add_constraints(s, model):
X = BoolVector('x', 4)
s.add(Or(X[0], False) == X[1])
s.add(Or(X[1], False) == X[0])
s.add(Or(Not(X[2]), False) == Or(X[0],X[1]))
s.add(Or(Not(X[3]), False) == Or(Not(X[0]),Not(X[1]),Not(X[2])))
notAgain = []
i = 0
for val in model:
  notAgain.append(X[i] != model[X[i]])
  i = i + 1
if len(notAgain) > 0:
  s.add(Or(notAgain))
  print Or(notAgain)
return s


s = Solver()
i = 0
add_constraints(s, [])
while s.check() == sat:
print s.model()
i = i + 1
add_constraints(s, s.model())
print i # solutions

Output:

[x1 = False, x0 = False, x3 = False, x2 = True]
x0 ≠ False ∨ x1 ≠ False ∨ x2 ≠ True ∨ x3 ≠ False
[x1 = True, x0 = True, x3 = False, x2 = False]
x0 ≠ True ∨ x1 ≠ True ∨ x2 ≠ False ∨ x3 ≠ False
2

Run this example online here

Many thanks.

Community
  • 1
  • 1
Juan Ospina
  • 1,317
  • 1
  • 7
  • 15
  • 1
    The problem in the second example is that no model is generated because the satisfiability of the constraint `Or(x, True) == True` is independent of an assignment to `x`. If you enable model completion (which maybe someone else can tell us how to do via z3py), that might give an assignment to `x`. But, that will still not solve the problem since whether `x` is true or false will not cause the constraint to become unsatisfiable, so it runs forever. In the first example, `Or(x, False) == True` requires `x` to be assigned true to be satisfiable, so a model is generated stating this. – Taylor T. Johnson May 31 '13 at 15:40
  • Many thanks for you answer. Please let me know what happens with the following example: http://rise4fun.com/Z3Py/kgqZ In this example the number of solutions in only one, but the code is given 2. It is wrong. – Juan Ospina May 31 '13 at 16:48
  • 1
    The code assumes an ordering on the list `model`: replace `notAgain.append(X[i] != model[val])` with `notAgain.append(X[i] != model[X[i]])`. You can see the problem if you `print val` in the loop over `model` – Taylor T. Johnson May 31 '13 at 18:41
  • Many, many thanks, now the code performs very well. – Juan Ospina May 31 '13 at 18:54

5 Answers5

3

See the following related questions:

Community
  • 1
  • 1
Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
1

It looks like your problems are purely propositional. If this is not accidentally so, you might want to look at #SAT solvers (sharpSAT, Dsharp, c2d - to name a few).

Vladimir Klebanov
  • 143
  • 4
0

The solution for the first example, using the modified Taylor`s code with Z3Py online is:

Code:

def add_constraints(s, model):
X = BoolVector('x', 4)
s.add(And(X[1],X[2])==X[0])
s.add(And(X[0],Not(X[3]))== X[1])
s.add(X[1] == X[2])
s.add(Not(X[2]) == X[3])
notAgain = []
i = 0
for val in model:
  notAgain.append(X[i] != model[X[i]])
  i = i + 1
if len(notAgain) > 0:
  s.add(Or(notAgain))
  print Or(notAgain)
return s


s = Solver()
i = 0
add_constraints(s, [])
while s.check() == sat:
print s.model()
i = i + 1
add_constraints(s, s.model())
print i # solutions

Output:

[x1 = False, x3 = True, x0 = False, x2 = False]
x0 ≠ False ∨ x1 ≠ False ∨ x2 ≠ False ∨ x3 ≠ True
[x1 = True, x0 = True, x3 = False, x2 = True]
x0 ≠ True ∨ x1 ≠ True ∨ x2 ≠ True ∨ x3 ≠ False
2

Run this example online here

The solution for the second example, using the modified Taylor`s code with Z3Py online is:

Code:

def add_constraints(s, model):
X = BoolVector('x', 5)
s.add(And(X[1],X[2],Not(X[3])) == X[0])
s.add(And(X[0],Not(X[3]),Not(X[4])) == X[1])
s.add(And(X[1],Not(X[4])) == X[2])
s.add(And(Not(X[2]),X[0]) == X[3])
s.add(And(X[1],X[2],Not(X[3])) == X[4])
notAgain = []
i = 0
for val in model:
  notAgain.append(X[i] != model[X[i]])
  i = i + 1
if len(notAgain) > 0:
  s.add(Or(notAgain))
  print Or(notAgain)
return s


s = Solver()
i = 0
add_constraints(s, [])
while s.check() == sat:
print s.model()
i = i + 1
add_constraints(s, s.model())
print i # solutions

Output:

[x0 = False, x3 = False, x4 = False, x2 = False, x1 = False]
x0 ≠ False ∨
x1 ≠ False ∨
x2 ≠ False ∨
x3 ≠ False ∨
x4 ≠ False
1

Run this example online here

Other example:

enter image description here

Code:

def add_constraints(s, model):
X = BoolVector('x', 5)
s.add(X[2] == X[0])
s.add(Or(X[2],X[4]) == X[1])
s.add(X[0]== X[2])
s.add(And(X[0],X[4]) == X[3])
s.add(And(X[2],X[3]) == X[4])
notAgain = []
i = 0
for val in model:
  notAgain.append(X[i] != model[X[i]])
  i = i + 1
if len(notAgain) > 0:
  s.add(Or(notAgain))
  print Or(notAgain)
return s


s = Solver()
i = 0
add_constraints(s, [])
while s.check() == sat:
print s.model()
i = i + 1
add_constraints(s, s.model())
print i # solutions

Output:

[x0 = False, x4 = False, x2 = False, x3 = False, x1 = False]
x0 ≠ False ∨
x1 ≠ False ∨
x2 ≠ False ∨
x3 ≠ False ∨
x4 ≠ False
[x1 = True, x0 = True, x4 = True, x3 = True, x2 = True]
x0 ≠ True ∨
x1 ≠ True ∨
x2 ≠ True ∨
x3 ≠ True ∨
x4 ≠ True
[x1 = True, x0 = True, x4 = False, x3 = False, x2 = True]
x0 ≠ True ∨
x1 ≠ True ∨
x2 ≠ True ∨
x3 ≠ False ∨
x4 ≠ False
3

Run this example online here

Other example:

enter image description here

Code:

def add_constraints(s, model):
X = BoolVector('x', 12)
s.add(Or(X[8],X[10]) == X[0])
s.add(And(Not(X[6]),X[11]) == X[1])
s.add(False == X[2])
s.add(And(X[0],Not(X[9])) == X[3])
s.add(And(X[1],Not(X[9])) == X[4])
s.add(And(X[2],Not(X[7])) == X[5])
s.add(X[3] == X[6])
s.add(X[4] == X[7])
s.add(And(X[5],Not(X[11]))== X[8])
s.add(Or(X[6], X[10]) == X[9])
s.add(And(Or(X[6],X[10]),Not(X[11])) == X[10])
s.add(And(X[7],Not(X[10])) == X[11])



notAgain = []
i = 0
for val in model:
  notAgain.append(X[i] != model[X[i]])
  i = i + 1
if len(notAgain) > 0:
  s.add(Or(notAgain))
  print Or(notAgain)
return s


s = Solver()
i = 0
add_constraints(s, [])
while s.check() == sat:
print s.model()
i = i + 1
add_constraints(s, s.model())
print i # solutions

Output:

[x11 = True,
x6 = False,
x10 = False,
x9 = False,
x8 = False,
x7 = True,
x5 = False,
x4 = True,
x3 = False,
x2 = False,
x1 = True,
x0 = False]
x0 ≠ False ∨
x1 ≠ True ∨
x2 ≠ False ∨
x3 ≠ False ∨
x4 ≠ True ∨
x5 ≠ False ∨
x6 ≠ False ∨
x7 ≠ True ∨
x8 ≠ False ∨
x9 ≠ False ∨
x10 ≠ False ∨
x11 ≠ True
[x11 = False,
x1 = False,
x5 = False,
x0 = False,
x10 = False,
x9 = False,
x4 = False,
x8 = False,
x6 = False,
x7 = False,
x3 = False,
x2 = False]
x0 ≠ False ∨
x1 ≠ False ∨
x2 ≠ False ∨
x3 ≠ False ∨
x4 ≠ False ∨
x5 ≠ False ∨
x6 ≠ False ∨
x7 ≠ False ∨
x8 ≠ False ∨
x9 ≠ False ∨
x10 ≠ False ∨
x11 ≠ False
[x11 = False,
x1 = False,
x5 = False,
x0 = True,
x10 = True,
x9 = True,
x4 = False,
x8 = False,
x6 = False,
x7 = False,
x3 = False,
x2 = False]
x0 ≠ True ∨
x1 ≠ False ∨
x2 ≠ False ∨
x3 ≠ False ∨
x4 ≠ False ∨
x5 ≠ False ∨
x6 ≠ False ∨
x7 ≠ False ∨
x8 ≠ False ∨
x9 ≠ True ∨
x10 ≠ True ∨
x11 ≠ False
3

Run this example online here

Many thanks Taylor.

Juan Ospina
  • 1,317
  • 1
  • 7
  • 15
0

Other example:

enter image description here

Code:

def add_constraints(s, model):
X = BoolVector('x', 23)
s.add(And(Or(X[0],X[20]),Not(X[21])) == X[0])
s.add(False == X[1])
s.add(X[1] == X[2])
s.add(And(Or(X[13],X[15],X[19],X[21]),Not(X[18])) == X[3])
s.add(X[3] == X[4])
s.add(X[0] == X[5])
s.add(X[5] == X[6])
s.add(False == X[7])
s.add(And(X[7],Not(X[20]))== X[8])
s.add(False == X[9])
s.add(And(X[9],Not(X[20])) == X[10])
s.add(And(X[0],Not(X[17])) == X[11])
s.add(And(X[11],Not(X[16])) == X[12])
s.add(X[10]==X[13])
s.add(And(X[4],Not(X[16]))== X[14])
s.add(X[22]==X[15])
s.add(Or(X[17],X[21]) == X[16])
s.add(Or(X[2],X[14]) == X[17])
s.add(X[6] == X[18])
s.add(And(X[8],Not(X[0])) == X[19])
s.add(X[12]== X[20])
s.add(And(Or(X[17],X[21]),Not(X[0])) == X[21])
s.add(False == X[22])




notAgain = []
i = 0
for val in model:
  notAgain.append(X[i] != model[X[i]])
  i = i + 1
if len(notAgain) > 0:
  s.add(Or(notAgain))

return s


s = Solver()
i = 0
add_constraints(s, [])
while s.check() == sat:
print "State ", (i + 1)
print s.model()
i = i + 1
add_constraints(s, s.model())
print "Number of States=", (i)

Output:

State  1
[x17 = False,
x0 = False,
x16 = True,
x21 = True,
x22 = False,
x20 = False,
x19 = False,
x15 = False,
x14 = False,
x13 = False,
x12 = False,
x11 = False,
x10 = False,
x9 = False,
x8 = False,
x7 = False,
x4 = True,
x3 = True,
x18 = False,
x6 = False,
x5 = False,
x2 = False,
x1 = False]
State  2
[x11 = False,
x22 = False,
x0 = False,
x10 = False,
x12 = False,
x3 = False,
x14 = False,
x21 = False,
x2 = False,
x1 = False,
x17 = False,
x5 = False,
x13 = False,
x20 = False,
x4 = False,
x9 = False,
x15 = False,
x19 = False,
x18 = False,
x6 = False,
x7 = False,
x8 = False,
x16 = False]
State  3
[x11 = True,
x22 = False,
x0 = True,
x10 = False,
x12 = True,
x3 = False,
x14 = False,
x21 = False,
x2 = False,
x1 = False,
x17 = False,
x5 = True,
x13 = False,
x20 = True,
x4 = False,
x9 = False,
x15 = False,
x19 = False,
x18 = True,
x6 = True,
x7 = False,
x8 = False,
x16 = False]
Number of States= 3

Run this example online here

Juan Ospina
  • 1,317
  • 1
  • 7
  • 15
0

Other example: Boolean network model of the control of flower morphogenesis in Arabidobis thaliana

enter image description here

Code:

def add_constraints(s, model):
X = BoolVector('x', 15)
s.add(Or(And(X[7],X[0],X[14]),And(Not(X[8]),Not(X[12])),And(X[7],Not(X[11])))== X[0])
s.add(Or(And(X[0],X[13],X[14],X[1]),And(X[5],X[13],X[14],X[1]),And(X[7],X[2])) == X[1])
s.add(X[2] == X[2])
s.add(And(Not(X[5]),Not(X[12])) == X[3])
s.add(Not(X[6]) == X[4])
s.add(Or(And(Not(X[0]),Not(X[12])),And(X[7],Not(X[0])),And(X[4],Not(X[0]))) == X[5])
s.add(Not(X[7]) == X[6])
s.add(Or(Not(X[12]),Not(X[6]))== X[7])
s.add(Not(X[12])== X[8])
s.add(Or(And(X[9],Not(X[14])),And(X[9],Not(X[0]))) == X[9])
s.add(True == X[10])
s.add(True == X[11])
s.add(And(Not(X[5]),X[6],Not(X[7])) == X[12])
       s.add(Or(And(X[5],X[13],X[14],X[1]),And(X[0],X[13],X[14],X[1]),And(X[7],X[0]),And(X[7],X[1]))==X[13])
s.add(X[7]== X[14])





notAgain = []
i = 0
for val in model:
  notAgain.append(X[i] != model[X[i]])
  i = i + 1
if len(notAgain) > 0:
  s.add(Or(notAgain))

return s


s = Solver()
i = 0
add_constraints(s, [])
while s.check() == sat:
print "========================================================================="  

print "State ", (i + 1), ":"
for c in s.model():
    if is_true((s.model())[c]):
        print c ,"=", 1
    else:
        print c, "=", 0
i = i + 1
add_constraints(s, s.model())
print "========================================================================="

print "Number of States=", (i)

Output:

Number of States= 14

Run this example on line here

Juan Ospina
  • 1,317
  • 1
  • 7
  • 15