多くのプログラミング言語では、分岐効率は、句が提供される順序に依存します。例えば、Pythonで、Z3の検索時間は式の順序に影響されますか？
if p or q :
はすぐpがtrueと評価されたので、一般的に最初の計算が光句を提供することをお勧めしてif文に分岐します。私はZ3の充足可能性チェックにも同じことが当てはまるのだろうかと思います。言い換えると、And(P, Q)とAnd(Q, P)のチェックの間に違いがありますか？ただし、一方の式が他方のものよりかなり複雑ですか？
はい、それは句を指定する順番を変えることができます。しかし、Z3に関しては、節を並べ替えることで得られることはあまりありません。また、あらかじめ一般的な「最適な順序」を決定することは難しいかもしれません。
他のSMTソルバーでは、あなたが極端に記述しているものを観察しました。いくつかのソルバでは、ソルバが1つの順序で提示されるときにソルバがタイムアウトする特定のケースを見てきたが、同じ句が異なる順序で提示されたときに迅速に解決策を見つけるという意味で、 。しかし、私にとっては、これはあまり設計されていないソルバの兆候です。 Z3やCVC4などの他の最新のSMTソルバは、古いタイプのSMTソルバやそれほど堅牢でないSMTソルバよりも、この種の問題に対して脆弱です。
実際に最適な順序付けを見つけることに関して、SMTソルバーの「計算上の軽い」または「より複雑な」構成は、従来のコンピューター言語とは異なります。本当に重要なのは、連合体の特定の条項が紛争につながる可能性があるかどうか、あるいは異論の中の特定の条項が解決策につながる可能性があるかどうかということです。これは、迷路からあなたの道を見出そうとするのと同じです。あなたが間違った方向に進むと、行き止まりの後に長い時間を費やしてから、最初に戻って別のブランチ。ここでも、現代のSMTとSATソルバーはこれを緩和する技術を持っています。
また、Z3について言えば、人間が理解可能で一般的な複雑さの尺度で節をソートすることで、Z3を実世界のアプリケーションでより効率的にすることができたら、 Z3への前処理ステップ。一般的に、複数の要因（例えばZ3実装の詳細）が存在するような複雑な最適化問題については、アプリケーションに関連する一連のテスト例に対して複数のことを試してベンチマークを行う必要があります。上記の私の主張のいくつかの証拠のビットとして
、私はSMTの問題、この小さな例を書いた：
(declare-fun p() Int)
(declare-fun q() Int)
(declare-fun n() Int)
(assert (> p 1))
(assert (> q 1))
(assert (and (= n 18679565357) (= n (* p q))))
(check-sat)
(get-value (p q n))
(exit)
をand文は私のシステムではほとんど違いに句の順番を入れ替える（以下1％以上）。私は2つの別々のアサーションに分割すると、その差は大きくなりますが、この違いが一般的に（このクラスの異なるSMTの問題を超えて）保持されているかどうかを知るために、私は多くのそのような問題を持つベンチマークスイートを実行しなければなりません。