如何确定给定实例的解的数量:代数生物学中的应用

Question

请考虑以下问题

(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)

相应的输出是

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) )

这个问题有两个解决方案。但是，请让我知道如何自动确定可能的解决方案的数量。

其他示例：

(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)

输出为：

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) )

我如何知道这个解决方案是否是唯一的解决方案？

其他在线here示例

我正在尝试应用在Z3-number of solutions提出的方法。这种方法在下面的示例中执行得很好：

代码：

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

输出：

[x = True]
x ≠ True
1

运行此示例在线here。

但该方法在以下示例中联机失败

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

输出：

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

运行此示例在线here

对于最后一个例子，正确答案是2。你能告诉我为什么这种方法在这种情况下失败了吗？

使用修改后的Taylor`s代码的其他示例：

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

输出：

[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

运行此示例在线here

非常感谢。

Answer 1

其他例子:控制拟南芥花朵形态发生的布尔网络模型

​

​

代码：

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)

输出：

Number of States= 14

在here行上运行此示例

Answer 2

请参阅以下相关问题：

• z3 number of solutions
• Z3: finding all satisfying models

Answer 3

看起来你的问题是纯粹的命题。如果这不是偶然的，你可能想看看#SAT解算器(sharpSAT，Dsharp，c2d -举几个例子)。