Z3での「最小化」の仕組み

Question

私はZ3のminimize関数をたくさん使っていますが、私はいくつかのスケーラビリティの問題（最小化する変数の数が増えると）について心配しています。 "最小化"の根底にあるアルゴリズムは何ですか？そして、物事をスピードアップする一般的な方法はありますか？

Answer 1

Z3で使用される最適化アルゴリズムの詳細については、paperを参照してください。物事をスピードアップする一般的な方法についてのあなたの質問について、あなたがしようとしていることを正確に見ていなくて、それをどのようにエンコードしているのかを見ることはできません。物事が「拡大縮小」しない具体的な例を投稿すると役立つかもしれません。