smtp - 複数のアサーションを追加するのと、単一の and を追加するのとでは、どちらが SMT のより良い方法ですか?

Question

SMT でモデル化したい 2 つの句があるとしましょう。

(assert (> x y))
(assert (< y 2))

または、このようなand演算子を使用して1つのアサーションを追加します

(assert (and 
(> x y)
(< y 2)
))

これは、SMT ソルバーのパフォーマンスに関して大規模な問題に関係しますか。Z3を使用しています。

Answer 1

結合は複数のアサーションに分割されるため、あまり重要ではありません。大きな結合を導入すると、Z3 のパーサーはすべての結合を含む項を作成しますが、これは結合を維持する上での一定のオーバーヘッドにすぎません。