z3をインクリメンタルに使用すると時間が増えます

Question

プッシュ方式で1つのインクリメンタル制約の問題を解決するために、たとえば（< Z100）、次に（< Z90）、次に< Z 80）。

しかし、私はインクリメンタル方式でZ3を使用していましたが、2回のインクリメンタルチェック後にチェック（< Z 80）よりもすぐに（< Z 80）だけチェックすると時間がかかります上記）。

• 理由を教えてもらえますか？
• 学習された節が大きすぎて検索が遅くなるからですか？
• この問題の解決に役立つ戦略はありますか？

Answer 1

は、あなたはそれが、小さいZ用で探すとき、あなたのアルゴリズムは非常に良い最適を見つけるためにあなたはおそらく一人で（< Z 80）とすぐにこの時間は、それを解決し、この時点

を幸運あなたがそれを使用した特定のケース。

これは、入力データが原因である可能性があります。直接（< Z 80）を探す方が良いということを示すには、明らかにそうではありませんが、多くの種類の入力データセットで多くの試みを行う必要があります。