z3 - z3 入力の最適化

Question

モデルから生成された z3 python 入力を最適化しようとしています。15k の制約 (200 状態) までのモデルで実行でき、z3 は妥当な時間 (<10 分) で終了を停止します。モデルから生成された制約を最適化する方法はありますか?

3 つの州のモデル:

http://pastebin.com/EHZ1P20C

Answer 1

スクリプトhttp://pastebin.com/F5iuhN42のパフォーマンスは、カスタム戦略を使用して改善できます。Z3 では、ユーザーはカスタム戦略/ソルバーを定義できます。このチュートリアルでは、Z3 Python API を使用して戦略/戦術を定義する方法を示します。スクリプトhttp://pastebin.com/F5iuhN42で、行を置き換えると

s = Solver()

と

s = Then('simplify', 'elim-term-ite', 'solve-eqs', 'smt').solver()

実行時間は 30 秒から 1 秒に短縮されます (私のマシンでは)。

手順Thenは、4 つのステップで構成される戦略/戦術を作成しています。

• x + 1 - x + ySimplifier (つまり、 ==>などのルールを適用するリライター)1 + y

• If(a, b, c)where bandcが Boolean でない形式の式の削除。スクリプトは、この種の表現を多用しています。戦術elim-term-iteは、この種の表現を排除する変換を適用します。

• 方程式ソルバー。x = a And F[x]==>などの変換を適用しますF[a]。上記のスクリプトでは、この戦術により 1000 を超える変数を排除できます。

• このタクsmtティックは、Z3 で汎用 SMT ソルバーを呼び出します。

このメソッドは、Z3 戦術/戦略をおよびメソッド.solver()を提供するソルバー オブジェクトに変換します。メッセージの最初に含めたチュートリアルに詳細があります。addcheck