1

次のコードは、SMT-LIB で Z3 を使用して、Tropical Arithmetic の基本的なプロパティを紹介します。

; This example illustrates basic tropical arithmetic 

(define-fun tropadd  ((a Real)(b Real)) Real (if (> a b)
                                        b
                                        a))
(define-fun tropmul ((a Real)(b Real)) Real (+ a b))
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(push)
(assert(not(= (tropadd x y) (tropadd y x))))
(check-sat)
(pop)
(push)
(assert(not(= (tropmul x y) (tropmul y x))))
(check-sat)
(pop)
(push)
(assert(not(= (tropmul x (tropmul y z)) (tropmul (tropmul x y) z))))
(check-sat)
(pop)
(push)
(assert(not(= (tropadd x (tropadd y z)) (tropadd (tropadd x y) z))))
(check-sat)
(pop)
(push)
(assert(not(= (tropmul x (tropadd y z)) (tropadd (tropmul x y) (tropmul x z)))))
(check-sat)
(pop)

(push)
(assert(not(= (tropmul x 0) x)))
(check-sat)
(pop)
(push)
(assert (= (tropmul x 2) 3))
(check-sat)
(get-model)
(pop)
(push)
(assert (= (tropadd x 2) 1))
(check-sat)
(get-model)

出力は次のとおりです。

unsat 
unsat 
unsat 
unsat 
unsat 
unsat 

sat 
(model (define-fun x () Real 1.0) 

sat 
(model (define-fun x () Real 1.0) )

ここでこのコードをオンラインで実行してください

このコードは、熱帯加算と熱帯乗算を導入します。次に、これらの操作が次を満たすことが証明されます。そして熱帯増殖の調節因子。

熱帯の加法を満たすためには、無限大を導入する必要があります。つまり、無限大 + a = aすべての a .

トロピカルコードにそのような無限を導入する方法を教えてください。どうもありがとう。

4

1 に答える 1

3

無限を含めるには、新しいタイプ、ある種の差別的な共用体を定義する必要があります。操作を拡張して、この新しいタイプをカバーします。SMT-Lib でこれを行う標準的な方法は、解釈されないソートを導入してから、適切な公理として mul/add などの定義をアサートすることです。基盤となるソルバーがそのような公理をどれだけうまく処理できるかは、量化子をどれだけうまく処理できるか、およびどのような種類の問題を投げるかによって異なります。

別の方法は、Z3Py や SBV (Z3 やその他の SMT ソルバーへの Haskell バインディング) によって提唱されているような高レベルのアプローチを使用することです。これらの言語で提供されるように、高レベル構造のほとんどの機構を隠すことができます。多くの未解釈のソートや公理などを扱うと、SMT-Lib は非常に冗長になり、エラーが発生しやすくなるため、これを最初に試してみます。

于 2013-06-05T18:14:04.030 に答える