2

モデルの出力 (私の場合は sat と unsat のみ) を別のモデルで使用したいと考えています。ここで、モデルとは、一連の論理式 (この場合は Z3 式) に含まれる定数への満足のいく代入です。私の目的は、次のように簡単に説明できます。

私の問題は、次のように詳細に説明できます。形式化された問題 P、つまり、いくつかの制約 (C) に対応する一連の論理式 (式) があります。そのうちの 1 つ (例: Ai > 0) が目的です。モデル/形式化 P を実行すると、すべての制約が満たされる場合、sat が返されます。Ai = 0 は常に可能であることに注意してください。ここで、特定の変数セットへの代入セットが、Ai > 0 (任意の i について) が不可能であることを保証する制約 (C) に対応することを見つけたいと考えています。現在、制約 (つまり、制約値) の DFS ベースの検索アルゴリズムを開発し、P を実行して "push/pop "。検索を改善しようとしましたが、あまり役に立ちません。問題のサイズが大きい場合、これは非常に非効率的です。このような満足できるセットを検索するために、P を使用する別の SMT プログラム (モデル) を作成できれば素晴らしいと思います。

問題 P (元の問題の短い SMT LIB 2 バージョン) の現在の形式化は次のとおりです。

(declare-fun th1 () Real)
(declare-fun th2 () Real)
(declare-fun th3 () Real)
(declare-fun th4 () Real)
(declare-fun th5 () Real)

(declare-fun l1 () Real)
(declare-fun l2 () Real)
(declare-fun l3 () Real)
(declare-fun l4 () Real)
(declare-fun l5 () Real)
(declare-fun l6 () Real)
(declare-fun l7 () Real)

(declare-fun p1 () Real)
(declare-fun p2 () Real)
(declare-fun p3 () Real)
(declare-fun p4 () Real)
(declare-fun p5 () Real)

(declare-fun sl1 () Int)
(declare-fun sl2 () Int)
(declare-fun sl3 () Int)
(declare-fun sl4 () Int)
(declare-fun sl5 () Int)
(declare-fun sl6 () Int)
(declare-fun sl7 () Int)

(declare-fun sp1 () Int)
(declare-fun sp2 () Int)
(declare-fun sp3 () Int)
(declare-fun sp4 () Int)
(declare-fun sp5 () Int)

(declare-fun a1 () Int)
(declare-fun a2 () Int)
(declare-fun a3 () Int)
(declare-fun a4 () Int)
(declare-fun a5 () Int)

(declare-fun na () Int)
(declare-fun ns () Int)
(declare-fun attack () Bool)

;;;; System
(assert (and      (= l1 (* (- th2 th1) 17.0))
        (= l2 (* (- th5 th1) 4.5))
        (= l3 (* (- th3 th2) 5.05))
        (= l4 (* (- th4 th2) 5.65))
        (= l5 (* (- th5 th2) 5.75))
        (= l6 (* (- th4 th3) 5.85))
        (= l7 (* (- th5 th4) 23.75))        

        (= p1 (+ l1 l2))
        (= p2 (+ l1 l3 l4 l5))
        (= p3 (+ l3 l6))
        (= p4 (+ l4 l6 l7))
        (= p5 (+ l2 l5 l7))
        )
)

;;;; Secured measurements
(assert (and    (or (= sl1 0) (= sl1 1))
        (or (= sl2 0) (= sl2 1))
        (or (= sl3 0) (= sl3 1))
        (or (= sl4 0) (= sl4 1))
        (or (= sl5 0) (= sl5 1))
        (or (= sl6 0) (= sl6 1))
        (or (= sl7 0) (= sl7 1))

        (or (= sp1 0) (= sp1 1))
        (or (= sp2 0) (= sp2 1))
        (or (= sp3 0) (= sp3 1))
        (or (= sp4 0) (= sp4 1))
        (or (= sp5 0) (= sp5 1))        
        )
)        

(assert (and    (=> (not (= l1 0.0)) (= sl1 0))
        (=> (not (= l2 0.0)) (= sl2 0))
        (=> (not (= l3 0.0)) (= sl3 0))
        (=> (not (= l4 0.0)) (= sl4 0))
        (=> (not (= l5 0.0)) (= sl5 0))
        (=> (not (= l6 0.0)) (= sl6 0))
        (=> (not (= l7 0.0)) (= sl7 0))     

        (=> (not (= p1 0.0)) (= sp1 0))
        (=> (not (= p2 0.0)) (= sp2 0))
        (=> (not (= p3 0.0)) (= sp3 0))
        (=> (not (= p4 0.0)) (= sp4 0))
        (=> (not (= p5 0.0)) (= sp5 0))          
    )
)

(assert (and (= sl1 1) (= sl2 1)))

;;;; Attacks
(assert (and    (or (= a1 0) (= a1 1))
        (or (= a2 0) (= a2 1))
        (or (= a3 0) (= a3 1))
        (or (= a4 0) (= a4 1))
        (or (= a5 0) (= a5 1))      
    )
)

(assert (and
        (= (not (= th1 0.0)) (= a1 1))
        (= (not (= th2 0.0)) (= a2 1))
        (= (not (= th3 0.0)) (= a3 1))
        (= (not (= th4 0.0)) (= a4 1))
        (= (not (= th5 0.0)) (= a5 1))      
    )
)

(assert (= th1 0.0)) // Base condition
(assert (= na (+ a1 a2 a3 a4 a5)))
(assert (=> attack (> na 1)))


;;;; Check for satisfiable model

(assert attack)

(check-sat)
(get-model)
(exit)

たとえば、次のように、制約が与えられた場合に攻撃が発生しないように (つまり、na が 0 になるように)、セキュリティ測定値を合成します (つまり、「sl」および「sp」項の割り当てを見つけます)。

(assert (= ns (+ sl1 sl2 sl3 sl4 sl5 sl6 sl7 sp1 sp2 sp3 sp4 sp5)))
(assert (<= ns 4))

この場合、アサーション (すなわち、'(assert (and (= sl1 1) (= sl2 1)))' ) はコメント化されます。現在、'sl' と 'sp' の割り当てを受け取り、(assert (and (= sl1 1) (= sl2 1) ...))' のようにアサートし、指定されたプログラムを実行する C# プログラムを開発しました。可能な攻撃があるかどうかを確認します。プログラムが unsat を返したら完了です (つまり、na > 1 はあり得ません)。SMT (Z3) のみを使用して問題を解決する方法はありますか?

4

2 に答える 2

3

質問を解決してくれてありがとう。私が理解していれば、 Z3を使用してsliおよびspj値の検索を実行できますが、SMT-LIBのみではこれを実行できず、APIを使用する必要があります。これらの回答で詳細に説明されているように、アイデアは、1 つの sat チェックからのモデル (満足のいく割り当て) を将来のチェックの制約として使用することです。

Z3: 満足のいくモデルをすべて見つける

Z3: モデルが一意かどうかを確認する

(Z3Py) 方程式のすべての解をチェック

Python API でエンコードされた例を次に示します (z3py リンク: http://rise4fun.com/Z3Py/KHzm ):

s = Solver()

th1, th2, th3, th4, th5 = Reals('th1 th2 th3 th4 th5')
th = { 'th1' : th1, 'th2' : th2, 'th3' : th3, 'th4' : th4, 'th5' : th5}
l1, l2, l3, l4, l5, l6, l7 = Reals('l1 l2 l3 l4 l5 l6 l7')
l = { 'l1' : l1, 'l2' : l2, 'l3' : l3, 'l4' : l4, 'l5' : l5, 'l6' : l6, 'l7' : l7 }
p1, p2, p3, p4, p5 = Reals('p1 p2 p3 p4 p5')
p = { 'p1' : p1, 'p2' : p2, 'p3' : p3, 'p4' : p4, 'p5' : p5 }
sl1, sl2, sl3, sl4, sl5, sl6, sl7 = Ints('sl1 sl2 sl3 sl4 sl5 sl6 sl7')
sl = { 'sl1' : sl1, 'sl2' : sl2, 'sl3' : sl3, 'sl4' : sl4, 'sl5' : sl5, 'sl6' : sl6, 'sl7' : sl7 }
sp1, sp2, sp3, sp4, sp5 = Ints('sp1 sp2 sp3 sp4 sp5')
sp = { 'sp1' : sp1, 'sp2' : sp2, 'sp3' : sp3, 'sp4' : sp4, 'sp5' : sp5 }
a1, a2, a3, a4, a5 = Ints('a1 a2 a3 a4 a5')
a = { 'a1' : a1, 'a2' : a2, 'a3' : a3, 'a4' : a4, 'a5' : a5 }
na, ns = Ints('na ns')
attack = Bool('attack')
n = { 'na' : na, 'ns' : ns, 'attack' : attack}
dict_decl = dict(th.items() + l.items() + p.items() + sl.items() + sp.items() + a.items() + n.items() )

assertions = []
assertions.append(parse_smt2_string('(assert (and      (= l1 (* (- th2 th1) 17.0)) (= l2 (* (- th5 th1) 4.5)) (= l3 (* (- th3 th2) 5.05)) (= l4 (* (- th4 th2) 5.65)) (= l5 (* (- th5 th2) 5.75)) (= l6 (* (- th4 th3) 5.85)) (= l7 (* (- th5 th4) 23.75)) (= p1 (+ l1 l2)) (= p2 (+ l1 l3 l4 l5)) (= p3 (+ l3 l6)) (= p4 (+ l4 l6 l7)) (= p5 (+ l2 l5 l7))))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (and    (or (= sl1 0) (= sl1 1)) (or (= sl2 0) (= sl2 1)) (or (= sl3 0) (= sl3 1)) (or (= sl4 0) (= sl4 1)) (or (= sl5 0) (= sl5 1)) (or (= sl6 0) (= sl6 1)) (or (= sl7 0) (= sl7 1)) (or (= sp1 0) (= sp1 1)) (or (= sp2 0) (= sp2 1)) (or (= sp3 0) (= sp3 1)) (or (= sp4 0) (= sp4 1)) (or (= sp5 0) (= sp5 1))        ))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (and    (=> (not (= l1 0.0)) (= sl1 0)) (=> (not (= l2 0.0)) (= sl2 0)) (=> (not (= l3 0.0)) (= sl3 0)) (=> (not (= l4 0.0)) (= sl4 0)) (=> (not (= l5 0.0)) (= sl5 0)) (=> (not (= l6 0.0)) (= sl6 0)) (=> (not (= l7 0.0)) (= sl7 0))      (=> (not (= p1 0.0)) (= sp1 0)) (=> (not (= p2 0.0)) (= sp2 0)) (=> (not (= p3 0.0)) (= sp3 0)) (=> (not (= p4 0.0)) (= sp4 0)) (=> (not (= p5 0.0)) (= sp5 0))           ))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (and (= sl1 1) (= sl2 1)))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (and    (or (= a1 0) (= a1 1))(or (= a2 0) (= a2 1))(or (= a3 0) (= a3 1))(or (= a4 0) (= a4 1))(or (= a5 0) (= a5 1))      ))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (and (= (not (= th1 0.0)) (= a1 1))(= (not (= th2 0.0)) (= a2 1))(= (not (= th3 0.0)) (= a3 1))(= (not (= th4 0.0)) (= a4 1))(= (not (= th5 0.0)) (= a5 1))      ))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (= ns (+ sl1 sl2 sl3 sl4 sl5 sl6 sl7 sp1 sp2 sp3 sp4 sp5)))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (<= ns 4))', decls=dict_decl))
#assertions.append(parse_smt2_string('(assert (and (= sl1 1) (= sl2 1)))', decls=dict_decl)) # commented as suggested
assertions.append(parse_smt2_string('(assert (= th1 0.0))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (= na (+ a1 a2 a3 a4 a5)))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert (=> attack (> na 1)))', decls=dict_decl))
assertions.append(parse_smt2_string('(assert attack)', decls=dict_decl))

print assertions

s.add(assertions)

synthesized = []

iters = 0
while s.check() == sat:
  print "Iteration " + str(iters)
  print s.model()
  avoid = []
  # key step: add constraint to prevent any values assigned (if possible) to constants from being equal to their satisfying assignments (models) in this sat iteration
  for sli in sl.values():
    avoid.append(sli != s.model()[sli])
  for spi in sp.values():
    avoid.append(spi != s.model()[spi])
  s.add(Or(avoid))
  # end key step
  synthesized.append(avoid)
  print avoid
  iters = iters + 1
  # unless you know how to guarantee termination (e.g., there is a constraint ensuring the slis and spis take values in finite sets)
  if iters >= 1000:
    break

print "Done"
print synthesized # all the constraints

すべての定数と数値についてお詫び申し上げます。SMT-LIB スクリプトの最も速い変換を使用しただけですが、かなり面倒でした。どこでもイテレータを使用します。sliこれにより、およびspj定数に対して次の制約が生成されました。

[[sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 1, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 1, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 1, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 0, sp3 ≠ 1, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 1, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 1, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 1, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 1, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 1, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 1, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 0, sp3 ≠ 0, sp4 ≠ 1, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 0, sp2 ≠ 1, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0], [sl4 ≠ 0, sl5 ≠ 0, sl6 ≠ 0, sl7 ≠ 0, sl1 ≠ 1, sl2 ≠ 1, sl3 ≠ 0, sp1 ≠ 1, sp2 ≠ 1, sp3 ≠ 0, sp4 ≠ 0, sp5 ≠ 0]]
于 2013-05-02T02:46:32.230 に答える
2

私がこれを正しく理解していれば、あなたは正確に（普遍的な）定量化を探しています. 疑似表記で申し訳ありませんが、次の自由変数 ( ) への満足のいく代入を探していませんconfig_paramsか?

config_constraints(config_params) -> forall attack_params: not attack_constraints(attack_params, config_params)

ここで、()表記は、制約が依存する変数 (セット) を示すだけです。Java API と同様に、量指定子が .Net API でもサポートされていることは確かです。

于 2013-05-01T07:24:30.777 に答える