bugfix> z3 > 投稿

私はZ3で実験しています(Python APIを使用)。クラス割り当てのスケジューリングモデルを構築しています。ここでは、モジュロをかなり頻繁に使用する必要があります(周期的であるため)。 Moduloはすでにz3の速度を大幅に低下させているように見えますが、いくつかの最適化(合計であるコスト関数の最小化)を試みると、かなり小さな問題にかなりの時間がかかります。

最適化がなければ、問題なく動作します(小さな問題の場合は数秒です)。ということで、2つの質問があります。

1)モジュロ関数を使用する方法のトリックはありますか?モジュロ値を関数に既に割り当てています。または、周期的/リング的な動作を表現する他の方法はありますか?

2)最適なソリューションを見つけることに興味はありません。良いものは、十分に良いでしょう。コスト関数にいくつかの境界を設定する方法はありますか。のように、その上限と下限を知っていれば?ドメインの知識を使用してソリューションをすばやく見つけることができる他のトリック。 さらに、タイムアウトオプションsolver.set( "timeout" 10000)を使用すると、ソルバーはこれまでのところ最適なソリューションでタイムアウトすると考えました。そうではないようです。ただタイムアウトします。

回答 2 件
  • mod についてコメントすることはできません  いくつかのコードを見ずに機能します。しかし、経験則として、分割は困難です。 Int を使用していますか  値、またはビットベクトル?制限のない整数を使用している場合は、より優れた内部ヒューリスティックの恩恵を受ける可能性のあるビットベクトルを試してみるとよいでしょう。または Real を試す  値、および適切な削減を行います。

    「これまでで最高の」最適値を取得する方法については、次の回答を参照してください。

  • 組み込みのモジュロと除算を使用する代わりに、未解釈の関数 mymod を導入できます。  および mydiv 、問題に必要な除算とモジュロの必要な公理のみを提供します。私の記憶が正しければ、MicrosoftのIroncladおよび/またはIronfleetチームは、モジュロ/除算に関連するパフォーマンスの問題があったときにそれを行いました(パイプラインDafny-> ブギー-> Z3)。

あなたの答え