z3 - 特定のインスタンスが持つ解の数を決定する方法: 代数生物学への応用

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

この問題には 2 つの解決策があります。しかし、可能な解の数を自動的に決定する方法を教えてください。

その他の例:

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

この解決策が唯一の解決策であるかどうかを知るにはどうすればよいですか?

オンラインの他の例はこちら

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

この例をここでオンラインで実行してください。

ただし、次の例では、このメソッドはオンラインで失敗します

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

ここでこの例をオンラインで実行します

この最後の例では、正解は 2 です。この場合、そのような方法が失敗する理由を教えてください。

Taylor のコードを変更した他の例:

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

ここでこの例をオンラインで実行します

どうもありがとう。

score 3 · Accepted Answer

次の関連する質問を参照してください。

score 1 · Accepted Answer

あなたの問題は純粋に命題のようです。これが偶然ではない場合は、#SAT ソルバー (sharpSAT、Dsharp、c2d など) を参照してください。

score 0 · Accepted Answer

その他の例:

ここに画像の説明を入力

コード：

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)

出力：

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

ここでこの例をオンラインで実行します

score 0 · Accepted Answer

その他の例：シロイヌナズナの花の形態形成制御のブールネットワークモデル

ここに画像の説明を入力

コード：

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

ここでこの例をオンラインで実行します

score 0 · Accepted Answer

Z3Py オンラインで変更された Taylor のコードを使用した最初の例の解決策は次のとおりです。

コード：

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

出力：

[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

ここでこの例をオンラインで実行します

Z3Py オンラインで変更された Taylor のコードを使用した 2 番目の例の解決策は次のとおりです。

コード：

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

出力：

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

ここでこの例をオンラインで実行します

その他の例:

ここに画像の説明を入力

コード：

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

出力：

[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

ここでこの例をオンラインで実行します

その他の例:

ここに画像の説明を入力

コード：

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

出力：

[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

ここでこの例をオンラインで実行します

テイラーに感謝します。

z3 - 特定のインスタンスが持つ解の数を決定する方法: 代数生物学への応用

5 に答える 5

Related

Reference